The Deligne bridge

Connecting the fibre-functor interface to the extraction: a braided monoidal functor into SuperVect carries a self-dual object with a supersymmetric form to a standard orthosymplectic model. The pairing transports by ExactPairing.map, the supersymmetry by the braided-functor axiom, and exists_std_model produces the coordinates.

theorem RS.braided_transported_supersymmetry {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (ω : CategoryTheory.Functor A SuperVect) [ω.Braided] (X : A) [CategoryTheory.ExactPairing X X] (hsym : CategoryTheory.CategoryStruct.comp (β_ X X).hom (ε_ X X) = ε_ X X) : SuperVect.Hom.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ ω X X) (CategoryTheory.CategoryStruct.comp (ω.map (ε_ X X)) (CategoryTheory.Functor.OplaxMonoidal.η ω))) ((ω.obj X).koszulBraiding (ω.obj X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ ω X X) (CategoryTheory.CategoryStruct.comp (ω.map (ε_ X X)) (CategoryTheory.Functor.OplaxMonoidal.η ω))

Supersymmetry transports along a braided functor into SuperVect: the transported form absorbs the Koszul braiding.

theorem RS.braided_std_model {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (ω : CategoryTheory.Functor A SuperVect) [ω.Braided] (X : A) [CategoryTheory.ExactPairing X X] (hsym : CategoryTheory.CategoryStruct.comp (β_ X X).hom (ε_ X X) = ε_ X X) : ∃ (k : ℕ) (ℓ : ℕ) (e : (stdSuperPair k ℓ).Hom (ω.obj X)) (e' : (ω.obj X).Hom (stdSuperPair k ℓ)), e'.comp e = SuperVect.Hom.id (stdSuperPair k ℓ) ∧ e.comp e' = SuperVect.Hom.id (ω.obj X) ∧ SuperVect.Hom.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ ω X X) (CategoryTheory.CategoryStruct.comp (ω.map (ε_ X X)) (CategoryTheory.Functor.OplaxMonoidal.η ω))) (SuperVect.tensorHom e e) = stdForm k ℓ ∧ (SuperVect.tensorHom e' e').comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε ω) (CategoryTheory.CategoryStruct.comp (ω.map (η_ X X)) (CategoryTheory.Functor.OplaxMonoidal.δ ω X X))) = stdCopair k ℓ

The Deligne bridge: a braided monoidal functor into SuperVect carries a self-dual object with a supersymmetric form to a standard orthosymplectic model — the transported form becomes the standard form and the transported copairing the standard copairing.