Edge complements and the zero-edge predicate

structure Q2Presentation.Induction.EdgeComplement {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)) : Type

An edge complement: a complement to the deck kernel inside the T-preimage (lem:radicaledge's s(T), subgroup form).

• W : Subgroup (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y
• le_tCover : self.W ≤ tCover chief K lam hinv
• disj : self.W ⊓ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N = ⊥
• sup : self.W ⊔ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N = tCover chief K lam hinv

theorem Q2Presentation.Induction.edgeComplement_nonempty {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) : Nonempty (EdgeComplement chief K lam hinv)

Edge complements exist (lem:radicaledge step 2): finite elementary-abelian complement extension inside T̃ — a subgroup maximal among those meeting relN trivially fills up to T̃, since any missed T̃-element (order ≤ 2, central in T̃) could be adjoined.

def Q2Presentation.Induction.ZeroEdge {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)) : Prop

The zero-edge predicate (lem:radicaledge's [ε̄] = 0 branch, cocycle-free): some edge complement is normal in the whole cover.

Equations

• Q2Presentation.Induction.ZeroEdge chief K lam hinv = ∃ (D : Q2Presentation.Induction.EdgeComplement chief K lam hinv), D.W.Normal

The unique W ⊕ relN decomposition of T̃

theorem Q2Presentation.Induction.tCover_decomp {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : ∃ w ∈ D.W, ∃ z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N, w * z = t

Every T̃-element decomposes as (complement)·(deck).

theorem Q2Presentation.Induction.tCover_decomp_unique {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)) (D : EdgeComplement chief K lam hinv) {w w' z z' : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y} (hw : w ∈ D.W) (hw' : w' ∈ D.W) (hz : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (hz' : z' ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (h : w * z = w' * z') : w = w' ∧ z = z'

The decomposition is unique (W ⊓ relN = ⊥; no commutativity needed).

def Q2Presentation.Induction.edgeW {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

The W-component of a T̃-element (choice-packaged).

Equations

• Q2Presentation.Induction.edgeW chief K lam hinv D hne t ht = ⋯.choose

theorem Q2Presentation.Induction.edgeW_mem {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : edgeW chief K lam hinv D hne t ht ∈ D.W

def Q2Presentation.Induction.edgeZ {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

The relN-component of a T̃-element (choice-packaged).

Equations

• Q2Presentation.Induction.edgeZ chief K lam hinv D hne t ht = ⋯.choose

theorem Q2Presentation.Induction.edgeZ_mem {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : edgeZ chief K lam hinv D hne t ht ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N

theorem Q2Presentation.Induction.edgeW_mul_edgeZ {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (t : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (ht : t ∈ tCover chief K lam hinv) : edgeW chief K lam hinv D hne t ht * edgeZ chief K lam hinv D hne t ht = t

The 𝔽₂-reading of the deck kernel and the edge defect

def Q2Presentation.Induction.relRead {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)) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : ZMod 2

The 𝔽₂-reading of the deck kernel: 1 ↦ 0, everything else ↦ 1 (on relN this is the λ-pinned isomorphism relN ≅ 𝔽₂, card_relKernel_eq_two).

Equations

• Q2Presentation.Induction.relRead chief K lam hinv z = if z = 1 then 0 else 1

theorem Q2Presentation.Induction.relRead_one {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)) : relRead chief K lam hinv 1 = 0

theorem Q2Presentation.Induction.relRead_eq_zero_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)) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : relRead chief K lam hinv z = 0 ↔ z = 1

theorem Q2Presentation.Induction.relRead_mul {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) (z z' : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hz : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (hz' : z' ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) : relRead chief K lam hinv (z * z') = relRead chief K lam hinv z + relRead chief K lam hinv z'

Additivity of the reading on the (order-2) deck kernel.

def Q2Presentation.Induction.edgeDefect {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (w : ↥D.W) : ZMod 2

The edge defect of a complement (eq:radicaledgecochain in defect form): the relN-component of the conjugation of a complement element, read in 𝔽₂.

Equations

• Q2Presentation.Induction.edgeDefect chief K lam hinv D hne b w = Q2Presentation.Induction.relRead chief K lam hinv (Q2Presentation.Induction.edgeZ chief K lam hinv D hne (b * ↑w * b⁻¹) ⋯)

def Q2Presentation.Induction.conjW {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (w : ↥D.W) : ↥D.W

The W-component of a conjugated complement element.

Equations

• Q2Presentation.Induction.conjW chief K lam hinv D hne b w = ⟨Q2Presentation.Induction.edgeW chief K lam hinv D hne (b * ↑w * b⁻¹) ⋯, ⋯⟩

theorem Q2Presentation.Induction.conjW_mul_defect {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (w : ↥D.W) : ∃ z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N, ↑(conjW chief K lam hinv D hne b w) * z = b * ↑w * b⁻¹ ∧ relRead chief K lam hinv z = edgeDefect chief K lam hinv D hne b w

The defining splitting: b·w·b⁻¹ = (conjW b w)·z with relRead z = edgeDefect b w.

theorem Q2Presentation.Induction.edgeDefect_eq_of_split {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (w : ↥D.W) {w' z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y} (hw' : w' ∈ D.W) (hz : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (hsplit : w' * z = b * ↑w * b⁻¹) : edgeDefect chief K lam hinv D hne b w = relRead chief K lam hinv z ∧ ↑(conjW chief K lam hinv D hne b w) = w'

The defect/component computation rule: any explicit splitting of the conjugation determines both.

Defect laws: additivity, cocycle, C-factorization

theorem Q2Presentation.Induction.edgeDefect_mul_right {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (w w' : ↥D.W) : edgeDefect chief K lam hinv D hne b (w * w') = edgeDefect chief K lam hinv D hne b w + edgeDefect chief K lam hinv D hne b w'

Additivity in the complement slot.

theorem Q2Presentation.Induction.edgeDefect_cocycle {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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b₁ b₂ : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (w : ↥D.W) : edgeDefect chief K lam hinv D hne (b₁ * b₂) w = edgeDefect chief K lam hinv D hne b₁ (conjW chief K lam hinv D hne b₂ w) + edgeDefect chief K lam hinv D hne b₂ w

The cocycle law (ε(b₁b₂) = ε(b₁)^{b₂-shift} + ε(b₂) in defect form; the deck component of b₁ acts trivially since relN is central).

theorem Q2Presentation.Induction.edgeDefect_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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hb : b ∈ mCover chief K lam hinv) (w : ↥D.W) : edgeDefect chief K lam hinv D hne b w = 0

C-factorization, vanishing clause (lem:radicaledge step 4, concrete): the defect vanishes on M̃ — for b ∈ M̃ the conjugation leak is the polar pairing against T, which is zero by the crux.

theorem Q2Presentation.Induction.conjW_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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hb : b ∈ mCover chief K lam hinv) (w : ↥D.W) : conjW chief K lam hinv D hne b w = w

M̃-conjugation fixes the W-component.

theorem Q2Presentation.Induction.edgeDefect_mul_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)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (b m : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hm : m ∈ mCover chief K lam hinv) (w : ↥D.W) : edgeDefect chief K lam hinv D hne (b * m) w = edgeDefect chief K lam hinv D hne b w

C-factorization (lem:radicaledge step 4): the defect depends only on the class of b modulo M̃ — i.e. on its image in C.

The dichotomy in defect form

theorem Q2Presentation.Induction.zeroEdge_iff_defect {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) : ZeroEdge chief K lam hinv ↔ ∃ (D : EdgeComplement chief K lam hinv), ∀ (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (w : ↥D.W), edgeDefect chief K lam hinv D hne b w = 0

Zero edge ⟺ identically vanishing defect (lem:radicaledge steps 3+7: a complement is normal iff conjugation never leaks into the deck kernel).

The descent construction (lem:radicaledge step 7)

def Q2Presentation.Induction.descTarget {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) : BoundaryFramedTarget

The descended target B_λ/W: a framed target over the zero-edge witness (its underlying group covers B/T' through descCollapse).

Equations

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

def Q2Presentation.Induction.descFrame {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) : BoundaryFrame (descTarget chief K lam hinv D hW)

The descended frame (the P1 frame transported twice).

Equations

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

def Q2Presentation.Induction.descProj {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y →* (descTarget chief K lam hinv D hW).Y

The descent projection B_λ ↠ B_λ/W (instance-packaged).

Equations

• Q2Presentation.Induction.descProj chief K lam hinv D hW = QuotientGroup.mk' D.W

def Q2Presentation.Induction.descKernel {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : Lifting.ElementaryKernel (descTarget chief K lam hinv D hW)

The descended deck kernel T̃/W ≤ B_λ/W: an order-2 central elementary kernel of the descended target.

Equations

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

theorem Q2Presentation.Induction.descKernel_N_eq {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : (descKernel chief K lam hinv D hW hne).N = Subgroup.map (descProj chief K lam hinv D hW) (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N

The descended kernel is the image of the deck kernel (T̃ = W·relN collapses to relN mod W).

theorem Q2Presentation.Induction.card_descKernel_eq_two {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : Nat.card ↥(descKernel chief K lam hinv D hW hne).N = 2

The descended cover is double: |T̃/W| = |relN| = 2.

theorem Q2Presentation.Induction.descKernel_le_center {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : (descKernel chief K lam hinv D hW hne).N ≤ Subgroup.center (descTarget chief K lam hinv D hW).Y

The descended deck kernel is central (card 2 + normality).

noncomputable def Q2Presentation.Induction.descCollapse {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : (descTarget chief K lam hinv D hW).Y ⧸ (descKernel chief K lam hinv D hW hne).N ≃* (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y ⧸ tCover chief K lam hinv

The descended cover collapses onto B_λ/T̃ (Noether III at W ≤ T̃); composed with tCoverCollapse this exhibits B_λ/W as a central double cover of B/T' — the manuscript's descended cover.

Equations

• Q2Presentation.Induction.descCollapse chief K lam hinv D hW hne = QuotientGroup.quotientQuotientEquivQuotient D.W (Q2Presentation.Induction.tCover chief K lam hinv) ⋯

noncomputable def Q2Presentation.Induction.descCollapseChild {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : (descTarget chief K lam hinv D hW).Y ⧸ (descKernel chief K lam hinv D hW hne).N ≃* (XRZero.xrChild chief K).fst.Y ⧸ tChild chief K

The full descent collapse: (B_λ/W) ⧸ (T̃/W) ≃* B ⧸ T'.

Equations

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