def Q2Presentation.Induction.radFamily {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : Lifting.OperatorFamily p.fst ↥(radicalW chief K hR)

The radical-layer conjugation family.

Equations

• Q2Presentation.Induction.radFamily chief K hR = (Q2Presentation.Lifting.conjFamily (Q2Presentation.Induction.mstageKernel chief K hR)).restrict (Q2Presentation.Induction.radicalW chief K hR) ⋯

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

Radical shadows commute with the inclusion.

theorem Q2Presentation.Induction.hrad_of_radical_rows_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (q : Marking p.fst.Y) (hsurj : ∀ (uv : ↥(radicalW chief K hR) × ↥(radicalW chief K hR)), ∃ (n : Gen → ↥(radicalW chief K hR)), (Lifting.foxShadowGen (radFamily chief K hR).op q n Q2Word.tameRelator, Lifting.foxShadowGen (radFamily chief K hR).op q n Q2Word.wildRelator) = uv) (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)

The radical-hit reduction.