Colimit of representables #
This file constructs an adjunction Presheaf.yonedaAdjunction between (Cᵒᵖ ⥤ Type u) and
ℰ given a functor A : C ⥤ ℰ, where the right adjoint restrictedYoneda
sends (E : ℰ) to c ↦ (A.obj c ⟶ E), and the left adjoint (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
is a pointwise left Kan extension of A along the Yoneda embedding, which
exists provided ℰ has colimits)
We also show that every presheaf is a colimit of representables. This result is also known as the density theorem, the co-Yoneda lemma and the Ninja Yoneda lemma. Two formulations are given:
colimitOfRepresentableuses the category of elements of a functor to types;isColimitTautologicalCoconeuses the category of costructured arrows.
In the lemma isLeftKanExtension_along_yoneda_iff, we show that
if L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ) and α : A ⟶ yoneda ⋙ L, then
α makes L the left Kan extension of L along yoneda if and only if
α is an isomorphism (i.e. L extends A) and L preserves colimits.
uniqueExtensionAlongYoneda shows yoneda.leftKanExtension A is unique amongst
functors preserving colimits with this property, establishing the
presheaf category as the free cocompletion of a category.
Given a functor F : C ⥤ D, we also show construct an
isomorphism compYonedaIsoYonedaCompLan : F ⋙ yoneda ≅ yoneda ⋙ F.op.lan, and
show that it makes F.op.lan a left Kan extension of F ⋙ yoneda.
Tags #
colimit, representable, presheaf, free cocompletion
References #
- [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
- https://ncatlab.org/nlab/show/Yoneda+extension
def
CategoryTheory.Presheaf.restrictedYoneda
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
:
The functor taking (E : ℰ) (c : Cᵒᵖ) to the homset (A.obj C ⟶ E). It is shown in L_adjunction
that this functor has a left adjoint (provided E has colimits) given by taking colimits over
categories of elements.
In the case where ℰ = Cᵒᵖ ⥤ Type u and A = yoneda, this functor is isomorphic to the identity.
Defined as in [MM92], Chapter I, Section 5, Theorem 2.
Equations
- CategoryTheory.Presheaf.restrictedYoneda A = CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ ℰᵒᵖ (Type ?u.44)).obj A.op)
@[simp]
theorem
CategoryTheory.Presheaf.restrictedYoneda_obj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
(X : ℰ)
{X✝ Y✝ : Cᵒᵖ}
(f : X✝ ⟶ Y✝)
(a✝ : (CategoryTheory.yoneda.obj X).obj (A.op.obj X✝))
:
((CategoryTheory.Presheaf.restrictedYoneda A).obj X).map f a✝ = CategoryTheory.CategoryStruct.comp (A.map f.unop) a✝
@[simp]
theorem
CategoryTheory.Presheaf.restrictedYoneda_obj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
(X : ℰ)
(X✝ : Cᵒᵖ)
:
((CategoryTheory.Presheaf.restrictedYoneda A).obj X).obj X✝ = (A.obj (Opposite.unop X✝) ⟶ X)
@[simp]
theorem
CategoryTheory.Presheaf.restrictedYoneda_map_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
{X✝ Y✝ : ℰ}
(f : X✝ ⟶ Y✝)
(X : Cᵒᵖ)
(a✝ : (CategoryTheory.yoneda.obj X✝).obj (A.op.obj X))
:
((CategoryTheory.Presheaf.restrictedYoneda A).map f).app X a✝ = CategoryTheory.CategoryStruct.comp a✝ f
def
CategoryTheory.Presheaf.restrictedYonedaHomEquiv'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
(E : ℰ)
:
((CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda P).comp A ⟶ (CategoryTheory.Functor.const (CategoryTheory.CostructuredArrow CategoryTheory.yoneda P)).obj E) ≃ (P ⟶ (CategoryTheory.Presheaf.restrictedYoneda A).obj E)
Auxiliary definition for restrictedYonedaHomEquiv.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Presheaf.restrictedYonedaHomEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(α : A ⟶ CategoryTheory.yoneda.comp L)
[L.IsLeftKanExtension α]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
(E : ℰ)
:
(L.obj P ⟶ E) ≃ (P ⟶ (CategoryTheory.Presheaf.restrictedYoneda A).obj E)
Auxiliary definition for yonedaAdjunction.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Presheaf.yonedaAdjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(α : A ⟶ CategoryTheory.yoneda.comp L)
[L.IsLeftKanExtension α]
:
If L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ is a pointwise left Kan extension
of a functor A : C ⥤ ℰ along the Yoneda embedding,
then L is a left adjoint of restrictedYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type v₁
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(α : A ⟶ CategoryTheory.yoneda.comp L)
[L.IsLeftKanExtension α]
:
Any left Kan extension along the Yoneda embedding preserves colimits.
theorem
CategoryTheory.Presheaf.isIso_of_isLeftKanExtension
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(α : A ⟶ CategoryTheory.yoneda.comp L)
[L.IsLeftKanExtension α]
:
noncomputable instance
CategoryTheory.Presheaf.preservesColimitsOfSize_leftKanExtension
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
:
CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, max v₁ u₁, v₁, max (v₁ + 1) u₁, u₂}
(CategoryTheory.yoneda.leftKanExtension A)
See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.instIsIsoFunctorLeftKanExtensionUnitOppositeTypeYoneda
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
:
CategoryTheory.IsIso (CategoryTheory.yoneda.leftKanExtensionUnit A)
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Presheaf.isExtensionAlongYoneda
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ)
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
:
CategoryTheory.yoneda.comp (CategoryTheory.yoneda.leftKanExtension A) ≅ A
A pointwise left Kan extension along the Yoneda embedding is an extension.
Equations
- CategoryTheory.Presheaf.isExtensionAlongYoneda A = (CategoryTheory.asIso (CategoryTheory.yoneda.leftKanExtensionUnit A)).symm
@[reducible]
def
CategoryTheory.Presheaf.functorToRepresentables
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
CategoryTheory.Functor P.Elementsᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type v₁))
A functor to the presheaf category in which everything in the image is representable (witnessed
by the fact that it factors through the yoneda embedding).
coconeOfRepresentable gives a cocone for this functor which is a colimit and has point P.
Equations
- CategoryTheory.Presheaf.functorToRepresentables P = (CategoryTheory.CategoryOfElements.π P).leftOp.comp CategoryTheory.yoneda
noncomputable def
CategoryTheory.Presheaf.coconeOfRepresentable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
This is a cocone with point P for the functor functorToRepresentables P. It is shown in
colimitOfRepresentable P that this cocone is a colimit: that is, we have exhibited an arbitrary
presheaf P as a colimit of representables.
The construction of [MM92], Chapter I, Section 5, Corollary 3.
Equations
- CategoryTheory.Presheaf.coconeOfRepresentable P = { pt := P, ι := { app := fun (x : P.Elementsᵒᵖ) => CategoryTheory.yonedaEquiv.symm (Opposite.unop x).snd, naturality := ⋯ } }
@[simp]
theorem
CategoryTheory.Presheaf.coconeOfRepresentable_ι_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
(x : P.Elementsᵒᵖ)
:
(CategoryTheory.Presheaf.coconeOfRepresentable P).ι.app x = CategoryTheory.yonedaEquiv.symm (Opposite.unop x).snd
@[simp]
theorem
CategoryTheory.Presheaf.coconeOfRepresentable_pt
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
theorem
CategoryTheory.Presheaf.coconeOfRepresentable_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P₁ P₂ : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(α : P₁ ⟶ P₂)
(j : P₁.Elementsᵒᵖ)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.coconeOfRepresentable P₁).ι.app j) α = (CategoryTheory.Presheaf.coconeOfRepresentable P₂).ι.app ((CategoryTheory.CategoryOfElements.map α).op.obj j)
The legs of the cocone coconeOfRepresentable are natural in the choice of presheaf.
noncomputable def
CategoryTheory.Presheaf.colimitOfRepresentable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
The cocone with point P given by coconeOfRepresentable is a colimit:
that is, we have exhibited an arbitrary presheaf P as a colimit of representables.
The result of [MM92], Chapter I, Section 5, Corollary 3.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Presheaf.instIsIsoFunctorOfIsLeftKanExtensionOppositeType
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(α : A ⟶ CategoryTheory.yoneda.comp L)
[L.IsLeftKanExtension α]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Presheaf.isLeftKanExtension_along_yoneda_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(α : A ⟶ CategoryTheory.yoneda.comp L)
:
L.IsLeftKanExtension α ↔ CategoryTheory.IsIso α ∧ CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
theorem
CategoryTheory.Presheaf.isLeftKanExtension_of_preservesColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(e : A ≅ CategoryTheory.yoneda.comp L)
[CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L]
:
L.IsLeftKanExtension e.hom
noncomputable def
CategoryTheory.Presheaf.uniqueExtensionAlongYoneda
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
{A : CategoryTheory.Functor C ℰ}
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension A]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
(e : A ≅ CategoryTheory.yoneda.comp L)
[CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L]
:
L ≅ CategoryTheory.yoneda.leftKanExtension A
Show that yoneda.leftKanExtension A is the unique colimit-preserving
functor which extends A to the presheaf category.
The second part of [MM92], Chapter I, Section 5, Corollary 4. See Property 3 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.
Equations
- CategoryTheory.Presheaf.uniqueExtensionAlongYoneda L e = L.leftKanExtensionUnique e.hom (CategoryTheory.yoneda.leftKanExtension A) (CategoryTheory.yoneda.leftKanExtensionUnit A)
instance
CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeIdCompYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ)
[CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L]
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension (CategoryTheory.yoneda.comp L)]
:
L.IsLeftKanExtension (CategoryTheory.CategoryStruct.id (CategoryTheory.yoneda.comp L))
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Presheaf.isLeftAdjoint_of_preservesColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ℰ : Type u₂}
[CategoryTheory.Category.{v₁, u₂} ℰ]
(L : CategoryTheory.Functor (CategoryTheory.Functor C (Type v₁)) ℰ)
[CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L]
[CategoryTheory.yoneda.HasPointwiseLeftKanExtension
(CategoryTheory.yoneda.comp ((CategoryTheory.opOpEquivalence C).congrLeft.functor.comp L))]
:
L.IsLeftAdjoint
If L preserves colimits and ℰ has them, then it is a left adjoint. Note this is a (partial)
converse to leftAdjointPreservesColimits.
instance
CategoryTheory.Presheaf.instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
(F : CategoryTheory.Functor C D)
(X : C)
(Y : F.op.LeftExtension (CategoryTheory.yoneda.obj X))
:
Unique
(CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.yoneda.obj (F.obj X)) (CategoryTheory.yonedaMap F X) ⟶ Y)
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
(F : CategoryTheory.Functor C D)
(X : C)
:
(CategoryTheory.yoneda.obj (F.obj X)).IsLeftKanExtension (CategoryTheory.yonedaMap F X)
Given F : C ⥤ D and X : C, yoneda.obj (F.obj X) : Dᵒᵖ ⥤ Type _ is the
left Kan extension of yoneda.obj X : Cᵒᵖ ⥤ Type _ along F.op.
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
(F : CategoryTheory.Functor C D)
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
:
F.comp CategoryTheory.yoneda ≅ CategoryTheory.yoneda.comp F.op.lan
F ⋙ yoneda is naturally isomorphic to yoneda ⋙ F.op.lan.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan_inv_app_app_apply_eq_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
(F : CategoryTheory.Functor C D)
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
(X : C)
:
((CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X))
((F.op.lanUnit.app (CategoryTheory.yoneda.obj X)).app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)) = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))
def
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(x : P.Elements)
:
CategoryTheory.yoneda.obj (Opposite.unop x.fst) ⟶ F.op.comp (G.obj P)
Auxiliary definition for presheafHom.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{x y : P.Elements}
(f : x ⟶ y)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (↑f).unop)
(CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ x) = CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ y
@[simp]
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp_naturality_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{x y : P.Elements}
(f : x ⟶ y)
{Z : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(h : F.op.comp (G.obj P) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (↑f).unop)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ x) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ y) h
noncomputable def
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
P ⟶ F.op.comp (G.obj P)
Given functors F : C ⥤ D and G : (Cᵒᵖ ⥤ Type v₁) ⥤ (Dᵒᵖ ⥤ Type v₁), and
a natural transformation φ : F ⋙ yoneda ⟶ yoneda ⋙ G, this is the
(natural) morphism P ⟶ F.op ⋙ G.obj P for all P : Cᵒᵖ ⥤ Type v₁ that is
determined by φ.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.yonedaEquiv_ι_presheafHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
{X : C}
(f : CategoryTheory.yoneda.obj X ⟶ P)
:
CategoryTheory.yonedaEquiv
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ P)) = (G.map f).app (Opposite.op (F.obj X))
((φ.app X).app (Opposite.op (F.obj X)) (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))))
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.yonedaEquiv_presheafHom_yoneda_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
(X : C)
:
CategoryTheory.yonedaEquiv
(CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ (CategoryTheory.yoneda.obj X)) = (φ.app X).app (F.op.obj (Opposite.op X)) (CategoryTheory.CategoryStruct.id (Opposite.unop (F.op.obj (Opposite.op X))))
@[simp]
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
{P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(f : P ⟶ Q)
:
@[simp]
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom_naturality_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
{P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(f : P ⟶ Q)
{Z : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(h : F.op.comp (G.obj Q) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ P)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F.op (G.map f)) h) = CategoryTheory.CategoryStruct.comp f
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ Q) h)
noncomputable def
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
:
F.op.lan ⟶ G
Given functors F : C ⥤ D and G : (Cᵒᵖ ⥤ Type v₁) ⥤ (Dᵒᵖ ⥤ Type v₁),
and a natural transformation φ : F ⋙ yoneda ⟶ yoneda ⋙ G, this is
the canonical natural transformation F.op.lan ⟶ G, which is part of the
that F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁ is the left Kan extension
of F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁ along yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans_app_yoneda_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))}
(φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G)
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
(X : C)
:
(CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans φ).app (CategoryTheory.yoneda.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).inv.app X) (φ.app X)
noncomputable def
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.extensionHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
(Φ : CategoryTheory.yoneda.LeftExtension (F.comp CategoryTheory.yoneda))
:
Given a functor F : C ⥤ D, this definition is part of the verification that
Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom
is universal, i.e. that F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁ is the
left Kan extension of F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁
along yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁.
theorem
CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.hom_ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
{F : CategoryTheory.Functor C D}
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
{Φ : CategoryTheory.yoneda.LeftExtension (F.comp CategoryTheory.yoneda)}
(f g : CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom ⟶ Φ)
:
f = g
noncomputable instance
CategoryTheory.Presheaf.instUniqueHomLeftExtensionFunctorOppositeTypeYonedaCompMkLanOpHomCompYonedaIsoYonedaCompLan
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
(F : CategoryTheory.Functor C D)
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
(Φ :
CategoryTheory.StructuredArrow (F.comp CategoryTheory.yoneda)
((CategoryTheory.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))).obj
CategoryTheory.yoneda))
:
Unique (CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom ⟶ Φ)
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompYonedaIsoYonedaCompLan
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₂} D]
(F : CategoryTheory.Functor C D)
[∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P]
:
F.op.lan.IsLeftKanExtension (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom
Given a functor F : C ⥤ D, F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁ is the
left Kan extension of F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁ along yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁.
Equations
- ⋯ = ⋯
def
CategoryTheory.Presheaf.tautologicalCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
CategoryTheory.Limits.Cocone
((CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda P).comp CategoryTheory.yoneda)
For a presheaf P, consider the forgetful functor from the category of representable
presheaves over P to the category of presheaves. There is a tautological cocone over this
functor whose leg for a natural transformation V ⟶ P with V representable is just that
natural transformation.
Equations
- CategoryTheory.Presheaf.tautologicalCocone P = { pt := P, ι := { app := fun (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P) => X.hom, naturality := ⋯ } }
@[simp]
theorem
CategoryTheory.Presheaf.tautologicalCocone_ι_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
(X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P)
:
(CategoryTheory.Presheaf.tautologicalCocone P).ι.app X = X.hom
@[simp]
theorem
CategoryTheory.Presheaf.tautologicalCocone_pt
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
def
CategoryTheory.Presheaf.isColimitTautologicalCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
The tautological cocone with point P is a colimit cocone, exhibiting P as a colimit of
representables.
Proposition 2.6.3(i) in [Kashiwara2006]
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{I : Type v₁}
[CategoryTheory.SmallCategory I]
(F : CategoryTheory.Functor I C)
{c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)}
(hc : CategoryTheory.Limits.IsColimit c)
:
(c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.pre F CategoryTheory.yoneda c.pt)).Final
Given a functor F : I ⥤ C, a cocone c on F ⋙ yoneda : I ⥤ Cᵒᵖ ⥤ Type v₁ induces a
functor I ⥤ CostructuredArrow yoneda c.pt which maps i : I to the leg
yoneda.obj (F.obj i) ⟶ c.pt. If c is a colimit cocone, then that functor is
final.
Proposition 2.6.3(ii) in [Kashiwara2006]