feat(CategoryTheory/Elements): initially small if functor is (co)representable (#34117)

We show that `Functor.Elements F` has an initial element if `F` is (co)representable and that categories with initial element are initially small.

Author: chrisflav

Mathlib/CategoryTheory/Elements.lean

@@ -306,6 +306,32 @@ end CategoryOfElements
 
 namespace Functor
 
+/-- The initial object in `F.Elements` if `F` is representable. -/
+@[simps]
+def Elements.initialOfRepresentableBy {F : Cᵒᵖ ⥤ Type*} {X : C} (h : F.RepresentableBy X) :
+    F.Elements :=
+  ⟨.op X, h.homEquiv (𝟙 X)⟩
+
+/-- If `F` is represented by `X`, `X` with its universal element is the initial object of
+`F.Elements.` -/
+def Elements.isInitialOfRepresentableBy {F : Cᵒᵖ ⥤ Type*} {X : C} (h : F.RepresentableBy X) :
+    Limits.IsInitial (initialOfRepresentableBy h) :=
+  .ofUniqueHom (fun Y ↦ ⟨h.homEquiv.symm Y.snd |>.op, by simp [← h.homEquiv_comp]⟩) fun Y m ↦ by
+    simp [← m.2, ← h.homEquiv_unop_comp]
+
+/-- The initial object in `F.Elements` if `F` is corepresentable. -/
+@[simps]
+def Elements.initialOfCorepresentableBy {F : C ⥤ Type*} {X : C} (h : F.CorepresentableBy X) :
+    F.Elements :=
+  ⟨X, h.homEquiv (𝟙 X)⟩
+
+/-- If `F` is corepresented by `X`, `X` with its universal element is the initial object of
+`F.Elements.` -/
+def Elements.isInitialOfCorepresentableBy {F : C ⥤ Type*} {X : C} (h : F.CorepresentableBy X) :
+    Limits.IsInitial (initialOfCorepresentableBy h) :=
+  .ofUniqueHom (fun Y ↦ ⟨h.homEquiv.symm Y.snd, by simp [← h.homEquiv_comp]⟩) fun Y m ↦ by
+    simp [← m.2, ← h.homEquiv_comp]
+
 /--
 The initial object in the category of elements for a representable functor. In `isInitial` it is
 shown that this is initial.
@@ -315,13 +341,8 @@ def Elements.initial (A : C) : (yoneda.obj A).Elements :=
 
 /-- Show that `Elements.initial A` is initial in the category of elements for the `yoneda` functor.
 -/
-def Elements.isInitial (A : C) : Limits.IsInitial (Elements.initial A) where
-  desc s := ⟨s.pt.2.op, Category.comp_id _⟩
-  uniq s m _ := by
-    simp_rw [← m.2]
-    dsimp [Elements.initial]
-    simp
-  fac := by rintro s ⟨⟨⟩⟩
+def Elements.isInitial (A : C) : Limits.IsInitial (Elements.initial A) :=
+  isInitialOfRepresentableBy (.yoneda A)
 
 end Functor
 

Mathlib/CategoryTheory/Limits/Elements.lean

@@ -9,6 +9,7 @@ public import Mathlib.CategoryTheory.Elements
 public import Mathlib.CategoryTheory.Limits.Types.Limits
 public import Mathlib.CategoryTheory.Limits.Creates
 public import Mathlib.CategoryTheory.Limits.Preserves.Limits
+public import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 
 /-!
 # Limits in the category of elements
@@ -17,6 +18,14 @@ We show that if `C` has limits of shape `I` and `A : C ⥤ Type w` preserves lim
 the category of elements of `A` has limits of shape `I` and the forgetful functor
 `π : A.Elements ⥤ C` creates them.
 
+## Further results
+
+- If `A` is (co)representable, then `A.Elements` has an initial object.
+
+## TODOs
+
+- Show that `A` is (co)representable if `A.Elements` has an initial object.
+
 -/
 
 @[expose] public section
@@ -105,6 +114,16 @@ noncomputable instance : CreatesLimitsOfShape I (π A) where
 instance : HasLimitsOfShape I A.Elements :=
   hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (π A)
 
+section Initial
+
+instance {F : Cᵒᵖ ⥤ Type*} [F.IsRepresentable] : HasInitial F.Elements :=
+  (Functor.Elements.isInitialOfRepresentableBy F.representableBy).hasInitial
+
+instance {F : C ⥤ Type*} [F.IsCorepresentable] : HasInitial F.Elements :=
+  (Functor.Elements.isInitialOfCorepresentableBy F.corepresentableBy).hasInitial
+
+end Initial
+
 end CategoryOfElements
 
 end CategoryTheory

Mathlib/CategoryTheory/Limits/FinallySmall.lean

@@ -81,6 +81,10 @@ theorem finallySmall_of_final_of_essentiallySmall [EssentiallySmall.{w} K] (F :
   have := finallySmall_of_essentiallySmall K
   finallySmall_of_final_of_finallySmall F
 
+instance [Limits.HasTerminal J] : FinallySmall.{w} J :=
+  have := Functor.final_const_terminal (C := PUnit.{w + 1}) (D := J)
+  .mk' ((Functor.const PUnit.{w + 1}).obj (⊤_ J))
+
 end FinallySmall
 
 section InitiallySmall
@@ -130,6 +134,10 @@ theorem initiallySmall_of_initial_of_essentiallySmall [EssentiallySmall.{w} K]
   have := initiallySmall_of_essentiallySmall K
   initiallySmall_of_initial_of_initiallySmall F
 
+instance [Limits.HasInitial J] : InitiallySmall.{w} J :=
+  have := Functor.initial_const_initial (C := PUnit.{w + 1}) (D := J)
+  .mk' ((Functor.const PUnit.{w + 1}).obj (⊥_ J))
+
 end InitiallySmall
 
 instance {J : Type u} [Category.{v} J] [InitiallySmall.{w} J] : FinallySmall.{w} Jᵒᵖ where

Mathlib/CategoryTheory/Yoneda.lean

@@ -242,6 +242,11 @@ lemma RepresentableBy.comp_homEquiv_symm {F : Cᵒᵖ ⥤ Type v} {Y : C}
     f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x) :=
   e.homEquiv.injective (by simp [homEquiv_comp])
 
+lemma RepresentableBy.homEquiv_unop_comp {F : Cᵒᵖ ⥤ Type*} {Y : C}
+    (h : F.RepresentableBy Y) {X : Cᵒᵖ} {X' : C} (f : Opposite.op X' ⟶ X) (g : X' ⟶ Y) :
+    h.homEquiv (f.unop ≫ g) = F.map f (h.homEquiv g) :=
+  h.homEquiv_comp _ _
+
 /-- If `F ≅ F'`, and `F` is representable, then `F'` is representable. -/
 def RepresentableBy.ofIso {F F' : Cᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) (e' : F ≅ F') :
     F'.RepresentableBy Y where
@@ -330,6 +335,15 @@ def representableByEquiv {F : Cᵒᵖ ⥤ Type v₁} {Y : C} :
     { homEquiv := (e.app _).toEquiv
       homEquiv_comp := fun {X X'} f g ↦ congr_fun (e.hom.naturality f.op) g }
 
+/-- `yoneda.obj X` is represented by `X`. -/
+protected def RepresentableBy.yoneda (X : C) : (yoneda.obj X).RepresentableBy X :=
+  Functor.representableByEquiv.symm (Iso.refl _)
+
+@[simp]
+lemma RepresentableBy.coyoneda_homEquiv (X Y : C) :
+    (RepresentableBy.yoneda X).homEquiv = Equiv.refl (Y ⟶ X) :=
+  rfl
+
 /-- The isomorphism `yoneda.obj Y ≅ F` induced by `e : F.RepresentableBy Y`. -/
 def RepresentableBy.toIso {F : Cᵒᵖ ⥤ Type v₁} {Y : C} (e : F.RepresentableBy Y) :
     yoneda.obj Y ≅ F :=
@@ -346,6 +360,16 @@ def corepresentableByEquiv {F : C ⥤ Type v₁} {X : C} :
     { homEquiv := (e.app _).toEquiv
       homEquiv_comp := fun {X X'} f g ↦ congr_fun (e.hom.naturality f) g }
 
+/-- `coyoneda.obj X` is represented by `X`. -/
+protected def CorepresentableBy.coyoneda (X : Cᵒᵖ) :
+    (coyoneda.obj X).CorepresentableBy X.unop :=
+  Functor.corepresentableByEquiv.symm (Iso.refl _)
+
+@[simp]
+lemma CorepresentableBy.coyoneda_homEquiv (X : Cᵒᵖ) (Y : C) :
+    (CorepresentableBy.coyoneda X).homEquiv = Equiv.refl (X.unop ⟶ Y) :=
+  rfl
+
 /-- The isomorphism `coyoneda.obj (op X) ≅ F` induced by `e : F.CorepresentableBy X`. -/
 def CorepresentableBy.toIso {F : C ⥤ Type v₁} {X : C} (e : F.CorepresentableBy X) :
     coyoneda.obj (op X) ≅ F :=