Documentation

TauCeti.CategoryTheory.Monoidal.DayConvolution.Colimits

Colimits and Day convolution #

Day convolution with a fixed left factor preserves colimits whenever left tensoring with its values does. The proof factors convolution into the external product and left Kan extension along the tensor functor. It does not require a closed monoidal structure.

The result applies to any lawful presentation of Day convolution whose interpretation functor preserves and reflects the colimits in question. In particular it applies to symmetric sequences, allowing colimits of modules over a sphere sequence to be formed on their carriers.

The Kan-extension comparison uses Mathlib's Functor.lanAdjunction and Functor.leftKanExtensionUnique.

References #

source
noncomputable def CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.tensorLeftCompιIsoLan (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategory D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] [∀ (F : Functor (C × C) V), (tensor C).HasLeftKanExtension F] (d : D) :
(tensorLeft d).comp (ι C V D) ≅ (ι C V D).comp ((((externalProductBifunctorCurried C C V).obj ((ι C V D).obj d)).comp Functor.uncurry).comp (tensor C).lan)

Tensoring on the left in a lawful Day presentation is external product followed by left Kan extension, after passing to underlying functors.

Instances For
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit_comp_tensorLeftCompιIsoLan_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategory D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] [∀ (F : Functor (C × C) V), (tensor C).HasLeftKanExtension F] (d d' : D) (x y : C) :
    CategoryStruct.comp ((convolutionExtensionUnit C V d d').app (x, y)) (((tensorLeftCompιIsoLan C V D d).hom.app d').app (tensorObj x y)) = ((tensor C).lanUnit.app (externalProduct ((ι C V D).obj d) ((ι C V D).obj d'))).app (x, y)

    The Kan-extension comparison respects the universal convolution maps.

    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit_comp_tensorLeftCompιIsoLan_hom_app_assoc (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategory D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] [∀ (F : Functor (C × C) V), (tensor C).HasLeftKanExtension F] (d d' : D) (x y : C) {Z : V} (h : ((tensor C).lan.obj (Functor.uncurry.obj (((externalProductBifunctorCurried C C V).obj ((ι C V D).obj d)).obj ((ι C V D).obj d')))).obj (tensorObj x y) ⟶ Z) :
    CategoryStruct.comp ((convolutionExtensionUnit C V d d').app (x, y)) (CategoryStruct.comp (((tensorLeftCompιIsoLan C V D d).hom.app d').app (tensorObj x y)) h) = CategoryStruct.comp (((tensor C).lanUnit.app (externalProduct ((ι C V D).obj d) ((ι C V D).obj d'))).app (x, y)) h

    The Kan-extension comparison respects the universal convolution maps.

    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.lanUnit_comp_tensorLeftCompιIsoLan_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategory D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] [∀ (F : Functor (C × C) V), (tensor C).HasLeftKanExtension F] (d d' : D) (x y : C) :
    CategoryStruct.comp (((tensor C).lanUnit.app (externalProduct ((ι C V D).obj d) ((ι C V D).obj d'))).app (x, y)) (((tensorLeftCompιIsoLan C V D d).inv.app d').app (tensorObj x y)) = (convolutionExtensionUnit C V d d').app (x, y)

    The inverse Kan-extension comparison recovers the universal convolution maps.

    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.lanUnit_comp_tensorLeftCompιIsoLan_inv_app_assoc (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategory D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] [∀ (F : Functor (C × C) V), (tensor C).HasLeftKanExtension F] (d d' : D) (x y : C) {Z : V} (h : ((ι C V D).obj ((tensorLeft d).obj d')).obj (tensorObj x y) ⟶ Z) :
    CategoryStruct.comp (((tensor C).lanUnit.app (externalProduct ((ι C V D).obj d) ((ι C V D).obj d'))).app (x, y)) (CategoryStruct.comp (((tensorLeftCompιIsoLan C V D d).inv.app d').app (tensorObj x y)) h) = CategoryStruct.comp ((convolutionExtensionUnit C V d d').app (x, y)) h

    The inverse Kan-extension comparison recovers the universal convolution maps.

    source
    theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.preservesColimitsOfShape_tensorLeft (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {J : Type u₄} [Category.{v₄, u₄} J] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategory D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] [∀ (F : Functor (C × C) V), (tensor C).HasLeftKanExtension F] (d : D) [Limits.HasColimitsOfShape J V] [∀ (x : C), Limits.PreservesColimitsOfShape J (tensorLeft (((ι C V D).obj d).obj x))] [Limits.PreservesColimitsOfShape J (ι C V D)] [Limits.ReflectsColimitsOfShape J (ι C V D)] :
    Limits.PreservesColimitsOfShape J (tensorLeft d)

    A lawful Day convolution preserves colimits on the left when its interpretation preserves and reflects them, and the tensor product in the value category preserves them on the left.