chore(category_theory/limits/*): Unify names for limit constructions. (#15810)

List of renames:
`limits_from_equalizers_and_products` -> `has_limits_of_has_equalizers_and_products`
`colimits_from_coequalizers_and_coproducts` -> `has_colimits_of_has_coequalizers_and_coproducts`
`finite_limits_from_equalizers_and_finite_products` -> `has_finite_limits_of_has_equalizers_and_finite_products`
`finite_colimits_from_coequalizers_and_finite_coproducts` -> `has_finite_colimits_of_has_coequalizers_and_finite_coproducts`
`has_binary_products_of_terminal_and_pullbacks` -> `has_binary_products_of_has_terminal_and_pullbacks`
`has_binary_coproducts_of_initial_and_pushouts` -> `has_binary_coproducts_of_has_initial_and_pushouts`
`has_equalizers_of_pullbacks_and_binary_products` -> `has_equalizers_of_has_pullbacks_and_binary_products`
`has_coequalizers_of_pushouts_and_binary_coproducts` -> `has_coequalizers_of_has_pushouts_and_binary_coproducts`
`preserves_equalizers_of_pullbacks_and_binary_products` -> `preserves_equalizers_of_preserves_pullbacks_and_binary_products`
`preserves_coequalizers_of_pushouts_and_binary_coproducts` -> `preserves_coequalizers_of_preserves_pushouts_and_binary_coproducts`
`has_finite_coproducts_of_has_binary_and_terminal` -> `has_finite_coproducts_of_has_binary_and_initial`



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

src/algebraic_geometry/locally_ringed_space/has_colimits.lean

@@ -291,7 +291,7 @@ end⟩
 
 end has_coequalizer
 
-instance : has_colimits LocallyRingedSpace := colimits_from_coequalizers_and_coproducts
+instance : has_colimits LocallyRingedSpace := has_colimits_of_has_coequalizers_and_coproducts
 
 noncomputable
 instance : preserves_colimits LocallyRingedSpace.forget_to_SheafedSpace :=

src/category_theory/abelian/basic.lean

@@ -460,11 +460,11 @@ has_pushouts_of_has_binary_coproducts_of_has_coequalizers C
 
 @[priority 100]
 instance has_finite_limits : has_finite_limits C :=
-limits.finite_limits_from_equalizers_and_finite_products
+limits.has_finite_limits_of_has_equalizers_and_finite_products
 
 @[priority 100]
 instance has_finite_colimits : has_finite_colimits C :=
-limits.finite_colimits_from_coequalizers_and_finite_coproducts
+limits.has_finite_colimits_of_has_coequalizers_and_finite_coproducts
 
 end
 

src/category_theory/abelian/opposite.lean

@@ -21,8 +21,8 @@ open category_theory.limits
 variables (C : Type*) [category C] [abelian C]
 
 local attribute [instance]
-  finite_limits_from_equalizers_and_finite_products
-  finite_colimits_from_coequalizers_and_finite_coproducts
+  has_finite_limits_of_has_equalizers_and_finite_products
+  has_finite_colimits_of_has_coequalizers_and_finite_coproducts
   has_finite_limits_opposite has_finite_colimits_opposite has_finite_products_opposite
 
 instance : abelian Cᵒᵖ :=

src/category_theory/limits/constructions/binary_products.lean

@@ -90,7 +90,7 @@ variable (C)
 
 /-- Any category with pullbacks and terminal object has binary products. -/
 -- This is not an instance, as it is not always how one wants to construct binary products!
-lemma has_binary_products_of_terminal_and_pullbacks
+lemma has_binary_products_of_has_terminal_and_pullbacks
   [has_terminal C] [has_pullbacks C] :
   has_binary_products C :=
 { has_limit := λ F, has_limit.mk (limit_cone_of_terminal_and_pullbacks F) }
@@ -187,7 +187,7 @@ variable (C)
 
 /-- Any category with pushouts and initial object has binary coproducts. -/
 -- This is not an instance, as it is not always how one wants to construct binary coproducts!
-lemma has_binary_coproducts_of_initial_and_pushouts
+lemma has_binary_coproducts_of_has_initial_and_pushouts
   [has_initial C] [has_pushouts C] :
   has_binary_coproducts C :=
 { has_colimit := λ F, has_colimit.mk (colimit_cocone_of_initial_and_pushouts F) }

src/category_theory/limits/constructions/equalizers.lean

@@ -29,7 +29,7 @@ variables {C : Type u} [category.{v} C]
 variables {D : Type u'} [category.{v'} D] (G : C ⥤ D)
 
 -- We hide the "implementation details" inside a namespace
-namespace has_equalizers_of_pullbacks_and_binary_products
+namespace has_equalizers_of_has_pullbacks_and_binary_products
 
 variables [has_binary_products C] [has_pullbacks C]
 
@@ -76,12 +76,13 @@ def equalizer_cone_is_limit (F : walking_parallel_pair ⥤ C) : is_limit (equali
     { erw [limit.lift_π, ← J0, pullback_fst_eq_pullback_snd] }
   end }
 
-end has_equalizers_of_pullbacks_and_binary_products
+end has_equalizers_of_has_pullbacks_and_binary_products
 
-open has_equalizers_of_pullbacks_and_binary_products
+open has_equalizers_of_has_pullbacks_and_binary_products
 /-- Any category with pullbacks and binary products, has equalizers. -/
 -- This is not an instance, as it is not always how one wants to construct equalizers!
-lemma has_equalizers_of_pullbacks_and_binary_products [has_binary_products C] [has_pullbacks C] :
+lemma has_equalizers_of_has_pullbacks_and_binary_products
+  [has_binary_products C] [has_pullbacks C] :
   has_equalizers C :=
 { has_limit := λ F, has_limit.mk
   { cone := equalizer_cone F,
@@ -90,7 +91,7 @@ lemma has_equalizers_of_pullbacks_and_binary_products [has_binary_products C] [h
 local attribute[instance] has_pullback_of_preserves_pullback
 
 /-- A functor that preserves pullbacks and binary products also presrves equalizers. -/
-def preserves_equalizers_of_pullbacks_and_binary_products
+def preserves_equalizers_of_preserves_pullbacks_and_binary_products
     [has_binary_products C] [has_pullbacks C]
     [preserves_limits_of_shape (discrete walking_pair) G]
     [preserves_limits_of_shape walking_cospan G] :
@@ -128,7 +129,7 @@ def preserves_equalizers_of_pullbacks_and_binary_products
 
 
 -- We hide the "implementation details" inside a namespace
-namespace has_coequalizers_of_pushouts_and_binary_coproducts
+namespace has_coequalizers_of_has_pushouts_and_binary_coproducts
 
 variables [has_binary_coproducts C] [has_pushouts C]
 
@@ -177,12 +178,12 @@ def coequalizer_cocone_is_colimit (F : walking_parallel_pair ⥤ C) :
     { rw [colimit.ι_desc, ← pushout_inl_eq_pushout_inr], exact J1 }
   end }
 
-end has_coequalizers_of_pushouts_and_binary_coproducts
+end has_coequalizers_of_has_pushouts_and_binary_coproducts
 
-open has_coequalizers_of_pushouts_and_binary_coproducts
+open has_coequalizers_of_has_pushouts_and_binary_coproducts
 /-- Any category with pullbacks and binary products, has equalizers. -/
 -- This is not an instance, as it is not always how one wants to construct equalizers!
-lemma has_coequalizers_of_pushouts_and_binary_coproducts
+lemma has_coequalizers_of_has_pushouts_and_binary_coproducts
   [has_binary_coproducts C] [has_pushouts C] : has_coequalizers C :=
 { has_colimit := λ F, has_colimit.mk
   { cocone := coequalizer_cocone F,
@@ -191,7 +192,7 @@ lemma has_coequalizers_of_pushouts_and_binary_coproducts
 local attribute[instance] has_pushout_of_preserves_pushout
 
 /-- A functor that preserves pushouts and binary coproducts also presrves coequalizers. -/
-def preserves_coequalizers_of_pushouts_and_binary_coproducts
+def preserves_coequalizers_of_preserves_pushouts_and_binary_coproducts
     [has_binary_coproducts C] [has_pushouts C]
     [preserves_colimits_of_shape (discrete walking_pair) G]
     [preserves_colimits_of_shape walking_span G] :

src/category_theory/limits/constructions/finite_products_of_binary_products.lean

@@ -303,7 +303,7 @@ begin
 end }
 
 /-- If `C` has an initial object and binary coproducts, then it has finite coproducts. -/
-lemma has_finite_coproducts_of_has_binary_and_terminal : has_finite_coproducts C :=
+lemma has_finite_coproducts_of_has_binary_and_initial : has_finite_coproducts C :=
 ⟨λ J 𝒥, begin
   resetI,
   apply has_colimits_of_shape_of_equivalence (discrete.equivalence (fintype.equiv_fin J)).symm,

src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

@@ -133,7 +133,7 @@ Any category with products and equalizers has all limits.
 
 See <https://stacks.math.columbia.edu/tag/002N>.
 -/
-lemma limits_from_equalizers_and_products
+lemma has_limits_of_has_equalizers_and_products
   [has_products.{w} C] [has_equalizers C] : has_limits_of_size.{w w} C :=
 { has_limits_of_shape := λ J 𝒥,
   { has_limit := λ F, by exactI has_limit_of_equalizer_and_product F } }
@@ -143,7 +143,7 @@ Any category with finite products and equalizers has all finite limits.
 
 See <https://stacks.math.columbia.edu/tag/002O>.
 -/
-lemma finite_limits_from_equalizers_and_finite_products
+lemma has_finite_limits_of_has_equalizers_and_finite_products
   [has_finite_products C] [has_equalizers C] : has_finite_limits C :=
 ⟨λ J _ _, { has_limit := λ F, by exactI has_limit_of_equalizer_and_product F }⟩
 
@@ -219,11 +219,11 @@ preserves_limits_of_size.{w w} G :=
 
 lemma has_finite_limits_of_has_terminal_and_pullbacks [has_terminal C] [has_pullbacks C] :
   has_finite_limits C :=
-@@finite_limits_from_equalizers_and_finite_products _
+@@has_finite_limits_of_has_equalizers_and_finite_products _
   (@@has_finite_products_of_has_binary_and_terminal _
-    (has_binary_products_of_terminal_and_pullbacks C) infer_instance)
-  (@@has_equalizers_of_pullbacks_and_binary_products _
-    (has_binary_products_of_terminal_and_pullbacks C) infer_instance)
+    (has_binary_products_of_has_terminal_and_pullbacks C) infer_instance)
+  (@@has_equalizers_of_has_pullbacks_and_binary_products _
+    (has_binary_products_of_has_terminal_and_pullbacks C) infer_instance)
 
 /-- If G preserves terminal objects and pullbacks, it preserves all finite limits. -/
 def preserves_finite_limits_of_preserves_terminal_and_pullbacks
@@ -236,7 +236,7 @@ begin
   haveI : preserves_limits_of_shape (discrete walking_pair) G :=
     preserves_binary_products_of_preserves_terminal_and_pullbacks G,
   exact @@preserves_finite_limits_of_preserves_equalizers_and_finite_products _ _ _ _ G
-    (preserves_equalizers_of_pullbacks_and_binary_products G)
+    (preserves_equalizers_of_preserves_pullbacks_and_binary_products G)
     (preserves_finite_products_of_preserves_binary_and_terminal G),
 end
 
@@ -341,7 +341,7 @@ Any category with coproducts and coequalizers has all colimits.
 
 See <https://stacks.math.columbia.edu/tag/002P>.
 -/
-lemma colimits_from_coequalizers_and_coproducts
+lemma has_colimits_of_has_coequalizers_and_coproducts
   [has_coproducts.{w} C] [has_coequalizers C] : has_colimits_of_size.{w w} C :=
 { has_colimits_of_shape := λ J 𝒥,
   { has_colimit := λ F, by exactI has_colimit_of_coequalizer_and_coproduct F } }
@@ -351,7 +351,7 @@ Any category with finite coproducts and coequalizers has all finite colimits.
 
 See <https://stacks.math.columbia.edu/tag/002Q>.
 -/
-lemma finite_colimits_from_coequalizers_and_finite_coproducts
+lemma has_finite_colimits_of_has_coequalizers_and_finite_coproducts
   [has_finite_coproducts C] [has_coequalizers C] : has_finite_colimits C :=
 ⟨λ J _ _, { has_colimit := λ F, by exactI has_colimit_of_coequalizer_and_coproduct F }⟩
 
@@ -426,11 +426,11 @@ preserves_colimits_of_size.{w} G :=
 
 lemma has_finite_colimits_of_has_initial_and_pushouts [has_initial C] [has_pushouts C] :
   has_finite_colimits C :=
-@@finite_colimits_from_coequalizers_and_finite_coproducts _
-  (@@has_finite_coproducts_of_has_binary_and_terminal _
-    (has_binary_coproducts_of_initial_and_pushouts C) infer_instance)
-  (@@has_coequalizers_of_pushouts_and_binary_coproducts _
-    (has_binary_coproducts_of_initial_and_pushouts C) infer_instance)
+@@has_finite_colimits_of_has_coequalizers_and_finite_coproducts _
+  (@@has_finite_coproducts_of_has_binary_and_initial _
+    (has_binary_coproducts_of_has_initial_and_pushouts C) infer_instance)
+  (@@has_coequalizers_of_has_pushouts_and_binary_coproducts _
+    (has_binary_coproducts_of_has_initial_and_pushouts C) infer_instance)
 
 /-- If G preserves initial objects and pushouts, it preserves all finite colimits. -/
 def preserves_finite_colimits_of_preserves_initial_and_pushouts
@@ -443,7 +443,7 @@ begin
   haveI : preserves_colimits_of_shape (discrete walking_pair) G :=
     preserves_binary_coproducts_of_preserves_initial_and_pushouts G,
   exact @@preserves_finite_colimits_of_preserves_coequalizers_and_finite_coproducts _ _ _ _ G
-    (preserves_coequalizers_of_pushouts_and_binary_coproducts G)
+    (preserves_coequalizers_of_preserves_pushouts_and_binary_coproducts G)
     (preserves_finite_coproducts_of_preserves_binary_and_initial G),
 end
 

src/category_theory/limits/constructions/over/default.lean

@@ -44,19 +44,19 @@ end
 
 instance has_finite_limits {B : C} [has_finite_wide_pullbacks C] : has_finite_limits (over B) :=
 begin
-  apply @finite_limits_from_equalizers_and_finite_products _ _ _ _,
+  apply @has_finite_limits_of_has_equalizers_and_finite_products _ _ _ _,
   { exact construct_products.over_finite_products_of_finite_wide_pullbacks, },
-  { apply @has_equalizers_of_pullbacks_and_binary_products _ _ _ _,
+  { apply @has_equalizers_of_has_pullbacks_and_binary_products _ _ _ _,
     { haveI : has_pullbacks C := ⟨by apply_instance⟩,
       exact construct_products.over_binary_product_of_pullback },
     { apply_instance, } }
 end
 
 instance has_limits {B : C} [has_wide_pullbacks.{w} C] : has_limits_of_size.{w} (over B) :=
 begin
-  apply @limits_from_equalizers_and_products _ _ _ _,
+  apply @has_limits_of_has_equalizers_and_products _ _ _ _,
   { exact construct_products.over_products_of_wide_pullbacks },
-  { apply @has_equalizers_of_pullbacks_and_binary_products _ _ _ _,
+  { apply @has_equalizers_of_has_pullbacks_and_binary_products _ _ _ _,
     { haveI : has_pullbacks C := ⟨infer_instance⟩,
       exact construct_products.over_binary_product_of_pullback },
     { apply_instance, } }

src/order/category/omega_complete_partial_order.lean

@@ -131,7 +131,7 @@ has_limit.mk ⟨_, has_equalizers.is_equalizer f g⟩
 
 instance : has_equalizers ωCPO.{v} := has_equalizers_of_has_limit_parallel_pair _
 
-instance : has_limits ωCPO.{v} := limits_from_equalizers_and_products
+instance : has_limits ωCPO.{v} := has_limits_of_has_equalizers_and_products
 
 end