The fibre functor of a mixed sum

A mixed sum of p copies of the unit and q copies of the odd line has for its fibre the free super module of rank (p | q): the unit contributes the algebra and the line contributes its parity shift, and the fibre functor is additive.

noncomputable def RS.superFree {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (p q : ℕ) : (gammaAlgebra D L R).Mod

The free super module of rank (p | q).

Equations

• RS.superFree L R p q = ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => (RS.gammaAlgebra D L R).unitMod) (fun (x : Fin q) => (RS.gammaAlgebra D L R).unitMod.shift) i

noncomputable def RS.fibreMixIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (p q : ℕ) : (fibreFun L R).obj (L.mix p q) ≅ superFree L R p q

The fibre of a mixed sum is free of the corresponding rank.

Equations

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