# mathlib3documentation

category_theory.limits.presheaf

# Colimit of representables #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

noncomputable 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) :
noncomputable 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

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
noncomputable 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
@[protected, instance]

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

Equations
@[simp]
noncomputable 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]
@[simp]
noncomputable 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]
@[simp]
@[simp]
theorem category_theory.colimit_adj.extend_of_comp_yoneda_iso_Lan_inv_app_app {C : Type u₁} {D : Type u₁} (F : C D) (X : Cᵒᵖ Type u₁) (x : Dᵒᵖ)  :
noncomputable def category_theory.colimit_adj.extend_of_comp_yoneda_iso_Lan {C : Type u₁} {D : Type u₁} (F : C D) :

extending F ⋙ yoneda along the yoneda embedding is isomorphic to Lan F.op.

Equations
noncomputable def category_theory.comp_yoneda_iso_yoneda_comp_Lan {C : Type u₁} {D : Type u₁} (F : C D) :

F ⋙ yoneda is naturally isomorphic to yoneda ⋙ Lan F.op.

Equations
@[simp]
theorem category_theory.comp_yoneda_iso_yoneda_comp_Lan_inv_app_app {C : Type u₁} {D : Type u₁} (F : C D) (X : C) (X_1 : Dᵒᵖ) (ᾰ : .obj X_1) :
@[simp]
theorem category_theory.comp_yoneda_iso_yoneda_comp_Lan_hom_app_app {C : Type u₁} {D : Type u₁} (F : C D) (X : C) (X_1 : Dᵒᵖ) (ᾰ : .obj X).obj X_1) :
noncomputable def category_theory.extend_along_yoneda_yoneda {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

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
noncomputable 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₁) :

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.

noncomputable 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
noncomputable 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
noncomputable 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
noncomputable 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
noncomputable 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