Module

ResidualPrimeExclusion.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualPrimeExclusion

3 declarations indexed from sourceView source ↗

Module documentation

Pro-p subgroups in the Sigma residual core

When p is outside sigma, every continuous map from a group with an open-normal p-group basis to a Hausdorff group with a Sigma-group basis is trivial. Thus every pro-p subgroup lies in the actual Sigma residual core. The subgroup need not be closed or normal, and no compactness is required.

Imports2

Imported by2

theorem

continuousMonoidHom_eq_one_of_proP_to_finite_sigmaGroup

L25 ↗

ProCGroups.ProC.continuousMonoidHom_eq_one_of_proP_to_finite_sigmaGroup

Documentation

A continuous map from a group with a pro-p basis to a finite discrete Sigma-group is trivial when p is excluded from sigma.

Source context 2 commands

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

namespace ProCGroups.ProC
universe u v

Lean source · statement

theorem continuousMonoidHom_eq_one_of_proP_to_finite_sigmaGroup
    {G : Type u} [Group G] [TopologicalSpace G]
    {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (p : ℕ) [Fact p.Prime] {sigma : Set ℕ} (hp : p ∉ sigma)
    (hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
    (hQ : FiniteGroupClass.sigmaGroup sigma Q)
    (f : G →ₜ* Q) (x : G) : f x = 1

theorem

continuousMonoidHom_eq_one_of_proP_to_proSigma

L50 ↗

ProCGroups.ProC.continuousMonoidHom_eq_one_of_proP_to_proSigma

Documentation

Finite Sigma quotients separate a Hausdorff group with a pro-Sigma basis, so every continuous map to it from a pro-p group is trivial for excluded p.

Source context 2 commands

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

namespace ProCGroups.ProC
universe u v

Lean source · statement

theorem continuousMonoidHom_eq_one_of_proP_to_proSigma
    {G : Type u} [Group G] [TopologicalSpace G]
    {H : Type v} [Group H] [TopologicalSpace H] [ContinuousMul H] [T2Space H]
    (p : ℕ) [Fact p.Prime] {sigma : Set ℕ} (hp : p ∉ sigma)
    (hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
    (hH : HasOpenNormalBasisInClass (FiniteGroupClass.sigmaGroup sigma) H)
    (f : G →ₜ* H) (x : G) : f x = 1

theorem

subgroup_le_sigmaResidualCore_of_proP

L65 ↗

ProCGroups.ProC.subgroup_le_sigmaResidualCore_of_proP

Documentation

Every subgroup with a pro-p basis lies in the actual Sigma residual core when p is excluded. Neither closedness nor normality of the subgroup is needed.

Source context 2 commands

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

namespace ProCGroups.ProC
universe u v

Lean source · statement

theorem subgroup_le_sigmaResidualCore_of_proP
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (p : ℕ) [Fact p.Prime] {sigma : Set ℕ} (hp : p ∉ sigma)
    (P : Subgroup G)
    (hP : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) P) :
    P ≤ proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G

Module documentation

Pro-p subgroups in the Sigma residual core

Declarations

continuousMonoidHom_eq_one_of_proP_to_finite_sigmaGroup

continuousMonoidHom_eq_one_of_proP_to_proSigma

subgroup_le_sigmaResidualCore_of_proP