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

@[reducible, inline]

abbrev CategoryTheory.Functor.DenseAt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (Y : D) : Type (max u₁ u₂ v₂)

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.

def CategoryTheory.Functor.denseAtEquiv {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (Y : D) : F.DenseAt Y ≃ Limits.IsColimit ((LeftExtension.mk (Functor.id D) F.rightUnitor.inv).coconeAt Y)

F is dense at Y if Y identifies to the colimit of the obvious functor CostructuredArrow F Y ⥤ D.

def CategoryTheory.Functor.DenseAt.ofIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} (hY : F.DenseAt Y) {Y' : D} (e : Y ≅ Y') : 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 CategoryTheory.Functor.DenseAt.ofNatIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} (hY : F.DenseAt Y) {G : Functor C D} (e : F ≅ G) : G.DenseAt Y

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.

noncomputable def CategoryTheory.Functor.DenseAt.precompEquivOfFinal {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} {C' : Type u_1} [Category.{v_1, u_1} C'] (G : Functor C' C) [(CostructuredArrow.pre G F Y).Final] : (G.comp F).DenseAt Y ≃ F.DenseAt Y

If the canonical functor CostructuredArrow (G ≫ F) Y ⥤ CostructuredArrow F Y is final, then G ⋙ F is dense at Y if and only if F is dense at Y.

noncomputable def CategoryTheory.Functor.DenseAt.precompOfFinal {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} (hY : F.DenseAt Y) {C' : Type u_1} [Category.{v_1, u_1} C'] (G : Functor C' C) [(CostructuredArrow.pre G F Y).Final] : (G.comp F).DenseAt Y

If F : C ⥤ D is dense at Y : D, then so is G ⋙ F if the canonical functor CostructuredArrow (G ≫ F) Y ⥤ CostructuredArrow F Y is final. This holds in particular if G is an equivalence.

@[deprecated CategoryTheory.Functor.DenseAt.precompOfFinal (since := "2025-12-17")]

def CategoryTheory.Functor.DenseAt.precompEquivalence {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} (hY : F.DenseAt Y) {C' : Type u_1} [Category.{v_1, u_1} C'] (G : Functor C' C) [(CostructuredArrow.pre G F Y).Final] : (G.comp F).DenseAt Y

Alias of CategoryTheory.Functor.DenseAt.precompOfFinal.

---

If F : C ⥤ D is dense at Y : D, then so is G ⋙ F if the canonical functor CostructuredArrow (G ≫ F) Y ⥤ CostructuredArrow F Y is final. This holds in particular if G is an equivalence.

noncomputable def CategoryTheory.Functor.DenseAt.postcompEquivalence {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} (hY : F.DenseAt Y) {D' : Type u_1} [Category.{v_1, u_1} D'] (G : Functor D D') [G.IsEquivalence] : (F.comp G).DenseAt (G.obj Y)

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.

def CategoryTheory.Functor.isDenseAt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) : ObjectProperty D

Given a functor F : C ⥤ D, this is the property of objects Y : D such that F is dense at Y.

theorem CategoryTheory.Functor.isDenseAt_eq_isPointwiseLeftKanExtensionAt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} : F.isDenseAt = (LeftExtension.mk (Functor.id D) F.rightUnitor.inv).isPointwiseLeftKanExtensionAt

theorem CategoryTheory.Functor.isDenseAt_iff {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {X : D} : F.isDenseAt X ↔ Nonempty (Limits.IsColimit ((LeftExtension.mk (Functor.id D) F.rightUnitor.inv).coconeAt X))

instance CategoryTheory.Functor.instIsClosedUnderIsomorphismsIsDenseAt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} : F.isDenseAt.IsClosedUnderIsomorphisms

theorem CategoryTheory.Functor.congr_isDenseAt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) : F.isDenseAt = G.isDenseAt

theorem CategoryTheory.Functor.IsDenseAt.iff_of_final {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} {C' : Type u_1} [Category.{v_1, u_1} C'] (G : Functor C' C) [(CostructuredArrow.pre G F Y).Final] : (G.comp F).isDenseAt Y ↔ F.isDenseAt Y

theorem CategoryTheory.Functor.IsDenseAt.of_final {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {Y : D} {C' : Type u_1} [Category.{v_1, u_1} C'] (G : Functor C' C) [(CostructuredArrow.pre G F Y).Final] (hY : F.isDenseAt Y) : (G.comp F).isDenseAt Y