def
Q2Presentation.Lifting.dualPairingFaithful
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
:
Dual-H¹ faithfulness: every non-coboundary dual-family cycle pairs nontrivially with some row-kernel tuple.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Q2Presentation.Lifting.gap_window_step
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(W : Submodule (ZMod 2) V)
(hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W)
(hodd : Odd (omega2Mod (Nat.card Yt.Y)).val)
(htame : Φ.op (Q2Word.tameRelator.eval q) = 1)
(hwild : Φ.op (Q2Word.wildRelator.eval q) = 1)
(hWhits :
∀ (u v : V),
u ∈ W →
v ∈ W →
u + v ∈ Submodule.map W.subtype (markedAug (Φ.restrict W hW) q) → ∃ (t : Gen → V), (famRowsMap Φ q) t = (u, v))
(hfaithful : dualPairingFaithful (Φ.descend W hW) q)
(p : V × V)
:
p ∈ gapWindow Φ q W → ∃ (n : Gen → V), (famRowsMap Φ q) n = p
The gap-window step: floor hits for the restricted marked window plus quotient dual-faithfulness give every gap pair.
theorem
Q2Presentation.Lifting.diamond_step_full
{Yt : BoundaryFramedTarget}
[Finite Yt.Y]
{V : Type}
[AddCommGroup V]
[Module (ZMod 2) V]
(Φ : OperatorFamily Yt V)
(q : Marking Yt.Y)
(W : Submodule (ZMod 2) V)
(hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W)
(hodd : Odd (omega2Mod (Nat.card Yt.Y)).val)
(htame : Φ.op (Q2Word.tameRelator.eval q) = 1)
(hwild : Φ.op (Q2Word.wildRelator.eval q) = 1)
(hWhits :
∀ (u v : V),
u ∈ W →
v ∈ W →
u + v ∈ Submodule.map W.subtype (markedAug (Φ.restrict W hW) q) → ∃ (t : Gen → V), (famRowsMap Φ q) t = (u, v))
(hfaithful : dualPairingFaithful (Φ.descend W hW) q)
(hquot :
∀ (ub vb : V ⧸ W),
ub + vb ∈ markedAug (Φ.descend W hW) q → ∃ (nb : Gen → V ⧸ W), (famRowsMap (Φ.descend W hW) q) nb = (ub, vb))
(u v : V)
(huv : u + v ∈ markedAug Φ q)
:
The full dévissage step: quotient window solved + floor hits + quotient dual-faithfulness give the ambient window.