Fixed lifts and the chiefness contradiction

The fixed-vector theorem produces a non-identity class in P/S fixed by Y. Here we convert such a class into the manuscript's chief-factor contradiction: the fixed classes lift to a Y-normal subgroup between S and P; since the class is nontrivial this subgroup is not S, hence chiefness forces it to be P, making the whole chief factor trivial.

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

The conjugation action on P/S is by group automorphisms.

Equations

• Q2Presentation.Induction.chiefFactorMulDistribMulAction chief = { toMulAction := Q2Presentation.Induction.chiefFactorMulAction chief, smul_mul := ⋯, smul_one := ⋯ }

def Q2Presentation.Induction.chiefFixedLift {p : FramedPair} (chief : NonScalarChiefFactor p) : Subgroup p.fst.Y

The subgroup of P whose classes in P/S are fixed by all of Y.

Equations

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

theorem Q2Presentation.Induction.chiefFixedLift_le_upper {p : FramedPair} (chief : NonScalarChiefFactor p) : chiefFixedLift chief ≤ chief.upper

The fixed lift lies in the chief upper term.

theorem Q2Presentation.Induction.chief_lower_le_fixedLift {p : FramedPair} (chief : NonScalarChiefFactor p) : chief.lower ≤ chiefFixedLift chief

The chief lower term lies in the fixed lift.

theorem Q2Presentation.Induction.chiefFixedLift_normal {p : FramedPair} (chief : NonScalarChiefFactor p) : (chiefFixedLift chief).Normal

The fixed lift is normal in the ambient finite target.

theorem Q2Presentation.Induction.chief_lower_lt_fixedLift_of_exists_nontrivial_fixed {p : FramedPair} (chief : NonScalarChiefFactor p) (hfix : ∃ (q : chiefFactor chief), q ≠ 1 ∧ ∀ (y : p.fst.Y), y • q = q) : chief.lower < chiefFixedLift chief

A nontrivial globally fixed class makes the fixed lift strictly larger than S.

theorem Q2Presentation.Induction.chiefFactorTrivial_of_exists_nontrivial_fixed {p : FramedPair} (chief : NonScalarChiefFactor p) (hfix : ∃ (q : chiefFactor chief), q ≠ 1 ∧ ∀ (y : p.fst.Y), y • q = q) : ChiefFactorTrivial p.fst chief.lower chief.upper

If a nontrivial globally fixed class exists, the chief factor is trivial.

theorem Q2Presentation.Induction.not_exists_nontrivial_chiefFactor_fixed_by_all {p : FramedPair} (chief : NonScalarChiefFactor p) : ¬∃ (q : chiefFactor chief), q ≠ 1 ∧ ∀ (y : p.fst.Y), y • q = q

A nontrivial globally fixed class contradicts the non-scalar chief choice.