theorem Q2Presentation.Lifting.finite_dual {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] : Finite (Module.Dual (ZMod 2) V)

Duals of finite modules are finite.

theorem Q2Presentation.Lifting.nontrivial_dual {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Nontrivial V] : Nontrivial (Module.Dual (ZMod 2) V)

Duals of nontrivial modules are nontrivial.

theorem Q2Presentation.Lifting.dual_stable_inv {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (U : Submodule (ZMod 2) (Module.Dual (ZMod 2) V)) (hU : ∀ m ∈ U, (dualOp Φ y) m ∈ U) (m : Module.Dual (ZMod 2) V) : m ∈ U → (dualOp Φ y⁻¹) m ∈ U

Stability under a transported dual upgrades to its inverse via the finite-order power expression.

theorem Q2Presentation.Lifting.dual_simple_of_simple {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (U : Submodule (ZMod 2) (Module.Dual (ZMod 2) V)) : (∀ m ∈ U, ((dualFamily Φ).op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, ((dualFamily Φ).op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤

σ/τ-simplicity transports to the dual family through the coannihilator lattice.

theorem Q2Presentation.Lifting.dual_action_nontrivial {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (haction : ¬∀ (y : Yt.Y), Φ.op y = 1) : ¬∀ (y : Yt.Y), (dualFamily Φ).op y = 1

Action nontriviality transports to the dual family.

theorem Q2Presentation.Lifting.famRows_dual_surjective_of_simple_structured {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] [Nontrivial V] (htwo : 2 ∣ Nat.card Yt.Y) (hx1LY : q Gen.x1 ∈ Yt.LY) (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (haction : ¬∀ (y : Yt.Y), Φ.op y = 1) (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) (uv : Module.Dual (ZMod 2) V × Module.Dual (ZMod 2) V) : ∃ (e : Gen → Module.Dual (ZMod 2) V), (foxShadowGen (dualFamily Φ).op q e Q2Word.tameRelator, foxShadowGen (dualFamily Φ).op q e Q2Word.wildRelator) = uv

Dual rows are surjective at nontrivial σ/τ-simple structured sections — the structured simple case applies verbatim to the dual family.