Documentation

Mathlib.CategoryTheory.Functor.KanExtension.Dense

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 #

source
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.

Instances
    source
    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
    Instances For
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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