feat: port CategoryTheory.Preadditive.Projective (#3615)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -611,6 +611,7 @@ import Mathlib.CategoryTheory.Preadditive.Generator
 import Mathlib.CategoryTheory.Preadditive.LeftExact
 import Mathlib.CategoryTheory.Preadditive.OfBiproducts
 import Mathlib.CategoryTheory.Preadditive.Opposite
+import Mathlib.CategoryTheory.Preadditive.Projective
 import Mathlib.CategoryTheory.Preadditive.SingleObj
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
 import Mathlib.CategoryTheory.Products.Associator

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -387,7 +387,7 @@ def wideCospan.limitCone [Finite ι] (X : C) : LimitCone (wideCospan ι X) where
       fac := fun s j => Option.casesOn j (Subsingleton.elim _ _) fun j => limit.lift_π _ _
       uniq := fun s f h => by
         dsimp
-        ext ⟨j⟩
+        ext j
         dsimp only [Limits.Pi.lift]
         rw [limit.lift_π]
         dsimp

Mathlib/CategoryTheory/Adjunction/Evaluation.lean

@@ -66,7 +66,7 @@ def evaluationAdjunctionRight (c : C) : evaluationLeftAdjoint D c ⊣ (evaluatio
             intro f
             ext x
             dsimp
-            ext ⟨g⟩
+            ext g
             simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ←f.naturality,
               evaluationLeftAdjoint_obj_map, colimit.ι_desc_assoc,
               Discrete.functor_obj, Cofan.mk_pt, Discrete.natTrans_app, Category.id_comp]
@@ -128,7 +128,7 @@ def evaluationAdjunctionLeft (c : C) : (evaluation _ _).obj c ⊣ evaluationRigh
             intro f
             ext x
             dsimp
-            ext ⟨g⟩
+            ext g
             simp only [Discrete.functor_obj, NatTrans.naturality_assoc,
               evaluationRightAdjoint_obj_obj, evaluationRightAdjoint_obj_map, limit.lift_π,
               Fan.mk_pt, Fan.mk_π_app, Discrete.natTrans_app, Category.comp_id] } }

Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

@@ -60,18 +60,26 @@ 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
 
-noncomputable instance (priority := 100) PreservesLimits.preservesFiniteLimitsOfSize (F : C ⥤ D)
+-- Porting note: this is a dangerous instance as it has unbound universe variables.
+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.PreservesLimits.preservesFiniteLimitsOfSize
+#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.
+noncomputable instance (priority := 120) PreservesLimitsOfSize0.preservesFiniteLimits
+    (F : C ⥤ D) [PreservesLimitsOfSize.{0, 0} F] : PreservesFiniteLimits F :=
+  PreservesLimitsOfSize.preservesFiniteLimits F
 
 noncomputable instance (priority := 120) PreservesLimits.preservesFiniteLimits (F : C ⥤ D)
     [PreservesLimits F] : PreservesFiniteLimits F :=
-  PreservesLimits.preservesFiniteLimitsOfSize F
+  PreservesLimitsOfSize.preservesFiniteLimits F
 #align category_theory.limits.preserves_limits.preserves_finite_limits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits
 
+-- Porting note: is this unnecessary given the instance
+-- `PreservesLimitsOfSize0.preservesFiniteLimits`?
 /-- We can always derive `PreservesFiniteLimits C` by showing that we are preserving limits at an
 arbitrary universe. -/
 def preservesFiniteLimitsOfPreservesFiniteLimitsOfSize (F : C ⥤ D)
@@ -120,15 +128,27 @@ 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
 
-noncomputable instance (priority := 100) PreservesColimits.preservesFiniteColimits (F : C ⥤ D)
+-- Porting note: this is a dangerous instance as it has unbound universe variables.
+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
+
+-- Porting note: added as a specialization of the dangerous instance above.
+noncomputable instance (priority := 120) PreservesColimitsOfSize0.preservesFiniteColimits
+    (F : C ⥤ D) [PreservesColimitsOfSize.{0, 0} F] : PreservesFiniteColimits F :=
+  PreservesColimitsOfSize.preservesFiniteColimits F
+
+noncomputable instance (priority := 120) PreservesColimits.preservesFiniteColimits (F : C ⥤ D)
+    [PreservesColimits F] : PreservesFiniteColimits F :=
+  PreservesColimitsOfSize.preservesFiniteColimits F
 #align category_theory.limits.preserves_colimits.preserves_finite_colimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits
 
-/-- We can always derive `PreservesFiniteLimits C` by showing that we are preserving limits at an
-arbitrary universe. -/
+-- Porting note: is this unnecessary given the instance
+-- `PreservesColimitsOfSize0.preservesFiniteColimits`?
+/-- We can always derive `PreservesFiniteColimits C`
+by showing that we are preserving colimits at an arbitrary universe. -/
 def preservesFiniteColimitsOfPreservesFiniteColimitsOfSize (F : C ⥤ D)
     (h :
       ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), PreservesColimitsOfShape J F) :

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

@@ -587,13 +587,13 @@ def coprodIsCoprod (X Y : C) [HasBinaryCoproduct X Y] :
   ))
 #align category_theory.limits.coprod_is_coprod CategoryTheory.Limits.coprodIsCoprod
 
-@[ext]
+@[ext 1100]
 theorem prod.hom_ext {W X Y : C} [HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y}
     (h₁ : f ≫ prod.fst = g ≫ prod.fst) (h₂ : f ≫ prod.snd = g ≫ prod.snd) : f = g :=
   BinaryFan.IsLimit.hom_ext (limit.isLimit _) h₁ h₂
 #align category_theory.limits.prod.hom_ext CategoryTheory.Limits.prod.hom_ext
 
-@[ext]
+@[ext 1100]
 theorem coprod.hom_ext {W X Y : C} [HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W}
     (h₁ : coprod.inl ≫ f = coprod.inl ≫ g) (h₂ : coprod.inr ≫ f = coprod.inr ≫ g) : f = g :=
   BinaryCofan.IsColimit.hom_ext (colimit.isColimit _) h₁ h₂

Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

@@ -528,7 +528,7 @@ noncomputable def multiforkEquivPiFork : Multifork I ≌ Fork I.fstPiMap I.sndPi
       fun {K₁ K₂} f => by dsimp; ext; simp
   counitIso :=
     NatIso.ofComponents
-      (fun K => Fork.ext (Iso.refl _) (by dsimp; ext ⟨j⟩; dsimp; simp))
+      (fun K => Fork.ext (Iso.refl _) (by dsimp; ext j; dsimp; simp))
       fun {K₁ K₂} f => by dsimp; ext; simp
 #align category_theory.limits.multicospan_index.multifork_equiv_pi_fork CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork
 

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -158,6 +158,19 @@ abbrev Sigma.ι (f : β → C) [HasCoproduct f] (b : β) : f b ⟶ ∐ f :=
   colimit.ι (Discrete.functor f) (Discrete.mk b)
 #align category_theory.limits.sigma.ι CategoryTheory.Limits.Sigma.ι
 
+-- porting note: added the next two lemmas to ease automation; without these lemmas,
+-- `limit.hom_ext` would be applied, but the goal would involve terms
+-- in `Discete β` rather than `β` itself
+@[ext 1050]
+lemma Pi.hom_ext {f : β → C} [HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ f)
+    (h : ∀ (b : β), g₁ ≫ Pi.π f b = g₂ ≫ Pi.π f b) : g₁ = g₂ :=
+  limit.hom_ext (fun ⟨j⟩ => h j)
+
+@[ext 1050]
+lemma Sigma.hom_ext {f : β → C} [HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X)
+    (h : ∀ (b : β), Sigma.ι f b ≫ g₁ = Sigma.ι f b ≫ g₂ ) : g₁ = g₂ :=
+  colimit.hom_ext (fun ⟨j⟩ => h j)
+
 /-- The fan constructed of the projections from the product is limiting. -/
 def productIsProduct (f : β → C) [HasProduct f] : IsLimit (Fan.mk _ (Pi.π f)) :=
   IsLimit.ofIsoLimit (limit.isLimit (Discrete.functor f)) (Cones.ext (Iso.refl _) (by aesop_cat))
@@ -241,7 +254,7 @@ theorem piComparison_comp_π [HasProduct f] [HasProduct fun b => G.obj (f b)] (b
 @[reassoc (attr := simp)]
 theorem map_lift_piComparison [HasProduct f] [HasProduct fun b => G.obj (f b)] (P : C)
     (g : ∀ j, P ⟶ f j) : G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j) := by
-  ext ⟨j⟩
+  ext j
   simp only [Discrete.functor_obj, Category.assoc, piComparison_comp_π, ← G.map_comp,
     limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
 #align category_theory.limits.map_lift_pi_comparison CategoryTheory.Limits.map_lift_piComparison
@@ -263,7 +276,7 @@ theorem ι_comp_sigmaComparison [HasCoproduct f] [HasCoproduct fun b => G.obj (f
 theorem sigmaComparison_map_desc [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (P : C)
     (g : ∀ j, f j ⟶ P) :
     sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j) := by
-  ext ⟨j⟩
+  ext j
   simp only [Discrete.functor_obj, ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc,
     Cofan.mk_pt, Cofan.mk_ι_app]
 #align category_theory.limits.sigma_comparison_map_desc CategoryTheory.Limits.sigmaComparison_map_desc