[Merged by Bors] - feat: allow differential objects with shifts in an AddMonoidWithOne

Mathlib/Algebra/Homology/DifferentialObject.lean

@@ -34,7 +34,7 @@ namespace CategoryTheory.DifferentialObject
 
 variable {β : Type _} [AddCommGroup β] {b : β}
 variable {V : Type _} [Category V] [HasZeroMorphisms V]
-variable (X : DifferentialObject (GradedObjectWithShift b V))
+variable (X : DifferentialObject ℤ (GradedObjectWithShift b V))
 
 /-- Since `eqToHom` only preserves the fact that `X.X i = X.X j` but not `i = j`, this definition
 is used to aid the simplifier. -/
@@ -59,7 +59,7 @@ theorem objEqToHom_d {x y : β} (h : x = y) :
 theorem d_squared_apply : X.d x ≫ X.d _ = 0 := congr_fun X.d_squared _
 
 @[reassoc (attr := simp)]
-theorem eqToHom_f' {X Y : DifferentialObject (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}
+theorem eqToHom_f' {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}
     (h : x = y) : X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h := by cases h; simp
 #align homological_complex.eq_to_hom_f' CategoryTheory.DifferentialObject.eqToHom_f'
 
@@ -85,7 +85,7 @@ set_option maxHeartbeats 800000 in
 -/
 @[simps]
 def dgoToHomologicalComplex :
-    DifferentialObject (GradedObjectWithShift b V) ⥤
+    DifferentialObject ℤ (GradedObjectWithShift b V) ⥤
       HomologicalComplex V (ComplexShape.up' b) where
   obj X :=
     { X := fun i => X.obj i
@@ -112,7 +112,7 @@ def dgoToHomologicalComplex :
 @[simps]
 def homologicalComplexToDGO :
     HomologicalComplex V (ComplexShape.up' b) ⥤
-      DifferentialObject (GradedObjectWithShift b V) where
+      DifferentialObject ℤ (GradedObjectWithShift b V) where
   obj X :=
     { obj := fun i => X.X i
       d := fun i => X.d i _ }
@@ -123,7 +123,7 @@ def homologicalComplexToDGO :
 -/
 @[simps!]
 def dgoEquivHomologicalComplexUnitIso :
-    𝟭 (DifferentialObject (GradedObjectWithShift b V)) ≅
+    𝟭 (DifferentialObject ℤ (GradedObjectWithShift b V)) ≅
       dgoToHomologicalComplex b V ⋙ homologicalComplexToDGO b V :=
   NatIso.ofComponents (fun X =>
     { hom := { f := fun i => 𝟙 (X.obj i) }
@@ -146,7 +146,8 @@ to the category of homological complexes in `V`.
 -/
 @[simps]
 def dgoEquivHomologicalComplex :
-    DifferentialObject (GradedObjectWithShift b V) ≌ HomologicalComplex V (ComplexShape.up' b) where
+    DifferentialObject ℤ (GradedObjectWithShift b V) ≌ 
+      HomologicalComplex V (ComplexShape.up' b) where
   functor := dgoToHomologicalComplex b V
   inverse := homologicalComplexToDGO b V
   unitIso := dgoEquivHomologicalComplexUnitIso b V

Mathlib/CategoryTheory/DifferentialObject.lean

@@ -28,10 +28,10 @@ universe v u
 
 namespace CategoryTheory
 
-variable (C : Type u) [Category.{v} C]
+variable (S : Type) [AddMonoidWithOne S] (C : Type u) [Category.{v} C]
 
--- TODO: generalize to `HasShift C A` for an arbitrary `[AddMonoid A]` `[One A]`.
-variable [HasZeroMorphisms C] [HasShift C ℤ]
+-- TODO: generalize to `HasShift C S` for an arbitrary `[AddMonoidWithOne S]`
+variable [HasZeroMorphisms C] [HasShift C S]
 
 /-- A differential object in a category with zero morphisms and a shift is
 an object `obj` equipped with
@@ -41,22 +41,22 @@ structure DifferentialObject where
   /-- The underlying object of a differential object. -/
   obj : C
   /-- The differential of a differential object. -/
-  d : obj ⟶ obj⟦(1 : ℤ)⟧
+  d : obj ⟶ obj⟦(1 : S)⟧
   /-- The differential `d` satisfies that `d² = 0`. -/
-  d_squared : d ≫ d⟦(1 : ℤ)⟧' = 0 := by aesop_cat
+  d_squared : d ≫ d⟦(1 : S)⟧' = 0 := by aesop_cat
 #align category_theory.differential_object CategoryTheory.DifferentialObject
 set_option linter.uppercaseLean3 false in
 #align category_theory.differential_object.X CategoryTheory.DifferentialObject.obj
 
 attribute [reassoc (attr := simp)] DifferentialObject.d_squared
 
-variable {C}
+variable {S C}
 
 namespace DifferentialObject
 
 /-- A morphism of differential objects is a morphism commuting with the differentials. -/
 @[ext] -- Porting note: Removed `nolint has_nonempty_instance`
-structure Hom (X Y : DifferentialObject C) where
+structure Hom (X Y : DifferentialObject S C) where
   /-- The morphism between underlying objects of the two differentiable objects. -/
   f : X.obj ⟶ Y.obj
   comm : X.d ≫ f⟦1⟧' = f ≫ Y.d := by aesop_cat
@@ -68,94 +68,98 @@ namespace Hom
 
 /-- The identity morphism of a differential object. -/
 @[simps]
-def id (X : DifferentialObject C) : Hom X X where
+def id (X : DifferentialObject S C) : Hom X X where
   f := 𝟙 X.obj
 #align category_theory.differential_object.hom.id CategoryTheory.DifferentialObject.Hom.id
 
 /-- The composition of morphisms of differential objects. -/
 @[simps]
-def comp {X Y Z : DifferentialObject C} (f : Hom X Y) (g : Hom Y Z) : Hom X Z where
+def comp {X Y Z : DifferentialObject S C} (f : Hom X Y) (g : Hom Y Z) : Hom X Z where
   f := f.f ≫ g.f
 #align category_theory.differential_object.hom.comp CategoryTheory.DifferentialObject.Hom.comp
 
 end Hom
 
-instance categoryOfDifferentialObjects : Category (DifferentialObject C) where
+instance categoryOfDifferentialObjects : Category (DifferentialObject S C) where
   Hom := Hom
   id := Hom.id
   comp f g := Hom.comp f g
 #align category_theory.differential_object.category_of_differential_objects CategoryTheory.DifferentialObject.categoryOfDifferentialObjects
 
 -- Porting note: added
 @[ext]
-theorem ext {A B : DifferentialObject C} {f g : A ⟶ B} (w : f.f = g.f := by aesop_cat) : f = g :=
+theorem ext {A B : DifferentialObject S C} {f g : A ⟶ B} (w : f.f = g.f := by aesop_cat) : f = g :=
   Hom.ext _ _ w
 
 @[simp]
-theorem id_f (X : DifferentialObject C) : (𝟙 X : X ⟶ X).f = 𝟙 X.obj := rfl
+theorem id_f (X : DifferentialObject S C) : (𝟙 X : X ⟶ X).f = 𝟙 X.obj := rfl
 #align category_theory.differential_object.id_f CategoryTheory.DifferentialObject.id_f
 
 @[simp]
-theorem comp_f {X Y Z : DifferentialObject C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).f = f.f ≫ g.f := rfl
+theorem comp_f {X Y Z : DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z) : 
+    (f ≫ g).f = f.f ≫ g.f := 
+  rfl
 #align category_theory.differential_object.comp_f CategoryTheory.DifferentialObject.comp_f
 
 @[simp]
-theorem eqToHom_f {X Y : DifferentialObject C} (h : X = Y) :
+theorem eqToHom_f {X Y : DifferentialObject S C} (h : X = Y) :
     Hom.f (eqToHom h) = eqToHom (congr_arg _ h) := by
   subst h
   rw [eqToHom_refl, eqToHom_refl]
   rfl
 #align category_theory.differential_object.eq_to_hom_f CategoryTheory.DifferentialObject.eqToHom_f
 
-variable (C)
+variable (S C)
 
 /-- The forgetful functor taking a differential object to its underlying object. -/
-def forget : DifferentialObject C ⥤ C where
+def forget : DifferentialObject S C ⥤ C where
   obj X := X.obj
   map f := f.f
 #align category_theory.differential_object.forget CategoryTheory.DifferentialObject.forget
 
-instance forget_faithful : Faithful (forget C) where
+instance forget_faithful : Faithful (forget S C) where
 #align category_theory.differential_object.forget_faithful CategoryTheory.DifferentialObject.forget_faithful
 
-instance {X Y : DifferentialObject C} : Zero (X ⟶ Y) := ⟨{f := 0}⟩
+variable [(shiftFunctor C (1 : S)).PreservesZeroMorphisms]
+
+instance {X Y : DifferentialObject S C} : Zero (X ⟶ Y) := ⟨{f := 0}⟩
 
-variable {C}
+variable {S C}
 
 @[simp]
-theorem zero_f (P Q : DifferentialObject C) : (0 : P ⟶ Q).f = 0 := rfl
+theorem zero_f (P Q : DifferentialObject S C) : (0 : P ⟶ Q).f = 0 := rfl
 #align category_theory.differential_object.zero_f CategoryTheory.DifferentialObject.zero_f
 
-instance hasZeroMorphisms : HasZeroMorphisms (DifferentialObject C) where
+instance hasZeroMorphisms : HasZeroMorphisms (DifferentialObject S C) where
 #align category_theory.differential_object.has_zero_morphisms CategoryTheory.DifferentialObject.hasZeroMorphisms
 
 /-- An isomorphism of differential objects gives an isomorphism of the underlying objects. -/
 @[simps]
-def isoApp {X Y : DifferentialObject C} (f : X ≅ Y) : X.obj ≅ Y.obj where
+def isoApp {X Y : DifferentialObject S C} (f : X ≅ Y) : X.obj ≅ Y.obj where
   hom := f.hom.f
   inv := f.inv.f
   hom_inv_id := by dsimp; rw [← comp_f, Iso.hom_inv_id, id_f]
   inv_hom_id := by dsimp; rw [← comp_f, Iso.inv_hom_id, id_f]
 #align category_theory.differential_object.iso_app CategoryTheory.DifferentialObject.isoApp
 
 @[simp]
-theorem isoApp_refl (X : DifferentialObject C) : isoApp (Iso.refl X) = Iso.refl X.obj := rfl
+theorem isoApp_refl (X : DifferentialObject S C) : isoApp (Iso.refl X) = Iso.refl X.obj := rfl
 #align category_theory.differential_object.iso_app_refl CategoryTheory.DifferentialObject.isoApp_refl
 
 @[simp]
-theorem isoApp_symm {X Y : DifferentialObject C} (f : X ≅ Y) : isoApp f.symm = (isoApp f).symm :=
+theorem isoApp_symm {X Y : DifferentialObject S C} (f : X ≅ Y) : isoApp f.symm = (isoApp f).symm :=
   rfl
 #align category_theory.differential_object.iso_app_symm CategoryTheory.DifferentialObject.isoApp_symm
 
 @[simp]
-theorem isoApp_trans {X Y Z : DifferentialObject C} (f : X ≅ Y) (g : Y ≅ Z) :
+theorem isoApp_trans {X Y Z : DifferentialObject S C} (f : X ≅ Y) (g : Y ≅ Z) :
     isoApp (f ≪≫ g) = isoApp f ≪≫ isoApp g := rfl
 #align category_theory.differential_object.iso_app_trans CategoryTheory.DifferentialObject.isoApp_trans
 
 /-- An isomorphism of differential objects can be constructed
 from an isomorphism of the underlying objects that commutes with the differentials. -/
 @[simps]
-def mkIso {X Y : DifferentialObject C} (f : X.obj ≅ Y.obj) (hf : X.d ≫ f.hom⟦1⟧' = f.hom ≫ Y.d) :
+def mkIso {X Y : DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : X.d ≫ f.hom⟦1⟧' = f.hom ≫ Y.d) :
     X ≅ Y where
   hom := ⟨f.hom, hf⟩
   inv := ⟨f.inv, by
@@ -174,19 +178,19 @@ universe v' u'
 
 variable (D : Type u') [Category.{v'} D]
 
-variable [HasZeroMorphisms D] [HasShift D ℤ]
+variable [HasZeroMorphisms D] [HasShift D S]
 
 /-- A functor `F : C ⥤ D` which commutes with shift functors on `C` and `D` and preserves zero
 morphisms can be lifted to a functor `DifferentialObject C ⥤ DifferentialObject D`. -/
 @[simps]
 def mapDifferentialObject (F : C ⥤ D)
-    (η : (shiftFunctor C (1 : ℤ)).comp F ⟶ F.comp (shiftFunctor D (1 : ℤ)))
-    (hF : ∀ c c', F.map (0 : c ⟶ c') = 0) : DifferentialObject C ⥤ DifferentialObject D where
+    (η : (shiftFunctor C (1 : S)).comp F ⟶ F.comp (shiftFunctor D (1 : S)))
+    (hF : ∀ c c', F.map (0 : c ⟶ c') = 0) : DifferentialObject S C ⥤ DifferentialObject S D where
   obj X :=
     { obj := F.obj X.obj
       d := F.map X.d ≫ η.app X.obj
       d_squared := by
-        rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : ℤ))]
+        rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : S))]
         slice_lhs 2 3 => rw [← η.naturality X.d]
         rw [Functor.comp_map]
         slice_lhs 1 2 => rw [← F.map_comp, X.d_squared, hF]
@@ -195,7 +199,7 @@ def mapDifferentialObject (F : C ⥤ D)
     { f := F.map f.f
       comm := by
         dsimp
-        slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : ℤ)), ← η.naturality f.f]
+        slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
         slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
         rw [Category.assoc] }
   map_id := by intros; ext; simp
@@ -210,13 +214,14 @@ namespace CategoryTheory
 
 namespace DifferentialObject
 
-variable (C : Type u) [Category.{v} C]
+variable (S : Type) [AddMonoidWithOne S] (C : Type u) [Category.{v} C]
 
-variable [HasZeroObject C] [HasZeroMorphisms C] [HasShift C ℤ]
+variable [HasZeroObject C] [HasZeroMorphisms C] [HasShift C S]
+variable [(shiftFunctor C (1 : S)).PreservesZeroMorphisms]
 
 open scoped ZeroObject
 
-instance hasZeroObject : HasZeroObject (DifferentialObject C) := by
+instance hasZeroObject : HasZeroObject (DifferentialObject S C) := by
   -- Porting note(https://github.com/leanprover-community/mathlib4/issues/4998): added `aesop_cat`
   -- Porting note: added `simp only [eq_iff_true_of_subsingleton]`
   refine' ⟨⟨⟨0, 0, by aesop_cat⟩, fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩,
@@ -228,15 +233,16 @@ end DifferentialObject
 
 namespace DifferentialObject
 
+variable (S : Type) [AddMonoidWithOne S]
 variable (C : Type (u + 1)) [LargeCategory C] [ConcreteCategory C] [HasZeroMorphisms C]
-  [HasShift C ℤ]
+variable [HasShift C S]
 
-instance concreteCategoryOfDifferentialObjects : ConcreteCategory (DifferentialObject C) where
-  forget := forget C ⋙ CategoryTheory.forget C
+instance concreteCategoryOfDifferentialObjects : ConcreteCategory (DifferentialObject S C) where
+  forget := forget S C ⋙ CategoryTheory.forget C
 #align category_theory.differential_object.concrete_category_of_differential_objects CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects
 
-instance : HasForget₂ (DifferentialObject C) C where
-  forget₂ := forget C
+instance : HasForget₂ (DifferentialObject S C) C where
+  forget₂ := forget S C
 
 end DifferentialObject
 
@@ -245,15 +251,15 @@ end DifferentialObject
 
 namespace DifferentialObject
 
-variable (C : Type u) [Category.{v} C]
+variable {S : Type} [AddCommGroupWithOne S] (C : Type u) [Category.{v} C]
 
-variable [HasZeroMorphisms C] [HasShift C ℤ]
+variable [HasZeroMorphisms C] [HasShift C S]
 
 noncomputable section
 
 /-- The shift functor on `DifferentialObject C`. -/
 @[simps]
-def shiftFunctor (n : ℤ) : DifferentialObject C ⥤ DifferentialObject C where
+def shiftFunctor (n : S) : DifferentialObject S C ⥤ DifferentialObject S C where
   obj X :=
     { obj := X.obj⟦n⟧
       d := X.d⟦n⟧' ≫ (shiftComm _ _ _).hom
@@ -271,9 +277,9 @@ def shiftFunctor (n : ℤ) : DifferentialObject C ⥤ DifferentialObject C where
   map_comp f g := by ext1; dsimp; rw [Functor.map_comp]
 #align category_theory.differential_object.shift_functor CategoryTheory.DifferentialObject.shiftFunctor
 
-/-- The shift functor on `DifferentialObject C` is additive. -/
+/-- The shift functor on `DifferentialObject S C` is additive. -/
 @[simps!]
-nonrec def shiftFunctorAdd (m n : ℤ) :
+nonrec def shiftFunctorAdd (m n : S) :
     shiftFunctor C (m + n) ≅ shiftFunctor C m ⋙ shiftFunctor C n := by
   refine' NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) _) (fun f => _)
   · dsimp
@@ -291,8 +297,8 @@ section
 
 /-- The shift by zero is naturally isomorphic to the identity. -/
 @[simps!]
-def shiftZero : shiftFunctor C 0 ≅ 𝟭 (DifferentialObject C) := by
-  refine' NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C ℤ).app X.obj) _) (fun f => _)
+def shiftZero : shiftFunctor C (0 : S) ≅ 𝟭 (DifferentialObject S C) := by
+  refine' NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C S).app X.obj) _) (fun f => _)
   · erw [← NatTrans.naturality]
     dsimp
     simp only [shiftFunctorZero_hom_app_shift, Category.assoc]
@@ -301,7 +307,7 @@ def shiftZero : shiftFunctor C 0 ≅ 𝟭 (DifferentialObject C) := by
 
 end
 
-instance : HasShift (DifferentialObject C) ℤ :=
+instance : HasShift (DifferentialObject S C) S :=
   hasShiftMk _ _
     { F := shiftFunctor C
       zero := shiftZero C