theorem Q2Presentation.Lifting.dual_fixed_gen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) [Finite V] (y : Yt.Y) (hfixy : ∀ (x : V), (Φ.op y) x = x → x = 0) (lam : Module.Dual (ZMod 2) V) : (dualOp Φ y) lam = lam → lam = 0

Generic dual fixed-space transport on finite modules.

theorem Q2Presentation.Lifting.one_add_ker_of_fixed_bot {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (A : Module.End (ZMod 2) V) (h : ∀ (x : V), A x = x → x = 0) (x : V) : (1 + A) x = 0 → x = 0

1 + A has trivial kernel at a trivial fixed space.

theorem Q2Presentation.Lifting.one_add_surj_of_fixed_bot {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (A : Module.End (ZMod 2) V) (h : ∀ (x : V), A x = x → x = 0) : Function.Surjective ⇑(1 + A)

1 + A is surjective at a trivial fixed space on finite modules.

theorem Q2Presentation.Lifting.op_sigma2_two_pow_order {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : ∃ (k : ℕ), Φ.op (Q2Word.sigma2.eval q) ^ 2 ^ k = 1

The σ₂-evaluation operator has 2-power order, with operational inverses.

theorem Q2Presentation.Lifting.op_sigma2_inv_laws {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : Φ.op (Q2Word.sigma2.eval q) * Φ.op (Q2Word.sigma2.eval q)⁻¹ = 1 ∧ Φ.op (Q2Word.sigma2.eval q)⁻¹ * Φ.op (Q2Word.sigma2.eval q) = 1

The operational inverse laws for the σ₂-evaluation.