feat(category_theory): limits of essentially small indexing categories (

#15377)

src/category_theory/essentially_small.lean

@@ -69,6 +69,10 @@ begin
     exact essentially_small.mk' (e.trans f), },
 end
 
+lemma discrete.essentially_small_of_small {α : Type u} [small.{w} α] :
+  essentially_small.{w} (discrete α) :=
+⟨⟨discrete (shrink α), ⟨infer_instance, ⟨discrete.equivalence (equiv_shrink _)⟩⟩⟩⟩
+
 /--
 A category is `w`-locally small if every hom set is `w`-small.
 

src/category_theory/limits/essentially_small.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import category_theory.limits.shapes.products
+import category_theory.essentially_small
+
+/-!
+# Limits over essentially small indexing categories
+
+If `C` has limits of size `w` and `J` is `w`-essentially small, then `C` has limits of shape `J`.
+
+-/
+
+universes w₁ w₂ v₁ v₂ u₁ u₂
+
+noncomputable theory
+
+open category_theory
+
+namespace category_theory.limits
+variables (J : Type u₂) [category.{v₂} J] (C : Type u₁) [category.{v₁} C]
+
+lemma has_limits_of_shape_of_essentially_small [essentially_small.{w₁} J]
+  [has_limits_of_size.{w₁ w₁} C] : has_limits_of_shape J C :=
+has_limits_of_shape_of_equivalence $ equivalence.symm $ equiv_small_model.{w₁} J
+
+lemma has_colimits_of_shape_of_essentially_small [essentially_small.{w₁} J]
+  [has_colimits_of_size.{w₁ w₁} C] : has_colimits_of_shape J C :=
+has_colimits_of_shape_of_equivalence $ equivalence.symm $ equiv_small_model.{w₁} J
+
+lemma has_products_of_shape_of_small (β : Type w₁) [small.{w₂} β] [has_products.{w₂} C] :
+  has_products_of_shape β C :=
+has_limits_of_shape_of_equivalence $ discrete.equivalence $ equiv.symm $ equiv_shrink β
+
+lemma has_coproducts_of_shape_of_small (β : Type w₁) [small.{w₂} β] [has_coproducts.{w₂} C] :
+  has_coproducts_of_shape β C :=
+has_colimits_of_shape_of_equivalence $ discrete.equivalence $ equiv.symm $ equiv_shrink β
+
+end category_theory.limits