Fixed-vector setup for the lower branch of lem:collapse

The remaining lower branch has a normal subgroup P0 ◁ Y of 2-power index such that [P,P0] ≤ S. This file starts the fixed-vector contradiction by building the literal conjugation action on the chief quotient P/S and proving that P0 fixes it pointwise.

@[reducible, inline]

abbrev Q2Presentation.Induction.chiefFactor {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

The chief quotient P/S as a group.

Equations

• Q2Presentation.Induction.chiefFactor chief = (↥chief.upper ⧸ chief.lower.subgroupOf chief.upper)

instance Q2Presentation.Induction.chiefLowerSubgroupOfNormal {p : FramedPair} (chief : NonScalarChiefFactor p) : (chief.lower.subgroupOf chief.upper).Normal

instance Q2Presentation.Induction.chiefFactorGroup {p : FramedPair} (chief : NonScalarChiefFactor p) : Group (chiefFactor chief)

Equations

• Q2Presentation.Induction.chiefFactorGroup chief = id inferInstance

instance Q2Presentation.Induction.chiefFactorFinite {p : FramedPair} (chief : NonScalarChiefFactor p) : Finite (chiefFactor chief)

def Q2Presentation.Induction.chiefUpperConjAut {p : FramedPair} (chief : NonScalarChiefFactor p) (y : p.fst.Y) : ↥chief.upper ≃* ↥chief.upper

Conjugation by an ambient element, restricted to the chief upper term.

Equations

• Q2Presentation.Induction.chiefUpperConjAut chief y = MulAut.conjNormal y

@[simp]

theorem Q2Presentation.Induction.chiefUpperConjAut_apply_coe {p : FramedPair} (chief : NonScalarChiefFactor p) (y : p.fst.Y) (u : ↥chief.upper) : ↑((chiefUpperConjAut chief y) u) = y * ↑u * y⁻¹

def Q2Presentation.Induction.chiefFactorConjHom {p : FramedPair} (chief : NonScalarChiefFactor p) (y : p.fst.Y) : chiefFactor chief →* chiefFactor chief

Conjugation by y on the chief quotient P/S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.Induction.chiefFactorConjHom_mk {p : FramedPair} (chief : NonScalarChiefFactor p) (y : p.fst.Y) (u : ↥chief.upper) : (chiefFactorConjHom chief y) ((QuotientGroup.mk' (chief.lower.subgroupOf chief.upper)) u) = (QuotientGroup.mk' (chief.lower.subgroupOf chief.upper)) ((chiefUpperConjAut chief y) u)

instance Q2Presentation.Induction.chiefFactorMulAction {p : FramedPair} (chief : NonScalarChiefFactor p) : MulAction p.fst.Y (chiefFactor chief)

The left conjugation action of Y on P/S.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.chiefFactor_fixed_by_of_commutator_le_lower {p : FramedPair} (chief : NonScalarChiefFactor p) (P0 : Subgroup p.fst.Y) (hact : ⁅chief.upper, P0⁆ ≤ chief.lower) (p0 : ↥P0) (q : chiefFactor chief) : ↑p0 • q = q

If [P,P0] ≤ S, every element of P0 fixes the chief quotient P/S.