Standard orthosymplectic coordinates

The coordinate-identification step of §5.1: a super vector space V carrying a supersymmetric nondegenerate form b : V ⊗ V ⟶ 𝟙 is isomorphic, as a graded space with form, to the standard model stdSuperPair k ℓ with the standard form.

The route:

• formEvenBlock / formOddBlock extract the two bilinear blocks of the even component of b (the mixed blocks land in the odd component, which is zero).
• Supersymmetry b ∘ β = b makes the even block symmetric and the odd block alternating (formEvenBlock_symm, formOddBlock_isAlt) — the Koszul sign on the odd⊗odd summand is exactly the antisymmetry.
• exists_even_coordinates and exists_odd_coordinates convert the orthonormal- and symplectic-basis theorems into linear coordinate equivalences carrying each block to stdFormEven / stdFormOdd.
• exists_coordinates assembles the graded statement.

The bilinear blocks of a form morphism

def RS.formEvenMap {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) : TensorProduct ℂ V.even V.even × TensorProduct ℂ V.odd V.odd →ₗ[ℂ] ℂ

The even component of a form morphism V ⊗ V ⟶ 𝟙, with its domain and codomain presented in reduced form.

Equations

• RS.formEvenMap b = b.evenMap

def RS.formEvenBlock {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) : LinearMap.BilinForm ℂ V.even

The even block of a form morphism, as a bilinear form on V.even.

Equations

• RS.formEvenBlock b = TensorProduct.curry (RS.formEvenMap b ∘ₗ LinearMap.inl ℂ (TensorProduct ℂ V.even V.even) (TensorProduct ℂ V.odd V.odd))

def RS.formOddBlock {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) : LinearMap.BilinForm ℂ V.odd

The odd block of a form morphism, as a bilinear form on V.odd.

Equations

• RS.formOddBlock b = TensorProduct.curry (RS.formEvenMap b ∘ₗ LinearMap.inr ℂ (TensorProduct ℂ V.even V.even) (TensorProduct ℂ V.odd V.odd))

theorem RS.formEvenBlock_apply {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (x y : V.even) : ((formEvenBlock b) x) y = (formEvenMap b) (x ⊗ₜ[ℂ] y, 0)

The even block evaluates the even map on the even⊗even summand.

theorem RS.formOddBlock_apply {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (x y : V.odd) : ((formOddBlock b) x) y = (formEvenMap b) (0, x ⊗ₜ[ℂ] y)

The odd block evaluates the even map on the odd⊗odd summand.

Supersymmetry makes the blocks symmetric and alternating

theorem RS.formEvenBlock_symm {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (hb : b.comp (V.koszulBraiding V) = b) (x y : V.even) : ((formEvenBlock b) x) y = ((formEvenBlock b) y) x

Supersymmetry restricted to the even block: the even map absorbs the Koszul braiding, whose even⊗even component is the plain swap.

theorem RS.formOddBlock_skew {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (hb : b.comp (V.koszulBraiding V) = b) (x y : V.odd) : ((formOddBlock b) x) y = -((formOddBlock b) y) x

Supersymmetry restricted to the odd block: the Koszul sign on the odd⊗odd summand makes the block skew-symmetric.

theorem RS.formOddBlock_isAlt {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (hb : b.comp (V.koszulBraiding V) = b) : (formOddBlock b).IsAlt

The odd block of a supersymmetric form is alternating.

The symplectic normal form matches the standard odd form

theorem RS.symplecticMatrix_eq_std (ℓ : ℕ) (i j : Fin (2 * ℓ)) : (if ↑i + ℓ = ↑j then 1 else if ↑j + ℓ = ↑i then -1 else 0) = if j = oddPartner ℓ i then -↑(oddPartnerSign ℓ i) else 0

The symplectic normal-form matrix delivered by exists_symplectic_basis equals the partner/sign matrix of stdFormOdd.

Coordinates for the two blocks

theorem RS.exists_even_coordinates {V : Type} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (B : LinearMap.BilinForm ℂ V) (hsymm : ∀ (x y : V), (B x) y = (B y) x) (hnd : ∀ (x : V), (∀ (y : V), (B x) y = 0) → x = 0) : ∃ (k : ℕ) (e : (Fin k → ℂ) ≃ₗ[ℂ] V), ∀ (x y : Fin k → ℂ), (B (e x)) (e y) = stdFormEven k x y

Even coordinates: a symmetric nondegenerate bilinear form is carried to the standard even form by the coordinate equivalence of an orthonormal basis.

theorem RS.exists_odd_coordinates {V : Type} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (B : LinearMap.BilinForm ℂ V) (hAlt : B.IsAlt) (hND : B.Nondegenerate) : ∃ (ℓ : ℕ) (e : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V), ∀ (x y : Fin (2 * ℓ) → ℂ), (B (e x)) (e y) = stdFormOdd ℓ x y

Odd coordinates: an alternating nondegenerate bilinear form is carried to the standard odd form by the coordinate equivalence of a symplectic basis.

The graded coordinate identification

theorem RS.exists_coordinates {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (hb : b.comp (V.koszulBraiding V) = b) (hndE : ∀ (x : V.even), (∀ (y : V.even), ((formEvenBlock b) x) y = 0) → x = 0) (hndO : (formOddBlock b).Nondegenerate) : ∃ (k : ℕ) (ℓ : ℕ) (eE : (Fin k → ℂ) ≃ₗ[ℂ] V.even) (eO : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V.odd), (∀ (x y : Fin k → ℂ), ((formEvenBlock b) (eE x)) (eE y) = stdFormEven k x y) ∧ ∀ (x y : Fin (2 * ℓ) → ℂ), ((formOddBlock b) (eO x)) (eO y) = stdFormOdd ℓ x y

Standard orthosymplectic coordinates (accompanying paper §5.1): a super vector space with a supersymmetric form whose blocks are nondegenerate admits graded coordinates carrying the blocks to the standard forms of stdSuperPair k ℓ.