theorem Q2Presentation.Lifting.heisEval_e_nfree {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n₁ n₂ : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : (heisEval Φ q n₁ φ w).e = (heisEval Φ q n₂ φ w).e

The dual coordinate ignores the values.

theorem Q2Presentation.Lifting.heisEval_d_phifree {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ₁ φ₂ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : (heisEval Φ q n φ₁ w).d = (heisEval Φ q n φ₂ w).d

The value coordinate ignores the duals.

theorem Q2Presentation.Lifting.betaShadow_add_left {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n₁ n₂ : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : betaShadow Φ q (n₁ + n₂) φ w = betaShadow Φ q n₁ φ w + betaShadow Φ q n₂ φ w

Left additivity of the cup coordinate.

theorem Q2Presentation.Lifting.heisEval_e_add {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ₁ φ₂ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : (heisEval Φ q n (φ₁ + φ₂) w).e = (heisEval Φ q n φ₁ w).e + (heisEval Φ q n φ₂ w).e

The dual coordinate is additive in the duals.

theorem Q2Presentation.Lifting.betaShadow_add_right {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ₁ φ₂ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : betaShadow Φ q n (φ₁ + φ₂) w = betaShadow Φ q n φ₁ w + betaShadow Φ q n φ₂ w

Right additivity of the cup coordinate.

theorem Q2Presentation.Lifting.betaShadow_zero_left {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) : betaShadow Φ q (fun (x : Gen) => 0) φ w = 0

The cup coordinate vanishes at zero values.

theorem Q2Presentation.Lifting.betaShadow_zero_right {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (w : GExpr) : betaShadow Φ q n (fun (x : Gen) => 0) w = 0

The cup coordinate vanishes at zero duals.

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

The traced cup form — the D¹-pairing of the deformation complex.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Lifting.cupForm_add_left {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n₁ n₂ : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) : cupForm Φ q (n₁ + n₂) φ = cupForm Φ q n₁ φ + cupForm Φ q n₂ φ

theorem Q2Presentation.Lifting.cupForm_add_right {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ₁ φ₂ : Gen → Module.Dual (ZMod 2) V) : cupForm Φ q n (φ₁ + φ₂) = cupForm Φ q n φ₁ + cupForm Φ q n φ₂

theorem Q2Presentation.Lifting.cupForm_zero_left {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) : cupForm Φ q (fun (x : Gen) => 0) φ = 0

theorem Q2Presentation.Lifting.cupForm_zero_right {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) : (cupForm Φ q n fun (x : Gen) => 0) = 0