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.

Equations

• F.DenseAt Y = (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D) F.rightUnitor.inv).IsPointwiseLeftKanExtensionAt Y

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.

Equations

• hY.ofIso e = (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D) F.rightUnitor.inv).isPointwiseLeftKanExtensionAtOfIso' hY e

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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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.{u_2, u_1} C'] (G : Functor C' C) [G.IsEquivalence] : (G.comp F).DenseAt Y

If F : C ⥤ D is dense at Y : D, then so is G ⋙ F if G is an equivalence.

Equations

• hY.precompEquivalence G = CategoryTheory.Limits.IsColimit.whiskerEquivalence hY (CategoryTheory.CostructuredArrow.pre G F Y).asEquivalence

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.{u_2, 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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• F.isDenseAt Y = Nonempty (F.DenseAt 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

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