Documentation

Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

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

Instances For

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.

Equations

F.denseAtEquiv Y = Equiv.refl (F.DenseAt Y)

Instances For

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') :

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

Instances For

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) :

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.

Instances For

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.

Equations

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

Instances For

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.

Equations

hY.precompOfFinal G = (CategoryTheory.Functor.DenseAt.precompEquivOfFinal G).symm hY

Instances For

@[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.

Equations

@CategoryTheory.Functor.DenseAt.precompEquivalence = @CategoryTheory.Functor.DenseAt.precompOfFinal

Instances For

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.

Equations

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

Instances For

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)

Instances For

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