Module

ProsolvableCriterion.lean

Nyll.ProCGroups.FiniteStepSolvableQuotients.ProsolvableCriterion

12 declarations indexed from sourceView source ↗

Module documentation

A local-abelianization criterion for prosolvable quotients

This file proves the profinite group-theoretic criterion used in the boundary argument: a continuous epimorphism inducing injections on the abelianizations of the preimages of all open normal subgroups admits a unique factorization of every finite solvable quotient of the source. It then identifies the concrete prosolvable residual quotients of source and target.

Imports8

Imported by5

def

OpenNormalAbelianizationInjective

L33 ↗

ProCGroups.FiniteStepSolvableQuotients.OpenNormalAbelianizationInjective

Documentation

The local abelianization maps over all open normal subgroups are injective. Surjectivity of these maps follows from surjectivity of the original homomorphism.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

def OpenNormalAbelianizationInjective
    {G Q : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (f : G →ₜ* Q) : Prop

def

OpenNormalFiniteDiscreteAbelianMapsKillKernel

L44 ↗

ProCGroups.FiniteStepSolvableQuotients.OpenNormalFiniteDiscreteAbelianMapsKillKernel

Documentation

On every open normal subgroup of the target, all finite discrete abelian representations of its preimage kill the kernel of the restricted map.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

def OpenNormalFiniteDiscreteAbelianMapsKillKernel
    {G Q : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (f : G →ₜ* Q) : Prop

theorem

injective_topMaxSolvQuotMap_one_of_finiteDiscreteAbelianMapsKillKernel

L54 ↗

ProCGroups.FiniteStepSolvableQuotients.injective_topMaxSolvQuotMap_one_of_finiteDiscreteAbelianMapsKillKernel

Documentation

A surjection whose kernel is killed by every finite discrete abelian representation induces an injective map on topological abelianizations.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem injective_topMaxSolvQuotMap_one_of_finiteDiscreteAbelianMapsKillKernel
    {G Q : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q] [T2Space Q]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hkill : ProCGroups.ProC.FiniteDiscreteAbelianMapsKillKernel f) :
    Function.Injective (topMaxSolvQuotMap f 1)

theorem

openNormalAbelianizationInjective_of_finiteDiscreteAbelianMapsKillKernel

L86 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalAbelianizationInjective_of_finiteDiscreteAbelianMapsKillKernel

Documentation

Finite discrete abelian representations on all open-normal preimages supply the local abelianization hypothesis used by the prosolvable quotient criterion.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem openNormalAbelianizationInjective_of_finiteDiscreteAbelianMapsKillKernel
    {G Q : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q] [T2Space Q]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hkill : OpenNormalFiniteDiscreteAbelianMapsKillKernel f) :
    OpenNormalAbelianizationInjective f

theorem

restrictPreimage_ker_le_topDerived_one

L114 ↗

ProCGroups.FiniteStepSolvableQuotients.restrictPreimage_ker_le_topDerived_one

Documentation

Injectivity on a preimage abelianization puts the kernel of the restricted map in the first closed derived subgroup.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem restrictPreimage_ker_le_topDerived_one
    {G Q : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {f : G →ₜ* Q} (hAb : OpenNormalAbelianizationInjective f)
    (H : OpenNormalSubgroup Q) :
    (ProCGroups.ContinuousMonoidHom.restrictPreimage f (H : Subgroup Q)).ker ≤
      topDerivedTop ↥((H : Subgroup Q).comap (f : G →* Q)) 1

def

openNormalAbelianizationContinuousMulEquiv

L143 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalAbelianizationContinuousMulEquiv

Documentation

A surjection satisfying the local injectivity condition induces a topological isomorphism on the abelianization over every open normal subgroup.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

def openNormalAbelianizationContinuousMulEquiv
    {G Q : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [CompactSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q] [T2Space Q]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hAb : OpenNormalAbelianizationInjective f)
    (H : OpenNormalSubgroup Q) :
    MaxSolvQuot ((H : Subgroup Q).comap (f : G →* Q)) 1 ≃ₜ*
      MaxSolvQuot (H : Subgroup Q) 1

def

factorThroughOfSurjective

L183 ↗

ProCGroups.FiniteStepSolvableQuotients.factorThroughOfSurjective

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

def factorThroughOfSurjective
    {G Q A : Type u} [TopologicalSpace G] [Group G] [CompactSpace G]
    [TopologicalSpace Q] [Group Q] [T2Space Q]
    [TopologicalSpace A] [Group A]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (q : G →ₜ* A) (hker : f.ker ≤ q.ker) : Q →ₜ* A

theorem

factorThroughOfSurjective_comp

L205 ↗

ProCGroups.FiniteStepSolvableQuotients.factorThroughOfSurjective_comp

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem factorThroughOfSurjective_comp
    {G Q A : Type u} [TopologicalSpace G] [Group G] [CompactSpace G]
    [TopologicalSpace Q] [Group Q] [T2Space Q]
    [TopologicalSpace A] [Group A]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (q : G →ₜ* A) (hker : f.ker ≤ q.ker) :
    (factorThroughOfSurjective f hf q hker).comp f = q

theorem

ker_le_ker_finite_solvable_quotient

L219 ↗

ProCGroups.FiniteStepSolvableQuotients.ker_le_ker_finite_solvable_quotient

Documentation

Under the open-normal abelianization hypothesis, the kernel of f is killed by every surjective continuous finite solvable quotient of the source.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem ker_le_ker_finite_solvable_quotient
    {G Q S : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [T2Space Q]
    [TopologicalSpace S] [Group S] [DiscreteTopology S] [Group.IsSolvable S]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hAb : OpenNormalAbelianizationInjective f)
    (q : G →ₜ* S) (hq : Function.Surjective q) :
    f.ker ≤ q.ker

theorem

finite_solvable_quotient_existsUnique_factorization

L300 ↗

ProCGroups.FiniteStepSolvableQuotients.finite_solvable_quotient_existsUnique_factorization

Documentation

Every surjective continuous finite solvable quotient of the source factors uniquely through f. This is the operational finite-quotient form of the prosolvable criterion.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem finite_solvable_quotient_existsUnique_factorization
    {G Q S : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [T2Space Q]
    [TopologicalSpace S] [Group S] [DiscreteTopology S] [Group.IsSolvable S]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hAb : OpenNormalAbelianizationInjective f)
    (q : G →ₜ* S) (hq : Function.Surjective q) :
    ∃! r : Q →ₜ* S, r.comp f = q

theorem

ker_le_prosolvableResidualCore

L324 ↗

ProCGroups.FiniteStepSolvableQuotients.ker_le_prosolvableResidualCore

Documentation

The kernel of f lies in the prosolvable residual core of the source.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem ker_le_prosolvableResidualCore
    {G Q : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q] [T2Space Q]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hAb : OpenNormalAbelianizationInjective f) :
    f.ker ≤ ProCGroups.ProC.proCResidualCore FiniteGroupClass.solvable G

def

prosolvableResidualQuotientContinuousMulEquiv

L363 ↗

ProCGroups.FiniteStepSolvableQuotients.prosolvableResidualQuotientContinuousMulEquiv

Documentation

A local isomorphism on all open-normal abelianizations induces an equivalence on the prosolvable residual quotients.

Source context 3 commands

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

open scoped ProCGroupsSolvableQuotients
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

def prosolvableResidualQuotientContinuousMulEquiv
    {G Q : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q] [T2Space Q]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hAb : OpenNormalAbelianizationInjective f) :
    (G ⧸ ProCGroups.ProC.proCResidualCore FiniteGroupClass.solvable G) ≃ₜ*
      (Q ⧸ ProCGroups.ProC.proCResidualCore FiniteGroupClass.solvable Q)

Module documentation

A local-abelianization criterion for prosolvable quotients

Declarations