Values of the Day convolution unit

The unit 𝟙_ (C ⊛⥤ V) of the Day convolution monoidal structure is the left Kan extension of 𝟙_ V along the inclusion of 𝟙_ C, so its value at d : C is the colimit of the constant diagram 𝟙_ V indexed by the morphisms 𝟙_ C ⟶ d. We compute this value in the two extreme cases:

• when 𝟙_ C has no endomorphism other than the identity, Mathlib's canonical map ν : 𝟙_ V ⟶ (𝟙_ (C ⊛⥤ V)).functor.obj (𝟙_ C) is an isomorphism;
• when there is no morphism 𝟙_ C ⟶ d, the value at d is an initial object.

For the finite-bijection groupoid both cases apply: the unit symmetric sequence is 𝟙_ V in level zero and initial in every positive level.

Main statements

• DayFunctor.isIso_ν: ν is an isomorphism when 𝟙_ C has only the identity endomorphism.
• DayFunctor.isInitialUnitObj: the unit is initial at objects receiving no morphism from 𝟙_ C.

instance CategoryTheory.MonoidalCategory.DayFunctor.isIso_ν {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)] [Subsingleton (tensorUnit C ⟶ tensorUnit C)] : IsIso (ν C V)

If the only endomorphism of 𝟙_ C is the identity, then the canonical map ν : 𝟙_ V ⟶ (𝟙_ (C ⊛⥤ V)).functor.obj (𝟙_ C) is an isomorphism: the Day convolution unit takes the value 𝟙_ V at 𝟙_ C.

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.isInitialUnitObj {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)] {d : C} [IsEmpty (tensorUnit C ⟶ d)] : Limits.IsInitial ((tensorUnit (DayFunctor C V)).functor.obj d)

If there is no morphism 𝟙_ C ⟶ d, then the Day convolution unit takes an initial value at d.