Module

DegreeTwo.lean

Nyll.ProCGroups.ProP.Zassenhaus.DegreeTwo

4 declarations indexed from sourceView source ↗

Module documentation

The second Zassenhaus subgroup

For a topologically finitely generated pro-p group, the closed power--commutator subgroup is open. Projection to this finite elementary quotient detects a degree-two completed augmentation relation. The finite degree-one criterion then gives the reverse inclusion to the elementary power--commutator subgroup, complementing the inclusion proved in Basic.

Imports3

Imported by2

def

closedPowerCommutatorOpenNormal

L38 ↗

ClassFieldTower.ProP.closedPowerCommutatorOpenNormal

Documentation

The closed power--commutator subgroup, bundled as an open normal subgroup when the ambient group is topologically finitely generated.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def closedPowerCommutatorOpenNormal
    (hfg : TopologicallyFinitelyGenerated G) : OpenNormalSubgroup G

theorem

mem_closedPowerCommutator_of_groupLikeDifference_mem_degree_two

L65 ↗

ClassFieldTower.ProP.mem_closedPowerCommutator_of_groupLikeDifference_mem_degree_two

Documentation

A completed degree-two augmentation relation forces membership in the closed power--commutator subgroup.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem mem_closedPowerCommutator_of_groupLikeDifference_mem_degree_two
    (hpG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : TopologicallyFinitelyGenerated G) (g : G)
    (hg : groupLikeDifference p G g ∈ closedAugmentationPower p G 2) :
    g ∈ closedPowerCommutator p G

theorem

zassenhausSubgroup_two_le_closedPowerCommutator

L202 ↗

ClassFieldTower.ProP.zassenhausSubgroup_two_le_closedPowerCommutator

Documentation

The second Zassenhaus subgroup is contained in the closed power--commutator subgroup for a finitely generated pro-p group.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem zassenhausSubgroup_two_le_closedPowerCommutator
    (hpG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : TopologicallyFinitelyGenerated G) :
    zassenhausSubgroup p G 2 ≤ closedPowerCommutator p G

theorem

zassenhausSubgroup_two_eq_closedPowerCommutator

L211 ↗

ClassFieldTower.ProP.zassenhausSubgroup_two_eq_closedPowerCommutator

Documentation

The second Zassenhaus subgroup is the closed subgroup generated by p-th powers and commutators.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem zassenhausSubgroup_two_eq_closedPowerCommutator
    (hpG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : TopologicallyFinitelyGenerated G) :
    zassenhausSubgroup p G 2 = closedPowerCommutator p G

Module documentation

The second Zassenhaus subgroup

Declarations

closedPowerCommutatorOpenNormal

mem_closedPowerCommutator_of_groupLikeDifference_mem_degree_two

zassenhausSubgroup_two_le_closedPowerCommutator

zassenhausSubgroup_two_eq_closedPowerCommutator