The corepresentable calculus of Day convolution on Type

Over a small monoidal category D, the Day-convolution monoidal structure on D ⊛⥤ Type v set up in RS.Classical.Deligne.DayType interacts with corepresentables in the classical way. This file records:

• RS.dayCoyonedaIso: the Day tensor of the corepresentable functors at a and b is the corepresentable functor at a ⊗ b (the co-Yoneda computation for Day convolution);
• RS.dayUnitIso: the Day unit is the corepresentable functor at 𝟙_ D;
• preservation of all v-small colimits by tensorLeft F and tensorRight F on D ⊛⥤ Type v, for every F.

The two isomorphisms follow from uniqueness of corepresenting objects: both sides corepresent evaluation of the underlying functor at the relevant object of D. The preservation instances are obtained by writing Day tensoring, on underlying functors, as an external-product functor followed by the left Kan extension functor along tensor D; the former preserves colimits pointwise because tensoring in Type v does, and the latter is a left adjoint.

def RS.dayEvaluation {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (d : D) : CategoryTheory.Functor (CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) (Type v)

Evaluation at d of the underlying functor, as a Type-valued functor on D ⊛⥤ Type v. Every corepresentability statement in this file corepresents a functor of this shape.

Equations

• RS.dayEvaluation d = (CategoryTheory.MonoidalCategory.DayFunctor.equiv D (Type ?u.1)).functor.comp ((CategoryTheory.evaluation D (Type ?u.1)).obj d)

def RS.coyonedaDayCorepresentableBy {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (c : D) : (dayEvaluation c).CorepresentableBy { functor := CategoryTheory.coyoneda.obj (Opposite.op c) }

The corepresentable Day functor at c corepresents evaluation at c: the Yoneda lemma, read through the DayFunctor synonym.

Equations

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

noncomputable def RS.dayCoyonedaCorepresentableBy {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b : D) : (dayEvaluation (CategoryTheory.MonoidalCategoryStruct.tensorObj a b)).CorepresentableBy (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) })

The Day tensor of the corepresentables at a and b corepresents evaluation at a ⊗ b: maps out of it are transformations out of the external product of the two corepresentables, which is definitionally the corepresentable of the product category at (a, b), so the Yoneda lemma evaluates. This is the co-Yoneda computation for Day convolution.

Equations

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

noncomputable def RS.dayCoyonedaIso {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) } ≅ { functor := CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.MonoidalCategoryStruct.tensorObj a b)) }

Day convolution of corepresentables: the Day tensor of the corepresentable functors at a and b is the corepresentable functor at a ⊗ b.

Equations

• RS.dayCoyonedaIso a b = (RS.dayCoyonedaCorepresentableBy a b).uniqueUpToIso (RS.coyonedaDayCorepresentableBy (CategoryTheory.MonoidalCategoryStruct.tensorObj a b))

noncomputable def RS.dayUnitCorepresentableBy {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] : (dayEvaluation (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).CorepresentableBy (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor D (Type v)))

The Day unit corepresents evaluation at 𝟙_ D: a map out of it is determined by an element of F.functor.obj (𝟙_ D), via the universal property of the unit as a left Kan extension along fromPUnit (𝟙_ D).

Equations

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

noncomputable def RS.dayUnitIso (D : Type v) [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) ≅ { functor := CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) }

The Day unit is the corepresentable functor at the monoidal unit of D.

Equations

• RS.dayUnitIso D = RS.dayUnitCorepresentableBy.uniqueUpToIso (RS.coyonedaDayCorepresentableBy (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))

def RS.externalLeftFunctor {D : Type v} [CategoryTheory.SmallCategory D] (K : CategoryTheory.Functor D (Type v)) : CategoryTheory.Functor (CategoryTheory.Functor D (Type v)) (CategoryTheory.Functor (D × D) (Type v))

Fixing the left factor of the external product gives a functor in the right factor.

Equations

• RS.externalLeftFunctor K = (CategoryTheory.Prod.sectR K (CategoryTheory.Functor D (Type ?u.1))).comp (CategoryTheory.MonoidalCategory.externalProductBifunctor D D (Type ?u.1))

def RS.externalRightFunctor {D : Type v} [CategoryTheory.SmallCategory D] (K : CategoryTheory.Functor D (Type v)) : CategoryTheory.Functor (CategoryTheory.Functor D (Type v)) (CategoryTheory.Functor (D × D) (Type v))

Fixing the right factor of the external product gives a functor in the left factor.

Equations

• RS.externalRightFunctor K = (CategoryTheory.Prod.sectL (CategoryTheory.Functor D (Type ?u.1)) K).comp (CategoryTheory.MonoidalCategory.externalProductBifunctor D D (Type ?u.1))

def RS.externalLeftFunctorEvaluationIso {D : Type v} [CategoryTheory.SmallCategory D] (K : CategoryTheory.Functor D (Type v)) (p : D × D) : ((CategoryTheory.evaluation D (Type v)).obj p.2).comp (CategoryTheory.MonoidalCategory.tensorLeft (K.obj p.1)) ≅ (externalLeftFunctor K).comp ((CategoryTheory.evaluation (D × D) (Type v)).obj p)

Pointwise, the external product with a fixed left factor is tensoring on the left in Type v.

Equations

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

def RS.externalRightFunctorEvaluationIso {D : Type v} [CategoryTheory.SmallCategory D] (K : CategoryTheory.Functor D (Type v)) (p : D × D) : ((CategoryTheory.evaluation D (Type v)).obj p.1).comp (CategoryTheory.MonoidalCategory.tensorRight (K.obj p.2)) ≅ (externalRightFunctor K).comp ((CategoryTheory.evaluation (D × D) (Type v)).obj p)

Pointwise, the external product with a fixed right factor is tensoring on the right in Type v.

Equations

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

instance RS.externalLeftFunctor_preservesColimits {D : Type v} [CategoryTheory.SmallCategory D] (K : CategoryTheory.Functor D (Type v)) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, v + 1, v + 1} (externalLeftFunctor K)

The external product with a fixed left factor preserves colimits in the right factor.

instance RS.externalRightFunctor_preservesColimits {D : Type v} [CategoryTheory.SmallCategory D] (K : CategoryTheory.Functor D (Type v)) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, v + 1, v + 1} (externalRightFunctor K)

The external product with a fixed right factor preserves colimits in the left factor.

noncomputable def RS.tensorObjLanIso {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F G : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) : (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).functor ≅ (CategoryTheory.MonoidalCategory.tensor D).lan.obj (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor)

The Day tensor, on underlying functors, is the left Kan extension of the external product along tensor D.

Equations

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

@[simp]

theorem RS.tensorObjLanIso_hom {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F G : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) : (tensorObjLanIso F G).hom = (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).functor.descOfIsLeftKanExtension (F.η G) ((CategoryTheory.MonoidalCategory.tensor D).lan.obj (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor)) ((CategoryTheory.MonoidalCategory.tensor D).lanUnit.app (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor))

@[simp]

theorem RS.tensorObjLanIso_inv {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F G : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) : (tensorObjLanIso F G).inv = ((CategoryTheory.MonoidalCategory.tensor D).lan.obj (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor)).descOfIsLeftKanExtension ((CategoryTheory.MonoidalCategory.tensor D).lanUnit.app (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor)) (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).functor (F.η G)

theorem RS.whiskerLeft_natTrans_tensorObjLanIso_hom {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) {G G' : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)} (g : G ⟶ G') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F g).natTrans (tensorObjLanIso F G').hom = CategoryTheory.CategoryStruct.comp (tensorObjLanIso F G).hom ((CategoryTheory.MonoidalCategory.tensor D).lan.map ((CategoryTheory.MonoidalCategory.externalProductBifunctor D D (Type v)).map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id F.functor) g.natTrans)))

Naturality in the right variable of RS.tensorObjLanIso.

theorem RS.whiskerRight_natTrans_tensorObjLanIso_hom {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) {G G' : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)} (g : G ⟶ G') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g F).natTrans (tensorObjLanIso G' F).hom = CategoryTheory.CategoryStruct.comp (tensorObjLanIso G F).hom ((CategoryTheory.MonoidalCategory.tensor D).lan.map ((CategoryTheory.MonoidalCategory.externalProductBifunctor D D (Type v)).map (CategoryTheory.Prod.mkHom g.natTrans (CategoryTheory.CategoryStruct.id F.functor))))

Naturality in the left variable of RS.tensorObjLanIso.

noncomputable def RS.tensorLeftCompIso {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) : (CategoryTheory.MonoidalCategory.tensorLeft F).comp (CategoryTheory.MonoidalCategory.DayFunctor.equiv D (Type v)).functor ≅ (CategoryTheory.MonoidalCategory.DayFunctor.equiv D (Type v)).functor.comp ((externalLeftFunctor F.functor).comp (CategoryTheory.MonoidalCategory.tensor D).lan)

Day tensoring on the left, transported to the plain functor category, is the external product followed by left Kan extension along tensor D.

Equations

• RS.tensorLeftCompIso F = CategoryTheory.NatIso.ofComponents (fun (G : CategoryTheory.MonoidalCategory.DayFunctor D (Type ?u.1)) => RS.tensorObjLanIso F G) ⋯

noncomputable def RS.tensorRightCompIso {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) : (CategoryTheory.MonoidalCategory.tensorRight F).comp (CategoryTheory.MonoidalCategory.DayFunctor.equiv D (Type v)).functor ≅ (CategoryTheory.MonoidalCategory.DayFunctor.equiv D (Type v)).functor.comp ((externalRightFunctor F.functor).comp (CategoryTheory.MonoidalCategory.tensor D).lan)

Day tensoring on the right, transported to the plain functor category, is the external product followed by left Kan extension along tensor D.

Equations

• RS.tensorRightCompIso F = CategoryTheory.NatIso.ofComponents (fun (G : CategoryTheory.MonoidalCategory.DayFunctor D (Type ?u.1)) => RS.tensorObjLanIso G F) ⋯

instance RS.instPreservesColimitsOfSizeDayFunctorTypeTensorLeft_leanPool {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, v + 1, v + 1} (CategoryTheory.MonoidalCategory.tensorLeft F)

Day tensoring on the left preserves v-small colimits: through RS.tensorLeftCompIso it is, up to the tautological equivalence, an external product followed by a left Kan extension, and both preserve colimits.

instance RS.instPreservesColimitsOfSizeDayFunctorTypeTensorRight_leanPool {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, v + 1, v + 1} (CategoryTheory.MonoidalCategory.tensorRight F)

Day tensoring on the right preserves v-small colimits: through RS.tensorRightCompIso it is, up to the tautological equivalence, an external product followed by a left Kan extension, and both preserve colimits.