noncomputable def Q2Presentation.Induction.mstageMEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : towerMgrp K ≃* ↥K.Ksub

The multiplicative identification K/Φ(K) ≅ K at the mstage stage.

Equations

• Q2Presentation.Induction.mstageMEquiv chief K hR = (QuotientGroup.quotientMulEquivOfEq ⋯).trans QuotientGroup.quotientBot

noncomputable def Q2Presentation.Induction.mstageMAddEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : towerM K ≃+ Lifting.NAdd (mstageKernel chief K hR)

The additive identification towerM K ≃+ NAdd (mstageKernel).

Equations

• Q2Presentation.Induction.mstageMAddEquiv chief K hR = MulEquiv.toAdditive (Q2Presentation.Induction.mstageMEquiv chief K hR)

noncomputable def Q2Presentation.Induction.mstageDualPull {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (f : Module.Dual (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))) : Module.Dual (ZMod 2) (towerM K)

Pull an mstage-kernel functional back to the tower module.

Equations

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

theorem Q2Presentation.Induction.mstage_hinv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (f : Module.Dual (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))) : (∀ (y : p.fst.Y) (m : Lifting.NAdd (mstageKernel chief K hR)), f ((Lifting.conjEndN (mstageKernel chief K hR) y) m) = f m) → f = 0

Invariant duals on the mstage kernel vanish (lem:simplehead, transported).