NYLL
Module

FiniteDegreeOne.lean

Nyll.ProCGroups.ProP.Zassenhaus.FiniteDegreeOne
6 declarations indexed from sourceView source ↗

Module documentation

Degree-one augmentation criterion for finite p-groups

Linear functionals on the elementary power--commutator quotient separate a nonzero class. Combined with dual-number linearization, this proves that [q]-1 ∈ I² forces q into the closed power--commutator subgroup. In a finite p-group, P03 identifies that subgroup with Frattini.

Imports3
Imported by2

Declarations

instance

finiteDegreeOneClosedPowerCommutatorNormal

L37 ↗
ClassFieldTower.ProP.finiteDegreeOneClosedPowerCommutatorNormal
Source context 9 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (Q : Type u) [Group Q]
section Separation
variable [TopologicalSpace Q] [IsTopologicalGroup Q]
Lean source · statement
instance finiteDegreeOneClosedPowerCommutatorNormal :
    (closedPowerCommutator p Q).Normal
instance

finiteDegreeOnePowerCommutatorComm

L41 ↗
ClassFieldTower.ProP.finiteDegreeOnePowerCommutatorComm
Source context 10 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (Q : Type u) [Group Q]
section Separation
variable [TopologicalSpace Q] [IsTopologicalGroup Q]
local instance finiteDegreeOneClosedPowerCommutatorNormal :
    (closedPowerCommutator p Q).Normal :=
  closedPowerCommutator_normal p Q
Lean source · statement
instance finiteDegreeOnePowerCommutatorComm :
    IsMulCommutative (powerCommutatorQuotient p Q)
instance

finiteDegreeOnePowerCommutatorModule

L45 ↗
ClassFieldTower.ProP.finiteDegreeOnePowerCommutatorModule
Source context 11 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (Q : Type u) [Group Q]
section Separation
variable [TopologicalSpace Q] [IsTopologicalGroup Q]
local instance finiteDegreeOneClosedPowerCommutatorNormal :
    (closedPowerCommutator p Q).Normal :=
  closedPowerCommutator_normal p Q
local instance finiteDegreeOnePowerCommutatorComm :
    IsMulCommutative (powerCommutatorQuotient p Q) :=
  powerCommutatorQuotient_isMulCommutative p Q
Lean source · statement
instance finiteDegreeOnePowerCommutatorModule :
    Module (ZMod p) (Additive (powerCommutatorQuotient p Q))
theorem

mem_closedPowerCommutator_of_generator_mem_augmentationIdeal_sq

L53 ↗
ClassFieldTower.ProP.mem_closedPowerCommutator_of_generator_mem_augmentationIdeal_sq
Documentation

Membership of a standard augmentation generator in I² forces the group element into the closed power--commutator subgroup.

Source context 12 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (Q : Type u) [Group Q]
section Separation
variable [TopologicalSpace Q] [IsTopologicalGroup Q]
local instance finiteDegreeOneClosedPowerCommutatorNormal :
    (closedPowerCommutator p Q).Normal :=
  closedPowerCommutator_normal p Q
local instance finiteDegreeOnePowerCommutatorComm :
    IsMulCommutative (powerCommutatorQuotient p Q) :=
  powerCommutatorQuotient_isMulCommutative p Q
local instance finiteDegreeOnePowerCommutatorModule :
    Module (ZMod p) (Additive (powerCommutatorQuotient p Q)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p Q (Additive.toMul x)
Lean source · statement
theorem mem_closedPowerCommutator_of_generator_mem_augmentationIdeal_sq
    (q : Q)
    (hq : groupAlgebraAugmentationGenerator (ZMod p) Q q ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2) :
    q ∈ closedPowerCommutator p Q
theorem

closedPowerCommutator_le_augmentationSquareSubgroup

L85 ↗
ClassFieldTower.ProP.closedPowerCommutator_le_augmentationSquareSubgroup
Documentation

In a finite T₁ group, every element of the closed power--commutator subgroup has its standard augmentation generator in I².

Source context 9 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (Q : Type u) [Group Q]
section FiniteComparison
variable [TopologicalSpace Q] [IsTopologicalGroup Q] [T1Space Q] [Finite Q]
Lean source · statement
theorem closedPowerCommutator_le_augmentationSquareSubgroup :
    closedPowerCommutator p Q ≤ augmentationSquareSubgroup p Q
theorem

groupAlgebraAugmentationGenerator_mem_sq_iff_mem_frattini

L94 ↗
ClassFieldTower.ProP.groupAlgebraAugmentationGenerator_mem_sq_iff_mem_frattini
Documentation

The degree-one augmentation criterion for a finite T₁ p-group.

Source context 9 commands

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

open scoped IsMulCommutative
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (Q : Type u) [Group Q]
section FiniteComparison
variable [TopologicalSpace Q] [IsTopologicalGroup Q] [T1Space Q] [Finite Q]
Lean source · statement
theorem groupAlgebraAugmentationGenerator_mem_sq_iff_mem_frattini
    (hQ : IsPGroup p Q) (q : Q) :
    groupAlgebraAugmentationGenerator (ZMod p) Q q ∈
        (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2 ↔
      q ∈ frattini Q

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