chore: forward-port backports (#3752)

kim-em · eric-wieser · kim-em · commit 4f4742084f9f · 2023-05-05T22:16:38.000Z
* `data.mv_polynomial.basic`, `data.mv_polynomial.funext`: leanprover-community/mathlib3#18839 * `category_theory.limits.preserves.finite`, `category_theory.preadditive.projective`: leanprover-community/mathlib3#18890 * `category_theory.abelian.basic`, `category_theory.abelian.opposite`: leanprover-community/mathlib3#18740 * `topology.category.Top.limits.basic`: leanprover-community/mathlib3#18871. Note that this does not show a useful diff on the dashboard pages as file splits aren't tracked well by git. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
diff --git a/Mathlib/CategoryTheory/Abelian/Basic.lean b/Mathlib/CategoryTheory/Abelian/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Johan Commelin, Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.abelian.basic
-! leanprover-community/mathlib commit 8c75ef3517d4106e89fe524e6281d0b0545f47fc
+! leanprover-community/mathlib commit a5ff45a1c92c278b03b52459a620cfd9c49ebc80
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -268,12 +268,12 @@ namespace CategoryTheory.Abelian
 
 variable {C : Type u} [Category.{v} C] [Abelian C]
 
-/-- An abelian category has finite biproducts. -/
--- Porting note: we would like this to be an instance, and indeed it worked in mathlib3
--- however it triggers https://github.com/leanprover/lean4/issues/2055
--- during the simpNF linter, so for now we turn it on locally in this file.
--- This will likely cause problems in downstream ports, unfortunately.
+-- Porting note: the below porting note is from mathlib3!
+-- Porting note: this should be an instance,
+-- but triggers https://github.com/leanprover/lean4/issues/2055
+-- We set it as a local instance instead.
 -- instance (priority := 100)
+/-- An abelian category has finite biproducts. -/
 theorem hasFiniteBiproducts : HasFiniteBiproducts C :=
   Limits.HasFiniteBiproducts.of_hasFiniteProducts
 #align category_theory.abelian.has_finite_biproducts CategoryTheory.Abelian.hasFiniteBiproducts
diff --git a/Mathlib/CategoryTheory/Abelian/Opposite.lean b/Mathlib/CategoryTheory/Abelian/Opposite.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.abelian.opposite
-! leanprover-community/mathlib commit 8c75ef3517d4106e89fe524e6281d0b0545f47fc
+! leanprover-community/mathlib commit a5ff45a1c92c278b03b52459a620cfd9c49ebc80
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -29,6 +29,7 @@ variable (C : Type _) [Category C] [Abelian C]
 --attribute [local instance]
 --  hasFiniteLimits_of_hasEqualizers_and_finite_products
 --  hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts
+--  Abelian.hasFiniteBiproducts
 
 instance : Abelian Cᵒᵖ := by
   -- porting note: priorities of `Abelian.has_kernels` and `Abelian.has_cokernels` have
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Finite.lean b/Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module category_theory.limits.preserves.finite
-! leanprover-community/mathlib commit 024a4231815538ac739f52d08dd20a55da0d6b23
+! leanprover-community/mathlib commit 3974a774a707e2e06046a14c0eaef4654584fada
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -60,19 +60,22 @@ noncomputable instance (priority := 100) preservesLimitsOfShapeOfPreservesFinite
   apply preservesLimitsOfShapeOfEquiv (FinCategory.equivAsType J)
 #align category_theory.limits.preserves_limits_of_shape_of_preserves_finite_limits CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits
 
--- Porting note: this is a dangerous instance as it has unbound universe variables.
+-- This is a dangerous instance as it has unbound universe variables.
+/-- If we preserve limits of some arbitrary size, then we preserve all finite limits. -/
 noncomputable def PreservesLimitsOfSize.preservesFiniteLimits (F : C ⥤ D)
     [PreservesLimitsOfSize.{w, w₂} F] : PreservesFiniteLimits F where
   preservesFiniteLimits J (sJ : SmallCategory J) fJ := by
     haveI := preservesSmallestLimitsOfPreservesLimits F
     exact preservesLimitsOfShapeOfEquiv (FinCategory.equivAsType J) F
 #align category_theory.limits.preserves_limits.preserves_finite_limits_of_size CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits
 
--- Porting note: added as a specialization of the dangerous instance above.
+-- Added as a specialization of the dangerous instance above, for limits indexed in Type 0.
 noncomputable instance (priority := 120) PreservesLimitsOfSize0.preservesFiniteLimits
     (F : C ⥤ D) [PreservesLimitsOfSize.{0, 0} F] : PreservesFiniteLimits F :=
   PreservesLimitsOfSize.preservesFiniteLimits F
+#align preserves_limits_of_size.zero.preserves_finite_limits CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits
 
+-- An alternative specialization of the dangerous instance for small limits.
 noncomputable instance (priority := 120) PreservesLimits.preservesFiniteLimits (F : C ⥤ D)
     [PreservesLimits F] : PreservesFiniteLimits F :=
   PreservesLimitsOfSize.preservesFiniteLimits F
@@ -128,18 +131,22 @@ noncomputable instance (priority := 100) preservesColimitsOfShapeOfPreservesFini
   apply preservesColimitsOfShapeOfEquiv (FinCategory.equivAsType J)
 #align category_theory.limits.preserves_colimits_of_shape_of_preserves_finite_colimits CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits
 
--- Porting note: this is a dangerous instance as it has unbound universe variables.
+-- This is a dangerous instance as it has unbound universe variables.
+/-- If we preserve colimits of some arbitrary size, then we preserve all finite colimits. -/
 noncomputable def PreservesColimitsOfSize.preservesFiniteColimits (F : C ⥤ D)
     [PreservesColimitsOfSize.{w, w₂} F] : PreservesFiniteColimits F where
   preservesFiniteColimits J (sJ : SmallCategory J) fJ := by
     haveI := preservesSmallestColimitsOfPreservesColimits F
     exact preservesColimitsOfShapeOfEquiv (FinCategory.equivAsType J) F
+#align category_theory.limits.preserves_colimits_of_size.preserves_finite_colimits CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits
 
--- Porting note: added as a specialization of the dangerous instance above.
+-- Added as a specialization of the dangerous instance above, for colimits indexed in Type 0.
 noncomputable instance (priority := 120) PreservesColimitsOfSize0.preservesFiniteColimits
     (F : C ⥤ D) [PreservesColimitsOfSize.{0, 0} F] : PreservesFiniteColimits F :=
   PreservesColimitsOfSize.preservesFiniteColimits F
+#align preserves_colimits_of_size.zero.preserves_finite_colimits CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits
 
+-- An alternative specialization of the dangerous instance for small colimits.
 noncomputable instance (priority := 120) PreservesColimits.preservesFiniteColimits (F : C ⥤ D)
     [PreservesColimits F] : PreservesFiniteColimits F :=
   PreservesColimitsOfSize.preservesFiniteColimits F
diff --git a/Mathlib/CategoryTheory/Preadditive/Projective.lean b/Mathlib/CategoryTheory/Preadditive/Projective.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.preadditive.projective
-! leanprover-community/mathlib commit f8d8465c3c392a93b9ed226956e26dee00975946
+! leanprover-community/mathlib commit 3974a774a707e2e06046a14c0eaef4654584fada
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
diff --git a/Mathlib/Data/MvPolynomial/Basic.lean b/Mathlib/Data/MvPolynomial/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.basic
-! leanprover-community/mathlib commit 2d5739b61641ee4e7e53eca5688a08f66f2e6a60
+! leanprover-community/mathlib commit 0b89934139d3be96f9dab477f10c20f9f93da580
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1148,7 +1148,11 @@ theorem eval_assoc {τ} (f : σ → MvPolynomial τ R) (g : τ → R) (p : MvPol
   congr with a; simp
 #align mv_polynomial.eval_assoc MvPolynomial.eval_assoc
 
--- Porting note: new theorem
+@[simp]
+theorem eval₂_id (p : MvPolynomial σ R) : eval₂ (RingHom.id _) g p = eval g p :=
+  rfl
+#align mv_polynomial.eval₂_id MvPolynomial.eval₂_id
+
 theorem eval_eval₂ [CommSemiring R] [CommSemiring S]
     (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (p : MvPolynomial σ R) :
     eval x (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => eval x (g s)) p := by
@@ -1158,6 +1162,7 @@ theorem eval_eval₂ [CommSemiring R] [CommSemiring S]
     simp [hp, hq]
   · intro p n hp
     simp [hp]
+#align mv_polynomial.eval_eval₂ MvPolynomial.eval_eval₂
 
 end Eval
 
@@ -1205,8 +1210,8 @@ theorem eval₂_eq_eval_map (g : σ → S₁) (p : MvPolynomial σ R) : p.eval
 
   have h := eval₂_comp_left (eval₂Hom (RingHom.id S₁) g) (C.comp f) X p
   -- porting note: the Lean 3 version of `h` was full of metavariables which
-  -- were later unified during `rw [h]`
-  dsimp at h
+  -- were later unified during `rw [h]`. Also needed to add `-eval₂_id`.
+  dsimp [-eval₂_id] at h
   rw [h]
   congr
   · ext1 a
@@ -1215,12 +1220,6 @@ theorem eval₂_eq_eval_map (g : σ → S₁) (p : MvPolynomial σ R) : p.eval
     simp only [comp_apply, eval₂_X]
 #align mv_polynomial.eval₂_eq_eval_map MvPolynomial.eval₂_eq_eval_map
 
--- Porting note: new theorem
--- This probably belongs earlier, but it breaks the fragile proof of `eval₂_eq_eval_map`
-@[simp]
-theorem eval₂_id (p : MvPolynomial σ R) : eval₂ (RingHom.id _) g p = eval g p :=
-  rfl
-
 theorem eval₂_comp_right {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) :
     k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p) := by
   apply MvPolynomial.induction_on p
diff --git a/Mathlib/Data/MvPolynomial/Funext.lean b/Mathlib/Data/MvPolynomial/Funext.lean
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.funext
-! leanprover-community/mathlib commit da01792ca4894d4f3a98d06b6c50455e5ed25da3
+! leanprover-community/mathlib commit 0b89934139d3be96f9dab477f10c20f9f93da580
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Polynomial.RingDivision
 import Mathlib.Data.MvPolynomial.Rename
-import Mathlib.Data.MvPolynomial.Polynomial
 import Mathlib.RingTheory.Polynomial.Basic
+import Mathlib.Data.MvPolynomial.Polynomial
 
 /-!
 ## Function extensionality for multivariate polynomials
diff --git a/Mathlib/Topology/Category/Top/Limits/Basic.lean b/Mathlib/Topology/Category/Top/Limits/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Scott Morrison, Mario Carneiro, Andrew Yang
 
 ! This file was ported from Lean 3 source module topology.category.Top.limits.basic
-! leanprover-community/mathlib commit 8195826f5c428fc283510bc67303dd4472d78498
+! leanprover-community/mathlib commit 178a32653e369dce2da68dc6b2694e385d484ef1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -219,3 +219,27 @@ instance forgetPreservesColimitsOfSize :
 instance forgetPreservesColimits : PreservesColimits (forget : TopCat.{u} ⥤ Type u) :=
   TopCat.forgetPreservesColimitsOfSize.{u, u}
 #align Top.forget_preserves_colimits TopCat.forgetPreservesColimits
+
+/-- The terminal object of `Top` is `PUnit`. -/
+def isTerminalPunit : IsTerminal (TopCat.of PUnit.{u + 1}) :=
+  haveI : ∀ X, Unique (X ⟶ TopCat.of PUnit.{u + 1}) := fun X =>
+    ⟨⟨⟨fun _ => PUnit.unit, by continuity⟩⟩, fun f => by ext; aesop⟩
+  Limits.IsTerminal.ofUnique _
+#align Top.is_terminal_punit TopCat.isTerminalPunit
+
+/-- The terminal object of `Top` is `PUnit`. -/
+def terminalIsoPunit : ⊤_ TopCat.{u} ≅ TopCat.of PUnit :=
+  terminalIsTerminal.uniqueUpToIso isTerminalPunit
+#align Top.terminal_iso_punit TopCat.terminalIsoPunit
+
+/-- The initial object of `Top` is `PEmpty`. -/
+def isInitialPempty : IsInitial (TopCat.of PEmpty.{u + 1}) :=
+  haveI : ∀ X, Unique (TopCat.of PEmpty.{u + 1} ⟶ X) := fun X =>
+    ⟨⟨⟨fun x => x.elim, by continuity⟩⟩, fun f => by ext ⟨⟩⟩
+  Limits.IsInitial.ofUnique _
+#align Top.is_initial_pempty TopCat.isInitialPempty
+
+/-- The initial object of `Top` is `PEmpty`. -/
+def initialIsoPempty : ⊥_ TopCat.{u} ≅ TopCat.of PEmpty :=
+  initialIsInitial.uniqueUpToIso isInitialPempty
+#align Top.initial_iso_pempty TopCat.initialIsoPempty
