Documentation

TauCeti.CategoryTheory.Monoidal.DayConvolution.Monoid

Lax monoidal functors as Day convolution monoids #

For monoidal categories C and V, a monoid for the Day convolution product on C ⊛⥤ V is the same thing as a lax monoidal functor C ⥤ V: by the universal property of the Day convolution F ⊗ F as a left Kan extension of F ⊠ F along the tensor product of C, a multiplication F ⊗ F ⟶ F is a natural family F x ⊗ F y ⟶ F (x ⊗ y), and a unit 𝟙_ ⟶ F is a morphism 𝟙_ V ⟶ F (𝟙_ C). This file constructs the direction used to build monoids: the tensorator and unit of a lax monoidal functor F make F a monoid object of C ⊛⥤ V, which is commutative when F is lax braided and the braiding of C is symmetric. Monoidal natural transformations become monoid morphisms.

The symmetry assumption on C comes from the convention of Mathlib's Day convolution braiding, which restricts along the units to F x ⊗ G y ⟶ G y ⊗ F x ⟶ (G ⊗ F) (y ⊗ x) ⟶ (G ⊗ F) (x ⊗ y), the last map being the braiding β_ y x of C.

The main application is the sphere symmetric sequence n ↦ (S¹)^∧n, a lax braided functor out of the finite-bijection groupoid, whose Day convolution monoid structure is the ring structure of the sphere symmetric spectrum.

The monoid laws are verified using the restatements, along the Day convolution units, of the whiskerings, the associator and the unitors of C ⊛⥤ V and the corresponding extensionality lemmas from TauCeti.CategoryTheory.Monoidal.DayConvolution.Basic. The unit and multiplication are built with DayFunctor.unitDesc and DayFunctor.tensorDesc from Robin Carlier's Day convolution formalization in Mathlib (Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor).

Main definitions #

Main statements #

References #

source
@[instance_reducible]
noncomputable instance CategoryTheory.MonoidalCategory.DayFunctor.monObj {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) [F.functor.LaxMonoidal] :
MonObj F

The Day convolution monoid structure on a lax monoidal functor F: its unit and multiplication are induced by the unit ε and the tensorator μ of F.

source
@[simp]
theorem CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_one_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) [F.functor.LaxMonoidal] :
CategoryStruct.comp (ν C V) (MonObj.one.natTrans.app (tensorUnit C)) = Functor.LaxMonoidal.ε F.functor

The unit of the Day convolution monoid F restricts along ν to the unit ε of F.

source
@[simp]
theorem CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_one_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) [F.functor.LaxMonoidal] {Z : V} (h : F.functor.obj (tensorUnit C) ⟶ Z) :
CategoryStruct.comp (ν C V) (CategoryStruct.comp (MonObj.one.natTrans.app (tensorUnit C)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε F.functor) h

The unit of the Day convolution monoid F restricts along ν to the unit ε of F.

source
@[simp]
theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_mul_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) [F.functor.LaxMonoidal] (x y : C) :
CategoryStruct.comp ((F.η F).app (x, y)) (MonObj.mul.natTrans.app (tensorObj x y)) = Functor.LaxMonoidal.μ F.functor x y

The multiplication of the Day convolution monoid F restricts along η F F to the tensorator μ of F.

source
@[simp]
theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_mul_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) [F.functor.LaxMonoidal] (x y : C) {Z : V} (h : F.functor.obj (tensorObj x y) ⟶ Z) :
CategoryStruct.comp ((F.η F).app (x, y)) (CategoryStruct.comp (MonObj.mul.natTrans.app (tensorObj x y)) h) = CategoryStruct.comp (Functor.LaxMonoidal.μ F.functor x y) h

The multiplication of the Day convolution monoid F restricts along η F F to the tensorator μ of F.

source
instance CategoryTheory.MonoidalCategory.DayFunctor.isMonHom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G : DayFunctor C V} [F.functor.LaxMonoidal] [G.functor.LaxMonoidal] (f : F ⟶ G) [NatTrans.IsMonoidal f.natTrans] :
IsMonHom f

A monoidal natural transformation of lax monoidal functors is a morphism of the associated Day convolution monoids.

source
instance CategoryTheory.MonoidalCategory.DayFunctor.isCommMonObj {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] [SymmetricCategory C] [BraidedCategory V] (F : DayFunctor C V) [F.functor.LaxBraided] :
IsCommMonObj F

The Day convolution monoid of a lax braided functor out of a symmetric monoidal category is commutative.