Ind-objects are closed under Day convolution

Over a small monoidal category C, the presheaf category Cᵒᵖ ⥤ Type v carries the Day-convolution monoidal structure through the synonym Cᵒᵖ ⊛⥤ Type v set up in RS.Classical.Deligne.DayType. This file proves that the ind-objects among presheaves are closed under the Day tensor and contain the Day unit:

• RS.dayYonedaIso: the Day tensor of the representables at x and y is the representable at x ⊗ y (this is RS.dayCoyonedaIso at the base Cᵒᵖ, read through Coyoneda.objOpOp and the definitional identification op x ⊗ op y = op (x ⊗ y) in Cᵒᵖ);
• RS.isIndObject_day_tensor: if F.functor and G.functor are ind-objects, so is (F ⊗ G).functor;
• RS.isIndObject_day_unit: the Day unit is an ind-object.

The argument is the classical one. Each tensor factor is a small filtered colimit of representables (IsIndObject.presentation); Day tensoring on either side preserves v-small colimits (the instances of RS.Classical.Deligne.DayCalculus), so the tensor is a small filtered colimit of tensors of representables, and those are representable by the co-Yoneda computation; closure of ind-objects under small filtered colimits (isIndObject_colimit) concludes. The two colimit steps are the same manoeuvre, factored out as RS.isIndObject_obj_of_preservesColimits.

def RS.dayMkIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)} (e : A ≅ B) : { functor := A } ≅ { functor := B }

Transport an isomorphism of plain presheaves to the Day synonym category.

Equations

• RS.dayMkIso e = (CategoryTheory.MonoidalCategory.DayFunctor.equiv Cᵒᵖ (Type ?u.1)).inverse.mapIso e

def RS.dayFunctorIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {F G : CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v)} (e : F ≅ G) : F.functor ≅ G.functor

Transport an isomorphism of the Day synonym category to the plain presheaf category.

Equations

• RS.dayFunctorIso e = (CategoryTheory.MonoidalCategory.DayFunctor.equiv Cᵒᵖ (Type ?u.1)).functor.mapIso e

noncomputable def RS.dayYonedaIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.yoneda.obj x } { functor := CategoryTheory.yoneda.obj y } ≅ { functor := CategoryTheory.yoneda.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) }

Day convolution of representables: the Day tensor of the yoneda presheaves at x and y is the yoneda presheaf at x ⊗ y. This is RS.dayCoyonedaIso at the base Cᵒᵖ, transported along Coyoneda.objOpOp, using that op x ⊗ op y = op (x ⊗ y) holds definitionally in Cᵒᵖ.

Equations

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

theorem RS.isIndObject_day_tensor_yoneda {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : CategoryTheory.Limits.IsIndObject (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.yoneda.obj x } { functor := CategoryTheory.yoneda.obj y }).functor

The Day tensor of two representable presheaves is an ind-object.

theorem RS.isIndObject_obj_of_preservesColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (T : CategoryTheory.Functor (CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v)) (CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v))) [CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, v + 1, v + 1} T] (hT : ∀ (y : C), CategoryTheory.Limits.IsIndObject (T.obj { functor := CategoryTheory.yoneda.obj y }).functor) {G : CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v)} (hG : CategoryTheory.Limits.IsIndObject G.functor) : CategoryTheory.Limits.IsIndObject (T.obj G).functor

A colimit-preserving endofunctor of the Day synonym category that sends representables to ind-objects sends every ind-object to an ind-object: apply the functor to a presentation of the argument as a small filtered colimit of representables and use closure of ind-objects under small filtered colimits. This is the induction step used twice below, for Day tensoring on either side.

theorem RS.isIndObject_day_tensor_yoneda_left {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) {G : CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v)} (hG : CategoryTheory.Limits.IsIndObject G.functor) : CategoryTheory.Limits.IsIndObject (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.yoneda.obj x } G).functor

The Day tensor of a representable presheaf with an ind-object is an ind-object.

theorem RS.isIndObject_day_tensor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {F G : CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v)} (hF : CategoryTheory.Limits.IsIndObject F.functor) (hG : CategoryTheory.Limits.IsIndObject G.functor) : CategoryTheory.Limits.IsIndObject (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).functor

Ind-objects are closed under Day convolution.

theorem RS.isIndObject_day_unit (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.IsIndObject (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v))).functor

The Day unit is an ind-object: by RS.dayUnitIso it is the representable at the monoidal unit of C.