The complete standard model

Transporting the snake identities along the standard-model isomorphism, and the resulting complete §5.1–5.2 package: 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 stdForm and the copairing to stdCopair (exists_std_model).

The transport itself is delegated to mathlib's exactPairingCongr; its transported evaluation and coevaluation are identified with the tensorHom-conjugated form and copairing via tensorHom_def', and the transported copairing is then pinned by stdCopair_unique.

@[instance_reducible]

def RS.exactPairingOfSnake {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (C : SuperVect.tensorUnit.Hom (V.tensorObj V)) (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) : CategoryTheory.ExactPairing V V

A form and copairing with the snake identities assemble into an exact pairing.

Equations

• RS.exactPairingOfSnake b C h1 h2 = { coevaluation' := C, evaluation' := b, coevaluation_evaluation' := h1, evaluation_coevaluation' := h2 }

theorem RS.exists_std_model {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 ℓ ∧ (SuperVect.tensorHom e' e').comp C = stdCopair k ℓ

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