mathlibdocumentation

category_theory.limits.presheaf

Colimit of representables #

This file constructs an adjunction yoneda_adjunction between (Cᵒᵖ ⥤ Type u) and ℰ given a functor A : C ⥤ ℰ, where the right adjoint sends (E : ℰ) to c ↦ (A.obj c ⟶ E) (provided ℰ has colimits).

This adjunction is used to show that every presheaf is a colimit of representables.

Further, the left adjoint colimit_adj.extend_along_yoneda : (Cᵒᵖ ⥤ Type u) ⥤ ℰ satisfies yoneda ⋙ L ≅ A, that is, an extension of A : C ⥤ ℰ to (Cᵒᵖ ⥤ Type u) ⥤ ℰ through yoneda : C ⥤ Cᵒᵖ ⥤ Type u. It is the left Kan extension of A along the yoneda embedding, sometimes known as the Yoneda extension, as proved in extend_along_yoneda_iso_Kan.

unique_extension_along_yoneda shows extend_along_yoneda is unique amongst cocontinuous functors with this property, establishing the presheaf category as the free cocompletion of a small category.

Tags #

colimit, representable, presheaf, free cocompletion

References #

@[simp]
theorem category_theory.colimit_adj.restricted_yoneda_map_app {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (_x _x_1 : ℰ) (f : _x _x_1) (X : Cᵒᵖ) (ᾰ : .obj (A.op.obj X)) :
= f
def category_theory.colimit_adj.restricted_yoneda {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) :
Cᵒᵖ Type u₁

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
@[simp]
theorem category_theory.colimit_adj.restricted_yoneda_obj_map {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (X : ℰ) (_x _x_1 : Cᵒᵖ) (f : _x _x_1) (ᾰ : (A.op.obj _x)) :
= A.map f.unop
@[simp]
theorem category_theory.colimit_adj.restricted_yoneda_obj_obj {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (X : ℰ) (X_1 : Cᵒᵖ) :
X_1 = (A.obj (opposite.unop X_1) X)

The functor restricted_yoneda is isomorphic to the identity functor when evaluated at the yoneda embedding.

Equations
def category_theory.colimit_adj.restrict_yoneda_hom_equiv {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (P : Cᵒᵖ Type u₁) (E : ℰ)  :
(c.X E)

(Implementation). The equivalence of homsets which helps construct the left adjoint to colimit_adj.restricted_yoneda. It is shown in restrict_yoneda_hom_equiv_natural that this is a natural bijection.

Equations
theorem category_theory.colimit_adj.restrict_yoneda_hom_equiv_natural {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (P : Cᵒᵖ Type u₁) (E₁ E₂ : ℰ) (g : E₁ E₂) (k : c.X E₁) :
(k g) =

(Implementation). Show that the bijection in restrict_yoneda_hom_equiv is natural (on the right).

def category_theory.colimit_adj.extend_along_yoneda {C : Type u₁} {ℰ : Type u₂} (A : C ℰ)  :
(Cᵒᵖ Type u₁)

The left adjoint to the functor restricted_yoneda (shown in yoneda_adjunction). It is also an extension of A along the yoneda embedding (shown in is_extension_along_yoneda), in particular it is the left Kan extension of A through the yoneda embedding.

Equations
@[simp]
theorem category_theory.colimit_adj.extend_along_yoneda_obj {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (P : Cᵒᵖ Type u₁) :
theorem category_theory.colimit_adj.extend_along_yoneda_map {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) {X Y : Cᵒᵖ Type u₁} (f : X Y) :
def category_theory.colimit_adj.yoneda_adjunction {C : Type u₁} {ℰ : Type u₂} (A : C ℰ)  :

Show extend_along_yoneda is left adjoint to restricted_yoneda.

The construction of [MM92], Chapter I, Section 5, Theorem 2.

Equations
def category_theory.colimit_adj.elements.initial {C : Type u₁} (A : C) :

The initial object in the category of elements for a representable functor. In is_initial it is shown that this is initial.

Equations

Show that elements.initial A is initial in the category of elements for the yoneda functor.

Equations
def category_theory.colimit_adj.is_extension_along_yoneda {C : Type u₁} {ℰ : Type u₂} (A : C ℰ)  :

extend_along_yoneda A is an extension of A to the presheaf category along the yoneda embedding. unique_extension_along_yoneda shows it is unique among functors preserving colimits with this property (up to isomorphism).

The first part of [MM92], Chapter I, Section 5, Corollary 4. See Property 1 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

Equations
@[instance]

See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

Equations
@[simp]
def category_theory.colimit_adj.extend_along_yoneda_iso_Kan_app {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (X : Cᵒᵖ Type u₁) :

Show that the images of X after extend_along_yoneda and Lan yoneda are indeed isomorphic. This follows from category_theory.category_of_elements.costructured_arrow_yoneda_equivalence.

Equations
@[simp]
theorem category_theory.colimit_adj.extend_along_yoneda_iso_Kan_app_inv {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (X : Cᵒᵖ Type u₁) :
@[simp]
theorem category_theory.colimit_adj.extend_along_yoneda_iso_Kan_inv_app {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (X : Cᵒᵖ Type u₁) :
def category_theory.colimit_adj.extend_along_yoneda_iso_Kan {C : Type u₁} {ℰ : Type u₂} (A : C ℰ)  :

Verify that extend_along_yoneda is indeed the left Kan extension along the yoneda embedding.

Equations
@[simp]
theorem category_theory.colimit_adj.extend_along_yoneda_iso_Kan_hom_app {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (X : Cᵒᵖ Type u₁) :

Since extend_along_yoneda A is adjoint to restricted_yoneda A, if we use A = yoneda then restricted_yoneda A is isomorphic to the identity, and so extend_along_yoneda A is as well.

Equations
def category_theory.functor_to_representables {C : Type u₁} (P : Cᵒᵖ Type u₁) :
(P.elements)ᵒᵖ Cᵒᵖ Type u₁

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). cocone_of_representable gives a cocone for this functor which is a colimit and has point P.

Equations
def category_theory.cocone_of_representable {C : Type u₁} (P : Cᵒᵖ Type u₁) :

This is a cocone with point P for the functor functor_to_representables P. It is shown in colimit_of_representable 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
@[simp]
theorem category_theory.cocone_of_representable_X {C : Type u₁} (P : Cᵒᵖ Type u₁) :
theorem category_theory.cocone_of_representable_ι_app {C : Type u₁} (P : Cᵒᵖ Type u₁) (j : (P.elements)ᵒᵖ) :

An explicit formula for the legs of the cocone cocone_of_representable.

theorem category_theory.cocone_of_representable_naturality {C : Type u₁} {P₁ P₂ : Cᵒᵖ Type u₁} (α : P₁ P₂) (j : (P₁.elements)ᵒᵖ) :

The legs of the cocone cocone_of_representable are natural in the choice of presheaf.

def category_theory.colimit_of_representable {C : Type u₁} (P : Cᵒᵖ Type u₁) :

The cocone with point P given by the_cocone 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
def category_theory.nat_iso_of_nat_iso_on_representables {C : Type u₁} {ℰ : Type u₂} (L₁ L₂ : (Cᵒᵖ Type u₁) ℰ) (h : ) :
L₁ L₂

Given two functors L₁ and L₂ which preserve colimits, if they agree when restricted to the representable presheaves then they agree everywhere.

Equations
def category_theory.unique_extension_along_yoneda {C : Type u₁} {ℰ : Type u₂} (A : C ℰ) (L : (Cᵒᵖ Type u₁) ℰ) (hL : A)  :

Show that extend_along_yoneda 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
def category_theory.is_left_adjoint_of_preserves_colimits_aux {C : Type u₁} {ℰ : Type u₂} (L : (Cᵒᵖ Type u₁) ℰ)  :

If L preserves colimits and ℰ has them, then it is a left adjoint. This is a special case of is_left_adjoint_of_preserves_colimits used to prove that.

Equations
def category_theory.is_left_adjoint_of_preserves_colimits {C : Type u₁} {ℰ : Type u₂} (L : (C Type u₁) ℰ)  :

If L preserves colimits and ℰ has them, then it is a left adjoint. Note this is a (partial) converse to left_adjoint_preserves_colimits.

Equations