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 #
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
The functor restricted_yoneda is isomorphic to the identity functor when evaluated at the yoneda
embedding.
Equations
- category_theory.colimit_adj.restricted_yoneda_yoneda = category_theory.nat_iso.of_components (λ (P : Cᵒᵖ ⥤ Type u₁), category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), category_theory.yoneda_sections_small (opposite.unop X) P) _) category_theory.colimit_adj.restricted_yoneda_yoneda._proof_2
(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
- category_theory.colimit_adj.restrict_yoneda_hom_equiv A P E t = ((category_theory.ulift_trivial (c.X ⟶ E)).symm ≪≫ t.hom_iso' E).to_equiv.trans {to_fun := λ (k : {p // ∀ {j j' : (P.elements)ᵒᵖ} (f : j ⟶ j'), ((category_theory.category_of_elements.π P).left_op ⋙ A).map f ≫ p j' = p j}), {app := λ (c : Cᵒᵖ) (p : P.obj c), k.val (opposite.op ⟨c, p⟩), naturality' := _}, inv_fun := λ (τ : P ⟶ (category_theory.colimit_adj.restricted_yoneda A).obj E), ⟨λ (p : (P.elements)ᵒᵖ), τ.app (opposite.unop p).fst (opposite.unop p).snd, _⟩, left_inv := _, right_inv := _}
(Implementation). Show that the bijection in restrict_yoneda_hom_equiv is natural (on the right).
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
Instances for category_theory.colimit_adj.extend_along_yoneda
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
- category_theory.colimit_adj.is_initial A = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty (category_theory.yoneda.obj A).elements)), ⟨quiver.hom.op s.X.snd, _⟩, fac' := _, uniq' := _}
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
- category_theory.colimit_adj.is_extension_along_yoneda A = category_theory.nat_iso.of_components (λ (X : C), (category_theory.limits.colimit.is_colimit ((category_theory.category_of_elements.π (category_theory.yoneda.obj X)).left_op ⋙ A)).cocone_point_unique_up_to_iso (category_theory.limits.colimit_of_diagram_terminal (category_theory.limits.terminal_op_of_initial (category_theory.colimit_adj.is_initial X)) ((category_theory.category_of_elements.π (category_theory.yoneda.obj X)).left_op ⋙ A))) _
See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.
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
- category_theory.colimit_adj.extend_along_yoneda_iso_Kan_app A X = let eq : (X.elements)ᵒᵖ ≌ category_theory.costructured_arrow category_theory.yoneda X := category_theory.category_of_elements.costructured_arrow_yoneda_equivalence X in {hom := category_theory.limits.colimit.pre (category_theory.Lan.diagram category_theory.yoneda A X) eq.functor _, inv := category_theory.limits.colimit.pre ((category_theory.category_of_elements.π X).left_op ⋙ A) eq.inverse _, hom_inv_id' := _, inv_hom_id' := _}
Verify that extend_along_yoneda is indeed the left Kan extension along the yoneda embedding.
extending F ⋙ yoneda along the yoneda embedding is isomorphic to Lan F.op.
Equations
- category_theory.colimit_adj.extend_of_comp_yoneda_iso_Lan F = (category_theory.colimit_adj.yoneda_adjunction (F ⋙ category_theory.yoneda)).nat_iso_of_right_adjoint_nat_iso (category_theory.Lan.adjunction (Type u₁) F.op) (category_theory.iso_whisker_right category_theory.curried_yoneda_lemma' ((category_theory.whiskering_left Cᵒᵖ Dᵒᵖ (Type u₁)).obj F.op))
F ⋙ yoneda is naturally isomorphic to yoneda ⋙ Lan F.op.
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.
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.
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.
An explicit formula for the legs of the cocone cocone_of_representable.
The legs of the cocone cocone_of_representable are natural in the choice of presheaf.
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.
Given two functors L₁ and L₂ which preserve colimits, if they agree when restricted to the representable presheaves then they agree everywhere.
Equations
- category_theory.nat_iso_of_nat_iso_on_representables L₁ L₂ h = category_theory.nat_iso.of_components (λ (P : Cᵒᵖ ⥤ Type u₁), (category_theory.limits.is_colimit_of_preserves L₁ (category_theory.colimit_of_representable P)).cocone_points_iso_of_nat_iso (category_theory.limits.is_colimit_of_preserves L₂ (category_theory.colimit_of_representable P)) ((category_theory.category_of_elements.π P).left_op.associator category_theory.yoneda L₁ ≪≫ category_theory.iso_whisker_left (category_theory.category_of_elements.π P).left_op h)) _
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.
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
- category_theory.is_left_adjoint_of_preserves_colimits_aux L = {right := category_theory.colimit_adj.restricted_yoneda (category_theory.yoneda ⋙ L), adj := (category_theory.colimit_adj.yoneda_adjunction (category_theory.yoneda ⋙ L)).of_nat_iso_left (category_theory.unique_extension_along_yoneda (category_theory.yoneda ⋙ L) L (category_theory.iso.refl (category_theory.yoneda ⋙ L))).symm}
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
- category_theory.is_left_adjoint_of_preserves_colimits L = let e : Cᵒᵖᵒᵖ ⥤ Type u₁ ≌ C ⥤ Type u₁ := (category_theory.op_op_equivalence C).congr_left, t : category_theory.is_left_adjoint (e.functor ⋙ L) := category_theory.is_left_adjoint_of_preserves_colimits_aux (e.functor ⋙ L) in category_theory.adjunction.left_adjoint_of_nat_iso (e.inv_fun_id_assoc L)