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

def CategoryTheory.ShiftedHom {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] (X Y : C) (m : M) : Type u_5

In a category C equipped with a shift by an additive monoid, this is the type of morphisms X ⟶ (Y⟦n⟧) for m : M.

instance CategoryTheory.instAddCommGroupShiftedHomOfPreadditive {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] [Preadditive C] (X Y : C) (n : M) : AddCommGroup (ShiftedHom X Y n)

noncomputable def CategoryTheory.ShiftedHom.comp {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b) (h : b + a = c) : ShiftedHom X Z c

The composition of f : X ⟶ Y⟦a⟧ and g : Y ⟶ Z⟦b⟧, as a morphism X ⟶ Z⟦c⟧ when b + a = c.

theorem CategoryTheory.ShiftedHom.comp_assoc {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z T : C} {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 γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

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 : ℕ.

noncomputable def CategoryTheory.ShiftedHom.mk₀ {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) : ShiftedHom X Y m₀

The element of ShiftedHom X Y m₀ (when m₀ = 0) attached to a morphism X ⟶ Y.

noncomputable def CategoryTheory.ShiftedHom.homEquiv {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) : (X ⟶ Y) ≃ ShiftedHom X Y m₀

The bijection (X ⟶ Y) ≃ ShiftedHom X Y m₀ when m₀ = 0.

@[simp]

theorem CategoryTheory.ShiftedHom.homEquiv_apply {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) : (homEquiv m₀ hm₀) f = mk₀ m₀ hm₀ f

theorem CategoryTheory.ShiftedHom.mk₀_comp {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) {a : M} (g : ShiftedHom Y Z a) : (mk₀ m₀ hm₀ f).comp g ⋯ = CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.ShiftedHom.mk₀_id_comp {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) {a : M} (f : ShiftedHom X Y a) : (mk₀ m₀ hm₀ (CategoryStruct.id X)).comp f ⋯ = f

theorem CategoryTheory.ShiftedHom.comp_mk₀ {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) : f.comp (mk₀ m₀ hm₀ g) ⋯ = CategoryStruct.comp f ((shiftFunctor C a).map g)

@[simp]

theorem CategoryTheory.ShiftedHom.comp_mk₀_id {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) : f.comp (mk₀ m₀ hm₀ (CategoryStruct.id Y)) ⋯ = f

@[simp]

theorem CategoryTheory.ShiftedHom.mk₀_comp_mk₀ {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {a b c : M} (h : b + a = c) (ha : a = 0) (hb : b = 0) : (mk₀ a ha f).comp (mk₀ b hb g) h = mk₀ c ⋯ (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.ShiftedHom.mk₀_comp_mk₀_assoc {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) {a : M} (ha : a = 0) {d : M} (h : ShiftedHom Z T d) : (mk₀ a ha f).comp ((mk₀ a ha g).comp h ⋯) ⋯ = (mk₀ a ha (CategoryStruct.comp f g)).comp h ⋯

@[simp]

theorem CategoryTheory.ShiftedHom.mk₀_zero {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] (X Y : C) [Preadditive C] (m₀ : M) (hm₀ : m₀ = 0) : mk₀ m₀ hm₀ 0 = 0

@[simp]

theorem CategoryTheory.ShiftedHom.comp_add {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] [∀ (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

@[simp]

theorem CategoryTheory.ShiftedHom.add_comp {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] {a b c : M} (α₁ α₂ : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) : (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

@[simp]

theorem CategoryTheory.ShiftedHom.comp_neg {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] [∀ (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

@[simp]

theorem CategoryTheory.ShiftedHom.neg_comp {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] {a b c : M} (α : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) : (-α).comp β h = -α.comp β h

@[simp]

theorem CategoryTheory.ShiftedHom.comp_zero {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (Z : C) [Preadditive C] [∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms] {a : M} (β : ShiftedHom X Y a) {b c : M} (h : b + a = c) : β.comp 0 h = 0

@[simp]

theorem CategoryTheory.ShiftedHom.zero_comp {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] (X : C) {Y Z : C} [Preadditive C] (a : M) {b c : M} (β : ShiftedHom Y Z b) (h : b + a = c) : comp 0 β h = 0

def CategoryTheory.ShiftedHom.map {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} {a : M} (f : ShiftedHom X Y a) (F : Functor C D) [F.CommShift M] : ShiftedHom (F.obj X) (F.obj Y) a

The action on ShiftedHom of a functor which commutes with the shift.

@[simp]

theorem CategoryTheory.ShiftedHom.id_map {C : Type u_1} [Category.{u_5, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} {a : M} (f : ShiftedHom X Y a) : f.map (Functor.id C) = f

theorem CategoryTheory.ShiftedHom.comp_map {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {E : Type u_3} [Category.{u_7, u_3} E] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] [HasShift E M] {X Y : C} {a : M} (f : ShiftedHom X Y a) (F : Functor C D) [F.CommShift M] (G : Functor D E) [G.CommShift M] : f.map (F.comp G) = (f.map F).map G

theorem CategoryTheory.ShiftedHom.map_comp {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y Z : C} {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b) (h : b + a = c) (F : Functor C D) [F.CommShift M] : (f.comp g h).map F = (f.map F).comp (g.map F) h