Documentation

Q2Presentation.Induction.Section7FixedVectorBranch

The fixed-vector branch for lem:collapse #

This file turns the lower-branch action statement [P,P0] ≤ S into the finite 2-group fixed-point input used in the manuscript's collapse argument.

source
theorem Q2Presentation.Induction.chiefFactor_isTwoGroup {p : FramedPair} (chief : NonScalarChiefFactor p) :
IsPGroup 2 (chiefFactor chief)

The chief quotient P/S is a finite 2-group.

source
theorem Q2Presentation.Induction.chiefFactor_nontrivial {p : FramedPair} (chief : NonScalarChiefFactor p) :
Nontrivial (chiefFactor chief)

The chief quotient P/S is nontrivial because S < P.

source
theorem Q2Presentation.Induction.two_dvd_card_chiefFactor {p : FramedPair} (chief : NonScalarChiefFactor p) :
2 ∣ Nat.card (chiefFactor chief)

The nontrivial chief quotient has even cardinality.

source
theorem Q2Presentation.Induction.quotient_isTwoGroup_of_index_pow_two {p : FramedPair} (P0 : Subgroup p.fst.Y) [P0.Normal] (hidx : ∃ (k : ℕ), P0.index = 2 ^ k) :
IsPGroup 2 (p.fst.Y ⧸ P0)

A normal subgroup of 2-power index has a finite 2-group quotient.

source
def Q2Presentation.Induction.chiefFactorFixedBySubgroupEquiv {p : FramedPair} (chief : NonScalarChiefFactor p) (P0 : Subgroup p.fst.Y) (hact : ⁅chief.upper, P0⁆ ≤ chief.lower) :
chiefFactor chief ≃ ↑(MulAction.fixedPoints (↥P0) (chiefFactor chief))

If P0 acts trivially on P/S, then all chief-factor elements are exactly the P0-fixed points.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Q2Presentation.Induction.two_dvd_card_chiefFactor_fixedBy {p : FramedPair} (chief : NonScalarChiefFactor p) (P0 : Subgroup p.fst.Y) (hact : ⁅chief.upper, P0⁆ ≤ chief.lower) :
    2 ∣ Nat.card ↑(MulAction.fixedPoints (↥P0) (chiefFactor chief))

    The P0-fixed-point set in P/S also has even cardinality.

    source
    theorem Q2Presentation.Induction.exists_nontrivial_chiefFactor_fixed_by_all_of_commutator_le_lower {p : FramedPair} (chief : NonScalarChiefFactor p) (P0 : Subgroup p.fst.Y) [P0.Normal] (hidx : ∃ (k : ℕ), P0.index = 2 ^ k) (hact : ⁅chief.upper, P0⁆ ≤ chief.lower) :
    ∃ (q : chiefFactor chief), q ≠ 1 ∧ ∀ (y : p.fst.Y), y • q = q

    If the normal 2-power-index subgroup P0 acts trivially on P/S, then some nontrivial element of P/S is fixed by all of Y.

    This is the finite 2-group fixed-point step in the remaining lower branch.