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

In the file Mathlib/CategoryTheory/Functor/KanExtension/DenseAtYoneda, we obtain the density of the Yoneda embedding. In Mathlib/CategoryTheory/Functor/KanExtension/DenseIff, we obtain a characterization of the density for a full functor F : C ⥤ D in terms of the full faithfulness of the restricted Yoneda functor D ⥤ Cᵒᵖ ⥤ Type _. In Mathlib/CategoryTheory/Functor/KanExtension/StrongGenerator, we show that the range of a dense functor is a strong generator.

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.instIsLeftKanExtensionIdInvRightUnitorOfIsDense {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] :
      (Functor.id D).IsLeftKanExtension F.rightUnitor.inv
      source
      instance CategoryTheory.Functor.instHasPointwiseLeftKanExtensionOfIsDense {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] :
      F.HasPointwiseLeftKanExtension F
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      noncomputable def CategoryTheory.Functor.IsDense.leftKanExtensionIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] :
      F.leftKanExtension F ≅ Functor.id D

      If F is dense, the left Kan extension of F along F is isomorphic to the identity.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] :
        CategoryStruct.comp (F.leftKanExtensionUnit F) (F.whiskerLeft (leftKanExtensionIso F).hom) = F.rightUnitor.inv
        source
        @[simp]
        theorem CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] {Z : Functor C D} (h : F.comp (Functor.id D) ⟶ Z) :
        CategoryStruct.comp (F.leftKanExtensionUnit F) (CategoryStruct.comp (F.whiskerLeft (leftKanExtensionIso F).hom) h) = CategoryStruct.comp F.rightUnitor.inv h
        source
        @[simp]
        theorem CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] (X : C) :
        CategoryStruct.comp ((F.leftKanExtensionUnit F).app X) ((leftKanExtensionIso F).hom.app (F.obj X)) = F.rightUnitor.inv.app X
        source
        @[simp]
        theorem CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_app_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [F.IsDense] (X : C) {Z : D} (h : F.obj X ⟶ Z) :
        CategoryStruct.comp ((F.leftKanExtensionUnit F).app X) (CategoryStruct.comp ((leftKanExtensionIso F).hom.app (F.obj X)) h) = CategoryStruct.comp (F.rightUnitor.inv.app X) h