Ambient helpers (decoration death, Frattini landings, central juggles)

theorem Q2Presentation.Induction.Ksub_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : p.fst.Y) (hm : m ∈ K.Ksub) : p.fst.thetaY m = 1

The decoration kills the kernel (lem:decorationblock, elementwise).

theorem Q2Presentation.Induction.sq_mem_kernelFrattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : p.fst.Y) (hx : x ∈ K.Ksub) : x ^ 2 ∈ kernelFrattini K

Squares of kernel elements land in the ambient Frattini layer.

theorem Q2Presentation.Induction.comm_mem_kernelFrattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x y : p.fst.Y) (hx : x ∈ K.Ksub) (hy : y ∈ K.Ksub) : ⁅x, y⁆ ∈ kernelFrattini K

Commutators of kernel elements land in the ambient Frattini layer.

The ambient radical preimage TAmb = (K∩S)·Φ(K)

def Q2Presentation.Induction.tAmbient {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup p.fst.Y

The ambient preimage of the radical layer: (K∩S)·Φ(K) ≤ Y (the manuscript's preimage of T = (K∩S)/R in Y).

Equations

• Q2Presentation.Induction.tAmbient chief K = chief.lower ⊓ K.Ksub ⊔ Q2Presentation.Induction.kernelFrattini K

theorem Q2Presentation.Induction.tAmbient_le {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : tAmbient chief K ≤ K.Ksub

theorem Q2Presentation.Induction.kernelFrattini_le_tAmbient {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : kernelFrattini K ≤ tAmbient chief K

instance Q2Presentation.Induction.tAmbient_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (tAmbient chief K).Normal

theorem Q2Presentation.Induction.mem_tAmbient_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : p.fst.Y) : x ∈ tAmbient chief K ↔ ∃ a ∈ chief.lower ⊓ K.Ksub, ∃ r ∈ kernelFrattini K, a * r = x

Elementwise decomposition x = a·r, a ∈ K∩S, r ∈ Φ(K).

theorem Q2Presentation.Induction.mem_towerT_of_lower {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (a : p.fst.Y) (haK : a ∈ K.Ksub) (haS : a ∈ chief.lower) : Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) ⟨a, haK⟩) ∈ towerT K

The Frattini class of a K∩S-element lies in the radical layer T.

The proven crux and the invariance bridge

theorem Q2Presentation.Induction.towerActR_invariance_of_conjInvDuals {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (c : towerC K) : lam ∘ₗ ↑((towerActR chief K) c) = lam

The invariance bridge (conjInvDuals-membership gives the towerActR-spelling the crux clauses consume) — the blockXR_eq_conjInvDuals computation restated without Bstar (conjOnR_eq_conjEndN_inv at y⁻¹).

noncomputable def Q2Presentation.Induction.sec7Crux {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Sec7SimpleHeadCruxData chief K

The proven crux, packaged once (prop:simpleheaddet, all-theorem chain: trivial-chain clause (i) + shear clause (ii) + radical clause).

Equations

• ⋯ = ⋯

The λ-alignment

theorem Q2Presentation.Induction.scalarProj_frattini_eq_one_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (r : p.fst.Y) (hr : r ∈ kernelFrattini K) : (Lifting.scalarProj (xrKernel chief K) lam hinv) r = 1 ↔ lam (Additive.ofMul ⟨r, hr⟩) = 0

λ-alignment: an ambient Frattini element dies in the cover iff λ kills it. This is the identification of the P1 cover's central-extension data with the concrete §7 tower form.

theorem Q2Presentation.Induction.scalarProj_sq_eq_form {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (k : ↥K.Ksub) : (Lifting.scalarProj (xrKernel chief K) lam hinv) (↑k ^ 2) = 1 ↔ (sec7SquareFamily chief K lam).form (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k)) = 0

Geometric squares compute the tower form: for k ∈ K, scalarProj (k²) = 1 ↔ q_λ(k̄) = 0.

theorem Q2Presentation.Induction.scalarProj_comm_eq_polar {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (k k' : ↥K.Ksub) : (Lifting.scalarProj (xrKernel chief K) lam hinv) ⁅↑k, ↑k'⁆ = 1 ↔ ((sec7SquareFamily chief K lam).polar (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k))) (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k')) = 0

Geometric commutators compute the tower polar form: for k, k' ∈ K, scalarProj ⁅k,k'⁆ = 1 ↔ b_λ(k̄, k̄') = 0.

The crux facts at the ambient radical preimage

theorem Q2Presentation.Induction.scalarProj_sq_tAmbient {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (x : p.fst.Y) (hx : x ∈ tAmbient chief K) : (Lifting.scalarProj (xrKernel chief K) lam hinv) (x ^ 2) = 1

Squares of TAmb-elements die in the cover (crux form_zero_on_T through the alignment): the Φ(K)-part cancels (central, exponent 2) and the K∩S-part carries a T-class, where the form vanishes.

theorem Q2Presentation.Induction.scalarProj_comm_tAmbient {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (x y : p.fst.Y) (hx : x ∈ tAmbient chief K) (hy : y ∈ K.Ksub) : (Lifting.scalarProj (xrKernel chief K) lam hinv) ⁅x, y⁆ = 1

Commutators of TAmb against K die in the cover (crux polar_zero_on_T through the alignment): the polar radical contains T.

The cover tower relN ≤ T̃ ≤ M̃ ≤ B_λ

theorem Q2Presentation.Induction.scalarProj_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : Function.Surjective ⇑(Lifting.scalarProj (xrKernel chief K) lam hinv)

def Q2Presentation.Induction.tCover {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : Subgroup (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

The T-preimage in the cover: T̃ = TAmb·(ker λ)/(ker λ) ≤ B_λ.

Equations

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

def Q2Presentation.Induction.mCover {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : Subgroup (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

The M-preimage in the cover: M̃ = K/(ker λ) ≤ B_λ.

Equations

• Q2Presentation.Induction.mCover chief K lam hinv = Subgroup.map (Q2Presentation.Lifting.scalarProj (Q2Presentation.Induction.xrKernel chief K) lam hinv) K.Ksub

theorem Q2Presentation.Induction.mem_tCover_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : t ∈ tCover chief K lam hinv ↔ ∃ x ∈ tAmbient chief K, (Lifting.scalarProj (xrKernel chief K) lam hinv) x = t

theorem Q2Presentation.Induction.mem_mCover_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : b ∈ mCover chief K lam hinv ↔ ∃ x ∈ K.Ksub, (Lifting.scalarProj (xrKernel chief K) lam hinv) x = b

theorem Q2Presentation.Induction.relN_le_tCover {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N ≤ tCover chief K lam hinv

The deck kernel sits inside the T-preimage: relN ≤ T̃.

theorem Q2Presentation.Induction.tCover_le_mCover {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : tCover chief K lam hinv ≤ mCover chief K lam hinv

instance Q2Presentation.Induction.tCover_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : (tCover chief K lam hinv).Normal

instance Q2Presentation.Induction.mCover_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : (mCover chief K lam hinv).Normal

theorem Q2Presentation.Induction.tCover_le_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : tCover chief K lam hinv ≤ (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).LY

theorem Q2Presentation.Induction.mCover_le_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : mCover chief K lam hinv ≤ (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).LY

theorem Q2Presentation.Induction.mCover_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hb : b ∈ mCover chief K lam hinv) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).thetaY b = 1

theorem Q2Presentation.Induction.tCover_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).thetaY t = 1

T̃ is elementary abelian; M̃ centralizes T̃

theorem Q2Presentation.Induction.tCover_comm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (a b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ha : a ∈ tCover chief K lam hinv) (hb : b ∈ tCover chief K lam hinv) : a * b = b * a

T̃ is abelian (lem:radicaledge step 1): commutators of TAmb-elements die in the cover.

theorem Q2Presentation.Induction.tCover_mul_self {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (a : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ha : a ∈ tCover chief K lam hinv) : a * a = 1

T̃ has exponent 2 (lem:radicaledge step 1): squares of TAmb-elements die in the cover.

theorem Q2Presentation.Induction.mCover_conj_fix {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hb : b ∈ mCover chief K lam hinv) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : b * t * b⁻¹ = t

M̃ centralizes T̃ (the concrete inflation input of lem:radicaledge step 4: the defect of an M̃-conjugation is the polar pairing against T, which vanishes by the crux).

The kernel-level collapses (Noether III)

noncomputable def Q2Presentation.Induction.mCoverCollapse {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y ⧸ mCover chief K lam hinv ≃* towerC K

B_λ ⧸ M̃ ≃* C = Y/K (the scalarCollapse idiom at the M-layer).

Equations

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

noncomputable def Q2Presentation.Induction.tCoverCollapseAmbient {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y ⧸ tCover chief K lam hinv ≃* p.fst.Y ⧸ tAmbient chief K

B_λ ⧸ T̃ ≃* Y ⧸ TAmb (ambient normal form of the T-collapse).

Equations

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

The child-side tower T' ≤ M' ≤ B = Y/Φ(K) (no λ)

def Q2Presentation.Induction.tChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup (XRZero.xrChild chief K).fst.Y

The child T-layer: T' = TAmb/Φ(K) ≤ B.

Equations

• Q2Presentation.Induction.tChild chief K = Subgroup.map (QuotientGroup.mk' (Q2Presentation.Induction.XRZero.NR chief K)) (Q2Presentation.Induction.tAmbient chief K)

def Q2Presentation.Induction.mChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup (XRZero.xrChild chief K).fst.Y

The child M-layer: M' = K/Φ(K) ≤ B.

Equations

• Q2Presentation.Induction.mChild chief K = Subgroup.map (QuotientGroup.mk' (Q2Presentation.Induction.XRZero.NR chief K)) K.Ksub

theorem Q2Presentation.Induction.mem_tChild_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (t : (XRZero.xrChild chief K).fst.Y) : t ∈ tChild chief K ↔ ∃ x ∈ tAmbient chief K, (QuotientGroup.mk' (XRZero.NR chief K)) x = t

theorem Q2Presentation.Induction.mem_mChild_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (b : (XRZero.xrChild chief K).fst.Y) : b ∈ mChild chief K ↔ ∃ x ∈ K.Ksub, (QuotientGroup.mk' (XRZero.NR chief K)) x = b

theorem Q2Presentation.Induction.tChild_le_mChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : tChild chief K ≤ mChild chief K

instance Q2Presentation.Induction.tChild_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (tChild chief K).Normal

instance Q2Presentation.Induction.mChild_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (mChild chief K).Normal

theorem Q2Presentation.Induction.mChild_le_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : mChild chief K ≤ (XRZero.xrChild chief K).fst.LY

theorem Q2Presentation.Induction.tChild_le_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : tChild chief K ≤ (XRZero.xrChild chief K).fst.LY

theorem Q2Presentation.Induction.mChild_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (b : (XRZero.xrChild chief K).fst.Y) (hb : b ∈ mChild chief K) : (XRZero.xrChild chief K).fst.thetaY b = 1

theorem Q2Presentation.Induction.tChild_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (t : (XRZero.xrChild chief K).fst.Y) (ht : t ∈ tChild chief K) : (XRZero.xrChild chief K).fst.thetaY t = 1

theorem Q2Presentation.Induction.mChild_comm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (a b : (XRZero.xrChild chief K).fst.Y) (ha : a ∈ mChild chief K) (hb : b ∈ mChild chief K) : a * b = b * a

M' is abelian: commutators of K-elements lie in Φ(K), the kernel of the child projection.

theorem Q2Presentation.Induction.mChild_mul_self {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (a : (XRZero.xrChild chief K).fst.Y) (ha : a ∈ mChild chief K) : a * a = 1

M' has exponent 2: squares of K-elements lie in Φ(K).

noncomputable def Q2Presentation.Induction.mChildCollapse {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (XRZero.xrChild chief K).fst.Y ⧸ mChild chief K ≃* towerC K

B ⧸ M' ≃* C = Y/K (the child collapse).

Equations

• Q2Presentation.Induction.mChildCollapse chief K = QuotientGroup.quotientQuotientEquivQuotient (Q2Presentation.Induction.XRZero.NR chief K) K.Ksub ⋯

noncomputable def Q2Presentation.Induction.tChildCollapseAmbient {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (XRZero.xrChild chief K).fst.Y ⧸ tChild chief K ≃* p.fst.Y ⧸ tAmbient chief K

B ⧸ T' ≃* Y ⧸ TAmb (ambient normal form of the child T-collapse).

Equations

• Q2Presentation.Induction.tChildCollapseAmbient chief K = QuotientGroup.quotientQuotientEquivQuotient (Q2Presentation.Induction.XRZero.NR chief K) (Q2Presentation.Induction.tAmbient chief K) ⋯

noncomputable def Q2Presentation.Induction.tCoverCollapse {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y ⧸ tCover chief K lam hinv ≃* (XRZero.xrChild chief K).fst.Y ⧸ tChild chief K

B_λ ⧸ T̃ ≃* B ⧸ T': the cover of B/T seen from the cover — the target of the zero-edge descent (lem:radicaledge step 7).

Equations

• Q2Presentation.Induction.tCoverCollapse chief K lam hinv = (Q2Presentation.Induction.tCoverCollapseAmbient chief K lam hinv).trans (Q2Presentation.Induction.tChildCollapseAmbient chief K).symm