Module

TopologicalAbelianizationKernel.lean

Nyll.ProCGroups.Abelian.TopologicalAbelianizationKernel

2 declarations indexed from sourceView source ↗

Module documentation

Kernels after topological abelianization

For a continuous surjection from a compact group to a Hausdorff group, the kernel of the induced map on topological abelianizations is the image of the original kernel. Compactness makes the image of the closed commutator closed, so every target commutator class has a lift in the source closed commutator.

Imports2

Imported by3

theorem

ker_map_of_surjective

L29 ↗

ProCGroups.Abelian.TopologicalAbelianization.ker_map_of_surjective

Documentation

The kernel after topological abelianization is the abelianized image of the original kernel of a continuous surjection from a compact group.

Source context 3 commands

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

namespace ProCGroups.Abelian.TopologicalAbelianization
universe u v
variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [CompactSpace G]
  {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H] [T2Space H]

Lean source · statement

theorem ker_map_of_surjective (f : G →ₜ* H) (hf : Function.Surjective f) :
    (map f).toMonoidHom.ker = f.toMonoidHom.ker.map (mk G)

theorem

injective_map_iff_ker_le_closedCommutator

L59 ↗

ProCGroups.Abelian.TopologicalAbelianization.injective_map_iff_ker_le_closedCommutator