The fibre functor is strong monoidal over a splitting algebra

Over an algebra for which every object becomes a mixed sum of copies of the unit and of the odd line, the monoidal comparison of Deligne's (2.11.1) is invertible at every pair of objects, and the unit comparison is invertible outright. The lax symmetric monoidal structure of the fibre functor is therefore strong.

def RS.Splits {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] : Prop

A splitting algebra: every object becomes a mixed sum of copies of the unit and of the odd line after base change.

Equations

• RS.Splits L R = ∀ (X : D), ∃ (p : ℕ) (q : ℕ), Nonempty (RS.freeMod R X ≅ RS.freeMod R (L.mix p q))

theorem RS.isIso_fibreMu_of_splits {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.HasCoequalizers D] [CategoryTheory.Limits.HasFiniteBiproducts D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (hsp : Splits L R) (V W : D) : CategoryTheory.IsIso (fibreMu L R V W)

Over a splitting algebra the monoidal comparison is invertible at every pair of objects.

@[implicit_reducible]

noncomputable def RS.fibreOverMonoidal {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.HasCoequalizers D] [CategoryTheory.Limits.HasFiniteBiproducts D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (hsp : Splits L R) : (fibreOver L R).Monoidal

Over a splitting algebra the fibre functor is strong monoidal.

Equations

• RS.fibreOverMonoidal L R hsp = CategoryTheory.Functor.Monoidal.ofLaxMonoidal (RS.fibreOver L R)