ModuleConnectedComponentQuotientCongr.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.ConnectedComponentQuotientCongr
3 declarations indexed from sourceView source ↗ Module documentation
Connected-component quotients under topological group equivalences
A topological group equivalence carries the connected component of one onto the connected component of one. It therefore induces an equivalence of the corresponding quotient topological groups.
Declarations
ClassFieldTheory.connectedComponentOfOne_map_equiv
DocumentationA topological group equivalence maps the identity component exactly onto the identity component.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
[Group G] [Group H]
[TopologicalSpace G] [TopologicalSpace H]
[IsTopologicalGroup G] [IsTopologicalGroup H]
ClassFieldTheory.connectedComponentQuotientCongr
DocumentationAn equivalence of topological groups descends to a topological group equivalence modulo the identity components.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
[Group G] [Group H]
[TopologicalSpace G] [TopologicalSpace H]
[IsTopologicalGroup G] [IsTopologicalGroup H]
ClassFieldTheory.connectedComponentQuotientCongr_mk
DocumentationOn representatives, the quotient equivalence applies the original map.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u v
variable {G : Type u} {H : Type v}
[Group G] [Group H]
[TopologicalSpace G] [TopologicalSpace H]
[IsTopologicalGroup G] [IsTopologicalGroup H]