NYLL
Module

SigmaCentralizers.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.SigmaCentralizers
2 declarations indexed from sourceView source ↗

Module documentation

Centralizers in sigma-residual quotients

Sigma-abelian faithfulness makes the action on an open normal subgroup injective. An element centralizing that subgroup in a sigma-residual quotient consequently belongs to the subgroup.

Imports5
Imported by2

Declarations

theorem

sigmaFaithful_openNormal_action

L28 ↗
Yamaguchi26AbfaithfulGalois.sigmaFaithful_openNormal_action
Documentation

Faithfulness on an open normal subgroup, with ambient group G.

Source context 4 commands

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

open scoped commutatorElement
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
theorem sigmaFaithful_openNormal_action {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (sigma : Set ℕ) (hG : IsSigmaAbFaithful sigma G) (N : OpenNormalSubgroup G) :
    Function.Injective (residualAbelianizationQuotientConjugation
      (FiniteGroupClass.sigmaGroup_fullFormation sigma) (N : Subgroup G) N.isClosed)
theorem

sigmaQuotient_mem_openNormal_of_centralizes

L46 ↗
Yamaguchi26AbfaithfulGalois.sigmaQuotient_mem_openNormal_of_centralizes
Source context 4 commands

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

open scoped commutatorElement
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
theorem sigmaQuotient_mem_openNormal_of_centralizes {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (sigma : Set ℕ) (hG : IsSigmaAbFaithful sigma G)
    (D : ClosedSubgroup G) [(D : Subgroup G).Normal]
    (N : OpenNormalSubgroup G) (hDN : (D : Subgroup G) ≤ (N : Subgroup G))
    (x : G) (hx : QuotientGroup.mk' (sigmaResidualKernel sigma D) x ∈
      Subgroup.centralizer ((N : Subgroup G).map (QuotientGroup.mk' (sigmaResidualKernel sigma D)) :
        Set (G ⧸ sigmaResidualKernel sigma D))) : x ∈ (N : Subgroup G)

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