Documentation

Q2Presentation.Induction.Section7ChiefCentral

The wild kernel centralizes the chief factor (lem:collapse, step (iii)) #

⁅P, L_Y⁆ ≤ S: the descending chain C₀ = P, Cₙ₊₁ = ⁅Cₙ, L_Y⁆ consists of Y-normal subgroups of P; at each stage the chief dichotomy either drops Cₙ₊₁ ⊔ S to S — which forces ⁅P, L_Y⁆ ≤ S by the sup decomposition — or keeps it at P. The chain is dominated by the lower central series of the finite nilpotent 2-group L_Y, which reaches ⊥; riding the second branch to the end would force P = S.

This is what makes the Y-action on the chief factor V = P/S factor through the tame quotient H = Y/L_Y — the input for the coprime steps of lem:collapse and the "action through a 2-group is trivial" contradiction.

Everything here is proved — no axioms.

source
def Q2Presentation.Induction.chiefDescC {p : FramedPair} (chief : NonScalarChiefFactor p) :
ℕ → Subgroup p.fst.Y

The descending commutator chain C₀ = P, Cₙ₊₁ = ⁅Cₙ, L_Y⁆.

Equations
Instances For
    source
    theorem Q2Presentation.Induction.chiefDescC_normal {p : FramedPair} {chief : NonScalarChiefFactor p} (n : ℕ) :
    (chiefDescC chief n).Normal
    source
    theorem Q2Presentation.Induction.chiefDescC_le_upper {p : FramedPair} {chief : NonScalarChiefFactor p} (n : ℕ) :
    chiefDescC chief n ≤ chief.upper
    source
    theorem Q2Presentation.Induction.chiefDescC_le_map_lcs {p : FramedPair} {chief : NonScalarChiefFactor p} (n : ℕ) :
    chiefDescC chief (n + 1) ≤ Subgroup.map p.fst.LY.subtype (lowerCentralSeries (↥p.fst.LY) n)

    The chain is dominated by the lower central series of L_Y.

    source
    theorem Q2Presentation.Induction.chief_LY_commutator_le_lower {p : FramedPair} {chief : NonScalarChiefFactor p} :
    ⁅chief.upper, p.fst.LY⁆ ≤ chief.lower

    The wild kernel centralizes the chief factor: ⁅P, L_Y⁆ ≤ S.

    source
    theorem Q2Presentation.Induction.chief_LY_commutator_mem_lower {p : FramedPair} {chief : NonScalarChiefFactor p} {l a : p.fst.Y} (hl : l ∈ p.fst.LY) (ha : a ∈ chief.upper) :
    ⁅l, a⁆ ∈ chief.lower

    Elementwise form: ⁅l, a⁆ ∈ S for l ∈ L_Y, a ∈ P.