Self-duality of the standard super space

The copairing C = Σ e_i ⊗ e_i + Σ f_i ⊗ g_i as a morphism 𝟙 ⟶ stdSuperPair ⊗ stdSuperPair, and the snake identities pairing it against the standard form: stdSuperPair is exactly self-dual in SuperVect. This is the categorical form of the §5.2 conventions — the contraction identities L_C = id distributed over the graded blocks.

noncomputable def RS.stdCopairEvenElem (k : ℕ) : TensorProduct ℂ (Fin k → ℂ) (Fin k → ℂ)

The even copairing element Σ e_i ⊗ e_i.

Equations

• RS.stdCopairEvenElem k = ∑ i : Fin k, RS.stdE k i ⊗ₜ[ℂ] RS.stdE k i

noncomputable def RS.stdCopairOddElem (ℓ : ℕ) : TensorProduct ℂ (Fin (2 * ℓ) → ℂ) (Fin (2 * ℓ) → ℂ)

The odd copairing element Σ f_i ⊗ g_i.

Equations

• RS.stdCopairOddElem ℓ = ∑ i : Fin (2 * ℓ), RS.stdF ℓ i ⊗ₜ[ℂ] RS.stdG ℓ i

noncomputable def RS.stdCopair (k ℓ : ℕ) : SuperVect.tensorUnit.Hom ((stdSuperPair k ℓ).tensorObj (stdSuperPair k ℓ))

The standard copairing as an even morphism 𝟙 ⟶ stdSuperPair ⊗ stdSuperPair.

Equations

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

@[instance_reducible]

noncomputable instance RS.stdExactPairing (k ℓ : ℕ) : CategoryTheory.ExactPairing (stdSuperPair k ℓ) (stdSuperPair k ℓ)

Self-duality of the standard super space: the standard form and copairing are an exact pairing.

Equations

• RS.stdExactPairing k ℓ = { coevaluation' := RS.stdCopair k ℓ, evaluation' := RS.stdForm k ℓ, coevaluation_evaluation' := ⋯, evaluation_coevaluation' := ⋯ }