Module

TopologicalAbelianizationCongr.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.TopologicalAbelianizationCongr

7 declarations indexed from sourceView source ↗

Module documentation

Functoriality of topological abelianization under equivalence

A continuous multiplicative equivalence carries the closure of the commutator subgroup onto the corresponding closure. It therefore descends to a continuous multiplicative equivalence of topological abelianizations.

Imports3

Mathlib.Topology.Algebra.ContinuousMonoidHom
Mathlib.Topology.Algebra.Group.Quotient
Mathlib.Topology.Algebra.Group.TopologicalAbelianization

Imported by4

theorem

topologicalCommutatorClosure_le_comap

L32 ↗

LocalClassFieldTheory.topologicalCommutatorClosure_le_comap

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
  [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
  [IsTopologicalGroup G] [IsTopologicalGroup H]

Lean source · statement

theorem topologicalCommutatorClosure_le_comap
    (e : G ≃ₜ* H) :
    (commutator G).topologicalClosure ≤
      (commutator H).topologicalClosure.comap
        e.toMulEquiv.toMonoidHom

def

topologicalAbelianizationMap

L53 ↗

LocalClassFieldTheory.topologicalAbelianizationMap

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
  [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
  [IsTopologicalGroup G] [IsTopologicalGroup H]

Lean source · statement

def topologicalAbelianizationMap (e : G ≃ₜ* H) :
    TopologicalAbelianization G →* TopologicalAbelianization H

theorem

topologicalAbelianizationMap_mk

L62 ↗

LocalClassFieldTheory.topologicalAbelianizationMap_mk

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
  [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
  [IsTopologicalGroup G] [IsTopologicalGroup H]

Lean source · statement

theorem topologicalAbelianizationMap_mk
    (e : G ≃ₜ* H) (x : G) :
    topologicalAbelianizationMap e (QuotientGroup.mk x) =
      QuotientGroup.mk (e x)

theorem

topologicalAbelianizationMap_continuous

L68 ↗

LocalClassFieldTheory.topologicalAbelianizationMap_continuous

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
  [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
  [IsTopologicalGroup G] [IsTopologicalGroup H]

Lean source · statement

theorem topologicalAbelianizationMap_continuous
    (e : G ≃ₜ* H) :
    Continuous (topologicalAbelianizationMap e)

def

topologicalAbelianizationMulEquiv

L76 ↗

LocalClassFieldTheory.topologicalAbelianizationMulEquiv

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
  [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
  [IsTopologicalGroup G] [IsTopologicalGroup H]

Lean source · full declaration

def topologicalAbelianizationMulEquiv (e : G ≃ₜ* H) :
    TopologicalAbelianization G ≃* TopologicalAbelianization H where
  toFun := topologicalAbelianizationMap e
  invFun := topologicalAbelianizationMap e.symm
  left_inv q := by
    refine q.inductionOn' ?_
    intro x
    simp
  right_inv q := by
    refine q.inductionOn' ?_
    intro x
    simp
  map_mul' x y := map_mul (topologicalAbelianizationMap e) x y

def