Module

ConjugationComparison.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ConjugationComparison

4 declarations indexed from sourceView source ↗

Module documentation

Conjugation through maximal pro-`C` subgroup comparisons

Ambient conjugation descends intrinsically to the residual quotient of a closed normal subgroup. The comparison with a subgroup of a maximal pro-C quotient intertwines this action, including after topological abelianization.

Imports3

Imported by13

def

residualQuotientConjugationContinuousMulEquiv

L30 ↗

ProCGroups.ProC.residualQuotientConjugationContinuousMulEquiv

Documentation

Conjugation on a normal subgroup descends to its intrinsic residual quotient.

Source context 5 commands

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

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

Lean source · statement

def residualQuotientConjugationContinuousMulEquiv
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) (g : G) :
    N ⧸ proCResidualCore C N ≃ₜ* N ⧸ proCResidualCore C N

theorem

residualQuotientConjugationContinuousMulEquiv_apply_mk

L44 ↗

ProCGroups.ProC.residualQuotientConjugationContinuousMulEquiv_apply_mk

Documentation

The descended conjugation is computed on subgroup representatives.

Source context 5 commands

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

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

Lean source · statement

theorem residualQuotientConjugationContinuousMulEquiv_apply_mk
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) (g : G) (n : N) :
    residualQuotientConjugationContinuousMulEquiv hC N hN g
      (QuotientGroup.mk' (proCResidualCore C N) n) =
        QuotientGroup.mk' (proCResidualCore C N) (MulAut.conjNormal g n)

theorem

residualQuotientPreimageContinuousMulEquiv_conjugation

L56 ↗

ProCGroups.ProC.residualQuotientPreimageContinuousMulEquiv_conjugation

Documentation

The subgroup comparison intertwines intrinsic ambient conjugation.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
  [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]

Lean source · statement

theorem residualQuotientPreimageContinuousMulEquiv_conjugation
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom)
    (U : Subgroup Q) [U.Normal] (hU : IsClosed (U : Set Q)) (g : G)
    (z : U.comap π.toMonoidHom ⧸ proCResidualCore C (U.comap π.toMonoidHom)) :
    residualQuotientPreimageContinuousMulEquiv hC π hπ U hU
      (residualQuotientConjugationContinuousMulEquiv hC (U.comap π.toMonoidHom)
        (hU.preimage π.continuous_toFun) g z) =
      MulAut.conjNormal (π g)
        (residualQuotientPreimageContinuousMulEquiv hC π hπ U hU z)

theorem

residualQuotientPreimage_abelianization_conjugation

L80 ↗

ProCGroups.ProC.residualQuotientPreimage_abelianization_conjugation

Documentation

The comparison on abelianizations also preserves the conjugation action.

Source context 7 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
  [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
open Abelian

Lean source · statement

theorem residualQuotientPreimage_abelianization_conjugation
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom)
    (U : Subgroup Q) [U.Normal] (hU : IsClosed (U : Set Q)) (g : G)
    (a : TopologicalAbelianization
      (U.comap π.toMonoidHom ⧸ proCResidualCore C (U.comap π.toMonoidHom))) :
    TopologicalAbelianization.congr
      (residualQuotientPreimageContinuousMulEquiv hC π hπ U hU)
      (TopologicalAbelianization.congr
        (residualQuotientConjugationContinuousMulEquiv hC (U.comap π.toMonoidHom)
          (hU.preimage π.continuous_toFun) g) a) =
      TopologicalAbelianization.congr (Subgroup.conjNormalContinuousMulEquiv U (π g))
        (TopologicalAbelianization.congr
          (residualQuotientPreimageContinuousMulEquiv hC π hπ U hU) a)

Module documentation

Conjugation through maximal pro-C subgroup comparisons

Declarations

residualQuotientConjugationContinuousMulEquiv

residualQuotientConjugationContinuousMulEquiv_apply_mk

residualQuotientPreimageContinuousMulEquiv_conjugation

residualQuotientPreimage_abelianization_conjugation

Conjugation through maximal pro-`C` subgroup comparisons