def Q2Presentation.Lifting.coboundary {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (a : V) : Gen → V

The coboundary tuple of a vector.

Equations

• Q2Presentation.Lifting.coboundary Φ q a g = (Φ.op (q g)) a - a

theorem Q2Presentation.Lifting.foxShadowGen_coboundary {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (a : V) (w : GExpr) : foxShadowGen Φ.op q (coboundary Φ q a) w = (Φ.op (w.eval q)) a - a

The Fox coboundary identity: shadows of coboundaries telescope.

theorem Q2Presentation.Lifting.rows_coboundary_eq_zero {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (a : V) (htame : Φ.op (Q2Word.tameRelator.eval q) = 1) (hwild : Φ.op (Q2Word.wildRelator.eval q) = 1) : (foxShadowGen Φ.op q (coboundary Φ q a) Q2Word.tameRelator, foxShadowGen Φ.op q (coboundary Φ q a) Q2Word.wildRelator) = (0, 0)

The complex property: when the relator defects act trivially, the row map kills coboundaries.