NYLL
Module

ResidualQuotientTransport.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualQuotientTransport
7 declarations indexed from sourceView source ↗

Module documentation

Transport of residual quotient conjugation

An ambient continuous group equivalence transports a closed subgroup's intrinsic residual quotient. The induced equivalence on topological abelianizations intertwines actual conjugation, so the corresponding quotient actions are faithful simultaneously.

Imports9
Imported by10

Declarations

def

subgroupMapContinuousMulEquiv

L36 ↗
ProCGroups.ProC.subgroupMapContinuousMulEquiv
Source context 5 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
Lean source · full declaration
def subgroupMapContinuousMulEquiv (e : G ≃ₜ* H) (N : Subgroup G) :
    N ≃ₜ* N.map e.toMulEquiv.toMonoidHom where
  toMulEquiv := e.toMulEquiv.subgroupMap N
  continuous_toFun := by
    apply Continuous.subtype_mk
    exact e.continuous_toFun.comp continuous_subtype_val
  continuous_invFun := by
    apply Continuous.subtype_mk
    exact e.symm.continuous_toFun.comp continuous_subtype_val
theorem

subgroupMap_normal

L46 ↗
ProCGroups.ProC.subgroupMap_normal
Source context 5 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
Lean source · statement
theorem subgroupMap_normal (e : G ≃ₜ* H) (N : Subgroup G) [h : N.Normal] :
    (N.map e.toMulEquiv.toMonoidHom).Normal
theorem

subgroupMap_isClosed

L50 ↗
ProCGroups.ProC.subgroupMap_isClosed
Source context 5 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
Lean source · statement
theorem subgroupMap_isClosed (e : G ≃ₜ* H) (N : Subgroup G)
    (hN : IsClosed (N : Set G)) :
    IsClosed ((N.map e.toMulEquiv.toMonoidHom : Subgroup H) : Set H)
def

residualQuotientSubgroupTransport

L62 ↗
ProCGroups.ProC.residualQuotientSubgroupTransport
Documentation

An ambient equivalence induces an equivalence of the actual residual quotients of a closed subgroup and its image.

Source context 7 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
attribute [local instance] subgroupMap_normal
variable [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [T2Space H] [TotallyDisconnectedSpace G]
Lean source · statement
def residualQuotientSubgroupTransport
    (hC : FiniteGroupClass.FullFormation C) (e : G ≃ₜ* H)
    (N : Subgroup G) (hN : IsClosed (N : Set G)) :
    N ⧸ proCResidualCore C N ≃ₜ*
      N.map e.toMulEquiv.toMonoidHom ⧸
        proCResidualCore C (N.map e.toMulEquiv.toMonoidHom)
theorem

residualQuotientSubgroupTransport_apply_mk

L80 ↗
ProCGroups.ProC.residualQuotientSubgroupTransport_apply_mk
Documentation

Transport is evaluated by the original ambient equivalence.

Source context 7 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
attribute [local instance] subgroupMap_normal
variable [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [T2Space H] [TotallyDisconnectedSpace G]
Lean source · statement
theorem residualQuotientSubgroupTransport_apply_mk
    (hC : FiniteGroupClass.FullFormation C) (e : G ≃ₜ* H)
    (N : Subgroup G) (hN : IsClosed (N : Set G)) (x : N) :
    residualQuotientSubgroupTransport hC e N hN
        (QuotientGroup.mk' (proCResidualCore C N) x) =
      QuotientGroup.mk' (proCResidualCore C (N.map e.toMulEquiv.toMonoidHom))
        (e.toMulEquiv.subgroupMap N x)
theorem

residualAbelianizationSubgroupTransport_conjugation

L93 ↗
ProCGroups.ProC.residualAbelianizationSubgroupTransport_conjugation
Documentation

The induced transport on abelianizations intertwines actual ambient conjugation, with the conjugating element transported by the same equivalence.

Source context 8 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
attribute [local instance] subgroupMap_normal
variable [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [T2Space H] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [TotallyDisconnectedSpace H]
Lean source · statement
theorem residualAbelianizationSubgroupTransport_conjugation
    (hC : FiniteGroupClass.FullFormation C) (e : G ≃ₜ* H)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) (g : G)
    (a : TopologicalAbelianization (N ⧸ proCResidualCore C N)) :
    TopologicalAbelianization.congr (residualQuotientSubgroupTransport hC e N hN)
        (TopologicalAbelianization.congr
          (residualQuotientConjugationContinuousMulEquiv hC N hN g) a) =
      TopologicalAbelianization.congr
        (residualQuotientConjugationContinuousMulEquiv hC
          (N.map e.toMulEquiv.toMonoidHom) (subgroupMap_isClosed e N hN) (e g))
        (TopologicalAbelianization.congr
          (residualQuotientSubgroupTransport hC e N hN) a)
theorem

residualAbelianizationQuotientConjugation_injective_map_iff

L122 ↗
ProCGroups.ProC.residualAbelianizationQuotientConjugation_injective_map_iff
Documentation

Faithfulness of residual abelianized quotient conjugation is preserved by an ambient continuous group equivalence.

Source context 8 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {G H : Type u} [Group G] [Group H]
  [TopologicalSpace G] [TopologicalSpace H]
attribute [local instance] subgroupMap_normal
variable [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [T2Space H] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [TotallyDisconnectedSpace H]
Lean source · statement
theorem residualAbelianizationQuotientConjugation_injective_map_iff
    (hC : FiniteGroupClass.FullFormation C) (e : G ≃ₜ* H)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :
    Function.Injective (residualAbelianizationQuotientConjugation hC
      (N.map e.toMulEquiv.toMonoidHom) (subgroupMap_isClosed e N hN)) ↔
      Function.Injective (residualAbelianizationQuotientConjugation hC N hN)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.