feat: shifted morphisms in categories with a shift (#13571)

Given a category `C` endowed with a shift by an additive monoid `M` and two objects `X` and `Y` in `C`, we consider the types `ShiftedHom X Y m` defined as `X ⟶ (Y⟦m⟧)` for all `m : M`, and the composition on these shifted hom.

Mathlib.lean

@@ -1584,6 +1584,7 @@ import Mathlib.CategoryTheory.Shift.Predicate
 import Mathlib.CategoryTheory.Shift.Pullback
 import Mathlib.CategoryTheory.Shift.Quotient
 import Mathlib.CategoryTheory.Shift.ShiftSequence
+import Mathlib.CategoryTheory.Shift.ShiftedHom
 import Mathlib.CategoryTheory.Shift.SingleFunctors
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Simple

Mathlib/CategoryTheory/Shift/Basic.lean

@@ -193,6 +193,11 @@ def shiftFunctorZero : shiftFunctor C (0 : A) ≅ 𝟭 C :=
   (shiftMonoidalFunctor C A).εIso.symm
 #align category_theory.shift_functor_zero CategoryTheory.shiftFunctorZero
 
+variable {A} in
+/-- Shifting by `a` such that `a = 0` identifies to the identity functor. -/
+def shiftFunctorZero' (a : A) (ha : a = 0) : shiftFunctor C a ≅ 𝟭 C :=
+  eqToIso (by rw [ha]) ≪≫ shiftFunctorZero C A
+
 variable {C A}
 
 lemma ShiftMkCore.shiftFunctor_eq (h : ShiftMkCore C A) (a : A) :

Mathlib/CategoryTheory/Shift/ShiftedHom.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Shift.Basic
+import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
+
+/-! Shifted morphisms
+
+Given a category `C` endowed with a shift by an additive monoid `M` and two
+objects `X` and `Y` in `C`, we consider the types `ShiftedHom X Y m`
+defined as `X ⟶ (Y⟦m⟧)` for all `m : M`, and the composition on these
+shifted hom.
+
+## TODO
+
+* redefine Ext-groups in abelian categories using `ShiftedHom` in the derived category.
+* study the `R`-module structures on `ShiftedHom` when `C` is `R`-linear
+
+-/
+
+namespace CategoryTheory
+
+open Category
+
+variable {C : Type*} [Category C]
+  {M : Type*} [AddMonoid M] [HasShift C M]
+
+/-- In a category `C` equipped with a shift by an additive monoid,
+this is the type of morphisms `X ⟶ (Y⟦n⟧)` for `m : M`.  -/
+def ShiftedHom (X Y : C) (m : M) : Type _ := X ⟶ (Y⟦m⟧)
+
+instance [Preadditive C] (X Y : C) (n : M) : AddCommGroup (ShiftedHom X Y n) := by
+  dsimp only [ShiftedHom]
+  infer_instance
+
+namespace ShiftedHom
+
+variable {X Y Z T : C}
+
+/-- The composition of `f : X ⟶ Y⟦a⟧` and `g : Y ⟶ Z⟦b⟧`, as a morphism `X ⟶ Z⟦c⟧`
+when `b + a = c`. -/
+noncomputable def comp {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b) (h : b + a = c) :
+    ShiftedHom X Z c :=
+  f ≫ g⟦a⟧' ≫ (shiftFunctorAdd' C b a c h).inv.app _
+
+lemma comp_assoc {a₁ a₂ a₃ a₁₂ a₂₃ a : M}
+    (α : ShiftedHom X Y a₁) (β : ShiftedHom Y Z a₂) (γ : ShiftedHom Z T a₃)
+    (h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) :
+    (α.comp β h₁₂).comp γ (show a₃ + a₁₂ = a by rw [← h₁₂, ← add_assoc, h]) =
+      α.comp (β.comp γ h₂₃) (by rw [← h₂₃, h]) := by
+  simp only [comp, assoc, Functor.map_comp,
+    shiftFunctorAdd'_assoc_inv_app a₃ a₂ a₁ a₂₃ a₁₂ a h₂₃ h₁₂ h,
+    ← NatTrans.naturality_assoc, Functor.comp_map]
+
+/-! In degree `0 : M`, shifted hom `ShiftedHom X Y 0` identify to morphisms `X ⟶ Y`.
+We generalize this to `m₀ : M` such that `m₀ : 0` as it shall be convenient when we
+apply this with `M := ℤ` and `m₀` the coercion of `0 : ℕ`. -/
+
+/-- The element of `ShiftedHom X Y m₀` (when `m₀ = 0`) attached to a morphism `X ⟶ Y`. -/
+noncomputable def mk₀ (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) : ShiftedHom X Y m₀ :=
+  f ≫ (shiftFunctorZero' C m₀ hm₀).inv.app Y
+
+/-- The bijection `(X ⟶ Y) ≃ ShiftedHom X Y m₀` when `m₀ = 0`. -/
+@[simps apply]
+noncomputable def homEquiv (m₀ : M) (hm₀ : m₀ = 0) : (X ⟶ Y) ≃ ShiftedHom X Y m₀ where
+  toFun f := mk₀ m₀ hm₀ f
+  invFun g := g ≫ (shiftFunctorZero' C m₀ hm₀).hom.app Y
+  left_inv f := by simp [mk₀]
+  right_inv g := by simp [mk₀]
+
+lemma mk₀_comp (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) {a : M} (g : ShiftedHom Y Z a) :
+    (mk₀ m₀ hm₀ f).comp g (by rw [hm₀, add_zero]) = f ≫ g := by
+  subst hm₀
+  simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero']
+
+@[simp]
+lemma mk₀_id_comp (m₀ : M) (hm₀ : m₀ = 0) {a : M} (f : ShiftedHom X Y a) :
+    (mk₀ m₀ hm₀ (𝟙 X)).comp f (by rw [hm₀, add_zero]) = f := by
+  simp [mk₀_comp]
+
+lemma comp_mk₀ {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) :
+    f.comp (mk₀ m₀ hm₀ g) (by rw [hm₀, zero_add]) = f ≫ g⟦a⟧' := by
+  subst hm₀
+  simp only [comp, shiftFunctorAdd'_zero_add_inv_app, mk₀, shiftFunctorZero',
+    eqToIso_refl, Iso.refl_trans, ← Functor.map_comp, assoc, Iso.inv_hom_id_app,
+    Functor.id_obj, comp_id]
+
+@[simp]
+lemma comp_mk₀_id {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) :
+    f.comp (mk₀ m₀ hm₀ (𝟙 Y)) (by rw [hm₀, zero_add]) = f := by
+  simp [comp_mk₀]
+
+section Preadditive
+
+variable [Preadditive C]
+
+@[simp]
+lemma comp_add [∀ (a : M), (shiftFunctor C a).Additive]
+    {a b c : M} (α : ShiftedHom X Y a) (β₁ β₂ : ShiftedHom Y Z b) (h : b + a = c) :
+    α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h := by
+  rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
+
+@[simp]
+lemma add_comp
+    {a b c : M} (α₁ α₂ : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
+    (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h := by
+  rw [comp, comp, comp, Preadditive.add_comp]
+
+variable (Z) in
+lemma comp_zero [∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms]
+    {a : M} (β : ShiftedHom X Y a) {b c : M} (h : b + a = c) :
+    β.comp (0 : ShiftedHom Y Z b) h = 0 := by
+  rw [comp, Functor.map_zero, Limits.zero_comp, Limits.comp_zero]
+
+variable (X) in
+lemma zero_comp (a : M) {b c : M} (β : ShiftedHom Y Z b) (h : b + a = c) :
+    (0 : ShiftedHom X Y a).comp β h = 0 := by
+  rw [comp, Limits.zero_comp]
+
+end Preadditive
+
+end ShiftedHom
+
+end CategoryTheory