The standard form as a morphism of super vector spaces

The §5.1 conventions at the categorical level: the orthosymplectic form on the standard super space is an even morphism stdSuperPair ⊗ stdSuperPair ⟶ 𝟙 in SuperVect, and it is supersymmetric — composing with the Koszul braiding returns the form. The even block is symmetric; the odd block is antisymmetric, and the Koszul sign of the braiding on the odd⊗odd summand exactly compensates.

noncomputable def RS.stdFormEvenBilin (k : ℕ) : (Fin k → ℂ) →ₗ[ℂ] (Fin k → ℂ) →ₗ[ℂ] ℂ

The even form as a bilinear map.

Equations

• RS.stdFormEvenBilin k = LinearMap.mk₂ ℂ (RS.stdFormEven k) ⋯ ⋯ ⋯ ⋯

noncomputable def RS.stdFormOddBilin (ℓ : ℕ) : (Fin (2 * ℓ) → ℂ) →ₗ[ℂ] (Fin (2 * ℓ) → ℂ) →ₗ[ℂ] ℂ

The odd form as a bilinear map.

Equations

• RS.stdFormOddBilin ℓ = LinearMap.mk₂ ℂ (RS.stdFormOdd ℓ) ⋯ ⋯ ⋯ ⋯

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

The standard form as an even morphism stdSuperPair ⊗ stdSuperPair ⟶ 𝟙 of super vector spaces.

Equations

• RS.stdForm k ℓ = { evenMap := id ((TensorProduct.lift (RS.stdFormEvenBilin k)).coprod (TensorProduct.lift (RS.stdFormOddBilin ℓ))), oddMap := id 0 }

theorem RS.stdFormEven_comm (k : ℕ) (x y : Fin k → ℂ) : stdFormEven k x y = stdFormEven k y x

The even form is symmetric.