theorem Q2Presentation.Lifting.markedAug_eq_aug_of_generates {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hgen : Subgroup.closure (Set.range q) = ⊤) : markedAug Φ q = augSubmodule Φ

With a generating marking the marked window is the full augmentation.

theorem Q2Presentation.Lifting.invariant_of_gen_of_cover {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hcover : ∀ (y : Yt.Y), ∃ c ∈ Subgroup.closure (Set.range q), Φ.op (y * c⁻¹) = 1) (f : Module.Dual (ZMod 2) V) (hf : ∀ (g : Gen) (v : V), f ((Φ.op (q g)) v) = f v) (y : Yt.Y) (v : V) : f ((Φ.op y) v) = f v

The invariance upgrade: generator-invariance is full invariance when the marking covers the group modulo trivially-acting elements.

theorem Q2Presentation.Lifting.markedAug_eq_top_of_cover {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hcover : ∀ (y : Yt.Y), ∃ c ∈ Subgroup.closure (Set.range q), Φ.op (y * c⁻¹) = 1) (hinvY : ∀ (f : Module.Dual (ZMod 2) V), (∀ (y : Yt.Y) (v : V), f ((Φ.op y) v) = f v) → f = 0) : markedAug Φ q = ⊤

Marked fullness from the proven all-of-Y invariant vanishing, through the cover upgrade.