Module

Basic.lean

Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.ProfiniteUnitDecomposition.Basic

5 declarations indexed from sourceView source ↗

Module documentation

Basic topological product equivalences for profinite units

This module contains the reusable, inexpensive product equivalences used by the compiled stages of the profinite-unit decomposition.

Imports4

Imported by3

instance

primeFact

L35 ↗

KummerTheory.ProfiniteUnitDecomposition.Internal.primeFact

Documentation

The prime certificate shared by every compiled stage of the profinite unit decomposition.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.Padic
namespace ProfiniteUnitDecomposition.Internal

Lean source · statement

instance primeFact (p : Nat.Primes) : Fact p.1.Prime

def

continuousMulEquivPiCongr

L41 ↗

KummerTheory.continuousMulEquivPiCongr

Documentation

Coordinatewise product of topological multiplicative equivalences.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.Padic

Lean source · statement

def continuousMulEquivPiCongr
    {ι : Type*} {A B : ι → Type*}
    [(i : ι) → TopologicalSpace (A i)]
    [(i : ι) → TopologicalSpace (B i)]
    [(i : ι) → Mul (A i)] [(i : ι) → Mul (B i)]
    (e : (i : ι) → A i ≃ₜ* B i) :
    ((i : ι) → A i) ≃ₜ* ((i : ι) → B i)

def

continuousMulEquivPiProd

L57 ↗

KummerTheory.continuousMulEquivPiProd

Documentation

A product of pairs is topologically equivalent to the pair of products.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.Padic

Lean source · full declaration

def continuousMulEquivPiProd
    {ι : Type*} (A B : ι → Type*)
    [(i : ι) → TopologicalSpace (A i)]
    [(i : ι) → TopologicalSpace (B i)]
    [(i : ι) → Mul (A i)] [(i : ι) → Mul (B i)] :
    ((i : ι) → A i × B i) ≃ₜ*
      ((i : ι) → A i) × ((i : ι) → B i) where
  toFun x := (fun i => (x i).1, fun i => (x i).2)
  invFun x i := (x.1 i, x.2 i)
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
  continuous_toFun :=
    (continuous_pi fun i =>
      continuous_fst.comp (continuous_apply i)).prodMk
        (continuous_pi fun i =>
          continuous_snd.comp (continuous_apply i))
  continuous_invFun :=
    continuous_pi fun i =>
      ((continuous_apply i).comp continuous_fst).prodMk
        ((continuous_apply i).comp continuous_snd)

def

continuousPiMultiplicative

L80 ↗

KummerTheory.continuousPiMultiplicative

Documentation

Multiplicative tagging commutes with topological products.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.Padic

Lean source · statement

def continuousPiMultiplicative
    {ι : Type*} (A : ι → Type*)
    [(i : ι) → TopologicalSpace (A i)]
    [(i : ι) → Add (A i)] :
    Multiplicative ((i : ι) → A i) ≃ₜ*
      ((i : ι) → Multiplicative (A i))

abbrev

CyclotomicFinitePart

L93 ↗

KummerTheory.CyclotomicFinitePart

Documentation

The product of all finite factors in the local unit decompositions.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.Padic

Lean source · statement

abbrev CyclotomicFinitePart

Module documentation

Basic topological product equivalences for profinite units

Declarations

primeFact

continuousMulEquivPiCongr

continuousMulEquivPiProd

continuousPiMultiplicative

CyclotomicFinitePart