Odd pairs and their vanishing under split functionals

The odd⊗odd block of a tensor lands in the even part; under a tensor of copoint functionals it vanishes, because copoints kill odd parts (the unit has no odd part). This disposes of the cross-split odd basis terms in the cap recursion.

def RS.oddPair {V W : SuperVect} (v : V.odd) (w : W.odd) : (V.tensorObj W).even

The even element carried by a pair of odd vectors.

Equations

• RS.oddPair v w = (0, v ⊗ₜ[ℂ] w)

theorem RS.tensorHom_oddPair {V₁ V₂ W₁ W₂ : SuperVect} (g : V₁ ⟶ V₂) (h : W₁ ⟶ W₂) (v : V₁.odd) (w : W₁.odd) : (CategoryTheory.MonoidalCategoryStruct.tensorHom g h).evenMap (oddPair v w) = oddPair (g.oddMap v) (h.oddMap w)

Tensors of morphisms act blockwise on odd pairs.

theorem RS.lambda_oddPair (v w : SuperVect.tensorUnit.odd) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect)).hom.evenMap (oddPair v w) = 0

The target unitor kills odd pairs of unit vectors.

theorem RS.omegaFun_tensor_oddPair {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {a b : ℕ} (q₁ : { arity := a } ⟶ { arity := 0 }) (q₂ : { arity := b } ⟶ { arity := 0 }) (v : (P.ω.obj { arity := a }).odd) (w : (P.ω.obj { arity := b }).odd) : (omegaFun f P (CategoryTheory.MonoidalCategoryStruct.tensorHom q₁ q₂)) ((CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := a } { arity := b }).evenMap (oddPair v w)) = 0

Split functionals vanish on odd pairs: the tensor of two copoint functionals kills a structure-map image of an odd pair.