theorem Q2Presentation.Lifting.dualOp_apply_eq_of_op_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (h : Φ.op y = 1) (lam : Module.Dual (ZMod 2) V) : (dualOp Φ y) lam = lam

Pointwise dual triviality from operator triviality.

theorem Q2Presentation.Lifting.heis_commutator_triple {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a b : Heis Φ) (ha : Φ.op a.y = 1) (hb : Φ.op b.y = 1) : (a⁻¹ * b⁻¹ * a * b).d = 0 ∧ (a⁻¹ * b⁻¹ * a * b).e = 0 ∧ (a⁻¹ * b⁻¹ * a * b).z = a.e b.d + b.e a.d

The commutator triple-law at trivially-acting parts: zero first-order coordinates, bilinear central value.

Operator triviality of the commutator factor evaluations

theorem Q2Presentation.Lifting.op_eval_d0_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (e : ℕ) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) : Φ.op (Q2Word.d0.eval q) = 1

The d₀-evaluation acts trivially: the ω₂-power collapses through the odd order.

theorem Q2Presentation.Lifting.op_eval_z0_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) : Φ.op (Q2Word.z0.eval q) = 1

The z₀-evaluation acts trivially: the conjugate collapses through the trivial wild operator.