From 69d149916459c1903cb70488d493fcc222988d5e Mon Sep 17 00:00:00 2001 From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> Date: Sun, 18 May 2025 15:39:03 +0200 Subject: [PATCH 1/5] definitions for day convolution --- Mathlib.lean | 2 + .../Functor/KanExtension/Basic.lean | 1 + .../Monoidal/DayConvolution.lean | 185 ++++++++++++++++++ .../Monoidal/ExternalProduct.lean | 98 ++++++++++ 4 files changed, 286 insertions(+) create mode 100644 Mathlib/CategoryTheory/Monoidal/DayConvolution.lean create mode 100644 Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean diff --git a/Mathlib.lean b/Mathlib.lean index 66d8089707617f..3bd0b214260d83 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2336,8 +2336,10 @@ 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 import Mathlib.CategoryTheory.Monoidal.Free.Basic import Mathlib.CategoryTheory.Monoidal.Free.Coherence import Mathlib.CategoryTheory.Monoidal.Functor diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean index 5666688ed76428..2c44f3a5834b78 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean +++ b/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 _ β diff --git a/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean new file mode 100644 index 00000000000000..ea9576f0ddbf55 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean @@ -0,0 +1,185 @@ +/- +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 + +-/ + +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 to 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`. -/ + unitPointwiseKan (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) := + unitPointwiseKan 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 + +@[simp] +lemma uniqueUpToIso_hom_unit (h : DayConvolution F G) (h' : DayConvolution F G) : + h.unit ≫ CategoryTheory.whiskerLeft (tensor C) (h.uniqueUpToIso h').hom = h'.unit := by + simp [uniqueUpToIso] + +@[simp] +lemma uniqueUpToIso_inv_unit (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 unit_naturality_id_right (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 unit_naturality_id_left (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 map_unit_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 corepresentableIso : coyoneda.obj (.op <| F ⊛ G) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G) := + NatIso.ofComponents + (fun H ↦ Equiv.toIso <| Functor.homEquivOfIsLeftKanExtension _ (unit F G) _) + +/-- The universal property of left Kan extensions characterizes the functor +corepresented by `F ⊛ G`. -/ +def corepresentable : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G)|>.CorepresentableBy + (F ⊛ G) := + Functor.corepresentableByEquiv.symm <| corepresentableIso F G + +/-- 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 := + ((unitPointwiseKan 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`. -/ + canPointwiseLeftKanExtension : 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 (canPointwiseLeftKanExtension c).hom_ext + intro j + simpa using e j.hom + +end DayConvolutionUnit + +end + +end CategoryTheory.MonoidalCategory diff --git a/Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean b/Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean new file mode 100644 index 00000000000000..b347293c9301b0 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean @@ -0,0 +1,98 @@ +/- +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.FunctorCategory +import Mathlib.CategoryTheory.Functor.Currying + +/-! +# External product of diagrams in a monoidal category + +In a monoidal category `C`, given a pair of diagrams `K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, we +introduce the external product `K₁ ⊠ K₂ : J₁ × J₂ ⥤ C` as the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. +The notation `- ⊠ -` is scoped to `MonoidalCategory.ExternalProduct`. +-/ + +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +namespace CategoryTheory.MonoidalCategory + +variable (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) + [Category.{v₁} J₁] [Category.{v₂} J₂] [Category.{v₃} C] [MonoidalCategory C] + +/-- The (uncurried version of the) external product bifunctor: Given diagrams +`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `j₁ ↦ j₂ ↦ K₁ j₁ ⊗ K₂ j₂`. -/ +@[simps!] +def externalProductBifunctorUncurried : (J₁ ⥤ C) ⥤ (J₂ ⥤ C) ⥤ J₁ ⥤ J₂ ⥤ C := + (Functor.postcompose₂.obj <| (evaluation _ _).obj <| curriedTensor C).obj <| whiskeringLeft₂ C + +/-- The external product bifunctor: Given diagrams +`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. -/ +@[simps!] +def externalProductBifunctor : ((J₁ ⥤ C) × (J₂ ⥤ C)) ⥤ J₁ × J₂ ⥤ C := + uncurry.obj <| (Functor.postcompose₂.obj <| uncurry).obj <| + externalProductBifunctorUncurried J₁ J₂ C + +variable {J₁ J₂ C} +/-- An abbreviation for the action of `externalProductBifunctor J₁ J₂ C` on objects. -/ +abbrev externalProduct (F₁ : J₁ ⥤ C) (F₂ : J₂ ⥤ C) := + externalProductBifunctor J₁ J₂ C|>.obj (F₁, F₂) + +namespace ExternalProduct +/-- Notation for `externalProduct`. +``` +open scoped CategoryTheory.MonoidalCategory.ExternalProduct +``` to bring this notation in scope. -/ +scoped infixr:80 " ⊠ " => externalProduct + +end ExternalProduct + +open scoped ExternalProduct + +variable (J₁ J₂ C) + +/-- When both diagrams have the same source category, composing the external product with +the diagonal gives the pointwise functor tensor product. +Note that `(externalProductCompDiagIso _ _).app (F₁, F₂) : Functor.diag J₁ ⋙ F₁ ⊠ F₂ ≅ F₁ ⊗ F₂` +type checks. -/ +@[simps!] +def externalProductCompDiagIso : + externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft _ _ _|>.obj <| Functor.diag J₁) ≅ + tensor (J₁ ⥤ C) := + NatIso.ofComponents + (fun _ ↦ NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp [tensorHom_def])) + (fun _ ↦ by ext; simp [tensorHom_def]) + +/-- When `C` is braided, there is an isomorphism `Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`, natural +in both `F₁` and `F₂`. +Note that `(externalProductSwap _ _ _).app (F₁, F₂) : Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁` +type checks. -/ +@[simps!] +def externalProductSwap [BraidedCategory C] : + externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft _ _ _|>.obj <| Prod.swap _ _) + ≅ Prod.swap _ _ ⋙ externalProductBifunctor J₂ J₁ C := + NatIso.ofComponents + (fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) (by simp [tensorHom_def, whisker_exchange])) + (fun _ ↦ by ext; simp [tensorHom_def, whisker_exchange]) + +/-- A version of `externalProductSwap` phrased in terms of the uncurried functors. -/ +@[simps!] +def externalProductFlip [BraidedCategory C] : + (Functor.postcompose₂.obj <| flipFunctor _ _ _).obj (externalProductBifunctorUncurried J₁ J₂ C) + ≅ (externalProductBifunctorUncurried J₂ J₁ C).flip := + NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents <| + fun _ ↦ NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) + +section Composition + +variable {J₁ J₂ C} {I₁ : Type u₃} {I₂ : Type u₄} [Category.{v₃} I₁] [Category.{v₄} I₂] + +/-- Composing F₁ × F₂ with (G₁ ⊠ G₂) is isomorphic to (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) -/ +@[simps!] +def prodCompExternalProduct (F₁ : I₁ ⥤ J₁) (G₁ : J₁ ⥤ C) (F₂ : I₂ ⥤ J₂) (G₂ : J₂ ⥤ C) : + F₁.prod F₂ ⋙ G₁ ⊠ G₂ ≅ (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) := NatIso.ofComponents (fun _ ↦ Iso.refl _) + +end Composition + +end CategoryTheory.MonoidalCategory From d64024101f81e6556fee42b0b6a0e8ebeaee76c1 Mon Sep 17 00:00:00 2001 From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> Date: Sun, 18 May 2025 15:40:22 +0200 Subject: [PATCH 2/5] Associators --- Mathlib.lean | 3 + .../Functor/KanExtension/Basic.lean | 1 + .../Monoidal/DayConvolution.lean | 417 ++++++++++++++++++ .../Monoidal/ExternalProduct/Basic.lean | 98 ++++ .../ExternalProduct/KanExtension.lean | 144 ++++++ 5 files changed, 663 insertions(+) create mode 100644 Mathlib/CategoryTheory/Monoidal/DayConvolution.lean create mode 100644 Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean create mode 100644 Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean diff --git a/Mathlib.lean b/Mathlib.lean index 66d8089707617f..f98013716bd93a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2336,8 +2336,11 @@ 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.Basic +import Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension import Mathlib.CategoryTheory.Monoidal.Free.Basic import Mathlib.CategoryTheory.Monoidal.Free.Coherence import Mathlib.CategoryTheory.Monoidal.Functor diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean index 5666688ed76428..2c44f3a5834b78 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean +++ b/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 _ β diff --git a/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean new file mode 100644 index 00000000000000..0fdb356083c5e4 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean @@ -0,0 +1,417 @@ +/- +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.KanExtension +import Mathlib.CategoryTheory.Products.Associator + +/-! +# Day convolution monoidal structure + +-/ + +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 to 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`. -/ + unitPointwiseKan (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) := + unitPointwiseKan 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 + +@[simp] +lemma uniqueUpToIso_hom_unit (h : DayConvolution F G) (h' : DayConvolution F G) : + h.unit ≫ CategoryTheory.whiskerLeft (tensor C) (h.uniqueUpToIso h').hom = h'.unit := by + simp [uniqueUpToIso] + +@[simp] +lemma uniqueUpToIso_inv_unit (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 unit_naturality_id_right (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 unit_naturality_id_left (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 map_unit_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 corepresentableIso : coyoneda.obj (.op <| F ⊛ G) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G) := + NatIso.ofComponents + (fun H ↦ Equiv.toIso <| Functor.homEquivOfIsLeftKanExtension _ (unit F G) _) + +/-- The universal property of left Kan extensions characterizes the functor +corepresented by `F ⊛ G`. -/ +def corepresentable : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G)|>.CorepresentableBy + (F ⊛ G) := + Functor.corepresentableByEquiv.symm <| corepresentableIso F G + +/-- 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 := + (unitPointwiseKan F G c).hom_ext (by simpa using h ·.hom) + + +section associator + +variable (H : C ⥤ V) + [DayConvolution G H] + [DayConvolution F (G ⊛ H)] + [DayConvolution (F ⊛ G) H] + [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (tensor C) d) (tensorLeft v)] + [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (tensor C) d) (tensorRight v)] + +open MonoidalCategory.ExternalProduct + +instance : (F ⊠ G ⊛ H).IsLeftKanExtension <| + extensionUnitRight (G ⊛ H) (unit G H) F := + (pointwiseLeftKanExtensionRight _ _ _ <| unitPointwiseKan G H).isLeftKanExtension + +instance : ((F ⊛ G) ⊠ H).IsLeftKanExtension <| + extensionUnitLeft (F ⊛ G) (unit F G) H := + (pointwiseLeftKanExtensionLeft _ _ _ <| unitPointwiseKan F G).isLeftKanExtension + +/-- An auxiliary equivalence used to build the associators, +characterizing morphism out of `F ⊛ G ⊛ H` via the universal property of Kan extensions. +-/ +@[simps!] +noncomputable def corepresentableIso₂ : + coyoneda.obj (.op <| F ⊛ G ⊛ H) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H) := + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ (G ⊛ H)) := + corepresentableIso F (G ⊛ H) + _ ≅ _ := NatIso.ofComponents + (fun _ ↦ Equiv.toIso <| Functor.homEquivOfIsLeftKanExtension _ + (extensionUnitRight (G ⊛ H) (unit G H) F) _) + +/-- An auxiliary equivalence used to build the associators, +characterizing morphism out of `F ⊛ G ⊛ H` via the universal property of Kan extensions. +-/ +@[simps!] +noncomputable def corepresentableIso₂' : + coyoneda.obj (.op <| (F ⊛ G) ⊛ H) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| (F ⊠ G) ⊠ H) := + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| (F ⊛ G) ⊠ H) := + corepresentableIso (F ⊛ G) H + _ ≅ _ := NatIso.ofComponents + (fun _ ↦ Equiv.toIso <| Functor.homEquivOfIsLeftKanExtension _ + (extensionUnitLeft (F ⊛ G) (unit F G) H) _) + +/-- The `CorepresentableBy` structure on `F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ -` +derived from `tensorCorepresentableIso₂`. -/ +def corepresentable₂ : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H)|>.CorepresentableBy (F ⊛ G ⊛ H) := + Functor.corepresentableByEquiv.symm (corepresentableIso₂ F G H) + +/-- The `CorepresentableBy` structure on `(F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ -` +derived from `tensorCorepresentableIso₂`. -/ +def corepresentable₂' : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| (F ⊠ G) ⊠ H)|>.CorepresentableBy ((F ⊛ G) ⊛ H) := + Functor.corepresentableByEquiv.symm (corepresentableIso₂' F G H) + +/-- The isomorphism of functors between +`((F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ -)` and +`(F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ -)` that copresents the associator isomorphism +for Day convolution. -/ +@[simps!] +def associatorCorepresentingIso : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| (F ⊠ G) ⊠ H) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H) := + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + (whiskeringLeft _ _ _).obj (prod.associativity C C C).inverse ⋙ + coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) := + isoWhiskerLeft _ (isoWhiskerLeft _ + (NatIso.ofComponents fun _ ↦ Equiv.toIso <| + (prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv)) + _ ≅ (whiskeringLeft _ _ _).obj + ((prod.associativity C C C).inverse ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C) ⋙ + coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) := + .refl _ + _ ≅ (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C) ⋙ tensor C) ⋙ + coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) := + isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents (fun _ ↦ α_ _ _ _)) _ + _ ≅ (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C) ⋙ tensor C) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H) := + isoWhiskerLeft _ <| + coyoneda.mapIso <| Iso.op <| NatIso.ofComponents (fun _ ↦ α_ _ _ _|>.symm) + +/-- The asociator morphism for Day convolution -/ +def associator : (F ⊛ G) ⊛ H ≅ F ⊛ G ⊛ H := + corepresentable₂' F G H|>.ofIso (associatorCorepresentingIso F G H)|>.uniqueUpToIso <| + corepresentable₂ F G H + +/-- Characterizing the forward direction of the associator isomorphism +with respect to the unit transformations. -/ +@[reassoc (attr := simp)] +lemma associator_hom_unit_unit (x y z : C) : + (unit F G).app (x, y) ▷ (H.obj z) ≫ + (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ + (associator F G H).hom.app ((x ⊗ y) ⊗ z) = + (α_ _ _ _).hom ≫ + (F.obj x ◁ (unit G H).app (y, z)) ≫ + (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ + (F ⊛ G ⊛ H).map (α_ _ _ _).inv := by + letI := congrArg (fun t ↦ t.app ((x, y), z)) <| + (corepresentableIso₂' F G H).app (F ⊛ (G ⊛ H))|>.toEquiv.rightInverse_symm <| + (corepresentable₂ F G H|>.ofIso + (associatorCorepresentingIso F G H).symm|>.homEquiv (𝟙 _)) + dsimp [associator, Coyoneda.fullyFaithful, corepresentable₂, + corepresentable₂', Functor.CorepresentableBy.ofIso, corepresentable₂, + Functor.corepresentableByEquiv, associatorCorepresentingIso] at this ⊢ + simp only [Category.assoc, corepresentableIso₂'_hom_app_app] at this + simp only [Category.assoc, this] + simp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity] + +/-- Characterizing associator_inv with respect to the unit transformations -/ +@[reassoc (attr := simp)] +lemma associator_inv_unit_unit (x y z : C) : + F.obj x ◁ (unit G H).app (y, z) ≫ + (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ + (associator F G H).inv.app (x ⊗ y ⊗ z) = + (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫ (unit F G).app (x, y) ▷ H.obj z ≫ + (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ + ((F ⊛ G) ⊛ H).map (α_ x y z).hom := by + letI := congrArg (fun t ↦ t.app (x, y, z)) <| + (corepresentableIso₂ F G H).app ((F ⊛ G) ⊛ H)|>.toEquiv.rightInverse_symm <| + (corepresentable₂' F G H|>.ofIso + (associatorCorepresentingIso F G H)|>.homEquiv (𝟙 _)) + dsimp [associator, Coyoneda.fullyFaithful, corepresentable₂, + corepresentable₂', Functor.CorepresentableBy.ofIso, corepresentable₂, + Functor.corepresentableByEquiv, associatorCorepresentingIso] at this ⊢ + simp only [Category.assoc, corepresentableIso₂_hom_app_app] at this + simp only [Category.assoc, this] + simp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity] + +variable {F G H} in +theorem associator_naturality {F' G' H' : C ⥤ V} + [DayConvolution F' G'] [DayConvolution G' H'] + [DayConvolution F' (G' ⊛ H')] [DayConvolution (F' ⊛ G') H'] + (f : F ⟶ F') (g : G ⟶ G') (h : H ⟶ H') : + map (map f g) h ≫ + (associator F' G' H').hom = + (associator F G H).hom ≫ map f (map g h) := by + apply (corepresentableIso₂' F G H).app (F' ⊛ G' ⊛ H')|>.toEquiv.injective + dsimp + ext + simp only [externalProductBifunctor_obj_obj, whiskeringLeft_obj_obj, Functor.comp_obj, + Functor.prod_obj, tensor_obj, Functor.id_obj, corepresentableIso₂'_hom_app_app, + NatTrans.comp_app, map_unit_app_assoc] + rw [associator_hom_unit_unit_assoc] + simp only [tensorHom_def, Category.assoc, externalProductBifunctor_obj_obj, tensor_obj, + NatTrans.naturality, map_unit_app_assoc] + rw [← comp_whiskerRight_assoc, map_unit_app] + simp only [Functor.comp_obj, tensor_obj, comp_whiskerRight, Category.assoc] + rw [← whisker_exchange_assoc, associator_hom_unit_unit, whisker_exchange_assoc, + ← MonoidalCategory.whiskerLeft_comp_assoc, map_unit_app] + simp [tensorHom_def] + +section pentagon + +variable [∀ (v : V) (d : C × C), + Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)] + +lemma pentagon (H K : C ⥤ V) + [DayConvolution G H] [DayConvolution (F ⊛ G) H] [DayConvolution F (G ⊛ H)] + [DayConvolution H K] [DayConvolution G (H ⊛ K)] [DayConvolution (G ⊛ H) K] + [DayConvolution ((F ⊛ G) ⊛ H) K] [DayConvolution (F ⊛ G) (H ⊛ K)] + [DayConvolution (F ⊛ G ⊛ H) K] [DayConvolution F (G ⊛ H ⊛ K)] + [DayConvolution F ((G ⊛ H) ⊛ K)] : + map (associator F G H).hom (𝟙 K) ≫ + (associator F (G ⊛ H) K).hom ≫ map (𝟙 F) (associator G H K).hom = + (associator (F ⊛ G) H K).hom ≫ (associator F G (H ⊛ K)).hom := by + -- We repeatedly apply the fact that the functors are left Kan extended + apply Functor.hom_ext_of_isLeftKanExtension (α := unit ((F ⊛ G) ⊛ H) K) + apply Functor.hom_ext_of_isLeftKanExtension + (α := extensionUnitLeft ((F ⊛ G) ⊛ H) (unit (F ⊛ G) H) K) + letI : (((F ⊛ G) ⊠ H) ⊠ K).IsLeftKanExtension + (α := extensionUnitLeft ((F ⊛ G) ⊠ H) + (extensionUnitLeft _ (unit F G) H) K) := + pointwiseLeftKanExtensionLeft _ _ _ + (pointwiseLeftKanExtensionLeft _ _ _ (unitPointwiseKan F G))|>.isLeftKanExtension + apply Functor.hom_ext_of_isLeftKanExtension (α := extensionUnitLeft ((F ⊛ G) ⊠ H) + (extensionUnitLeft _ (unit F G) H) K) + -- And then we compute... + ext ⟨⟨⟨i, j⟩, k⟩, l⟩ + have aux : + ((unit F G).app (i, j) ⊗ (unit H K).app (k, l)) ≫ + (unit (F ⊛ G) (H ⊛ K)).app ((i ⊗ j), (k ⊗ l)) = + (α_ (F.obj i) (G.obj j) (H.obj k ⊗ K.obj l)).hom ≫ + F.obj i ◁ (G.obj j ◁ (unit H K).app (k, l)) ≫ F.obj i ◁ (unit G (H ⊛ K)).app (j, (k ⊗ l)) ≫ + (unit F (G ⊛ H ⊛ K)).app (i, (j ⊗ k ⊗ l)) ≫ (F ⊛ G ⊛ H ⊛ K).map (α_ i j (k ⊗ l)).inv ≫ + (associator F G (H ⊛ K)).inv.app ((i ⊗ j) ⊗ k ⊗ l) := by + conv_rhs => simp only [Functor.comp_obj, tensor_obj, NatTrans.naturality, + associator_inv_unit_unit_assoc, externalProductBifunctor_obj_obj, Iso.map_hom_inv_id, + Category.comp_id] + simp only [tensor_whiskerLeft_symm, Category.assoc, Iso.hom_inv_id_assoc, + ← tensorHom_def'_assoc] + dsimp + simp only [MonoidalCategory.whiskerLeft_id, Category.comp_id, map_unit_app_assoc, + externalProductBifunctor_obj_obj, NatTrans.id_app, tensorHom_id, associator_hom_unit_unit_assoc, + tensor_obj, NatTrans.naturality] + conv_rhs => + simp only [whiskerRight_tensor_symm_assoc, Iso.inv_hom_id_assoc, ← tensorHom_def_assoc] + rw [reassoc_of% aux] + simp only [Iso.inv_hom_id_app_assoc, ← comp_whiskerRight_assoc, associator_hom_unit_unit F G H] + simp only [Functor.comp_obj, tensor_obj, comp_whiskerRight, whisker_assoc, Category.assoc, + reassoc_of% unit_naturality_id_right (F ⊛ G ⊛ H) K l (α_ i j k).inv, NatTrans.naturality_assoc, + NatTrans.naturality, associator_hom_unit_unit_assoc, externalProductBifunctor_obj_obj, + tensor_obj, NatTrans.naturality_assoc, map_unit_app_assoc, NatTrans.id_app, + id_tensorHom, Iso.inv_hom_id_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, + associator_hom_unit_unit] + simp [← Functor.map_comp, reassoc_of% unit_naturality_id_left F (G ⊛ H ⊛ K) i (α_ j k l).inv, + pentagon_inv, pentagon_assoc] + +end pentagon + +end associator + +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`. -/ + canPointwiseLeftKanExtension : 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 (canPointwiseLeftKanExtension c).hom_ext + intro j + simpa using e j.hom + +end DayConvolutionUnit + +end + +end CategoryTheory.MonoidalCategory diff --git a/Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean new file mode 100644 index 00000000000000..b347293c9301b0 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean @@ -0,0 +1,98 @@ +/- +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.FunctorCategory +import Mathlib.CategoryTheory.Functor.Currying + +/-! +# External product of diagrams in a monoidal category + +In a monoidal category `C`, given a pair of diagrams `K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, we +introduce the external product `K₁ ⊠ K₂ : J₁ × J₂ ⥤ C` as the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. +The notation `- ⊠ -` is scoped to `MonoidalCategory.ExternalProduct`. +-/ + +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +namespace CategoryTheory.MonoidalCategory + +variable (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) + [Category.{v₁} J₁] [Category.{v₂} J₂] [Category.{v₃} C] [MonoidalCategory C] + +/-- The (uncurried version of the) external product bifunctor: Given diagrams +`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `j₁ ↦ j₂ ↦ K₁ j₁ ⊗ K₂ j₂`. -/ +@[simps!] +def externalProductBifunctorUncurried : (J₁ ⥤ C) ⥤ (J₂ ⥤ C) ⥤ J₁ ⥤ J₂ ⥤ C := + (Functor.postcompose₂.obj <| (evaluation _ _).obj <| curriedTensor C).obj <| whiskeringLeft₂ C + +/-- The external product bifunctor: Given diagrams +`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. -/ +@[simps!] +def externalProductBifunctor : ((J₁ ⥤ C) × (J₂ ⥤ C)) ⥤ J₁ × J₂ ⥤ C := + uncurry.obj <| (Functor.postcompose₂.obj <| uncurry).obj <| + externalProductBifunctorUncurried J₁ J₂ C + +variable {J₁ J₂ C} +/-- An abbreviation for the action of `externalProductBifunctor J₁ J₂ C` on objects. -/ +abbrev externalProduct (F₁ : J₁ ⥤ C) (F₂ : J₂ ⥤ C) := + externalProductBifunctor J₁ J₂ C|>.obj (F₁, F₂) + +namespace ExternalProduct +/-- Notation for `externalProduct`. +``` +open scoped CategoryTheory.MonoidalCategory.ExternalProduct +``` to bring this notation in scope. -/ +scoped infixr:80 " ⊠ " => externalProduct + +end ExternalProduct + +open scoped ExternalProduct + +variable (J₁ J₂ C) + +/-- When both diagrams have the same source category, composing the external product with +the diagonal gives the pointwise functor tensor product. +Note that `(externalProductCompDiagIso _ _).app (F₁, F₂) : Functor.diag J₁ ⋙ F₁ ⊠ F₂ ≅ F₁ ⊗ F₂` +type checks. -/ +@[simps!] +def externalProductCompDiagIso : + externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft _ _ _|>.obj <| Functor.diag J₁) ≅ + tensor (J₁ ⥤ C) := + NatIso.ofComponents + (fun _ ↦ NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp [tensorHom_def])) + (fun _ ↦ by ext; simp [tensorHom_def]) + +/-- When `C` is braided, there is an isomorphism `Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`, natural +in both `F₁` and `F₂`. +Note that `(externalProductSwap _ _ _).app (F₁, F₂) : Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁` +type checks. -/ +@[simps!] +def externalProductSwap [BraidedCategory C] : + externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft _ _ _|>.obj <| Prod.swap _ _) + ≅ Prod.swap _ _ ⋙ externalProductBifunctor J₂ J₁ C := + NatIso.ofComponents + (fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) (by simp [tensorHom_def, whisker_exchange])) + (fun _ ↦ by ext; simp [tensorHom_def, whisker_exchange]) + +/-- A version of `externalProductSwap` phrased in terms of the uncurried functors. -/ +@[simps!] +def externalProductFlip [BraidedCategory C] : + (Functor.postcompose₂.obj <| flipFunctor _ _ _).obj (externalProductBifunctorUncurried J₁ J₂ C) + ≅ (externalProductBifunctorUncurried J₂ J₁ C).flip := + NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents <| + fun _ ↦ NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) + +section Composition + +variable {J₁ J₂ C} {I₁ : Type u₃} {I₂ : Type u₄} [Category.{v₃} I₁] [Category.{v₄} I₂] + +/-- Composing F₁ × F₂ with (G₁ ⊠ G₂) is isomorphic to (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) -/ +@[simps!] +def prodCompExternalProduct (F₁ : I₁ ⥤ J₁) (G₁ : J₁ ⥤ C) (F₂ : I₂ ⥤ J₂) (G₂ : J₂ ⥤ C) : + F₁.prod F₂ ⋙ G₁ ⊠ G₂ ≅ (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) := NatIso.ofComponents (fun _ ↦ Iso.refl _) + +end Composition + +end CategoryTheory.MonoidalCategory diff --git a/Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean new file mode 100644 index 00000000000000..c79aec7d1aea79 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean @@ -0,0 +1,144 @@ +/- +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.Basic +import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise +import Mathlib.CategoryTheory.Limits.Final + +/-! +# Preservation of pointwise left Kan extensions by external products + +We prove that if a functor `H' : D' ⥤ V` is pointwise left Kan extended from +`H : D ⥤ V` along `L : D ⥤ D'`, and if `K : E ⥤ V` is any functor such that +for any `e : E`, the functor `tensorRight (K.obj e)` commutes with colimits of +shape `CostructuredArrow L d`, then the functor `H' ⊠ K` is pointwise left kan extended +from `H ⊠ K` along `L.prod (𝟭 E)`. + +We also prove a similar criterion to establish that `K ⊠ H'` is pointwise left Kan +extended from `K ⊠ H` along `(𝟭 E).prod L`. +-/ +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +namespace CategoryTheory.MonoidalCategory.ExternalProduct + +noncomputable section + +variable {V : Type u₁} [Category.{v₁} V] [MonoidalCategory V] + {D : Type u₂} {D' : Type u₃} {E : Type u₄} + [Category.{v₂} D] [Category.{v₃} D'] [Category.{v₄} E] + {H : D ⥤ V} {L : D ⥤ D'} (H' : D' ⥤ V) (α : H ⟶ L ⋙ H') (K : E ⥤ V) + +/-- Given an extension `α : H ⟶ L ⋙ H'`, this is the canonical extension +`H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K` it induces through bifunctoriality of the external product. -/ +abbrev extensionUnitLeft : H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K := + (externalProductBifunctor D E V).map ((α, K.leftUnitor.inv) : (H, K) ⟶ (L ⋙ H', 𝟭 E ⋙ K)) + +/-- Given an extension `α : H ⟶ L ⋙ H'`, this is the canonical extension +`K ⊠ H ⟶ (𝟭 E).prod L ⋙ K ⊠ H'` it induces through bifunctoriality of the external product. -/ +abbrev extensionUnitRight : K ⊠ H ⟶ (𝟭 E).prod L ⋙ K ⊠ H' := + (externalProductBifunctor E D V).map ((K.leftUnitor.inv, α) : (K, H) ⟶ (𝟭 E ⋙ K, L ⋙ H')) + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'` at `(d : D')`, +and if tensoring right with an object preserves colimis in `V` +then `H' ⊠ K : D' × E ⥤ V` is pointwise left Kan extended along `L × (𝟭 E)` at `(d, e)` +for every `e : E`. -/ +def pointwiseLeftKanExtensionAtLeft + (d : D') (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d) (e : E) + [Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight <| K.obj e)] : + Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)|>.IsPointwiseLeftKanExtensionAt + (d, e) := by + dsimp [Functor.LeftExtension.IsPointwiseLeftKanExtensionAt] + set cone := Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)|>.coconeAt (d, e) + let equiv := CostructuredArrow.prodEquivalence L (𝟭 E) d e|>.symm + apply Limits.IsColimit.ofWhiskerEquivalence equiv + let I : CostructuredArrow L d ⥤ (CostructuredArrow L d) × CostructuredArrow (𝟭 E) e := + -- this definition makes it easier to prove finality of I + (prod.rightUnitorEquivalence (CostructuredArrow L d)).inverse ⋙ + (𝟭 _).prod (Functor.fromPUnit.{0} <| .mk <| 𝟙 _) + letI : I.Final := by + letI : Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e)|>.Final := + Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e) + haveI := Functor.final_iff_final_comp + (F := (prod.rightUnitorEquivalence <| CostructuredArrow L d).inverse) + (G := (𝟭 _).prod <| Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e)) + dsimp [I] at this ⊢ + rw [← this] + infer_instance + apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone)|>.toFun + -- through all the equivalences above, the new cocone we consider is in fact + -- `(tensorRight (H.obj y)).mapCocone (dayConvolutionExtension G H).coconeAt y` + let diag_iso : + (CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e) ≅ + I ⋙ equiv.functor ⋙ CostructuredArrow.proj (L.prod <| 𝟭 E) (d, e) ⋙ H ⊠ K := + NatIso.ofComponents (fun _ ↦ Iso.refl _) + apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso + (d := Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone)) + (c := tensorRight (K.obj e)|>.mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d) + (Limits.Cocones.ext <| .refl _)|>.toFun + exact Limits.PreservesColimit.preserves (F := tensorRight <| K.obj e) P|>.some + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'`, +and if tensoring right with an object preserves colimis in `V` +then `H' ⊠ K : D' × E ⥤ V` is pointwise left Kan extended along `L × (𝟭 E)`. -/ +def pointwiseLeftKanExtensionLeft + [∀ d : D', ∀ e : E, + Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight <| K.obj e)] + (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtension) : + Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)|>.IsPointwiseLeftKanExtension := + fun ⟨d, e⟩ ↦ pointwiseLeftKanExtensionAtLeft H' α K d (P d) e + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'` at `d : D'` and +if tensoring left with an object preserves colimis in `V`, +then `K ⊠ H' : D' × E ⥤ V` is pointwise left Kan extended along `(𝟭 E) × L` at `(e, d)` for +every `e`. -/ +def pointwiseLeftKanExtensionAtRight + (d : D') (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d) (e : E) + [Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft <| K.obj e)] : + (Functor.LeftExtension.mk (K ⊠ H') + (extensionUnitRight H' α K)).IsPointwiseLeftKanExtensionAt (e, d) := by + dsimp [Functor.LeftExtension.IsPointwiseLeftKanExtensionAt] + set cone := Functor.LeftExtension.mk (K ⊠ H') + (extensionUnitRight H' α K)|>.coconeAt (e, d) + let equiv := CostructuredArrow.prodEquivalence (𝟭 E) L e d|>.symm + apply Limits.IsColimit.ofWhiskerEquivalence equiv + let I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d := + -- this definition makes it easier to prove finality of I + (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse ⋙ + (Functor.fromPUnit.{0} <| .mk <| 𝟙 _).prod (𝟭 _) + letI : I.Final := by + letI : Functor.fromPUnit.{0} (.mk (𝟙 e) : (CostructuredArrow (𝟭 E) e))|>.Final := + Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e) + haveI := Functor.final_iff_final_comp + (F := (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse) + (G := Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e)|>.prod <| 𝟭 _) + dsimp [I] at this ⊢ + rw [← this] + infer_instance + apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone)|>.toFun + -- through all the equivalences above, the new cocone we consider is in fact + -- `(tensorRight (H.obj y)).mapCocone (dayConvolutionExtension G H).coconeAt y` + let diag_iso : + (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e) ≅ + I ⋙ equiv.functor ⋙ CostructuredArrow.proj (𝟭 E|>.prod L) (e, d) ⋙ K ⊠ H := + NatIso.ofComponents (fun _ ↦ Iso.refl _) + apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso + (d := Limits.Cocone.whisker I <| Limits.Cocone.whisker equiv.functor cone) + (c := (tensorLeft <| K.obj e).mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d) + (Limits.Cocones.ext <| .refl _)|>.toFun + exact Limits.PreservesColimit.preserves (F := tensorLeft <| K.obj e) P|>.some + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'` and +if tensoring left with an object preserves colimis in `V`, +then `K ⊠ H' : D' × E ⥤ V` is pointwise left Kan extended along `(𝟭 E) × L`. -/ +def pointwiseLeftKanExtensionRight + [∀ d : D', ∀ e : E, + Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft <| K.obj e)] + (P : Functor.LeftExtension.mk H' α|>.IsPointwiseLeftKanExtension) : + Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)|>.IsPointwiseLeftKanExtension := + fun ⟨e, d⟩ ↦ pointwiseLeftKanExtensionAtRight H' α K d (P d) e + +end + +end CategoryTheory.MonoidalCategory.ExternalProduct From fa614a600f3d6e8f04974dfa04776d3395a171fa Mon Sep 17 00:00:00 2001 From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> Date: Sun, 18 May 2025 15:41:10 +0200 Subject: [PATCH 3/5] unitors --- Mathlib.lean | 3 + .../Functor/KanExtension/Basic.lean | 1 + .../Monoidal/DayConvolution.lean | 685 ++++++++++++++++++ .../Monoidal/ExternalProduct/Basic.lean | 98 +++ .../ExternalProduct/KanExtension.lean | 144 ++++ 5 files changed, 931 insertions(+) create mode 100644 Mathlib/CategoryTheory/Monoidal/DayConvolution.lean create mode 100644 Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean create mode 100644 Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean diff --git a/Mathlib.lean b/Mathlib.lean index 66d8089707617f..f98013716bd93a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2336,8 +2336,11 @@ 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.Basic +import Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension import Mathlib.CategoryTheory.Monoidal.Free.Basic import Mathlib.CategoryTheory.Monoidal.Free.Coherence import Mathlib.CategoryTheory.Monoidal.Functor diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean index 5666688ed76428..2c44f3a5834b78 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean +++ b/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 _ β diff --git a/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean new file mode 100644 index 00000000000000..c4c8a92af47913 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean @@ -0,0 +1,685 @@ +/- +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.KanExtension +import Mathlib.CategoryTheory.Products.Associator + +/-! +# Day convolution monoidal structure + +-/ + +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 to 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`. -/ + unitPointwiseKan (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) := + unitPointwiseKan 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 + +@[simp] +lemma uniqueUpToIso_hom_unit (h : DayConvolution F G) (h' : DayConvolution F G) : + h.unit ≫ CategoryTheory.whiskerLeft (tensor C) (h.uniqueUpToIso h').hom = h'.unit := by + simp [uniqueUpToIso] + +@[simp] +lemma uniqueUpToIso_inv_unit (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 unit_naturality_id_right (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 unit_naturality_id_left (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 map_unit_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 corepresentableIso : coyoneda.obj (.op <| F ⊛ G) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G) := + NatIso.ofComponents + (fun H ↦ Equiv.toIso <| Functor.homEquivOfIsLeftKanExtension _ (unit F G) _) + +/-- The universal property of left Kan extensions characterizes the functor +corepresented by `F ⊛ G`. -/ +def corepresentable : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G)|>.CorepresentableBy + (F ⊛ G) := + Functor.corepresentableByEquiv.symm <| corepresentableIso F G + +/-- 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 := + ((unitPointwiseKan F G) c).hom_ext (fun j ↦ by simpa using h j.hom) + + +section associator + +variable (H : C ⥤ V) + [DayConvolution G H] + [DayConvolution F (G ⊛ H)] + [DayConvolution (F ⊛ G) H] + [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (tensor C) d) (tensorLeft v)] + [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (tensor C) d) (tensorRight v)] + +open MonoidalCategory.ExternalProduct + +instance : (F ⊠ G ⊛ H).IsLeftKanExtension <| + extensionUnitRight (G ⊛ H) (unit G H) F := + (pointwiseLeftKanExtensionRight _ _ _ (unitPointwiseKan G H)).isLeftKanExtension + +instance : ((F ⊛ G) ⊠ H).IsLeftKanExtension <| + extensionUnitLeft (F ⊛ G) (unit F G) H := + (pointwiseLeftKanExtensionLeft _ _ _ (unitPointwiseKan F G)).isLeftKanExtension + +/-- An auxiliary equivalence used to build the associators, +characterizing morphism out of `F ⊛ G ⊛ H` via the universal property of Kan extensions. +-/ +@[simps!] +noncomputable def corepresentableIso₂ : + coyoneda.obj (.op <| F ⊛ G ⊛ H) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H) := + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ (G ⊛ H)) := + corepresentableIso F (G ⊛ H) + _ ≅ _ := NatIso.ofComponents + (fun _ ↦ Equiv.toIso <| Functor.homEquivOfIsLeftKanExtension _ + (extensionUnitRight (G ⊛ H) (unit G H) F) _) + +/-- An auxiliary equivalence used to build the associators, +characterizing morphism out of `F ⊛ G ⊛ H` via the universal property of Kan extensions. +-/ +@[simps!] +noncomputable def corepresentableIso₂' : + coyoneda.obj (.op <| (F ⊛ G) ⊛ H) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| (F ⊠ G) ⊠ H) := + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| (F ⊛ G) ⊠ H) := + corepresentableIso (F ⊛ G) H + _ ≅ _ := NatIso.ofComponents + (fun _ ↦ Equiv.toIso <| Functor.homEquivOfIsLeftKanExtension _ + (extensionUnitLeft (F ⊛ G) (unit F G) H) _) + +/-- The `CorepresentableBy` structure on `F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ -` +derived from `tensorCorepresentableIso₂`. -/ +def corepresentable₂ : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H)|>.CorepresentableBy (F ⊛ G ⊛ H) := + Functor.corepresentableByEquiv.symm (corepresentableIso₂ F G H) + +/-- The `CorepresentableBy` structure on `(F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ -` +derived from `tensorCorepresentableIso₂`. -/ +def corepresentable₂' : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| (F ⊠ G) ⊠ H)|>.CorepresentableBy ((F ⊛ G) ⊛ H) := + Functor.corepresentableByEquiv.symm (corepresentableIso₂' F G H) + +/-- The isomorphism of functors between +`((F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ -)` and +`(F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ -)` that copresents the associator isomorphism +for Day convolution. -/ +@[simps!] +def associatorCorepresentingIso : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| (F ⊠ G) ⊠ H) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H) := + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ + (whiskeringLeft _ _ _).obj (prod.associativity C C C).inverse ⋙ + coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) := + isoWhiskerLeft _ (isoWhiskerLeft _ + (NatIso.ofComponents fun _ ↦ Equiv.toIso <| + (prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv)) + _ ≅ (whiskeringLeft _ _ _).obj + ((prod.associativity C C C).inverse ⋙ (tensor C).prod (𝟭 C) ⋙ (tensor C)) ⋙ + coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) := + .refl _ + _ ≅ (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C) ⋙ (tensor C)) ⋙ + coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) := + isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents (fun _ ↦ α_ _ _ _)) _ + _ ≅ (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C) ⋙ (tensor C)) ⋙ + coyoneda.obj (.op <| F ⊠ G ⊠ H) := + isoWhiskerLeft _ <| + coyoneda.mapIso <| Iso.op <| NatIso.ofComponents (fun _ ↦ α_ _ _ _|>.symm) + +/-- The asociator morphism for Day convolution -/ +def associator : (F ⊛ G) ⊛ H ≅ F ⊛ G ⊛ H := + corepresentable₂' F G H|>.ofIso (associatorCorepresentingIso F G H)|>.uniqueUpToIso + <| corepresentable₂ F G H + +/-- Characterizing the forward direction of the associator isomorphism +with respect to the unit transformations. -/ +@[reassoc (attr := simp)] +lemma associator_hom_unit_unit (x y z : C) : + (unit F G).app (x, y) ▷ (H.obj z) ≫ + (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ + (associator F G H).hom.app ((x ⊗ y) ⊗ z) = + (α_ _ _ _).hom ≫ + (F.obj x ◁ (unit G H).app (y, z)) ≫ + (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ + (F ⊛ G ⊛ H).map (α_ _ _ _).inv := by + letI := congrArg (fun t ↦ t.app ((x, y), z)) <| + (corepresentableIso₂' F G H).app (F ⊛ (G ⊛ H))|>.toEquiv.rightInverse_symm <| + (corepresentable₂ F G H|>.ofIso + (associatorCorepresentingIso F G H).symm|>.homEquiv (𝟙 _)) + dsimp [associator, Coyoneda.fullyFaithful, corepresentable₂, + corepresentable₂', Functor.CorepresentableBy.ofIso, corepresentable₂, + Functor.corepresentableByEquiv, associatorCorepresentingIso] at this ⊢ + simp only [Category.assoc, corepresentableIso₂'_hom_app_app] at this + simp only [Category.assoc, this] + simp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity] + +/-- Characterizing associator_inv with respect to the unit transformations -/ +@[reassoc (attr := simp)] +lemma associator_inv_unit_unit (x y z : C) : + F.obj x ◁ (unit G H).app (y, z) ≫ + (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ + (associator F G H).inv.app (x ⊗ y ⊗ z) = + (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫ (unit F G).app (x, y) ▷ H.obj z ≫ + (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ + ((F ⊛ G) ⊛ H).map (α_ x y z).hom := by + letI := congrArg (fun t ↦ t.app (x, y, z)) <| + (corepresentableIso₂ F G H).app ((F ⊛ G) ⊛ H)|>.toEquiv.rightInverse_symm <| + (corepresentable₂' F G H|>.ofIso + (associatorCorepresentingIso F G H)|>.homEquiv (𝟙 _)) + dsimp [associator, Coyoneda.fullyFaithful, corepresentable₂, + corepresentable₂', Functor.CorepresentableBy.ofIso, corepresentable₂, + Functor.corepresentableByEquiv, associatorCorepresentingIso] at this ⊢ + simp only [Category.assoc, corepresentableIso₂_hom_app_app] at this + simp only [Category.assoc, this] + simp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity] + +variable {F G H} in +theorem associator_naturality {F' G' H' : C ⥤ V} + [DayConvolution F' G'] [DayConvolution G' H'] + [DayConvolution F' (G' ⊛ H')] [DayConvolution (F' ⊛ G') H'] + (f : F ⟶ F') (g : G ⟶ G') (h : H ⟶ H') : + map (map f g) h ≫ + (associator F' G' H').hom = + (associator F G H).hom ≫ map f (map g h) := by + apply (corepresentableIso₂' F G H).app (F' ⊛ G' ⊛ H')|>.toEquiv.injective + dsimp + ext + simp only [externalProductBifunctor_obj_obj, whiskeringLeft_obj_obj, Functor.comp_obj, + Functor.prod_obj, tensor_obj, Functor.id_obj, corepresentableIso₂'_hom_app_app, + NatTrans.comp_app, map_unit_app_assoc] + rw [associator_hom_unit_unit_assoc] + simp only [tensorHom_def, Category.assoc, externalProductBifunctor_obj_obj, tensor_obj, + NatTrans.naturality, map_unit_app_assoc] + rw [← comp_whiskerRight_assoc, map_unit_app] + simp only [Functor.comp_obj, tensor_obj, comp_whiskerRight, Category.assoc] + rw [← whisker_exchange_assoc, associator_hom_unit_unit, whisker_exchange_assoc, + ← MonoidalCategory.whiskerLeft_comp_assoc, map_unit_app] + simp [tensorHom_def] + +section pentagon + +variable [∀ (v : V) (d : C × C), + Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)] + +lemma pentagon (H K : C ⥤ V) + [DayConvolution G H] [DayConvolution (F ⊛ G) H] [DayConvolution F (G ⊛ H)] + [DayConvolution H K] [DayConvolution G (H ⊛ K)] [DayConvolution (G ⊛ H) K] + [DayConvolution ((F ⊛ G) ⊛ H) K] [DayConvolution (F ⊛ G) (H ⊛ K)] + [DayConvolution (F ⊛ G ⊛ H) K] [DayConvolution F (G ⊛ H ⊛ K)] + [DayConvolution F ((G ⊛ H) ⊛ K)] : + map (associator F G H).hom (𝟙 K) ≫ + (associator F (G ⊛ H) K).hom ≫ map (𝟙 F) (associator G H K).hom = + (associator (F ⊛ G) H K).hom ≫ (associator F G (H ⊛ K)).hom := by + -- We repeatedly apply the fact that the functors are left Kan extended + apply Functor.hom_ext_of_isLeftKanExtension (α := unit ((F ⊛ G) ⊛ H) K) + apply Functor.hom_ext_of_isLeftKanExtension + (α := extensionUnitLeft ((F ⊛ G) ⊛ H) (unit (F ⊛ G) H) K) + letI : (((F ⊛ G) ⊠ H) ⊠ K).IsLeftKanExtension + (α := extensionUnitLeft ((F ⊛ G) ⊠ H) + (extensionUnitLeft _ (unit F G) H) K) := + pointwiseLeftKanExtensionLeft _ _ _ + (pointwiseLeftKanExtensionLeft _ _ _ (unitPointwiseKan F G))|>.isLeftKanExtension + apply Functor.hom_ext_of_isLeftKanExtension (α := extensionUnitLeft ((F ⊛ G) ⊠ H) + (extensionUnitLeft _ (unit F G) H) K) + -- And then we compute... + ext ⟨⟨⟨i, j⟩, k⟩, l⟩ + have aux : + ((unit F G).app (i, j) ⊗ (unit H K).app (k, l)) ≫ + (unit (F ⊛ G) (H ⊛ K)).app ((i ⊗ j), (k ⊗ l)) = + (α_ (F.obj i) (G.obj j) (H.obj k ⊗ K.obj l)).hom ≫ + F.obj i ◁ (G.obj j ◁ (unit H K).app (k, l)) ≫ F.obj i ◁ (unit G (H ⊛ K)).app (j, (k ⊗ l)) ≫ + (unit F (G ⊛ H ⊛ K)).app (i, (j ⊗ k ⊗ l)) ≫ (F ⊛ G ⊛ H ⊛ K).map (α_ i j (k ⊗ l)).inv ≫ + (associator F G (H ⊛ K)).inv.app ((i ⊗ j) ⊗ k ⊗ l) := by + conv_rhs => simp only [Functor.comp_obj, tensor_obj, NatTrans.naturality, + associator_inv_unit_unit_assoc, externalProductBifunctor_obj_obj, Iso.map_hom_inv_id, + Category.comp_id] + simp only [tensor_whiskerLeft_symm, Category.assoc, Iso.hom_inv_id_assoc, + ← tensorHom_def'_assoc] + dsimp + simp only [MonoidalCategory.whiskerLeft_id, Category.comp_id, map_unit_app_assoc, + externalProductBifunctor_obj_obj, NatTrans.id_app, tensorHom_id, associator_hom_unit_unit_assoc, + tensor_obj, NatTrans.naturality] + conv_rhs => + simp only [whiskerRight_tensor_symm_assoc, Iso.inv_hom_id_assoc, ← tensorHom_def_assoc] + rw [reassoc_of% aux] + simp only [Iso.inv_hom_id_app_assoc, ← comp_whiskerRight_assoc, associator_hom_unit_unit F G H] + simp only [Functor.comp_obj, tensor_obj, comp_whiskerRight, whisker_assoc, Category.assoc, + reassoc_of% unit_naturality_id_right (F ⊛ G ⊛ H) K l (α_ i j k).inv, NatTrans.naturality_assoc, + NatTrans.naturality, associator_hom_unit_unit_assoc, externalProductBifunctor_obj_obj, + tensor_obj, NatTrans.naturality_assoc, map_unit_app_assoc, NatTrans.id_app, + id_tensorHom, Iso.inv_hom_id_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, + associator_hom_unit_unit] + simp [← Functor.map_comp, reassoc_of% unit_naturality_id_left F (G ⊛ H ⊛ K) i (α_ j k l).inv, + pentagon_inv, pentagon_assoc] + +end pentagon + +end associator + +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`. -/ + canPointwiseLeftKanExtension : 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 +open ExternalProduct + +/-- 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 (canPointwiseLeftKanExtension c).hom_ext + intro j + simpa using e j.hom + +variable (F : C ⥤ V) + [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)] + [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)] + -- [∀ v : V, Limits.PreservesColimitsOfSize.{0, v₁} (tensorRight v)] + +instance : (F ⊠ U).IsLeftKanExtension <| extensionUnitRight U (φ U) F := + pointwiseLeftKanExtensionRight U (φ U) F canPointwiseLeftKanExtension|>.isLeftKanExtension + +instance : (U ⊠ F).IsLeftKanExtension <| extensionUnitLeft U (φ U) F := + pointwiseLeftKanExtensionLeft U (φ U) F canPointwiseLeftKanExtension|>.isLeftKanExtension + +/-- An isomorphism that computes the functor corepresented by `U ⊛ F` using the +fact that `U ⊠ F` is left Kan extended from `(fromPUnit 𝟙_ V) ⊠ F`. -/ +@[simps!] +def corepresentableIsoLeft [DayConvolution U F] : + coyoneda.obj (.op <| U ⊛ F) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) := + NatIso.ofComponents + (fun H ↦ Equiv.toIso <| + calc + _ ≃ (U ⊠ F ⟶ (tensor C) ⋙ H) := + Functor.homEquivOfIsLeftKanExtension _ (DayConvolution.unit U F) _ + _ ≃ _ := + Functor.homEquivOfIsLeftKanExtension _ (extensionUnitLeft U (φ U) F) (tensor C ⋙ H)) + +/-- The `CorepresentableBy` structure attached to the isomorphism +`convolutionUnitCorepresentableIsoLeft`. -/ +def corepresentableLeft [DayConvolution U F] : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| Functor.fromPUnit.{0} (𝟙_ V) ⊠ F)|>.CorepresentableBy (U ⊛ F) := + Functor.corepresentableByEquiv.symm <| corepresentableIsoLeft U F + +/-- An isomorphism that computes the functor corepresented by `U ⊛ F` using the +fact that `F ⊠ U` is left Kan extended from `F ⊠ (fromPUnit 𝟙_ V)`. -/ +@[simps!] +def corepresentableIsoRight [DayConvolution F U] : + coyoneda.obj (.op <| F ⊛ U) ≅ + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙ + coyoneda.obj (.op <| F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) := + NatIso.ofComponents + (fun H ↦ Equiv.toIso <| + calc + _ ≃ (F ⊠ U ⟶ (tensor C) ⋙ H) := + Functor.homEquivOfIsLeftKanExtension _ (DayConvolution.unit F U) _ + _ ≃ _ := + Functor.homEquivOfIsLeftKanExtension _ (extensionUnitRight U (φ U) F) (tensor C ⋙ H)) + +/-- The `CorepresentableBy` structure attached to the isomorphism +`convolutionUnitCorepresentableIsoRight`. -/ +def corepresentableRight [DayConvolution F U] : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙ + coyoneda.obj (.op <| F ⊠ Functor.fromPUnit.{0} (𝟙_ V))|>.CorepresentableBy (F ⊛ U) := + Functor.corepresentableByEquiv.symm <| corepresentableIsoRight U F + +/-- The isomorphism of corepresentable functors that defines the left unitor for +Day convolution. -/ +@[simps!] +def leftUnitorCorepresentingIso : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙ + coyoneda.obj (.op <| Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) ≅ + coyoneda.obj (.op <| F) := by + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙ + (whiskeringLeft _ _ _).obj (prod.leftUnitorEquivalence C).inverse ⋙ + coyoneda.obj (.op <| + (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) := + isoWhiskerLeft _ (isoWhiskerLeft _ + (NatIso.ofComponents fun _ ↦ Equiv.toIso <| + (prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv)) + _ ≅ (whiskeringLeft _ _ _).obj + ((prod.leftUnitorEquivalence C).inverse ⋙ (Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C) ⋙ + tensor C) ⋙ + coyoneda.obj (.op <| + (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) := + .refl _ + _ ≅ (whiskeringLeft _ _ _).obj (𝟭 _) ⋙ coyoneda.obj (.op <| + (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) := + isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents fun _ ↦ λ_ _) _ + _ ≅ _ := coyoneda.mapIso <| Iso.op <| NatIso.ofComponents fun _ ↦ (λ_ _).symm + +/-- The isomorphism of corepresentable functors that defines the right unitor for +Day convolution. -/ +@[simps!] +def rightUnitorCorepresentingIso : + (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙ + coyoneda.obj (.op <| F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) ≅ + coyoneda.obj (.op <| F) := by + calc + _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙ + (whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙ + (whiskeringLeft _ _ _).obj (prod.rightUnitorEquivalence C).inverse ⋙ + coyoneda.obj (.op <| + (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) := + isoWhiskerLeft _ (isoWhiskerLeft _ + (NatIso.ofComponents fun _ ↦ Equiv.toIso <| + (prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv)) + _ ≅ (whiskeringLeft _ _ _).obj + ((prod.rightUnitorEquivalence C).inverse ⋙ + ((𝟭 C).prod (Functor.fromPUnit.{u₁} (𝟙_ C))) ⋙ tensor C) ⋙ + coyoneda.obj (.op <| + (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) := + .refl _ + _ ≅ (whiskeringLeft _ _ _).obj (𝟭 _) ⋙ coyoneda.obj (.op <| + (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) := + isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents fun _ ↦ ρ_ _) _ + _ ≅ _ := coyoneda.mapIso <| Iso.op <| NatIso.ofComponents fun _ ↦ (ρ_ _).symm + +/-- The left unitor isomorphism for Day convolution. -/ +def leftUnitor [DayConvolution U F] : U ⊛ F ≅ F := + corepresentableLeft U F|>.ofIso (leftUnitorCorepresentingIso F)|>.uniqueUpToIso + <| Functor.corepresentableByEquiv.symm (.refl _) + +/-- The right unitor isomorphism for Day convolution. -/ +def rightUnitor [DayConvolution F U] : F ⊛ U ≅ F := + corepresentableRight U F|>.ofIso (rightUnitorCorepresentingIso F)|>.uniqueUpToIso + <| Functor.corepresentableByEquiv.symm (.refl _) + +section + +omit [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)] +variable [DayConvolution U F] + +/-- Characterizing the forward direction of `leftUnitor` via the universal maps. -/ +@[reassoc (attr := simp)] +lemma leftUnitor_hom_unit_app (y : C) : + can ▷ F.obj y ≫ (DayConvolution.unit U F).app (𝟙_ C, y) ≫ + (leftUnitor U F).hom.app (𝟙_ C ⊗ y) = + (λ_ (F.obj y)).hom ≫ F.map ((λ_ y).inv) := by + letI := congrArg (fun t ↦ t.app (.mk PUnit.unit, y)) <| + (corepresentableIsoLeft U F).app F|>.toEquiv.rightInverse_symm <| + ((leftUnitorCorepresentingIso F).symm.hom.app (F)) (𝟙 _) + dsimp [leftUnitor, Coyoneda.fullyFaithful, corepresentableLeft, corepresentableIsoLeft, + leftUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso, + Functor.corepresentableByEquiv] at this ⊢ + simp only [whiskerLeft_id, Category.comp_id] at this + simp only [Category.comp_id, this] + simp [prod.leftUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor, + Functor.FullyFaithful.homEquiv] + +@[simp, reassoc] +lemma leftUnitor_inv_app (x : C) : + (leftUnitor U F).inv.app x = + (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ + (U ⊛ F).map (λ_ x).hom := by + dsimp [leftUnitor, Coyoneda.fullyFaithful, corepresentableLeft, corepresentableIsoLeft, + leftUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso, + Functor.corepresentableByEquiv] + simp [prod.leftUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor, + Functor.FullyFaithful.homEquiv] + +variable {F} in +@[reassoc (attr := simp)] +lemma leftUnitor_naturality {G : C ⥤ V} [DayConvolution U G] (f : F ⟶ G) : + DayConvolution.map (𝟙 _) f ≫ (leftUnitor U G).hom = + (leftUnitor U F).hom ≫ f := by + apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _ + apply Functor.hom_ext_of_isLeftKanExtension _ (extensionUnitLeft U (φ U) F) _ + ext ⟨x₁, x₂⟩ + simp [← whisker_exchange_assoc] + +end + +section + +omit [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)] +variable [DayConvolution F U] + +/-- Characterizing the forward direction of `leftUnitor` via the universal maps. -/ +@[reassoc (attr := simp)] +lemma rightUnitor_hom_unit_app (x : C) : + F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ + (rightUnitor U F).hom.app (x ⊗ 𝟙_ C) = + (ρ_ _).hom ≫ F.map ((ρ_ x).inv) := by + letI := congrArg (fun t ↦ t.app (x, .mk PUnit.unit)) <| + (corepresentableIsoRight U F).app F|>.toEquiv.rightInverse_symm <| + ((rightUnitorCorepresentingIso F).symm.hom.app (F)) (𝟙 _) + dsimp [rightUnitor, Coyoneda.fullyFaithful, corepresentableRight, corepresentableIsoRight, + rightUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso, + Functor.corepresentableByEquiv] at this ⊢ + simp only [MonoidalCategory.whiskerRight_id, Category.id_comp, Iso.hom_inv_id, + Category.comp_id] at this + simp only [Category.comp_id, this] + simp [prod.rightUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor, + Functor.FullyFaithful.homEquiv] + +@[simp, reassoc] +lemma rightUnitor_inv_app (x : C) : + (rightUnitor U F).inv.app x = + (ρ_ (F.obj x)).inv ≫ F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ + (F ⊛ U).map (ρ_ x).hom := by + dsimp [rightUnitor, Coyoneda.fullyFaithful, corepresentableRight, corepresentableIsoRight, + rightUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso, + Functor.corepresentableByEquiv] + simp [prod.rightUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor, + Functor.FullyFaithful.homEquiv] + +variable {F} in +@[reassoc (attr := simp)] +lemma rightUnitor_naturality {G : C ⥤ V} [DayConvolution G U] (f : F ⟶ G) : + DayConvolution.map f (𝟙 _) ≫ (rightUnitor U G).hom = + (rightUnitor U F).hom ≫ f := by + apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _ + apply Functor.hom_ext_of_isLeftKanExtension _ (extensionUnitRight U (φ U) F) _ + ext ⟨x₁, x₂⟩ + simp [whisker_exchange_assoc] + +end + +end DayConvolutionUnit + +section triangle + +open scoped DayConvolution +open DayConvolutionUnit +open ExternalProduct + +variable [∀ (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 <| 𝟙_ C) d) (tensorLeft v)] + [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape + (CostructuredArrow (Functor.fromPUnit <| 𝟙_ C) d) (tensorRight v)] + [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape + (CostructuredArrow ((𝟭 C).prod <| Functor.fromPUnit.{0} <| 𝟙_ C) d) (tensorRight v)] + +lemma DayConvolution.triangle (F G U : C ⥤ V) [DayConvolutionUnit U] + [DayConvolution F U] [DayConvolution U G] + [DayConvolution F (U ⊛ G)] [DayConvolution (F ⊛ U) G] [DayConvolution F G] : + (DayConvolution.associator F U G).hom ≫ + DayConvolution.map (𝟙 F) (DayConvolutionUnit.leftUnitor U G).hom = + DayConvolution.map (DayConvolutionUnit.rightUnitor U F).hom (𝟙 G) := by + apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _ + apply Functor.hom_ext_of_isLeftKanExtension + (α := extensionUnitLeft (F ⊛ U) (DayConvolution.unit F U) G) + letI : (F ⊠ U) ⊠ G|>.IsLeftKanExtension + (α := extensionUnitLeft (F ⊠ U) (extensionUnitRight U (DayConvolutionUnit.φ U) F) G) := + pointwiseLeftKanExtensionLeft (F ⊠ U) _ G + (pointwiseLeftKanExtensionRight U (DayConvolutionUnit.φ U) F <| + DayConvolutionUnit.canPointwiseLeftKanExtension (F := U))|>.isLeftKanExtension + apply Functor.hom_ext_of_isLeftKanExtension + (α := extensionUnitLeft (F ⊠ U) (extensionUnitRight U (DayConvolutionUnit.φ U) F) G) + ext ⟨⟨x, _⟩, y⟩ + dsimp + simp only [MonoidalCategory.whiskerRight_id, Category.id_comp, Iso.hom_inv_id, whisker_assoc, + MonoidalCategory.whiskerLeft_id, Category.comp_id, + DayConvolution.associator_hom_unit_unit_assoc, externalProductBifunctor_obj_obj, tensor_obj, + NatTrans.naturality, DayConvolution.map_unit_app_assoc, NatTrans.id_app, id_tensorHom, + Category.assoc, Iso.inv_hom_id_assoc, DayConvolution.map_unit_app, Functor.comp_obj, + tensorHom_id, Iso.cancel_iso_hom_left] + simp only [← MonoidalCategory.whiskerLeft_comp_assoc, leftUnitor_hom_unit_app, + associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, rightUnitor_hom_unit_app] + simp [← Functor.map_comp] + +end triangle + +end + +end CategoryTheory.MonoidalCategory diff --git a/Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean new file mode 100644 index 00000000000000..b347293c9301b0 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean @@ -0,0 +1,98 @@ +/- +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.FunctorCategory +import Mathlib.CategoryTheory.Functor.Currying + +/-! +# External product of diagrams in a monoidal category + +In a monoidal category `C`, given a pair of diagrams `K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, we +introduce the external product `K₁ ⊠ K₂ : J₁ × J₂ ⥤ C` as the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. +The notation `- ⊠ -` is scoped to `MonoidalCategory.ExternalProduct`. +-/ + +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +namespace CategoryTheory.MonoidalCategory + +variable (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) + [Category.{v₁} J₁] [Category.{v₂} J₂] [Category.{v₃} C] [MonoidalCategory C] + +/-- The (uncurried version of the) external product bifunctor: Given diagrams +`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `j₁ ↦ j₂ ↦ K₁ j₁ ⊗ K₂ j₂`. -/ +@[simps!] +def externalProductBifunctorUncurried : (J₁ ⥤ C) ⥤ (J₂ ⥤ C) ⥤ J₁ ⥤ J₂ ⥤ C := + (Functor.postcompose₂.obj <| (evaluation _ _).obj <| curriedTensor C).obj <| whiskeringLeft₂ C + +/-- The external product bifunctor: Given diagrams +`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. -/ +@[simps!] +def externalProductBifunctor : ((J₁ ⥤ C) × (J₂ ⥤ C)) ⥤ J₁ × J₂ ⥤ C := + uncurry.obj <| (Functor.postcompose₂.obj <| uncurry).obj <| + externalProductBifunctorUncurried J₁ J₂ C + +variable {J₁ J₂ C} +/-- An abbreviation for the action of `externalProductBifunctor J₁ J₂ C` on objects. -/ +abbrev externalProduct (F₁ : J₁ ⥤ C) (F₂ : J₂ ⥤ C) := + externalProductBifunctor J₁ J₂ C|>.obj (F₁, F₂) + +namespace ExternalProduct +/-- Notation for `externalProduct`. +``` +open scoped CategoryTheory.MonoidalCategory.ExternalProduct +``` to bring this notation in scope. -/ +scoped infixr:80 " ⊠ " => externalProduct + +end ExternalProduct + +open scoped ExternalProduct + +variable (J₁ J₂ C) + +/-- When both diagrams have the same source category, composing the external product with +the diagonal gives the pointwise functor tensor product. +Note that `(externalProductCompDiagIso _ _).app (F₁, F₂) : Functor.diag J₁ ⋙ F₁ ⊠ F₂ ≅ F₁ ⊗ F₂` +type checks. -/ +@[simps!] +def externalProductCompDiagIso : + externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft _ _ _|>.obj <| Functor.diag J₁) ≅ + tensor (J₁ ⥤ C) := + NatIso.ofComponents + (fun _ ↦ NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp [tensorHom_def])) + (fun _ ↦ by ext; simp [tensorHom_def]) + +/-- When `C` is braided, there is an isomorphism `Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`, natural +in both `F₁` and `F₂`. +Note that `(externalProductSwap _ _ _).app (F₁, F₂) : Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁` +type checks. -/ +@[simps!] +def externalProductSwap [BraidedCategory C] : + externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft _ _ _|>.obj <| Prod.swap _ _) + ≅ Prod.swap _ _ ⋙ externalProductBifunctor J₂ J₁ C := + NatIso.ofComponents + (fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) (by simp [tensorHom_def, whisker_exchange])) + (fun _ ↦ by ext; simp [tensorHom_def, whisker_exchange]) + +/-- A version of `externalProductSwap` phrased in terms of the uncurried functors. -/ +@[simps!] +def externalProductFlip [BraidedCategory C] : + (Functor.postcompose₂.obj <| flipFunctor _ _ _).obj (externalProductBifunctorUncurried J₁ J₂ C) + ≅ (externalProductBifunctorUncurried J₂ J₁ C).flip := + NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents <| + fun _ ↦ NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) + +section Composition + +variable {J₁ J₂ C} {I₁ : Type u₃} {I₂ : Type u₄} [Category.{v₃} I₁] [Category.{v₄} I₂] + +/-- Composing F₁ × F₂ with (G₁ ⊠ G₂) is isomorphic to (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) -/ +@[simps!] +def prodCompExternalProduct (F₁ : I₁ ⥤ J₁) (G₁ : J₁ ⥤ C) (F₂ : I₂ ⥤ J₂) (G₂ : J₂ ⥤ C) : + F₁.prod F₂ ⋙ G₁ ⊠ G₂ ≅ (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) := NatIso.ofComponents (fun _ ↦ Iso.refl _) + +end Composition + +end CategoryTheory.MonoidalCategory diff --git a/Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean new file mode 100644 index 00000000000000..c79aec7d1aea79 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean @@ -0,0 +1,144 @@ +/- +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.Basic +import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise +import Mathlib.CategoryTheory.Limits.Final + +/-! +# Preservation of pointwise left Kan extensions by external products + +We prove that if a functor `H' : D' ⥤ V` is pointwise left Kan extended from +`H : D ⥤ V` along `L : D ⥤ D'`, and if `K : E ⥤ V` is any functor such that +for any `e : E`, the functor `tensorRight (K.obj e)` commutes with colimits of +shape `CostructuredArrow L d`, then the functor `H' ⊠ K` is pointwise left kan extended +from `H ⊠ K` along `L.prod (𝟭 E)`. + +We also prove a similar criterion to establish that `K ⊠ H'` is pointwise left Kan +extended from `K ⊠ H` along `(𝟭 E).prod L`. +-/ +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +namespace CategoryTheory.MonoidalCategory.ExternalProduct + +noncomputable section + +variable {V : Type u₁} [Category.{v₁} V] [MonoidalCategory V] + {D : Type u₂} {D' : Type u₃} {E : Type u₄} + [Category.{v₂} D] [Category.{v₃} D'] [Category.{v₄} E] + {H : D ⥤ V} {L : D ⥤ D'} (H' : D' ⥤ V) (α : H ⟶ L ⋙ H') (K : E ⥤ V) + +/-- Given an extension `α : H ⟶ L ⋙ H'`, this is the canonical extension +`H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K` it induces through bifunctoriality of the external product. -/ +abbrev extensionUnitLeft : H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K := + (externalProductBifunctor D E V).map ((α, K.leftUnitor.inv) : (H, K) ⟶ (L ⋙ H', 𝟭 E ⋙ K)) + +/-- Given an extension `α : H ⟶ L ⋙ H'`, this is the canonical extension +`K ⊠ H ⟶ (𝟭 E).prod L ⋙ K ⊠ H'` it induces through bifunctoriality of the external product. -/ +abbrev extensionUnitRight : K ⊠ H ⟶ (𝟭 E).prod L ⋙ K ⊠ H' := + (externalProductBifunctor E D V).map ((K.leftUnitor.inv, α) : (K, H) ⟶ (𝟭 E ⋙ K, L ⋙ H')) + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'` at `(d : D')`, +and if tensoring right with an object preserves colimis in `V` +then `H' ⊠ K : D' × E ⥤ V` is pointwise left Kan extended along `L × (𝟭 E)` at `(d, e)` +for every `e : E`. -/ +def pointwiseLeftKanExtensionAtLeft + (d : D') (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d) (e : E) + [Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight <| K.obj e)] : + Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)|>.IsPointwiseLeftKanExtensionAt + (d, e) := by + dsimp [Functor.LeftExtension.IsPointwiseLeftKanExtensionAt] + set cone := Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)|>.coconeAt (d, e) + let equiv := CostructuredArrow.prodEquivalence L (𝟭 E) d e|>.symm + apply Limits.IsColimit.ofWhiskerEquivalence equiv + let I : CostructuredArrow L d ⥤ (CostructuredArrow L d) × CostructuredArrow (𝟭 E) e := + -- this definition makes it easier to prove finality of I + (prod.rightUnitorEquivalence (CostructuredArrow L d)).inverse ⋙ + (𝟭 _).prod (Functor.fromPUnit.{0} <| .mk <| 𝟙 _) + letI : I.Final := by + letI : Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e)|>.Final := + Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e) + haveI := Functor.final_iff_final_comp + (F := (prod.rightUnitorEquivalence <| CostructuredArrow L d).inverse) + (G := (𝟭 _).prod <| Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e)) + dsimp [I] at this ⊢ + rw [← this] + infer_instance + apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone)|>.toFun + -- through all the equivalences above, the new cocone we consider is in fact + -- `(tensorRight (H.obj y)).mapCocone (dayConvolutionExtension G H).coconeAt y` + let diag_iso : + (CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e) ≅ + I ⋙ equiv.functor ⋙ CostructuredArrow.proj (L.prod <| 𝟭 E) (d, e) ⋙ H ⊠ K := + NatIso.ofComponents (fun _ ↦ Iso.refl _) + apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso + (d := Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone)) + (c := tensorRight (K.obj e)|>.mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d) + (Limits.Cocones.ext <| .refl _)|>.toFun + exact Limits.PreservesColimit.preserves (F := tensorRight <| K.obj e) P|>.some + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'`, +and if tensoring right with an object preserves colimis in `V` +then `H' ⊠ K : D' × E ⥤ V` is pointwise left Kan extended along `L × (𝟭 E)`. -/ +def pointwiseLeftKanExtensionLeft + [∀ d : D', ∀ e : E, + Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight <| K.obj e)] + (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtension) : + Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)|>.IsPointwiseLeftKanExtension := + fun ⟨d, e⟩ ↦ pointwiseLeftKanExtensionAtLeft H' α K d (P d) e + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'` at `d : D'` and +if tensoring left with an object preserves colimis in `V`, +then `K ⊠ H' : D' × E ⥤ V` is pointwise left Kan extended along `(𝟭 E) × L` at `(e, d)` for +every `e`. -/ +def pointwiseLeftKanExtensionAtRight + (d : D') (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d) (e : E) + [Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft <| K.obj e)] : + (Functor.LeftExtension.mk (K ⊠ H') + (extensionUnitRight H' α K)).IsPointwiseLeftKanExtensionAt (e, d) := by + dsimp [Functor.LeftExtension.IsPointwiseLeftKanExtensionAt] + set cone := Functor.LeftExtension.mk (K ⊠ H') + (extensionUnitRight H' α K)|>.coconeAt (e, d) + let equiv := CostructuredArrow.prodEquivalence (𝟭 E) L e d|>.symm + apply Limits.IsColimit.ofWhiskerEquivalence equiv + let I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d := + -- this definition makes it easier to prove finality of I + (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse ⋙ + (Functor.fromPUnit.{0} <| .mk <| 𝟙 _).prod (𝟭 _) + letI : I.Final := by + letI : Functor.fromPUnit.{0} (.mk (𝟙 e) : (CostructuredArrow (𝟭 E) e))|>.Final := + Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e) + haveI := Functor.final_iff_final_comp + (F := (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse) + (G := Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e)|>.prod <| 𝟭 _) + dsimp [I] at this ⊢ + rw [← this] + infer_instance + apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone)|>.toFun + -- through all the equivalences above, the new cocone we consider is in fact + -- `(tensorRight (H.obj y)).mapCocone (dayConvolutionExtension G H).coconeAt y` + let diag_iso : + (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e) ≅ + I ⋙ equiv.functor ⋙ CostructuredArrow.proj (𝟭 E|>.prod L) (e, d) ⋙ K ⊠ H := + NatIso.ofComponents (fun _ ↦ Iso.refl _) + apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso + (d := Limits.Cocone.whisker I <| Limits.Cocone.whisker equiv.functor cone) + (c := (tensorLeft <| K.obj e).mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d) + (Limits.Cocones.ext <| .refl _)|>.toFun + exact Limits.PreservesColimit.preserves (F := tensorLeft <| K.obj e) P|>.some + +/-- If `H' : D' ⥤ V` is pointwise left Kan extended along `L : D ⥤ D'` and +if tensoring left with an object preserves colimis in `V`, +then `K ⊠ H' : D' × E ⥤ V` is pointwise left Kan extended along `(𝟭 E) × L`. -/ +def pointwiseLeftKanExtensionRight + [∀ d : D', ∀ e : E, + Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft <| K.obj e)] + (P : Functor.LeftExtension.mk H' α|>.IsPointwiseLeftKanExtension) : + Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)|>.IsPointwiseLeftKanExtension := + fun ⟨e, d⟩ ↦ pointwiseLeftKanExtensionAtRight H' α K d (P d) e + +end + +end CategoryTheory.MonoidalCategory.ExternalProduct From 2d76940e32c8e99014ae8b79bfe73e5444019982 Mon Sep 17 00:00:00 2001 From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> Date: Sun, 18 May 2025 16:10:46 +0200 Subject: [PATCH 4/5] docstring --- .../Monoidal/DayConvolution.lean | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean index ea9576f0ddbf55..a1b392b3dd252f 100644 --- a/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean +++ b/Mathlib/CategoryTheory/Monoidal/DayConvolution.lean @@ -9,6 +9,29 @@ 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₅ From 8e7521490c7ff4c5bde5033346c36545409e183d Mon Sep 17 00:00:00 2001 From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> Date: Sun, 18 May 2025 16:22:18 +0200 Subject: [PATCH 5/5] stray file --- .../Monoidal/ExternalProduct.lean | 98 ------------------- 1 file changed, 98 deletions(-) delete mode 100644 Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean diff --git a/Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean b/Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean deleted file mode 100644 index b347293c9301b0..00000000000000 --- a/Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean +++ /dev/null @@ -1,98 +0,0 @@ -/- -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.FunctorCategory -import Mathlib.CategoryTheory.Functor.Currying - -/-! -# External product of diagrams in a monoidal category - -In a monoidal category `C`, given a pair of diagrams `K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, we -introduce the external product `K₁ ⊠ K₂ : J₁ × J₂ ⥤ C` as the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. -The notation `- ⊠ -` is scoped to `MonoidalCategory.ExternalProduct`. --/ - -universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ - -namespace CategoryTheory.MonoidalCategory - -variable (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) - [Category.{v₁} J₁] [Category.{v₂} J₂] [Category.{v₃} C] [MonoidalCategory C] - -/-- The (uncurried version of the) external product bifunctor: Given diagrams -`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `j₁ ↦ j₂ ↦ K₁ j₁ ⊗ K₂ j₂`. -/ -@[simps!] -def externalProductBifunctorUncurried : (J₁ ⥤ C) ⥤ (J₂ ⥤ C) ⥤ J₁ ⥤ J₂ ⥤ C := - (Functor.postcompose₂.obj <| (evaluation _ _).obj <| curriedTensor C).obj <| whiskeringLeft₂ C - -/-- The external product bifunctor: Given diagrams -`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. -/ -@[simps!] -def externalProductBifunctor : ((J₁ ⥤ C) × (J₂ ⥤ C)) ⥤ J₁ × J₂ ⥤ C := - uncurry.obj <| (Functor.postcompose₂.obj <| uncurry).obj <| - externalProductBifunctorUncurried J₁ J₂ C - -variable {J₁ J₂ C} -/-- An abbreviation for the action of `externalProductBifunctor J₁ J₂ C` on objects. -/ -abbrev externalProduct (F₁ : J₁ ⥤ C) (F₂ : J₂ ⥤ C) := - externalProductBifunctor J₁ J₂ C|>.obj (F₁, F₂) - -namespace ExternalProduct -/-- Notation for `externalProduct`. -``` -open scoped CategoryTheory.MonoidalCategory.ExternalProduct -``` to bring this notation in scope. -/ -scoped infixr:80 " ⊠ " => externalProduct - -end ExternalProduct - -open scoped ExternalProduct - -variable (J₁ J₂ C) - -/-- When both diagrams have the same source category, composing the external product with -the diagonal gives the pointwise functor tensor product. -Note that `(externalProductCompDiagIso _ _).app (F₁, F₂) : Functor.diag J₁ ⋙ F₁ ⊠ F₂ ≅ F₁ ⊗ F₂` -type checks. -/ -@[simps!] -def externalProductCompDiagIso : - externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft _ _ _|>.obj <| Functor.diag J₁) ≅ - tensor (J₁ ⥤ C) := - NatIso.ofComponents - (fun _ ↦ NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp [tensorHom_def])) - (fun _ ↦ by ext; simp [tensorHom_def]) - -/-- When `C` is braided, there is an isomorphism `Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`, natural -in both `F₁` and `F₂`. -Note that `(externalProductSwap _ _ _).app (F₁, F₂) : Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁` -type checks. -/ -@[simps!] -def externalProductSwap [BraidedCategory C] : - externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft _ _ _|>.obj <| Prod.swap _ _) - ≅ Prod.swap _ _ ⋙ externalProductBifunctor J₂ J₁ C := - NatIso.ofComponents - (fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) (by simp [tensorHom_def, whisker_exchange])) - (fun _ ↦ by ext; simp [tensorHom_def, whisker_exchange]) - -/-- A version of `externalProductSwap` phrased in terms of the uncurried functors. -/ -@[simps!] -def externalProductFlip [BraidedCategory C] : - (Functor.postcompose₂.obj <| flipFunctor _ _ _).obj (externalProductBifunctorUncurried J₁ J₂ C) - ≅ (externalProductBifunctorUncurried J₂ J₁ C).flip := - NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents <| - fun _ ↦ NatIso.ofComponents <| fun _ ↦ NatIso.ofComponents (fun _ ↦ β_ _ _) - -section Composition - -variable {J₁ J₂ C} {I₁ : Type u₃} {I₂ : Type u₄} [Category.{v₃} I₁] [Category.{v₄} I₂] - -/-- Composing F₁ × F₂ with (G₁ ⊠ G₂) is isomorphic to (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) -/ -@[simps!] -def prodCompExternalProduct (F₁ : I₁ ⥤ J₁) (G₁ : J₁ ⥤ C) (F₂ : I₂ ⥤ J₂) (G₂ : J₂ ⥤ C) : - F₁.prod F₂ ⋙ G₁ ⊠ G₂ ≅ (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) := NatIso.ofComponents (fun _ ↦ Iso.refl _) - -end Composition - -end CategoryTheory.MonoidalCategory