Module

ResidualEquivalence.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualEquivalence

2 declarations indexed from sourceView source ↗

Module documentation

Continuous equivalences of actual residual quotients

A continuous group equivalence carries the pro-C residual core onto the corresponding core. Applying functoriality in both directions requires only hereditariness of C, so total disconnectedness is unnecessary.

Imports4

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualCore
Nyll.ProCGroups.ProC.MaximalQuotients.UniversalProperty
Nyll.ProCGroups.Topologies.QuotientMaps
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by5

def

residualQuotientContinuousMulEquiv

L32 ↗

ProCGroups.ProC.residualQuotientContinuousMulEquiv

Documentation

A continuous equivalence of compact Hausdorff groups induces an equivalence of their actual pro-C residual quotients.

Source context 4 commands

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

namespace ProCGroups.ProC
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [CompactSpace H] [T2Space G] [T2Space H]

Lean source · statement

def residualQuotientContinuousMulEquiv
    (hC : FiniteGroupClass.Hereditary C) (e : G ≃ₜ* H) :
    G ⧸ proCResidualCore C G ≃ₜ* H ⧸ proCResidualCore C H

theorem

residualQuotientContinuousMulEquiv_apply_mk

L49 ↗

ProCGroups.ProC.residualQuotientContinuousMulEquiv_apply_mk