Restricting the fibre functor along a monoidal functor

A splitting algebra need not split every object of the ambient category — after all, the ambient category here is an Ind-completion and a filtered colimit is not a finite mixed sum. What is needed is only that it split the objects in the image of a chosen monoidal functor; the composite of that functor with the fibre functor is then strong monoidal.

def RS.SplitsOn {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] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (F : CategoryTheory.Functor C D) : Prop

The algebra splits the image of a functor: every object in the image becomes a mixed sum of copies of the unit and of the odd line after base change.

Equations

• RS.SplitsOn L R F = ∀ (X : C), ∃ (p : ℕ) (q : ℕ), Nonempty (RS.freeMod R (F.obj X) ≅ RS.freeMod R (L.mix p q))

@[implicit_reducible]

noncomputable def RS.fibreRestrictMonoidal {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] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor C D) [F.Monoidal] (hsp : SplitsOn L R F) : (F.comp (fibreOver L R)).Monoidal

The restricted fibre functor is strong monoidal.

Equations

• RS.fibreRestrictMonoidal L R F hsp = CategoryTheory.Functor.Monoidal.ofLaxMonoidal (F.comp (RS.fibreOver L R))