refactor(CategoryTheory/Shift): export Functor.CommShift.commShiftIso (#31504)

The isomorphism of commutation with shifts `Functor.CommShift.iso` is renamed `Functor.CommShift.commShiftIso` and exported as `Functor.commShiftIso` (which was a definition previously). This allows to generate a few equational lemmas automatically. A few `erw` are also removed.

Author: joelriou

Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean

@@ -231,14 +231,14 @@ def mapCochainComplexShiftIso (n : ℤ) :
 
 instance commShiftMapCochainComplex :
     (F.mapHomologicalComplex (ComplexShape.up ℤ)).CommShift ℤ where
-  iso := F.mapCochainComplexShiftIso
-  zero := by
+  commShiftIso := F.mapCochainComplexShiftIso
+  commShiftIso_zero := by
     ext
     rw [CommShift.isoZero_hom_app]
     dsimp
     simp only [CochainComplex.shiftFunctorZero_inv_app_f, CochainComplex.shiftFunctorZero_hom_app_f,
        HomologicalComplex.XIsoOfEq, eqToIso, eqToHom_map, eqToHom_trans, eqToHom_refl]
-  add := fun a b => by
+  commShiftIso_add := fun a b => by
     ext
     rw [CommShift.isoAdd_hom_app]
     dsimp

Mathlib/CategoryTheory/Shift/Adjunction.lean

@@ -227,17 +227,15 @@ namespace CommShift
 
 
 /-- Constructor for `Adjunction.CommShift`. -/
-lemma mk' (h : NatTrans.CommShift adj.unit A) :
+lemma mk' (_ : NatTrans.CommShift adj.unit A) :
     adj.CommShift A where
   commShift_counit := ⟨fun a ↦ by
     ext
     simp only [Functor.comp_obj, Functor.id_obj, NatTrans.comp_app,
       Functor.commShiftIso_comp_hom_app, Functor.whiskerRight_app, assoc, Functor.whiskerLeft_app,
       Functor.commShiftIso_id_hom_app, comp_id]
     refine (compatibilityCounit_of_compatibilityUnit adj _ _ (fun X ↦ ?_) _).symm
-    simpa only [NatTrans.comp_app,
-      Functor.commShiftIso_id_hom_app, Functor.whiskerRight_app, id_comp,
-      Functor.commShiftIso_comp_hom_app] using congr_app (h.shift_comm a) X⟩
+    simpa [Functor.commShiftIso_comp_hom_app] using NatTrans.shift_app_comm adj.unit a X⟩
 
 variable [adj.CommShift A]
 
@@ -370,15 +368,15 @@ open RightAdjointCommShift in
 Given an adjunction `F ⊣ G` and a `CommShift` structure on `F`, this constructs
 the unique compatible `CommShift` structure on `G`.
 -/
-@[simps]
+@[simps -isSimp]
 noncomputable def rightAdjointCommShift [F.CommShift A] : G.CommShift A where
-  iso a := iso adj a
-  zero := by
+  commShiftIso a := iso adj a
+  commShiftIso_zero := by
     refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso 0) _ _
       (compatibilityUnit_iso adj 0) ?_
     rw [F.commShiftIso_zero]
     exact CommShift.compatibilityUnit_isoZero adj
-  add a b := by
+  commShiftIso_add a b := by
     refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b)) _ _
       (compatibilityUnit_iso adj (a + b)) ?_
     rw [F.commShiftIso_add]
@@ -454,15 +452,15 @@ open LeftAdjointCommShift in
 Given an adjunction `F ⊣ G` and a `CommShift` structure on `G`, this constructs
 the unique compatible `CommShift` structure on `F`.
 -/
-@[simps]
+@[simps -isSimp]
 noncomputable def leftAdjointCommShift [G.CommShift A] : F.CommShift A where
-  iso a := iso adj a
-  zero := by
+  commShiftIso a := iso adj a
+  commShiftIso_zero := by
     refine CommShift.compatibilityUnit_unique_left adj _ _ (G.commShiftIso 0)
       (compatibilityUnit_iso adj 0) ?_
     rw [G.commShiftIso_zero]
     exact CommShift.compatibilityUnit_isoZero adj
-  add a b := by
+  commShiftIso_add a b := by
     refine CommShift.compatibilityUnit_unique_left adj _ _ (G.commShiftIso (a + b))
       (compatibilityUnit_iso adj (a + b)) ?_
     rw [G.commShiftIso_add]

Mathlib/CategoryTheory/Shift/CommShift.lean

@@ -104,24 +104,25 @@ end CommShift
 /-- A functor `F` commutes with the shift by a monoid `A` if it is equipped with
 commutation isomorphisms with the shifts by all `a : A`, and these isomorphisms
 satisfy coherence properties with respect to `0 : A` and the addition in `A`. -/
-class CommShift where
+class CommShift (F : C ⥤ D) (A : Type*) [AddMonoid A] [HasShift C A] [HasShift D A] where
   /-- The commutation isomorphisms for all `a`-shifts this functor is equipped with -/
-  iso (a : A) : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
-  zero : iso 0 = CommShift.isoZero F A := by cat_disch
-  add (a b : A) : iso (a + b) = CommShift.isoAdd (iso a) (iso b) := by cat_disch
+  commShiftIso (F) (a : A) : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
+  commShiftIso_zero (F) (A) : commShiftIso 0 = CommShift.isoZero F A := by cat_disch
+  commShiftIso_add (F) (a b : A) :
+    commShiftIso (a + b) = CommShift.isoAdd (commShiftIso a) (commShiftIso b) := by cat_disch
 
 variable {A}
 
+export CommShift (commShiftIso commShiftIso_zero commShiftIso_add)
+
+@[deprecated (since := "2025-11-11")] alias CommShift.iso := commShiftIso
+@[deprecated (since := "2025-11-11")] alias CommShift.zero := commShiftIso_zero
+@[deprecated (since := "2025-11-11")] alias CommShift.add := commShiftIso_add
+
 section
 
 variable [F.CommShift A]
 
-/-- If a functor `F` commutes with the shift by `A` (i.e. `[F.CommShift A]`), then
-`F.commShiftIso a` is the given isomorphism `shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a`. -/
-def commShiftIso (a : A) :
-    shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a :=
-  CommShift.iso a
-
 -- Note: The following two lemmas are introduced in order to have more proofs work `by simp`.
 -- Indeed, `simp only [(F.commShiftIso a).hom.naturality f]` would almost never work because
 -- of the compositions of functors which appear in both the source and target of
@@ -139,23 +140,12 @@ lemma commShiftIso_inv_naturality {X Y : C} (f : X ⟶ Y) (a : A) :
       (F.commShiftIso a).inv.app X ≫ F.map (f⟦a⟧') :=
   (F.commShiftIso a).inv.naturality f
 
-variable (A)
-
-lemma commShiftIso_zero :
-    F.commShiftIso (0 : A) = CommShift.isoZero F A :=
-  CommShift.zero
-
+variable (A) in
 set_option linter.docPrime false in
 lemma commShiftIso_zero' (a : A) (h : a = 0) :
     F.commShiftIso a = CommShift.isoZero' F A a h := by
   subst h; rw [CommShift.isoZero'_eq_isoZero, commShiftIso_zero]
 
-variable {A}
-
-lemma commShiftIso_add (a b : A) :
-    F.commShiftIso (a + b) = CommShift.isoAdd (F.commShiftIso a) (F.commShiftIso b) :=
-  CommShift.add a b
-
 lemma commShiftIso_add' {a b c : A} (h : a + b = c) :
     F.commShiftIso c = CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b) := by
   subst h
@@ -166,19 +156,21 @@ end
 namespace CommShift
 
 variable (C) in
+@[simps! -isSimp commShiftIso_hom_app commShiftIso_inv_app]
 instance id : CommShift (𝟭 C) A where
-  iso := fun _ => rightUnitor _ ≪≫ (leftUnitor _).symm
+  commShiftIso := fun _ => rightUnitor _ ≪≫ (leftUnitor _).symm
 
+@[simps! -isSimp commShiftIso_hom_app commShiftIso_inv_app]
 instance comp [F.CommShift A] [G.CommShift A] : (F ⋙ G).CommShift A where
-  iso a := (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (F.commShiftIso a) _ ≪≫
+  commShiftIso a := (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (F.commShiftIso a) _ ≪≫
     Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (G.commShiftIso a) ≪≫
     (Functor.associator _ _ _).symm
-  zero := by
+  commShiftIso_zero := by
     ext X
     dsimp
     simp only [id_comp, comp_id, commShiftIso_zero, isoZero_hom_app, ← Functor.map_comp_assoc,
       assoc, Iso.inv_hom_id_app, id_obj, comp_map, comp_obj]
-  add := fun a b => by
+  commShiftIso_add := fun a b => by
     ext X
     dsimp
     simp only [commShiftIso_add, isoAdd_hom_app]
@@ -188,23 +180,12 @@ instance comp [F.CommShift A] [G.CommShift A] : (F ⋙ G).CommShift A where
 
 end CommShift
 
-@[simp]
-lemma commShiftIso_id_hom_app (a : A) (X : C) :
-    (commShiftIso (𝟭 C) a).hom.app X = 𝟙 _ := comp_id _
-
-@[simp]
-lemma commShiftIso_id_inv_app (a : A) (X : C) :
-    (commShiftIso (𝟭 C) a).inv.app X = 𝟙 _ := comp_id _
-
-lemma commShiftIso_comp_hom_app [F.CommShift A] [G.CommShift A] (a : A) (X : C) :
-    (commShiftIso (F ⋙ G) a).hom.app X =
-      G.map ((commShiftIso F a).hom.app X) ≫ (commShiftIso G a).hom.app (F.obj X) := by
-  simp [commShiftIso, CommShift.iso]
+alias commShiftIso_id_hom_app := CommShift.id_commShiftIso_hom_app
+alias commShiftIso_id_inv_app := CommShift.id_commShiftIso_inv_app
+alias commShiftIso_comp_hom_app := CommShift.comp_commShiftIso_hom_app
+alias commShiftIso_comp_inv_app := CommShift.comp_commShiftIso_inv_app
 
-lemma commShiftIso_comp_inv_app [F.CommShift A] [G.CommShift A] (a : A) (X : C) :
-    (commShiftIso (F ⋙ G) a).inv.app X =
-      (commShiftIso G a).inv.app (F.obj X) ≫ G.map ((commShiftIso F a).inv.app X) := by
-  simp [commShiftIso, CommShift.iso]
+attribute [simp] commShiftIso_id_hom_app commShiftIso_id_inv_app
 
 variable {B}
 
@@ -354,16 +335,13 @@ variable {C D E : Type*} [Category C] [Category D]
 
 /-- If `e : F ≅ G` is an isomorphism of functors and if `F` commutes with the
 shift, then `G` also commutes with the shift. -/
+@[simps! -isSimp commShiftIso_hom_app commShiftIso_inv_app]
 def ofIso : G.CommShift A where
-  iso a := isoWhiskerLeft _ e.symm ≪≫ F.commShiftIso a ≪≫ isoWhiskerRight e _
-  zero := by
+  commShiftIso a := isoWhiskerLeft _ e.symm ≪≫ F.commShiftIso a ≪≫ isoWhiskerRight e _
+  commShiftIso_zero := by
     ext X
-    simp only [comp_obj, F.commShiftIso_zero A, Iso.trans_hom, isoWhiskerLeft_hom,
-      Iso.symm_hom, isoWhiskerRight_hom, NatTrans.comp_app, whiskerLeft_app,
-      isoZero_hom_app, whiskerRight_app, assoc]
-    erw [← e.inv.naturality_assoc, ← NatTrans.naturality,
-      e.inv_hom_id_app_assoc]
-  add a b := by
+    simp [F.commShiftIso_zero, ← NatTrans.naturality]
+  commShiftIso_add a b := by
     ext X
     simp only [comp_obj, F.commShiftIso_add, Iso.trans_hom, isoWhiskerLeft_hom,
       Iso.symm_hom, isoWhiskerRight_hom, NatTrans.comp_app, whiskerLeft_app,
@@ -376,9 +354,7 @@ lemma ofIso_compatibility :
     letI := ofIso e A
     NatTrans.CommShift e.hom A := by
   letI := ofIso e A
-  refine ⟨fun a => ?_⟩
-  dsimp [commShiftIso, ofIso]
-  rw [← whiskerLeft_comp_assoc, e.hom_inv_id, whiskerLeft_id', id_comp]
+  exact ⟨fun a => by ext; simp [ofIso_commShiftIso_hom_app]⟩
 
 end CommShift
 

Mathlib/CategoryTheory/Shift/Induced.lean

@@ -209,20 +209,21 @@ noncomputable def Functor.CommShift.ofInduced :
     F.CommShift A := by
   letI := HasShift.induced F A s i
   exact
-    { iso := fun a => (i a).symm
-      zero := by
+    { commShiftIso := fun a => (i a).symm
+      commShiftIso_zero := by
         ext X
         dsimp
         simp only [isoZero_hom_app, shiftFunctorZero_inv_app_obj_of_induced,
           ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-      add := fun a b => by
+      commShiftIso_add := fun a b => by
         ext X
         dsimp
         simp only [isoAdd_hom_app, Iso.symm_hom, shiftFunctorAdd_inv_app_obj_of_induced,
           shiftFunctor_of_induced]
-        erw [← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
-          Category.id_comp, Iso.inv_hom_id_app_assoc, ← F.map_comp_assoc, Iso.hom_inv_id_app,
-          F.map_id, Category.id_comp] }
+        rw [← Functor.map_comp_assoc, Iso.inv_hom_id_app]
+        dsimp
+        rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
+          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp] }
 
 lemma Functor.commShiftIso_eq_ofInduced (a : A) :
     letI := HasShift.induced F A s i

Mathlib/CategoryTheory/Shift/Localization.lean

@@ -167,8 +167,8 @@ end commShiftOfLocalization
 is induced by a functor which commutes with the shift, then
 this functor commutes with the shift. -/
 noncomputable def commShiftOfLocalization : F'.CommShift A where
-  iso := commShiftOfLocalization.iso L W F F'
-  zero := by
+  commShiftIso := commShiftOfLocalization.iso L W F F'
+  commShiftIso_zero := by
     ext1
     apply natTrans_ext L W
     intro X
@@ -179,7 +179,7 @@ noncomputable def commShiftOfLocalization : F'.CommShift A where
     dsimp
     simp only [← Functor.map_comp_assoc, ← Functor.map_comp,
       Iso.inv_hom_id_app, id_obj, map_id, Category.id_comp, Iso.hom_inv_id_app_assoc]
-  add a b := by
+  commShiftIso_add a b := by
     ext1
     apply natTrans_ext L W
     intro X

Mathlib/CategoryTheory/Shift/Opposite.lean

@@ -77,9 +77,7 @@ with the naive shift: `shiftFunctor (OppositeShift C A) n` is `(shiftFunctor C n
 @[nolint unusedArguments]
 def OppositeShift (A : Type*) [AddMonoid A] [HasShift C A] := Cᵒᵖ
 
-instance : Category (OppositeShift C A) := by
-  dsimp only [OppositeShift]
-  infer_instance
+instance : Category (OppositeShift C A) := inferInstanceAs (Category Cᵒᵖ)
 
 noncomputable instance : HasShift (OppositeShift C A) A :=
   hasShiftMk Cᵒᵖ A (HasShift.mkShiftCoreOp C A)
@@ -88,9 +86,8 @@ instance [HasZeroObject C] : HasZeroObject (OppositeShift C A) := by
   dsimp only [OppositeShift]
   infer_instance
 
-instance [Preadditive C] : Preadditive (OppositeShift C A) := by
-  dsimp only [OppositeShift]
-  infer_instance
+instance [Preadditive C] : Preadditive (OppositeShift C A) :=
+  inferInstanceAs (Preadditive Cᵒᵖ)
 
 instance [Preadditive C] (n : A) [(shiftFunctor C n).Additive] :
     (shiftFunctor (OppositeShift C A) n).Additive := by
@@ -166,15 +163,15 @@ Given a `CommShift` structure on `F`, this is the corresponding `CommShift` stru
 -/
 noncomputable instance commShiftOp [CommShift F A] :
     CommShift (OppositeShift.functor A F) A where
-  iso a := (NatIso.op (F.commShiftIso a)).symm
-  zero := by
+  commShiftIso a := (NatIso.op (F.commShiftIso a)).symm
+  commShiftIso_zero := by
     rw [commShiftIso_zero]
     ext
     simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app,
       CommShift.isoZero_inv_app, op_comp, CommShift.isoZero_hom_app]
     erw [oppositeShiftFunctorZero_inv_app, oppositeShiftFunctorZero_hom_app]
     rfl
-  add a b := by
+  commShiftIso_add a b := by
     rw [commShiftIso_add]
     ext
     simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app,
@@ -189,18 +186,18 @@ lemma commShiftOp_iso_eq [CommShift F A] (a : A) :
 Given a `CommShift` structure on `OppositeShift.functor F` (for the naive shifts on the opposite
 categories), this is the corresponding `CommShift` structure on `F`.
 -/
-@[simps]
+@[simps -isSimp]
 noncomputable def commShiftUnop
     [CommShift (OppositeShift.functor A F) A] : CommShift F A where
-  iso a := NatIso.removeOp ((OppositeShift.functor A F).commShiftIso a).symm
-  zero := by
+  commShiftIso a := NatIso.removeOp ((OppositeShift.functor A F).commShiftIso a).symm
+  commShiftIso_zero := by
     rw [commShiftIso_zero]
     ext
     simp only [comp_obj, NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app, op_obj,
       CommShift.isoZero_inv_app, unop_comp, CommShift.isoZero_hom_app]
     erw [oppositeShiftFunctorZero_hom_app, oppositeShiftFunctorZero_inv_app]
     rfl
-  add a b := by
+  commShiftIso_add a b := by
     rw [commShiftIso_add]
     ext
     simp only [comp_obj, NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app, op_obj,
@@ -244,7 +241,7 @@ instance : NatTrans.CommShift (OppositeShift.natIsoId C A).hom A where
   shift_comm _ := by
     ext
     dsimp [OppositeShift.natIsoId, Functor.commShiftOp_iso_eq]
-    simp only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, Functor.map_id,
+    simp only [Functor.commShiftIso_id_hom_app, Functor.map_id,
       comp_id, Functor.commShiftIso_id_inv_app, CategoryTheory.op_id, id_comp]
     rfl
 

Mathlib/CategoryTheory/Shift/Pullback.lean

@@ -161,16 +161,16 @@ namespace Functor
 commutes with their pullbacks by an additive map `φ`.
 -/
 noncomputable instance commShiftPullback : (PullbackShift.functor φ F).CommShift A where
-  iso a := isoWhiskerRight (pullbackShiftIso C φ a (φ a) rfl) F ≪≫
+  commShiftIso a := isoWhiskerRight (pullbackShiftIso C φ a (φ a) rfl) F ≪≫
     F.commShiftIso (φ a) ≪≫ isoWhiskerLeft _  (pullbackShiftIso D φ a (φ a) rfl).symm
-  zero := by
+  commShiftIso_zero := by
     ext
     dsimp
     simp only [F.commShiftIso_zero' (A := B) (φ 0) (by rw [map_zero]), CommShift.isoZero'_hom_app,
       assoc, CommShift.isoZero_hom_app, pullbackShiftFunctorZero'_hom_app, map_comp,
       pullbackShiftFunctorZero'_inv_app]
     rfl
-  add _ _ := by
+  commShiftIso_add _ _ := by
     ext
     simp only [PullbackShift.functor, comp_obj, Iso.trans_hom, isoWhiskerRight_hom,
       isoWhiskerLeft_hom, Iso.symm_hom, NatTrans.comp_app, whiskerRight_app, whiskerLeft_app,