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)
:
A functor F : C ⥤ D is dense if any Y : D is a canonical colimit
relatively to F.
- isDenseAt (Y : D) : F.isDenseAt Y
Instances
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 ⋯
Instances For
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)
:
instance
CategoryTheory.Functor.instIsLeftKanExtensionIdInvRightUnitorOfIsDense
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsDense]
:
instance
CategoryTheory.Functor.instHasPointwiseLeftKanExtensionOfIsDense
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsDense]
:
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)
:
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]
:
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]
:
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]
:
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]
:
instance
CategoryTheory.Functor.instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsDense]
:
instance
CategoryTheory.Functor.instFullOppositeTypeRestrictedULiftYonedaOfIsDense
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsDense]
:
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]
:
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]
:
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]
:
If F is dense, the left Kan extension of F along F is isomorphic to the identity.
Equations
Instances For
@[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
@[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)
:
@[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
@[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
yoneda is dense: Every X : Cᵒᵖ ⥤ Type v₁ is the colimit over
CostructuredArrow.proj yoneda X ⋙ yoneda.
Instances For
def
CategoryTheory.denseAtUliftYoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Functor Cᵒᵖ (Type (max w v₁)))
:
uliftYoneda is dense: Every X : Cᵒᵖ ⥤ Type max w v₁ is the colimit over
CostructuredArrow.proj uliftYoneda X ⋙ uliftYoneda.