Merge remote-tracking branch 'origin/master' into bump/v4.22.0

Author: mathlib4-bot

Mathlib.lean

@@ -2380,6 +2380,7 @@ import Mathlib.CategoryTheory.Monoidal.CommGrp_
 import Mathlib.CategoryTheory.Monoidal.CommMon_
 import Mathlib.CategoryTheory.Monoidal.Comon_
 import Mathlib.CategoryTheory.Monoidal.Conv
+import Mathlib.CategoryTheory.Monoidal.DayConvolution
 import Mathlib.CategoryTheory.Monoidal.Discrete
 import Mathlib.CategoryTheory.Monoidal.End
 import Mathlib.CategoryTheory.Monoidal.ExternalProduct

Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean

@@ -189,6 +189,7 @@ lemma hom_ext_of_isLeftKanExtension {G : D ⥤ H} (γ₁ γ₂ : F' ⟶ G)
 
 /-- If `(F', α)` is a left Kan extension of `F` along `L`, then this
 is the induced bijection `(F' ⟶ G) ≃ (F ⟶ L ⋙ G)` for all `G`. -/
+@[simps!]
 noncomputable def homEquivOfIsLeftKanExtension (G : D ⥤ H) :
     (F' ⟶ G) ≃ (F ⟶ L ⋙ G) where
   toFun β := α ≫ whiskerLeft _ β

Mathlib/CategoryTheory/Monoidal/DayConvolution.lean

@@ -0,0 +1,203 @@
+/-
+Copyright (c) 2025 Robin Carlier. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Carlier
+-/
+import Mathlib.CategoryTheory.Monoidal.ExternalProduct
+import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
+
+/-!
+# Day convolution monoidal structure
+
+Given functors `F G : C ⥤ V` between two monoidal categories,
+this file defines a typeclass `DayConvolution` on functors `F` `G` that contains
+a functor `F ⊛ G`, as well as the required data to exhibit `F ⊛ G` as a pointwise
+left Kan extension of `F ⊠ G` (see `CategoryTheory/Monoidal/ExternalProduct` for the definition)
+along the tensor product of `C`. Such a functor is called a Day convolution of `F` and `G`, and
+although we do not show it yet, this operation defines a monoidal structure on `C ⥤ V`.
+
+We also define a typeclass `DayConvolutionUnit` on a functor `U : C ⥤ V` that bundle the data
+required to make it a unit for the Day convolution monoidal structure: said data is that of
+a map `𝟙_ V ⟶ U.obj (𝟙_ C)` that exhibits `U` as a pointwise left Kan extension of
+`fromPUnit (𝟙_ V)` along `fromPUnit (𝟙_ C)`.
+
+## References
+- [nLab page: Day convolution](https://ncatlab.org/nlab/show/Day+convolution)
+
+## TODOs (@robin-carlier)
+- Define associators and unitors, prove the pentagon and triangle identities.
+- Braided/symmetric case.
+- Case where `V` is closed.
+- Define a typeclass `DayConvolutionMonoidalCategory` extending `MonoidalCategory`
+- Characterization of lax monoidal functors out of a day convolution monoidal category.
+- Case `V = Type u` and its universal property.
+
+-/
+
+universe v₁ v₂ v₃ v₄ v₅ u₁ u₂ u₃ u₄ u₅
+
+namespace CategoryTheory.MonoidalCategory
+open scoped ExternalProduct
+
+noncomputable section
+
+variable {C : Type u₁} [Category.{v₁} C] {V : Type u₂} [Category.{v₂} V]
+  [MonoidalCategory C] [MonoidalCategory V]
+
+/-- A `DayConvolution` structure on functors `F G : C ⥤ V` is the data of
+a functor `F ⊛ G : C ⥤ V`, along with a unit `F ⊠ G ⟶ tensor C ⋙ F ⊛ G`
+that exhibits this functor as a pointwise left Kan extension of `F ⊠ G` along
+`tensor C`. This is a `class` used to prove various property of such extensions,
+but registering global instances of this class is probably a bad idea. -/
+class DayConvolution (F G : C ⥤ V) where
+  /-- The chosen convolution between the functors. Denoted `F ⊛ G`. -/
+  convolution : C ⥤ V
+  /-- The chosen convolution between the functors. -/
+  unit (F) (G) : F ⊠ G ⟶ tensor C ⋙ convolution
+  /-- The transformation `unit` exhibits `F ⊛ G` as a pointwise left Kan extension
+  of `F ⊠ G` along `tensor C`. -/
+  isPointwiseLeftKanExtensionUnit (F G) :
+    (Functor.LeftExtension.mk (convolution) unit).IsPointwiseLeftKanExtension
+
+namespace DayConvolution
+
+section
+
+/-- A notation for the Day convolution of two functors. -/
+scoped infixr:80 " ⊛ " => convolution
+
+variable (F G : C ⥤ V)
+
+instance leftKanExtension [DayConvolution F G] :
+    (F ⊛ G).IsLeftKanExtension (unit F G) :=
+  isPointwiseLeftKanExtensionUnit F G|>.isLeftKanExtension
+
+variable {F G}
+
+/-- Two day convolution structures on the same functors gives an isomorphic functor. -/
+def uniqueUpToIso (h : DayConvolution F G) (h' : DayConvolution F G) :
+    h.convolution ≅ h'.convolution :=
+  Functor.leftKanExtensionUnique h.convolution h.unit h'.convolution h'.unit
+
+@[reassoc (attr := simp)]
+lemma unit_uniqueUpToIso_hom (h : DayConvolution F G) (h' : DayConvolution F G) :
+    h.unit ≫ CategoryTheory.whiskerLeft (tensor C) (h.uniqueUpToIso h').hom = h'.unit := by
+  simp [uniqueUpToIso]
+
+@[reassoc (attr := simp)]
+lemma unit_uniqueUpToIso_inv (h : DayConvolution F G) (h' : DayConvolution F G) :
+    h'.unit ≫ CategoryTheory.whiskerLeft (tensor C) (h.uniqueUpToIso h').inv = h.unit := by
+  simp [uniqueUpToIso]
+
+variable (F G) [DayConvolution F G]
+
+section unit
+
+variable {x x' y y' : C}
+
+@[reassoc (attr := simp)]
+lemma unit_naturality (f : x ⟶ x') (g : y ⟶ y') :
+    (F.map f ⊗ₘ G.map g) ≫ (unit F G).app (x', y') =
+    (unit F G).app (x, y) ≫ (F ⊛ G).map (f ⊗ₘ g) := by
+  simpa [tensorHom_def] using (unit F G).naturality ((f, g) : (x, y) ⟶ (x', y'))
+
+variable (y) in
+@[reassoc (attr := simp)]
+lemma whiskerRight_comp_unit_app (f : x ⟶ x') :
+    F.map f ▷ G.obj y ≫ (unit F G).app (x', y) =
+    (unit F G).app (x, y) ≫ (F ⊛ G).map (f ▷ y) := by
+  simpa [tensorHom_def] using (unit F G).naturality ((f, 𝟙 _) : (x, y) ⟶ (x', y))
+
+variable (x) in
+@[reassoc (attr := simp)]
+lemma whiskerLeft_comp_unit_app (g : y ⟶ y') :
+    F.obj x ◁ G.map g ≫ (unit F G).app (x, y') =
+    (unit F G).app (x, y) ≫ (F ⊛ G).map (x ◁ g) := by
+  simpa [tensorHom_def] using (unit F G).naturality ((𝟙 _, g) : (x, y) ⟶ (x, y'))
+
+end unit
+
+variable {F G}
+
+section map
+
+variable {F' G' : C ⥤ V} [DayConvolution F' G']
+
+/-- The morphism between day convolutions (provided they exist) induced by a pair of morphisms. -/
+def map (f : F ⟶ F') (g : G ⟶ G') : F ⊛ G ⟶ F' ⊛ G' :=
+  Functor.descOfIsLeftKanExtension (F ⊛ G) (unit F G) (F' ⊛ G') <|
+    (externalProductBifunctor C C V).map ((f, g) : (F, G) ⟶ (F', G')) ≫ unit F' G'
+
+variable (f : F ⟶ F') (g : G ⟶ G') (x y : C)
+
+@[reassoc (attr := simp)]
+lemma unit_app_map_app :
+  (unit F G).app (x, y) ≫ (map f g).app (x ⊗ y : C) =
+    (f.app x ⊗ₘ g.app y) ≫ (unit F' G').app (x, y) := by
+  simpa [tensorHom_def] using
+    (Functor.descOfIsLeftKanExtension_fac_app (F ⊛ G) (unit F G) (F' ⊛ G') <|
+      (externalProductBifunctor C C V).map ((f, g) : (F, G) ⟶ (F', G')) ≫ unit F' G') (x, y)
+
+end map
+
+variable (F G)
+
+/-- The universal property of left Kan extensions characterizes the functor
+corepresented by `F ⊛ G`. -/
+@[simps!]
+def corepresentableBy :
+    (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G)|>.CorepresentableBy
+      (F ⊛ G) where
+  homEquiv := Functor.homEquivOfIsLeftKanExtension _ (unit F G) _
+  homEquiv_comp := by aesop
+
+/-- Use the fact that `(F ⊛ G).obj c` is a colimit to characterize morphisms out of it at a
+point. -/
+theorem convolution_hom_ext_at (c : C) {v : V} {f g : (F ⊛ G).obj c ⟶ v}
+    (h : ∀ {x y : C} (u : x ⊗ y ⟶ c),
+      (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ f = (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ g) :
+    f = g :=
+  ((isPointwiseLeftKanExtensionUnit F G) c).hom_ext (fun j ↦ by simpa using h j.hom)
+
+end
+
+end DayConvolution
+
+/-- A `DayConvolutionUnit` structure on a functor `C ⥤ V` is the data of a pointwise
+left Kan extension of `fromPUnit (𝟙_ V)` along `fromPUnit (𝟙_ C)`. Again, this is
+made a class to ease proofs when constructing `DayConvolutionMonoidalCategory` structures, but one
+should avoid registering it globally. -/
+class DayConvolutionUnit (F : C ⥤ V) where
+  /-- A "canonical" structure map `𝟙_ V ⟶ F.obj (𝟙_ C)` that defines a natural transformation
+  `fromPUnit (𝟙_ V) ⟶ fromPUnit (𝟙_ C) ⋙ F`. -/
+  can : 𝟙_ V ⟶ F.obj (𝟙_ C)
+  /-- The canonical map `𝟙_ V ⟶ F.obj (𝟙_ C)` exhibits `F` as a pointwise left kan extension
+  of `fromPUnit.{0} 𝟙_ V` along `fromPUnit.{0} 𝟙_ C`. -/
+  isPointwiseLeftKanExtensionCan : Functor.LeftExtension.mk F
+    ({app _ := can} : Functor.fromPUnit.{0} (𝟙_ V) ⟶
+      Functor.fromPUnit.{0} (𝟙_ C) ⋙ F)|>.IsPointwiseLeftKanExtension
+
+namespace DayConvolutionUnit
+
+variable (U : C ⥤ V) [DayConvolutionUnit U]
+open scoped DayConvolution
+
+/-- A shorthand for the natural transformation of functors out of PUnit defined by
+the canonical morphism `𝟙_ V ⟶ U.obj (𝟙_ C)` when `U` is a unit for Day convolution. -/
+abbrev φ : Functor.fromPUnit.{0} (𝟙_ V) ⟶ Functor.fromPUnit.{0} (𝟙_ C) ⋙ U where
+  app _ := can
+
+/-- Since a convolution unit is a pointwise left Kan extension, maps out of it at
+any object are uniquely characterized. -/
+lemma hom_ext {c : C} {v : V} {g h : U.obj c ⟶ v}
+    (e : ∀ f : 𝟙_ C ⟶ c, can ≫ U.map f ≫ g = can ≫ U.map f ≫ h) :
+    g = h := by
+  apply (isPointwiseLeftKanExtensionCan c).hom_ext
+  intro j
+  simpa using e j.hom
+
+end DayConvolutionUnit
+
+end
+
+end CategoryTheory.MonoidalCategory