feat: every presheaf on a large category is a colimit of representabl…

…es (#6387)

Mathlib/CategoryTheory/Limits/Presheaf.lean

@@ -20,7 +20,8 @@ This file constructs an adjunction `yonedaAdjunction` between `(Cᵒᵖ ⥤ Type
 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.
+This adjunction is used to 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.
 
 Further, the left adjoint `colimitAdj.extendAlongYoneda : (Cᵒᵖ ⥤ Type u) ⥤ ℰ` satisfies
 `yoneda ⋙ L ≅ A`, that is, an extension of `A : C ⥤ ℰ` to `(Cᵒᵖ ⥤ Type u) ⥤ ℰ` through
@@ -30,6 +31,9 @@ sometimes known as the Yoneda extension, as proved in `extendAlongYonedaIsoKan`.
 `uniqueExtensionAlongYoneda` shows `extendAlongYoneda` is unique amongst cocontinuous functors
 with this property, establishing the presheaf category as the free cocompletion of a small category.
 
+We also give a direct pedestrian proof that every presheaf is a colimit of representables. This
+version of the proof is valid for any category `C`, even if it is not small.
+
 ## Tags
 colimit, representable, presheaf, free cocompletion
 
@@ -43,7 +47,9 @@ namespace CategoryTheory
 
 open Category Limits
 
-universe u₁ u₂
+universe v₁ v₂ u₁ u₂
+
+section SmallCategory
 
 variable {C : Type u₁} [SmallCategory C]
 
@@ -429,4 +435,48 @@ noncomputable def isLeftAdjointOfPreservesColimits (L : (C ⥤ Type u₁) ⥤ 
   Adjunction.leftAdjointOfNatIso (e.invFunIdAssoc _)
 #align category_theory.is_left_adjoint_of_preserves_colimits CategoryTheory.isLeftAdjointOfPreservesColimits
 
+end SmallCategory
+
+section ArbitraryUniverses
+
+variable {C : Type u₁} [Category.{v₁} C] (P : Cᵒᵖ ⥤ Type v₁)
+
+/-- 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. -/
+@[simps]
+def tautologicalCocone : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda) where
+  pt := P
+  ι := { app := fun X => X.hom }
+
+/-- The tautological cocone with point `P` is a colimit cocone, exhibiting `P` as a colimit of
+    representables. -/
+def isColimitTautologicalCocone : IsColimit (tautologicalCocone P) where
+  desc := fun s => by
+    refine' ⟨fun X t => yonedaEquiv (s.ι.app (CostructuredArrow.mk (yonedaEquiv.symm t))), _⟩
+    intros X Y f
+    ext t
+    dsimp
+    rw [yonedaEquiv_naturality', yonedaEquiv_symm_map]
+    simpa using (s.ι.naturality
+      (CostructuredArrow.homMk' (CostructuredArrow.mk (yonedaEquiv.symm t)) f.unop)).symm
+  fac := by
+    intro s t
+    dsimp
+    apply yonedaEquiv.injective
+    rw [yonedaEquiv_comp]
+    dsimp only
+    rw [Equiv.symm_apply_apply]
+    rfl
+  uniq := by
+    intro s j h
+    ext V x
+    obtain ⟨t, rfl⟩ := yonedaEquiv.surjective x
+    dsimp
+    rw [Equiv.symm_apply_apply, ← yonedaEquiv_comp']
+    exact congr_arg _ (h (CostructuredArrow.mk t))
+
+end ArbitraryUniverses
+
 end CategoryTheory

Mathlib/CategoryTheory/StructuredArrow.lean

@@ -113,13 +113,12 @@ def homMk {f f' : StructuredArrow S T} (g : f.right ⟶ f'.right)
 picks up on it (seems like a bug). Either way simp solves it.  -/
 attribute [-simp, nolint simpNF] homMk_left
 
-/-- Given a structured arrow `X ⟶ F(U)`, and an arrow `U ⟶ Y`, we can construct a morphism of
-structured arrow given by `(X ⟶ F(U)) ⟶ (X ⟶ F(U) ⟶ F(Y))`.
--/
-def homMk' {F : C ⥤ D} {X : D} {Y : C} (U : StructuredArrow X F) (f : U.right ⟶ Y) :
-    U ⟶ mk (U.hom ≫ F.map f) where
+/-- Given a structured arrow `X ⟶ T(Y)`, and an arrow `Y ⟶ Y'`, we can construct a morphism of
+    structured arrows given by `(X ⟶ T(Y)) ⟶ (X ⟶ T(Y) ⟶ T(Y'))`.  -/
+@[simps]
+def homMk' (f : StructuredArrow S T) (g : f.right ⟶ Y') : f ⟶ mk (f.hom ≫ T.map g) where
   left := eqToHom (by ext)
-  right := f
+  right := g
 #align category_theory.structured_arrow.hom_mk' CategoryTheory.StructuredArrow.homMk'
 
 /-- To construct an isomorphism of structured arrows,
@@ -171,11 +170,10 @@ instance epi_homMk {A B : StructuredArrow S T} (f : A.right ⟶ B.right) (w) [h
   (proj S T).epi_of_epi_map h
 #align category_theory.structured_arrow.epi_hom_mk CategoryTheory.StructuredArrow.epi_homMk
 
-/-- Eta rule for structured arrows. Prefer `StructuredArrow.eta`, since equality of objects tends
-    to cause problems. -/
-theorem eq_mk (f : StructuredArrow S T) : f = mk f.hom := by
-  cases f
-  congr
+/-- Eta rule for structured arrows. Prefer `StructuredArrow.eta` for rewriting, since equality of
+    objects tends to cause problems. -/
+theorem eq_mk (f : StructuredArrow S T) : f = mk f.hom :=
+  rfl
 #align category_theory.structured_arrow.eq_mk CategoryTheory.StructuredArrow.eq_mk
 
 /-- Eta rule for structured arrows. -/
@@ -390,6 +388,13 @@ def homMk {f f' : CostructuredArrow S T} (g : f.left ⟶ f'.left)
 picks up on it. Either way simp can prove this -/
 attribute [-simp, nolint simpNF] homMk_right_down_down
 
+/-- Given a costructured arrow `S(Y) ⟶ X`, and an arrow `Y' ⟶ Y'`, we can construct a morphism of
+    costructured arrows given by `(S(Y) ⟶ X) ⟶ (S(Y') ⟶ S(Y) ⟶ X)`. -/
+@[simps]
+def homMk' (f : CostructuredArrow S T) (g : Y' ⟶ f.left) : mk (S.map g ≫ f.hom) ⟶ f where
+  left := g
+  right := eqToHom (by ext)
+
 /-- To construct an isomorphism of costructured arrows,
 we need an isomorphism of the objects underlying the source,
 and to check that the triangle commutes.
@@ -437,11 +442,10 @@ instance epi_homMk {A B : CostructuredArrow S T} (f : A.left ⟶ B.left) (w) [h
   (proj S T).epi_of_epi_map h
 #align category_theory.costructured_arrow.epi_hom_mk CategoryTheory.CostructuredArrow.epi_homMk
 
-/-- Eta rule for costructured arrows. Prefer `CostructuredArrow.eta`, as equality of objects tends
-    to cause problems. -/
-theorem eq_mk (f : CostructuredArrow S T) : f = mk f.hom := by
-  cases f
-  congr
+/-- Eta rule for costructured arrows. Prefer `CostructuredArrow.eta` for rewriting, as equality of
+    objects tends to cause problems. -/
+theorem eq_mk (f : CostructuredArrow S T) : f = mk f.hom :=
+  rfl
 #align category_theory.costructured_arrow.eq_mk CategoryTheory.CostructuredArrow.eq_mk
 
 /-- Eta rule for costructured arrows. -/

Mathlib/CategoryTheory/Yoneda.lean

@@ -415,6 +415,28 @@ theorem yonedaEquiv_naturality {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda
   simp
 #align category_theory.yoneda_equiv_naturality CategoryTheory.yonedaEquiv_naturality
 
+lemma yonedaEquiv_naturality' {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F)
+    (g : X ⟶ Y) : F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f) :=
+  yonedaEquiv_naturality _ _
+
+lemma yonedaEquiv_comp {X : C} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda.obj X ⟶ F) (β : F ⟶ G)  :
+    yonedaEquiv (α ≫ β) = β.app _ (yonedaEquiv α) :=
+  rfl
+
+lemma yonedaEquiv_comp' {X : Cᵒᵖ} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda.obj (unop X) ⟶ F) (β : F ⟶ G)  :
+    yonedaEquiv (α ≫ β) = β.app X (yonedaEquiv α) :=
+  rfl
+
+@[simp]
+lemma yonedaEquiv_yoneda_map {X Y : C} (f : X ⟶ Y) : yonedaEquiv (yoneda.map f) = f := by
+  rw [yonedaEquiv_apply]
+  simp
+
+lemma yonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Cᵒᵖ ⥤ Type v₁} (t : F.obj X) :
+    yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t := by
+  obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
+  rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
+
 /-- When `C` is a small category, we can restate the isomorphism from `yoneda_sections`
 without having to change universes.
 -/