Dense functors

A functor F : C ⥤ D is dense (F.IsDense) if 𝟭 D is a pointwise left Kan extension of F along itself, i.e. any Y : D is the colimit of all F.obj X for all morphisms F.obj X ⟶ Y (which is the condition F.DenseAt Y). When F is full, we show that this is equivalent to saying that the restricted Yoneda functor D ⥤ Cᵒᵖ ⥤ Type _ is fully faithful (see the lemma Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda).

We also show that the range of a dense functor is a strong generator (see Functor.isStrongGenerator_of_isDense).

References

• https://ncatlab.org/nlab/show/dense+subcategory

class CategoryTheory.Functor.IsDense {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) : Prop

A functor F : C ⥤ D is dense if any Y : D is a canonical colimit relatively to F.

• isDenseAt (Y : D) : F.isDenseAt Y

noncomputable def CategoryTheory.Functor.denseAt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] (Y : D) : F.DenseAt Y

This is a choice of structure F.DenseAt Y when F : C ⥤ D is dense, and Y : D.

Equations

• F.denseAt Y = Nonempty.some ⋯

theorem CategoryTheory.Functor.isDense_iff_nonempty_isPointwiseLeftKanExtension {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) : F.IsDense ↔ Nonempty (LeftExtension.mk (Functor.id D) F.rightUnitor.inv).IsPointwiseLeftKanExtension

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

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

instance CategoryTheory.Functor.instIsDenseCompOfIsEquivalence {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] (F : Functor C D) (G : Functor C' C) [F.IsDense] [G.IsEquivalence] : (G.comp F).IsDense

theorem CategoryTheory.Functor.IsDense.comp_left_iff_of_isEquivalence {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] (F : Functor C D) (G : Functor C' C) [G.IsEquivalence] : (G.comp F).IsDense ↔ F.IsDense

instance CategoryTheory.Functor.instIsDenseCompOfIsEquivalence_1 {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] (F : Functor C D) (G : Functor D C') [F.IsDense] [G.IsEquivalence] : (F.comp G).IsDense

theorem CategoryTheory.Functor.IsDense.comp_right_iff_of_isEquivalence {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] (F : Functor C D) (G : Functor D C') [G.IsEquivalence] : (F.comp G).IsDense ↔ F.IsDense

instance CategoryTheory.Functor.instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] : (Presheaf.restrictedULiftYoneda F).Faithful

instance CategoryTheory.Functor.instFullOppositeTypeRestrictedULiftYonedaOfIsDense {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] : (Presheaf.restrictedULiftYoneda F).Full

theorem CategoryTheory.Functor.IsDense.of_fullyFaithful_restrictedULiftYoneda {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} [F.Full] (h : (Presheaf.restrictedULiftYoneda F).FullyFaithful) : F.IsDense

theorem CategoryTheory.Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] : F.IsDense ↔ Nonempty (Presheaf.restrictedULiftYoneda F).FullyFaithful

theorem CategoryTheory.Functor.isStrongGenerator_of_isDense {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] : (ObjectProperty.ofObj F.obj).IsStrongGenerator