def Q2Presentation.Induction.radicalW {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : Submodule (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))

The radical layer as a submodule of the kernel module.

Equations

• Q2Presentation.Induction.radicalW chief K hR = (AddSubgroup.toZModSubmodule 2) (Subgroup.toAddSubgroup (chief.lower.subgroupOf K.Ksub))

theorem Q2Presentation.Induction.mem_radicalW {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (m : Lifting.NAdd (mstageKernel chief K hR)) : m ∈ radicalW chief K hR ↔ ↑(Additive.toMul m) ∈ chief.lower

theorem Q2Presentation.Induction.radicalW_stable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (y : p.fst.Y) (m : Lifting.NAdd (mstageKernel chief K hR)) (hm : m ∈ radicalW chief K hR) : (Lifting.conjEndN (mstageKernel chief K hR) y) m ∈ radicalW chief K hR

The radical layer is conjugation-stable (lower ◁ Y).

@[reducible, inline]

abbrev Q2Presentation.Induction.HeadMod {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : Type

The head module.

Equations

• Q2Presentation.Induction.HeadMod chief K hR = (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) ⧸ Q2Presentation.Induction.radicalW chief K hR)

def Q2Presentation.Induction.headOp {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (y : p.fst.Y) : Module.End (ZMod 2) (HeadMod chief K hR)

Conjugation descends to the head.

Equations

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

theorem Q2Presentation.Induction.head_descent {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (q : Marking p.fst.Y) (n : Gen → Lifting.NAdd (mstageKernel chief K hR)) (w : GExpr) : (radicalW chief K hR).mkQ (Lifting.foxShadowGen (Lifting.conjEndN (mstageKernel chief K hR)) q n w) = Lifting.foxShadowGen (headOp chief K hR) q (fun (a : Gen) => (radicalW chief K hR).mkQ (n a)) w

Head descent: the projection intertwines the shadows.

theorem Q2Presentation.Induction.rowMap_surjective_of_head_and_radical {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (q : Marking p.fst.Y) (hhead : ∀ (uv : HeadMod chief K hR × HeadMod chief K hR), ∃ (nh : Gen → HeadMod chief K hR), (Lifting.foxShadowGen (headOp chief K hR) q nh Q2Word.tameRelator, Lifting.foxShadowGen (headOp chief K hR) q nh Q2Word.wildRelator) = uv) (hrad : ∀ (u v : Lifting.NAdd (mstageKernel chief K hR)), u ∈ radicalW chief K hR → v ∈ radicalW chief K hR → ∃ (n : Gen → Lifting.NAdd (mstageKernel chief K hR)), (Lifting.rowMap (mstageKernel chief K hR) q) n = (u, v)) : Function.Surjective ⇑(Lifting.rowMap (mstageKernel chief K hR) q)

The five-lemma assembly: row-map surjectivity at M follows from head-level surjectivity and radical-targets-hit.