chore(CategoryTheory/Limits): make Pi.mapIso a def (#38368)

Currently, `simp` unfolds `Pi.mapIso` which makes the general (co)limit API leak through. We also fix `Sigma.mapIso`, `Pi.map` and `Sigma.map`.

Author: chrisflav

Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean

@@ -161,9 +161,7 @@ def liftToFinsetColimIso : liftToFinset C α ⋙ colim ≅ colim :=
       ext J
       simp only [liftToFinset_obj_obj]
       ext j
-      simp only [liftToFinset, ι_colimMap_assoc, liftToFinsetObj_obj, Discrete.functor_obj_eq_as,
-        Discrete.natTrans_app, liftToFinsetColimIso_aux, liftToFinsetColimIso_aux_assoc,
-        ι_colimMap])
+      simp [liftToFinset, liftToFinsetColimIso_aux, liftToFinsetColimIso_aux_assoc])
 
 end
 
@@ -273,7 +271,7 @@ def liftToFinsetEvaluationIso (I : Finset (Discrete α)) :
     liftToFinset C α ⋙ (evaluation _ _).obj ⟨I⟩ ≅
     (Functor.whiskeringLeft _ _ _).obj (Discrete.functor (·.val)) ⋙ lim (J := Discrete I) :=
   NatIso.ofComponents (fun _ => HasLimit.isoOfNatIso (Discrete.natIso fun _ => Iso.refl _))
-    fun _ => by dsimp; ext; simp
+    fun _ => by dsimp; ext; simp [Pi.map]
 
 end ProductsFromFiniteCofiltered
 

Mathlib/CategoryTheory/Limits/FormalCoproducts/Cech.lean

@@ -142,9 +142,7 @@ lemma mapPower_comp (U : FormalCoproduct.{w} C) {α β γ : Type t}
   · cat_disch
   · dsimp
     ext
-    dsimp
-    simp only [Category.comp_id, Category.assoc, Pi.lift_π]
-    apply Pi.lift_π
+    simp [Function.comp_def]
 
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc]
@@ -155,9 +153,7 @@ lemma mapPower_powerMap {U V : FormalCoproduct.{w} C} (f : U ⟶ V)
   · cat_disch
   · dsimp
     ext
-    simp only [Function.comp_apply, limit.lift_map, Cone.postcompose, Fan.mk_pt, Category.comp_id,
-      Category.assoc, limit.lift_π, Fan.mk_π_app, Pi.map_π]
-    apply limit.lift_π
+    simp [Function.comp_def]
 
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc (attr := simp)]

Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

@@ -611,9 +611,9 @@ instance biproduct.map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p
   have : biproduct.map p =
       (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
     ext
-    simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
-      ι_colimMap_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app, colimit.ι_desc_assoc,
-      Cofan.mk_pt, Cofan.mk_ι_app, ι_π, ι_π_assoc]
+    simp only [map_π, ι_π_assoc, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
+      Sigma.ι_map_assoc, colimit.ι_desc_assoc, Discrete.functor_obj_eq_as, Cofan.mk_pt,
+      Cofan.mk_ι_app, ι_π]
     split
     all_goals simp_all
   rw [this]

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -325,13 +325,13 @@ def Cofan.isColimitTrans {X : α → C} (c : Cofan X) (hc : IsColimit c)
 /-- Construct a morphism between categorical products (indexed by the same type)
 from a family of morphisms between the factors.
 -/
-abbrev Pi.map {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g :=
+def Pi.map {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g :=
   limMap (Discrete.natTrans fun X => p X.as)
 
 set_option backward.isDefEq.respectTransparency false in
-@[reassoc (attr := simp high), elementwise nosimp]
+@[reassoc (attr := simp), elementwise nosimp]
 lemma Pi.map_π {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) (b : β) :
-    Pi.map p ≫ Pi.π g b = Pi.π f b ≫ p b := by simp
+    Pi.map p ≫ Pi.π g b = Pi.π f b ≫ p b := by simp [Pi.map]
 
 @[simp]
 lemma Pi.map_id {f : α → C} [HasProduct f] : Pi.map (fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f) := by
@@ -390,9 +390,19 @@ lemma Pi.map'_eq {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] {p
 /-- Construct an isomorphism between categorical products (indexed by the same type)
 from a family of isomorphisms between the factors.
 -/
-abbrev Pi.mapIso {f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∏ᶜ f ≅ ∏ᶜ g :=
+def Pi.mapIso {f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∏ᶜ f ≅ ∏ᶜ g :=
   lim.mapIso (Discrete.natIso fun X => p X.as)
 
+@[reassoc (attr := simp)]
+lemma Pi.mapIso_hom_π {f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ≅ g b) (b : β) :
+    (Pi.mapIso p).hom ≫ π _ _ = π _ _ ≫ (p b).hom :=
+  limMap_π _ _
+
+@[reassoc (attr := simp)]
+lemma Pi.mapIso_inv_π {f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ≅ g b) (b : β) :
+    (Pi.mapIso p).inv ≫ π _ _ = π _ _ ≫ (p b).inv :=
+  limMap_π _ _
+
 instance Pi.map_isIso {f g : β → C} [HasProductsOfShape β C] (p : ∀ b, f b ⟶ g b)
     [∀ b, IsIso <| p b] : IsIso <| Pi.map p :=
   inferInstanceAs (IsIso (Pi.mapIso (fun b ↦ asIso (p b))).hom)
@@ -445,14 +455,14 @@ end
 /-- Construct a morphism between categorical coproducts (indexed by the same type)
 from a family of morphisms between the factors.
 -/
-abbrev Sigma.map {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) :
+def Sigma.map {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) :
     ∐ f ⟶ ∐ g :=
   colimMap (Discrete.natTrans fun X => p X.as)
 
 set_option backward.isDefEq.respectTransparency false in
-@[reassoc (attr := simp high)]
+@[reassoc (attr := simp)]
 lemma Sigma.ι_map {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) (b : β) :
-    Sigma.ι f b ≫ Sigma.map p = p b ≫ Sigma.ι g b := by simp
+    Sigma.ι f b ≫ Sigma.map p = p b ≫ Sigma.ι g b := by simp [Sigma.map]
 
 @[simp]
 lemma Sigma.map_id {f : α → C} [HasCoproduct f] : Sigma.map (fun a => 𝟙 (f a)) = 𝟙 (∐ f) := by
@@ -514,9 +524,19 @@ lemma Sigma.map'_eq {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct
 /-- Construct an isomorphism between categorical coproducts (indexed by the same type)
 from a family of isomorphisms between the factors.
 -/
-abbrev Sigma.mapIso {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∐ f ≅ ∐ g :=
+def Sigma.mapIso {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ≅ g b) : ∐ f ≅ ∐ g :=
   colim.mapIso (Discrete.natIso fun X => p X.as)
 
+@[reassoc (attr := simp)]
+lemma Sigma.ι_mapIso_hom {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ≅ g b) (b : β) :
+    ι _ _ ≫ (Sigma.mapIso p).hom = (p b).hom ≫ ι _ _ :=
+  ι_colimMap _ _
+
+@[reassoc (attr := simp)]
+lemma Sigma.ι_mapIso_inv {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ≅ g b) (b : β) :
+    ι _ _ ≫ (Sigma.mapIso p).inv = (p b).inv ≫ ι _ _ :=
+  ι_colimMap _ _
+
 instance Sigma.map_isIso {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b ⟶ g b)
     [∀ b, IsIso <| p b] : IsIso (Sigma.map p) :=
   inferInstanceAs (IsIso (Sigma.mapIso (fun b ↦ asIso (p b))).hom)

Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean

@@ -86,7 +86,7 @@ lemma functorMap_commSq_aux {n m k : ℕ} (h : n ≤ m) (hh : ¬(k < m)) :
     rw [this, op_comp, Functor.map_comp]
     slice_lhs 2 4 => rw [ih]
     simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
-      functorMap, dite_eq_ite, limMap_π_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app]
+      functorMap, dite_eq_ite, Pi.map_π_assoc]
     split_ifs
     simp [dif_neg (by lia : ¬(k < m))]
 
@@ -129,10 +129,9 @@ noncomputable def cone : Cone (Functor.ofOpSequence (functorMap f)) where
         f m ≫ eqToHom (functorObj_eq_neg h).symm) (fun n ↦ ?_)
     apply Limits.Pi.hom_ext
     intro m
-    simp only [Functor.const_obj_obj, Functor.ofOpSequence_obj, homOfLE_leOfHom,
-      Functor.const_obj_map, Category.id_comp, limMap_π, Discrete.functor_obj_eq_as,
-      Discrete.natTrans_app, Functor.ofOpSequence_map_homOfLE_succ, functorMap, Category.assoc,
-      limMap_π_assoc]
+    simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, homOfLE_leOfHom,
+      Functor.const_obj_map, Category.id_comp, Pi.map_π, Functor.ofOpSequence_map_homOfLE_succ,
+      functorMap, Category.assoc, Pi.map_π_assoc]
     split
     · simp [dif_pos (by lia : m < n + 1)]
     · split
@@ -147,16 +146,14 @@ set_option backward.isDefEq.respectTransparency false in
 lemma cone_π_app_comp_Pi_π_pos (m n : ℕ) (h : n < m) : (cone f).π.app ⟨m⟩ ≫
     Pi.π (fun i ↦ if _ : i < m then M i else N i) n =
     Pi.π _ n ≫ eqToHom (functorObj_eq_pos h).symm := by
-  simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
-    Discrete.functor_obj_eq_as, Discrete.natTrans_app]
+  simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, Pi.map_π]
   rw [dif_pos h]
 
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc]
 lemma cone_π_app_comp_Pi_π_neg (m n : ℕ) (h : ¬(n < m)) : (cone f).π.app ⟨m⟩ ≫ Pi.π _ n =
     Pi.π _ n ≫ f n ≫ eqToHom (functorObj_eq_neg h).symm := by
-  simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
-    Discrete.functor_obj_eq_as, Discrete.natTrans_app]
+  simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, Pi.map_π]
   rw [dif_neg h]
 
 set_option backward.isDefEq.respectTransparency false in
@@ -196,8 +193,7 @@ noncomputable def isLimit : IsLimit (cone f) where
           rw [dif_pos h, dif_pos (by lia)]
         rw [← eqToHom_trans h₁ h₂]
         slice_lhs 2 4 => rw [ih (by lia)]
-        simp only [functorMap, dite_eq_ite, Pi.π, limMap_π_assoc, Discrete.functor_obj_eq_as,
-          Discrete.natTrans_app]
+        simp only [functorMap, dite_eq_ite, Pi.π, Pi.map_π_assoc]
         split_ifs
         rw [dif_pos (by lia)]
         simp

Mathlib/CategoryTheory/SmallObject/Construction.lean

@@ -255,9 +255,7 @@ lemma functorMap_comm :
     functorObjLeft f πX ≫ functorMapTgt f τ =
       functorMapSrc f τ ≫ functorObjLeft f πY := by
   ext ⟨i, t, b, w⟩
-  simp only [ι_colimMap_assoc, Discrete.natTrans_app, ι_colimMap,
-    ι_functorMapTgt f τ i t b w _ rfl,
-    ι_functorMapSrc_assoc f τ i t b w _ rfl]
+  simp [ι_functorMapTgt f τ i t b w _ rfl, ι_functorMapSrc_assoc f τ i t b w _ rfl]
 
 variable [HasPushout (functorObjTop f πX) (functorObjLeft f πX)]
   [HasPushout (functorObjTop f πY) (functorObjLeft f πY)]

Mathlib/CategoryTheory/Triangulated/Basic.lean

@@ -368,10 +368,6 @@ def productTriangle.π (j : J) :
   hom₁ := Pi.π _ j
   hom₂ := Pi.π _ j
   hom₃ := Pi.π _ j
-  comm₃ := by
-    dsimp
-    rw [← piComparison_comp_π, assoc, IsIso.inv_hom_id_assoc]
-    simp only [limMap_π, Discrete.natTrans_app]
 
 /-- The fan given by `productTriangle T`. -/
 @[simp]
@@ -411,9 +407,7 @@ lemma productTriangle.zero₃₁ [HasZeroMorphisms C]
   change _ ≫ (Pi.lift (fun j => Pi.π _ j ≫ (T j).mor₁))⟦(1 : ℤ)⟧' = 0
   rw [assoc, ← cancel_mono (piComparison _ _), zero_comp, assoc, assoc]
   ext j
-  simp only [map_lift_piComparison, assoc, limit.lift_π, Fan.mk_π_app, zero_comp,
-    Functor.map_comp, ← piComparison_comp_π_assoc, IsIso.inv_hom_id_assoc,
-    limMap_π_assoc, Discrete.natTrans_app, h j, comp_zero]
+  simp [h j]
 
 end
 

Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean

@@ -144,15 +144,11 @@ def diagram.isoOfIso (α : F ≅ G) : diagram F U ≅ diagram.{v'} G U :=
       rintro ⟨⟩ ⟨⟩ ⟨⟩
       · simp
       · dsimp
-        ext
-        simp only [leftRes, limit.lift_map, limit.lift_π, Cone.postcompose_obj_π,
-          NatTrans.comp_app, Fan.mk_π_app, Discrete.natIso_hom_app, Iso.app_hom, Category.assoc,
-          NatTrans.naturality, limMap_π_assoc]
+        refine Pi.hom_ext _ _ fun b ↦ ?_
+        simp [leftRes]
       · dsimp [diagram]
-        ext
-        simp only [rightRes, limit.lift_map, limit.lift_π, Cone.postcompose_obj_π,
-          NatTrans.comp_app, Fan.mk_π_app, Discrete.natIso_hom_app, Iso.app_hom, Category.assoc,
-          NatTrans.naturality, limMap_π_assoc]
+        refine Pi.hom_ext _ _ fun b ↦ ?_
+        simp [rightRes]
       · simp)
 
 set_option backward.isDefEq.respectTransparency false in
@@ -166,13 +162,9 @@ def fork.isoOfIso (α : F ≅ G) :
   fapply Fork.ext
   · apply α.app
   · dsimp
-    ext
+    refine Pi.hom_ext _ _ fun b ↦ ?_
     dsimp only [Fork.ι]
-    -- Ugh, `simp` can't unfold abbreviations.
-    simp only [res, diagram.isoOfIso, piOpens.isoOfIso, Cone.postcompose_obj_π,
-      NatTrans.comp_app, fork_π_app_walkingParallelPair_zero, NatIso.ofComponents_inv_app,
-      Functor.mapIso_inv, lim_map, limit.lift_map, Category.assoc, limit.lift_π, Fan.mk_π_app,
-      Discrete.natIso_inv_app, Iso.app_inv, NatTrans.naturality, Iso.hom_inv_id_app_assoc]
+    simp [res, diagram.isoOfIso]
 
 end SheafConditionEqualizerProducts