def Q2Presentation.Lifting.HeisRel {Yt : BoundaryFramedTarget} {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] (Φ : OperatorFamily Yt V) (Φ' : OperatorFamily Yt V') (f : V →ₗ[ZMod 2] V') (a : Heis Φ) (a' : Heis Φ') : Prop

The transport relation between evaluations over the two modules.

Equations

• Q2Presentation.Lifting.HeisRel Φ Φ' f a a' = (a'.y = a.y ∧ a'.d = f a.d ∧ a'.e ∘ₗ f = a.e ∧ a'.z = a.z)

theorem Q2Presentation.Lifting.heisRel_dual {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) (y : Yt.Y) (lam : Module.Dual (ZMod 2) V') : (dualOp Φ' y) lam ∘ₗ f = (dualOp Φ y) (lam ∘ₗ f)

theorem Q2Presentation.Lifting.heisRel_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} : HeisRel Φ Φ' f 1 1

theorem Q2Presentation.Lifting.heisRel_mul {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) {a b : Heis Φ} {a' b' : Heis Φ'} (ha : HeisRel Φ Φ' f a a') (hb : HeisRel Φ Φ' f b b') : HeisRel Φ Φ' f (a * b) (a' * b')

theorem Q2Presentation.Lifting.heisRel_inv {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) {a : Heis Φ} {a' : Heis Φ'} (ha : HeisRel Φ Φ' f a a') : HeisRel Φ Φ' f a⁻¹ a'⁻¹

theorem Q2Presentation.Lifting.heisRel_pow {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) {a : Heis Φ} {a' : Heis Φ'} (ha : HeisRel Φ Φ' f a a') (k : ℕ) : HeisRel Φ Φ' f (a ^ k) (a' ^ k)

theorem Q2Presentation.Lifting.heisEval_natural {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) (q : Marking Yt.Y) (n : Gen → V) (φ' : Gen → Module.Dual (ZMod 2) V') (w : GExpr) : HeisRel Φ Φ' f (heisEval Φ q n (fun (g : Gen) => φ' g ∘ₗ f) w) (heisEval Φ' q (fun (g : Gen) => f (n g)) φ' w)

Joint strict naturality of the evaluation coordinates.

theorem Q2Presentation.Lifting.betaShadow_natural {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) (q : Marking Yt.Y) (n : Gen → V) (φ' : Gen → Module.Dual (ZMod 2) V') (w : GExpr) : betaShadow Φ' q (fun (g : Gen) => f (n g)) φ' w = betaShadow Φ q n (fun (g : Gen) => φ' g ∘ₗ f) w

β-naturality (lem:heisnatural): the cup coordinate transports strictly along intertwiners.

theorem Q2Presentation.Lifting.foxShadowGen_natural_of_rel {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) (q : Marking Yt.Y) (n : Gen → V) (φ' : Gen → Module.Dual (ZMod 2) V') (w : GExpr) : (heisEval Φ' q (fun (g : Gen) => f (n g)) φ' w).d = f (heisEval Φ q n (fun (g : Gen) => φ' g ∘ₗ f) w).d

Value-coordinate naturality, recovered from the relation.

theorem Q2Presentation.Lifting.foxShadowDual_natural_of_rel {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V V' : Type} [AddCommGroup V] [Module (ZMod 2) V] [AddCommGroup V'] [Module (ZMod 2) V'] {Φ : OperatorFamily Yt V} {Φ' : OperatorFamily Yt V'} {f : V →ₗ[ZMod 2] V'} (hf : ∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x)) (q : Marking Yt.Y) (n : Gen → V) (φ' : Gen → Module.Dual (ZMod 2) V') (w : GExpr) : (heisEval Φ' q (fun (g : Gen) => f (n g)) φ' w).e ∘ₗ f = (heisEval Φ q n (fun (g : Gen) => φ' g ∘ₗ f) w).e

Dual-coordinate naturality, recovered from the relation.