def Q2Presentation.Lifting.markedAugOn {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W : Submodule (ZMod 2) V) : Submodule (ZMod 2) V

The ambient marked window of a submodule: closure differences of its elements.

Equations

• Q2Presentation.Lifting.markedAugOn Φ q W = Submodule.span (ZMod 2) {x : V | ∃ c ∈ Subgroup.closure (Set.range q), ∃ δ ∈ W, (Φ.op c) δ - δ = x}

theorem Q2Presentation.Lifting.markedAugOn_top {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : markedAugOn Φ q ⊤ = markedAug Φ q

theorem Q2Presentation.Lifting.markedAugOn_eq_map {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) : markedAugOn Φ q W = Submodule.map W.subtype (markedAug (Φ.restrict W hW) q)

The ambient marked window is the image of the restricted one.

theorem Q2Presentation.Lifting.restrict_op_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (y : Yt.Y) (h : Φ.op y = 1) : (Φ.restrict W hW).op y = 1

Relator operator triviality restricts.

theorem Q2Presentation.Lifting.doubleRestrict_markedAug_coe {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (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') (s : ↥(Submodule.comap W.subtype W')) (hs : s ∈ markedAug ((Φ.restrict W hW).restrict (Submodule.comap W.subtype W') ⋯) q) : (W.subtype ∘ₗ (Submodule.comap W.subtype W').subtype) s ∈ markedAugOn Φ q W'

Coefficients of the doubly-restricted marked window embed in the ambient window of the inner submodule.

def Q2Presentation.Lifting.diamondAtW {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) : Prop

The floor-valued (♦)-window predicate, ambient coordinates.

Equations

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

theorem Q2Presentation.Lifting.diamondAtW_bot {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : diamondAtW Φ q ⊥

theorem Q2Presentation.Lifting.rows_surjective_of_diamondAtW_top {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hd : diamondAtW Φ q ⊤) (hfull : markedAug Φ q = ⊤) (uv : V × V) : ∃ (n : Gen → V), (famRowsMap Φ q) n = uv

The top-window consumer: with full marked augmentation the rows are surjective.

theorem Q2Presentation.Lifting.diamondAtW_of_section_step {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W' W : Submodule (ZMod 2) V) (hle : W' ≤ W) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (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) (hquot : ∀ (ub vb : ↥W ⧸ Submodule.comap W.subtype W'), ub + vb ∈ markedAug (sectionFamily Φ W' W hW hW') q → ∃ (nb : Gen → ↥W ⧸ Submodule.comap W.subtype W'), (famRowsMap (sectionFamily Φ W' W hW hW') q) nb = (ub, vb)) (hfaithful : dualPairingFaithful (sectionFamily Φ W' W hW hW') q) (hprev : diamondAtW Φ q W') : diamondAtW Φ q W

The (♦)-section step: quotient window solvability and quotient dual-faithfulness push the window predicate up a stable pair.