The standard-model isomorphism

The morphism-level packaging of the coordinate identification: a super vector space carrying a supersymmetric form with a rigid copairing is isomorphic to a standard model stdSuperPair k ℓ, by an isomorphism pulling the form back to the standard form (exists_std_iso). This is the full statement of the §5.1 coordinate conventions: every self-dual object of SuperVect is a standard orthosymplectic space, form and all.

def RS.coordHom {V : SuperVect} {k ℓ : ℕ} (eE : (Fin k → ℂ) ≃ₗ[ℂ] V.even) (eO : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V.odd) : (stdSuperPair k ℓ).Hom V

The graded coordinate equivalences packaged as a morphism of super vector spaces.

Equations

• RS.coordHom eE eO = { evenMap := id ↑eE, oddMap := id ↑eO }

def RS.coordInv {V : SuperVect} {k ℓ : ℕ} (eE : (Fin k → ℂ) ≃ₗ[ℂ] V.even) (eO : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V.odd) : V.Hom (stdSuperPair k ℓ)

The inverse coordinate morphism.

Equations

• RS.coordInv eE eO = { evenMap := id ↑eE.symm, oddMap := id ↑eO.symm }

theorem RS.coordInv_comp_coordHom {V : SuperVect} {k ℓ : ℕ} (eE : (Fin k → ℂ) ≃ₗ[ℂ] V.even) (eO : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V.odd) : (coordInv eE eO).comp (coordHom eE eO) = SuperVect.Hom.id (stdSuperPair k ℓ)

One round trip of the coordinate identification is the identity.

theorem RS.coordHom_comp_coordInv {V : SuperVect} {k ℓ : ℕ} (eE : (Fin k → ℂ) ≃ₗ[ℂ] V.even) (eO : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V.odd) : (coordHom eE eO).comp (coordInv eE eO) = SuperVect.Hom.id V

And so is the other — the two are mutually inverse.

theorem RS.coordHom_form {V : SuperVect} {k ℓ : ℕ} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (eE : (Fin k → ℂ) ≃ₗ[ℂ] V.even) (eO : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V.odd) (hE : ∀ (x y : Fin k → ℂ), ((formEvenBlock b) (eE x)) (eE y) = stdFormEven k x y) (hO : ∀ (x y : Fin (2 * ℓ) → ℂ), ((formOddBlock b) (eO x)) (eO y) = stdFormOdd ℓ x y) : b.comp (SuperVect.tensorHom (coordHom eE eO) (coordHom eE eO)) = stdForm k ℓ

Pullback of the form along the coordinate morphism: when the coordinate equivalences carry the blocks of b to the standard forms, the coordinate morphism pulls b back to stdForm as a morphism equation.

theorem RS.exists_std_iso {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (C : SuperVect.tensorUnit.Hom (V.tensorObj V)) (hb : b.comp (V.koszulBraiding V) = b) (h1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := C; this)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := b; this) V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv) (h2 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := C; this) V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := b; this))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv) : ∃ (k : ℕ) (ℓ : ℕ) (e : (stdSuperPair k ℓ).Hom V) (e' : V.Hom (stdSuperPair k ℓ)), e'.comp e = SuperVect.Hom.id (stdSuperPair k ℓ) ∧ e.comp e' = SuperVect.Hom.id V ∧ b.comp (SuperVect.tensorHom e e) = stdForm k ℓ

The standard-model isomorphism (accompanying paper §5.1): a super vector space with a supersymmetric form and a rigid copairing is isomorphic to a standard model, by an isomorphism carrying the form to the standard form.