The monoidal fibre functor at a complex point

The comparison and the unit of Comparison.lean, with the coherence proved in Coherence.lean, assemble the fibre functor at a ℂ-point into a lax monoidal functor; both comparisons being invertible it is strong monoidal, and it is braided as soon as the functor upstream of it is. Applied to a splitting algebra this gives a braided fibre functor out of the ambient category.

Contents

• RS.superVectFunctorLaxMonoidal, RS.superVectFunctorMonoidal: the fibre functor at a point is lax monoidal, and strong monoidal as soon as the functor upstream of it is.
• RS.isIso_superVectHom: the fibre functor carries an isomorphism to an isomorphism.
• RS.superVectFunctorBraided: the fibre functor at a point is braided as soon as the functor upstream of it is.
• RS.nonempty_braided_deligneFibre: the fibre functor of a splitting algebra at a complex point is braided.

The lax monoidal structure of the fibre functor

instance RS.finiteDimensional_tensor_base_even {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] : FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even

The base change of a tensor product is finite dimensional in even degree as soon as the two factors are: the comparison is a linear equivalence onto it.

instance RS.finiteDimensional_tensor_base_odd {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] : FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd

The base change of a tensor product is finite dimensional in odd degree.

instance RS.finiteDimensional_tensorObj_base_even {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] : FiniteDimensional ℂ ((CategoryTheory.MonoidalCategoryStruct.tensorObj M N).tensor (SuperCommAlgebra.pointMod P)).even

The same, for the monoidal notation.

instance RS.finiteDimensional_tensorObj_base_odd {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] : FiniteDimensional ℂ ((CategoryTheory.MonoidalCategoryStruct.tensorObj M N).tensor (SuperCommAlgebra.pointMod P)).odd

The same in odd degree, for the monoidal notation.

@[implicit_reducible]

noncomputable def RS.superVectFunctorLaxMonoidal {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] [CategoryTheory.MonoidalCategory E] (G : CategoryTheory.Functor E S.Mod) [G.LaxMonoidal] [hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even] [hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] : (superVectFunctor P G hE hO).LaxMonoidal

The fibre functor at a point is lax monoidal whenever the functor it is applied to is: the comparison of the base change is composed with the comparison upstream.

Equations

• One or more equations did not get rendered due to their size.

instance RS.isIso_superVectHom {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (u : M ⟶ N) [CategoryTheory.IsIso u] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] : CategoryTheory.IsIso (superVectHom P u)

Base change carries an isomorphism to an isomorphism.

@[implicit_reducible]

noncomputable def RS.superVectFunctorMonoidal {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] [CategoryTheory.MonoidalCategory E] (G : CategoryTheory.Functor E S.Mod) [G.Monoidal] [hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even] [hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] : (superVectFunctor P G hE hO).Monoidal

The fibre functor at a point is strong monoidal whenever the functor it is applied to is: both comparisons are invertible, the one of the base change unconditionally.

Equations

• RS.superVectFunctorMonoidal P G = CategoryTheory.Functor.Monoidal.ofLaxMonoidal (RS.superVectFunctor P G hE hO)

The braided structure of the fibre functor

@[implicit_reducible]

noncomputable def RS.superVectFunctorBraided {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (G : CategoryTheory.Functor E S.Mod) [G.Braided] [hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even] [hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] : (superVectFunctor P G hE hO).Braided

The fibre functor at a point is braided whenever the functor it is applied to is: the comparison of the base change intertwines the braidings, and so does the comparison upstream.

Equations

• RS.superVectFunctorBraided P G = { toMonoidal := RS.superVectFunctorMonoidal P G, braided := ⋯ }

The fibre functor of a splitting algebra is braided

theorem RS.nonempty_braided_deligneFibre {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsp : SplitsOn L 𝔸 indOf) (pt : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) : Nonempty (deligneFibre L 𝔸 hsp pt).Braided

The fibre functor of a splitting algebra at a complex point is braided. Upstream, the restriction of the fibre functor along the embedding is strong monoidal and lax braided; downstream, base change at the point is strong monoidal and intertwines the Koszul sign of the super vector spaces with the sign of the braiding of the super modules.