theorem
Q2Presentation.Lifting.diamondAtW_all
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
[Finite V]
(htwo : 2 ∣ Nat.card Yt.Y)
(h4Y : 4 ∣ Nat.card Yt.Y)
(hx1LY : q Gen.x1 ∈ Yt.LY)
(hdecomp : ∀ (y : Yt.Y), ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ Yt.LY)
(hrel : rconj (Yt.piY (q Gen.tau)) (Yt.piY (q Gen.sigma)) = Yt.piY (q Gen.tau) ^ 2)
(htame : Φ.op (Q2Word.tameRelator.eval q) = 1)
(hwild : Φ.op (Q2Word.wildRelator.eval q) = 1)
(hfaithNT :
∀ (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W)
(hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W'),
W' < W →
(∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') →
(¬∀ (y : Yt.Y), (sectionFamily Φ W' W hW hW').op y = 1) → dualPairingFaithful (sectionFamily Φ W' W hW hW') q)
(W : Submodule (ZMod 2) V)
:
(∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) → diamondAtW Φ q W
The (♦)-window predicate holds at every stable window, given dual-pairing faithfulness at the nontrivial simple sections.
theorem
Q2Presentation.Lifting.famRows_surjective_of_diamond
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
[Finite V]
(htwo : 2 ∣ Nat.card Yt.Y)
(h4Y : 4 ∣ Nat.card Yt.Y)
(hx1LY : q Gen.x1 ∈ Yt.LY)
(hdecomp : ∀ (y : Yt.Y), ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ Yt.LY)
(hrel : rconj (Yt.piY (q Gen.tau)) (Yt.piY (q Gen.sigma)) = Yt.piY (q Gen.tau) ^ 2)
(htame : Φ.op (Q2Word.tameRelator.eval q) = 1)
(hwild : Φ.op (Q2Word.wildRelator.eval q) = 1)
(hfaithNT :
∀ (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W)
(hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W'),
W' < W →
(∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') →
(¬∀ (y : Yt.Y), (sectionFamily Φ W' W hW hW').op y = 1) → dualPairingFaithful (sectionFamily Φ W' W hW hW') q)
(hfull : markedAug Φ q = ⊤)
(uv : V × V)
:
∃ (n : Gen → V), (famRowsMap Φ q) n = uv
Row surjectivity from the dévissage at a fully marked module.
theorem
Q2Presentation.Lifting.bockstein_witness_of_rows_surjective
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(hsurj : ∀ (uv : V × V), ∃ (n : Gen → V), (famRowsMap Φ q) n = uv)
(W : Submodule (ZMod 2) V)
(w : V)
:
∃ (n : Gen → V), foxShadowGen Φ.op q n Q2Word.tameRelator - w ∈ W ∧ foxShadowGen Φ.op q n Q2Word.wildRelator ∈ W
The Bockstein witness shape from full row surjectivity: hit
(w, 0) on the nose.