def Q2Presentation.Lifting.pAElem {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : V) : Heis Φ

The primal translation element.

Equations

• Q2Presentation.Lifting.pAElem Φ a = { d := a, e := 0, z := 0, y := 1 }

theorem Q2Presentation.Lifting.pAElem_sq {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : V) : pAElem Φ a * pAElem Φ a = 1

theorem Q2Presentation.Lifting.pAElem_conj_gen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : V) (y0 : Module.Dual (ZMod 2) V) (c : Yt.Y) : pAElem Φ a * { d := 0, e := y0, z := 0, y := c } * pAElem Φ a = zElem Φ (y0 a) * { d := (Φ.op c) a + a, e := y0, z := 0, y := c }

The primal generator conjugation: coboundary entry plus central correction.

theorem Q2Presentation.Lifting.heis_pow_dz {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (h : Heis Φ) (hd : h.d = 0) (hz : h.z = 0) (k : ℕ) : (h ^ k).d = 0 ∧ (h ^ k).z = 0

Zero-value power evaluations keep zero value and central parts.

theorem Q2Presentation.Lifting.heisEval_dz_zero {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : (heisEval Φ q (fun (x : Gen) => 0) φ w).d = 0 ∧ (heisEval Φ q (fun (x : Gen) => 0) φ w).z = 0

The zero-value evaluation has zero value and central coordinates.

def Q2Presentation.Lifting.foxShadowDualGen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : Module.Dual (ZMod 2) V

The dual Fox shadow: the dual coordinate of the zero-value evaluation.

Equations

• Q2Presentation.Lifting.foxShadowDualGen Φ q φ w = (Q2Presentation.Lifting.heisEval Φ q (fun (x : Q2Presentation.Gen) => 0) φ w).e

def Q2Presentation.Lifting.primalCorrection {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (φ : Gen → Module.Dual (ZMod 2) V) (a : V) (w : GExpr) : ZMod 2

The primal Stokes correction.

Equations

• Q2Presentation.Lifting.primalCorrection φ a w = ∑ g : Q2Presentation.Gen, Q2Presentation.Lifting.expSum g w * (φ g) a

theorem Q2Presentation.Lifting.primalCorrection_one {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (φ : Gen → Module.Dual (ZMod 2) V) (a : V) : primalCorrection φ a GExpr.one = 0

theorem Q2Presentation.Lifting.primalCorrection_gen {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (φ : Gen → Module.Dual (ZMod 2) V) (a : V) (b : Gen) : primalCorrection φ a (GExpr.gen b) = (φ b) a

theorem Q2Presentation.Lifting.primalCorrection_mul {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (φ : Gen → Module.Dual (ZMod 2) V) (a : V) (u v : GExpr) : primalCorrection φ a (u.mul v) = primalCorrection φ a u + primalCorrection φ a v

theorem Q2Presentation.Lifting.primalCorrection_inv {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (φ : Gen → Module.Dual (ZMod 2) V) (a : V) (u : GExpr) : primalCorrection φ a u.inv = primalCorrection φ a u

theorem Q2Presentation.Lifting.primalCorrection_powNat {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (φ : Gen → Module.Dual (ZMod 2) V) (a : V) (u : GExpr) (k : ℕ) : primalCorrection φ a (u.powNat k) = ↑k * primalCorrection φ a u

theorem Q2Presentation.Lifting.primalCorrection_powOmega2 {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (φ : Gen → Module.Dual (ZMod 2) V) (a : V) (u : GExpr) : primalCorrection φ a u.powOmega2 = primalCorrection φ a u

theorem Q2Presentation.Lifting.stokes_conj_primal {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (φ : Gen → Module.Dual (ZMod 2) V) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (a : V) (w : GExpr) : pAElem Φ a * heisEval Φ q (fun (x : Gen) => 0) φ w * pAElem Φ a = zElem Φ (primalCorrection φ a w) * heisEval Φ q (coboundary Φ q a) φ w

The primal conjugation telescope.

theorem Q2Presentation.Lifting.word_stokes_primal {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (φ : Gen → Module.Dual (ZMod 2) V) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (a : V) (w : GExpr) : betaShadow Φ q (coboundary Φ q a) φ w = (foxShadowDualGen Φ q φ w) a + primalCorrection φ a w

The primal finite-word Stokes identity (eq:wordstokes1).

theorem Q2Presentation.Lifting.traced_stokes_primal {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (φ : Gen → Module.Dual (ZMod 2) V) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (a : V) : betaShadow Φ q (coboundary Φ q a) φ Q2Word.tameRelator + betaShadow Φ q (coboundary Φ q a) φ Q2Word.wildRelator = (foxShadowDualGen Φ q φ Q2Word.tameRelator) a + (foxShadowDualGen Φ q φ Q2Word.wildRelator) a

The traced primal Stokes identity: at the relator pair the corrections cancel.