NYLL
Module

ResidualQuotientAction.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualQuotientAction
4 declarations indexed from sourceView source ↗

Module documentation

Quotient conjugation on abelianized residual quotients

Ambient conjugation acts on the actual residual quotient of a closed normal subgroup. Its topological abelianization kills internal conjugation, giving an action of the original quotient group, with a representative-wise criterion for faithfulness.

Imports4
Imported by15

Declarations

def

residualAbelianizationConjugationHom

L31 ↗
ProCGroups.ProC.residualAbelianizationConjugationHom
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 : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · full declaration
def residualAbelianizationConjugationHom
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :
    G →* MulAut (TopologicalAbelianization (N ⧸ proCResidualCore C N)) where
  toFun g := (TopologicalAbelianization.congr
    (residualQuotientConjugationContinuousMulEquiv hC N hN g)).toMulEquiv
  map_one' := by
    apply MulEquiv.ext
    intro a
    obtain ⟨z, rfl⟩ := TopologicalAbelianization.surjective_mk
      (N ⧸ proCResidualCore C N) a
    obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective (proCResidualCore C N) z
    change TopologicalAbelianization.congr
        (residualQuotientConjugationContinuousMulEquiv hC N hN (1 : G))
        (TopologicalAbelianization.mk (N ⧸ proCResidualCore C N)
          (QuotientGroup.mk' (proCResidualCore C N) x)) =
      TopologicalAbelianization.mk (N ⧸ proCResidualCore C N)
        (QuotientGroup.mk' (proCResidualCore C N) x)
    rw [TopologicalAbelianization.congr_apply_mk,
      residualQuotientConjugationContinuousMulEquiv_apply_mk]
    exact congrArg
      (fun y : N => TopologicalAbelianization.mk (N ⧸ proCResidualCore C N)
        (QuotientGroup.mk' (proCResidualCore C N) y))
      (DFunLike.congr_fun (map_one (MulAut.conjNormal (H := N))) x)
  map_mul' g h := by
    apply MulEquiv.ext
    intro a
    obtain ⟨z, rfl⟩ := TopologicalAbelianization.surjective_mk
      (N ⧸ proCResidualCore C N) a
    obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective (proCResidualCore C N) z
    change TopologicalAbelianization.congr
        (residualQuotientConjugationContinuousMulEquiv hC N hN (g * h))
        (TopologicalAbelianization.mk (N ⧸ proCResidualCore C N)
          (QuotientGroup.mk' (proCResidualCore C N) x)) =
      TopologicalAbelianization.congr
        (residualQuotientConjugationContinuousMulEquiv hC N hN g)
        (TopologicalAbelianization.congr
          (residualQuotientConjugationContinuousMulEquiv hC N hN h)
          (TopologicalAbelianization.mk (N ⧸ proCResidualCore C N)
            (QuotientGroup.mk' (proCResidualCore C N) x)))
    simp only [TopologicalAbelianization.congr_apply_mk,
      residualQuotientConjugationContinuousMulEquiv_apply_mk]
    simpa only [MulAut.mul_apply] using congrArg
      (fun y : N => TopologicalAbelianization.mk (N ⧸ proCResidualCore C N)
        (QuotientGroup.mk' (proCResidualCore C N) y))
      (DFunLike.congr_fun (map_mul (MulAut.conjNormal (H := N)) g h) x)
def

residualAbelianizationQuotientConjugation

L80 ↗
ProCGroups.ProC.residualAbelianizationQuotientConjugation
Documentation

The original quotient acts by actual conjugation on the abelianized residual quotient of its closed normal subgroup.

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 : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def residualAbelianizationQuotientConjugation
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :
    (G ⧸ N) →* MulAut (TopologicalAbelianization (N ⧸ proCResidualCore C N))
theorem

residualAbelianizationQuotientConjugation_mk

L114 ↗
ProCGroups.ProC.residualAbelianizationQuotientConjugation_mk
Documentation

On an ambient representative, the quotient action is the already constructed continuous residual conjugation followed by abelianization.

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 : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem residualAbelianizationQuotientConjugation_mk
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) (g : G) :
    residualAbelianizationQuotientConjugation hC N hN (QuotientGroup.mk' N g) =
      (TopologicalAbelianization.congr
        (residualQuotientConjugationContinuousMulEquiv hC N hN g)).toMulEquiv
theorem

residualAbelianizationQuotientConjugation_injective_iff

L124 ↗
ProCGroups.ProC.residualAbelianizationQuotientConjugation_injective_iff
Documentation

Faithfulness is exactly nontriviality of actual conjugation for every ambient representative outside the subgroup; no quotient finiteness is needed.

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 : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem residualAbelianizationQuotientConjugation_injective_iff
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :
    Function.Injective (residualAbelianizationQuotientConjugation hC N hN) ↔
      ∀ g : G, g ∉ N →
        (TopologicalAbelianization.congr
          (residualQuotientConjugationContinuousMulEquiv hC N hN g)).toMulEquiv ≠ 1

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