[Merged by Bors] - feat(CategoryTheory): functors that are dense at an object

Mathlib.lean

@@ -2292,6 +2292,7 @@ import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
 import Mathlib.CategoryTheory.Functor.KanExtension.Basic
+import Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
 import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
 import Mathlib.CategoryTheory.Functor.KanExtension.Preserves
 import Mathlib.CategoryTheory.Functor.OfSequence

Mathlib/CategoryTheory/Functor/KanExtension/DenseAt.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
+
+/-!
+# Canonical colimits, or functors that are dense at an object
+
+Given a functor `F : C ⥤ D` and `Y : D`, we say that `F` is dense at `Y` (`F.DenseAt Y`),
+if `Y` identifies to the colimit of all `F.obj X` for `X : C`
+and `f : F.obj X ⟶ Y`, i.e. `Y` identifies to the colimit of
+the obvious functor `CostructuredArrow F Y ⥤ D`. In some references,
+it is also said that `Y` is a canonical colimit relatively to `F`.
+While `F.DenseAt Y` contains data, we also introduce the
+corresponding property `isDenseAt F` of objects of `D`.
+
+## TODO
+
+* formalize dense subcategories
+* show the presheaves of types are canonical colimits relatively
+to the Yoneda embedding
+
+## References
+* https://ncatlab.org/nlab/show/dense+functor
+
+-/
+
+universe v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+open Limits
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
+  (F : C ⥤ D)
+
+namespace Functor
+
+/-- A functor `F : C ⥤ D` is dense at `Y : D` if the obvious natural transformation
+`F ⟶ F ⋙ 𝟭 D` makes `𝟭 D` a pointwise left Kan extension of `F` along itself at `Y`,
+i.e. `Y` identifies to the colimit of the obvious functor `CostructuredArrow F Y ⥤ D`. -/
+abbrev DenseAt (Y : D) : Type max u₁ u₂ v₂ :=
+  (Functor.LeftExtension.mk (𝟭 D) F.rightUnitor.inv).IsPointwiseLeftKanExtensionAt Y
+
+variable {F} {Y : D} (hY : F.DenseAt Y)
+
+/-- If `F : C ⥤ D` is dense at `Y : D`, then it is also at `Y'`
+if `Y` and `Y'` are isomorphic. -/
+def DenseAt.ofIso {Y' : D} (e : Y ≅ Y') : F.DenseAt Y' :=
+  LeftExtension.isPointwiseLeftKanExtensionAtOfIso' _ hY e
+
+/-- If `F : C ⥤ D` is dense at `Y : D`, and `G` is a functor that is isomorphic to `F`,
+then `G` is also dense at `Y`. -/
+def DenseAt.ofNatIso {G : C ⥤ D} (e : F ≅ G) : G.DenseAt Y :=
+  (IsColimit.equivOfNatIsoOfIso
+    ((Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerLeft _ e) _ _
+    (by exact Cocones.ext (Iso.refl _))).1
+    (hY.whiskerEquivalence (CostructuredArrow.mapNatIso e.symm))
+
+/-- If `F : C ⥤ D` is dense at `Y : D`, then so is `G ⋙ F` if `G` is an equivalence. -/
+noncomputable def DenseAt.precompEquivalence
+    {C' : Type*} [Category C'] (G : C' ⥤ C) [G.IsEquivalence] :
+    (G ⋙ F).DenseAt Y :=
+  hY.whiskerEquivalence (CostructuredArrow.pre G F Y).asEquivalence
+
+/-- If `F : C ⥤ D` is dense at `Y : D` and `G : D ⥤ D'` is an equivalence,
+then `F ⋙ G` is dense at `G.obj Y`. -/
+noncomputable def DenseAt.postcompEquivalence
+    {D' : Type*} [Category D'] (G : D ⥤ D') [G.IsEquivalence] :
+    (F ⋙ G).DenseAt (G.obj Y) :=
+  IsColimit.ofWhiskerEquivalence (CostructuredArrow.post F G Y).asEquivalence
+    (IsColimit.ofIsoColimit ((isColimitOfPreserves G hY)) (Cocones.ext (Iso.refl _)))
+
+variable (F) in
+/-- Given a functor `F : C ⥤ D`, this is the property of objects `Y : D` such
+that `F` is dense at `Y`. -/
+def isDenseAt : ObjectProperty D :=
+  fun Y ↦ Nonempty (F.DenseAt Y)
+
+lemma isDenseAt_eq_isPointwiseLeftKanExtensionAt :
+    F.isDenseAt =
+      (Functor.LeftExtension.mk (𝟭 D) F.rightUnitor.inv).isPointwiseLeftKanExtensionAt :=
+  rfl
+
+instance : F.isDenseAt.IsClosedUnderIsomorphisms := by
+  rw [isDenseAt_eq_isPointwiseLeftKanExtensionAt]
+  infer_instance
+
+lemma congr_isDenseAt {G : C ⥤ D} (e : F ≅ G) :
+    F.isDenseAt = G.isDenseAt := by
+  ext X
+  exact ⟨fun ⟨h⟩ ↦ ⟨h.ofNatIso e⟩, fun ⟨h⟩ ↦ ⟨h.ofNatIso e.symm⟩⟩
+
+end Functor
+
+end CategoryTheory

Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

@@ -226,6 +226,12 @@ namespace IsPointwiseLeftKanExtensionAt
 
 variable {E} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y)
 
+include h in
+lemma hom_ext' {T : H} {f g : E.right.obj Y ⟶ T}
+    (hfg : ∀ ⦃X : C⦄ (φ : L.obj X ⟶ Y),
+      E.hom.app X ≫ E.right.map φ ≫ f = E.hom.app X ≫ E.right.map φ ≫ g) : f = g :=
+  h.hom_ext (fun j ↦ by simpa using hfg j.hom)
+
 @[reassoc]
 lemma comp_homEquiv_symm {Z : H}
     (φ : CostructuredArrow.proj L Y ⋙ F ⟶ (Functor.const _).obj Z)
@@ -254,6 +260,14 @@ lemma ι_isoColimit_hom (g : CostructuredArrow L Y) :
 
 end IsPointwiseLeftKanExtensionAt
 
+/-- Given `E : Functor.LeftExtension L F`, this is the property of objects where
+`E` is a pointwise left Kan extension. -/
+def isPointwiseLeftKanExtensionAt : ObjectProperty D :=
+  fun Y ↦ Nonempty (E.IsPointwiseLeftKanExtensionAt Y)
+
+instance : E.isPointwiseLeftKanExtensionAt.IsClosedUnderIsomorphisms where
+  of_iso e h := ⟨E.isPointwiseLeftKanExtensionAtOfIso' h.some e⟩
+
 /-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension when
 it is a pointwise left Kan extension at any object. -/
 abbrev IsPointwiseLeftKanExtension := ∀ (Y : D), E.IsPointwiseLeftKanExtensionAt Y
@@ -391,7 +405,14 @@ def isPointwiseRightKanExtensionAtEquivOfIso' {Y Y' : D} (e : Y ≅ Y') :
 namespace IsPointwiseRightKanExtensionAt
 
 variable {E} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y)
-  [HasLimit (StructuredArrow.proj Y L ⋙ F)]
+
+include h in
+lemma hom_ext' {T : H} {f g : T ⟶ E.left.obj Y}
+    (hfg : ∀ ⦃X : C⦄ (φ : Y ⟶ L.obj X),
+      f ≫ E.left.map φ ≫ E.hom.app X = g ≫ E.left.map φ ≫ E.hom.app X) : f = g :=
+  h.hom_ext (fun j ↦ hfg j.hom)
+
+variable [HasLimit (StructuredArrow.proj Y L ⋙ F)]
 
 /-- A pointwise right Kan extension of `F` along `L` applied to an object `Y` is isomorphic to
 `limit (StructuredArrow.proj Y L ⋙ F)`. -/
@@ -412,6 +433,14 @@ lemma isoLimit_inv_π (g : StructuredArrow Y L) :
 
 end IsPointwiseRightKanExtensionAt
 
+/-- Given `E : Functor.RightExtension L F`, this is the property of objects where
+`E` is a pointwise right Kan extension. -/
+def isPointwiseRightKanExtensionAt : ObjectProperty D :=
+  fun Y ↦ Nonempty (E.IsPointwiseRightKanExtensionAt Y)
+
+instance : E.isPointwiseRightKanExtensionAt.IsClosedUnderIsomorphisms where
+  of_iso e h := ⟨E.isPointwiseRightKanExtensionAtOfIso' h.some e⟩
+
 /-- A right extension `E : RightExtension L F` is a pointwise right Kan extension when
 it is a pointwise right Kan extension at any object. -/
 abbrev IsPointwiseRightKanExtension := ∀ (Y : D), E.IsPointwiseRightKanExtensionAt Y