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} [CategoryTheory.Category.{u_3, u_1} C] {M : Type u_2} [AddMonoid M] [CategoryTheory.HasShift C M] (X : C) (Y : C) (m : M) : Type u_3

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

Equations

• CategoryTheory.ShiftedHom X Y m = (X ⟶ (CategoryTheory.shiftFunctor C m).obj Y)

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

Equations

• CategoryTheory.instAddCommGroupShiftedHomOfPreadditive X Y n = id inferInstance

noncomputable def CategoryTheory.ShiftedHom.comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {M : Type u_2} [AddMonoid M] [CategoryTheory.HasShift C M] {X : C} {Y : C} {Z : C} {a : M} {b : M} {c : M} (f : CategoryTheory.ShiftedHom X Y a) (g : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c) : CategoryTheory.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.

Equations

• f.comp g h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map g) ((CategoryTheory.shiftFunctorAdd' C b a c h).inv.app Z))

theorem CategoryTheory.ShiftedHom.comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {M : Type u_2} [AddMonoid M] [CategoryTheory.HasShift C M] {X : C} {Y : C} {Z : C} {T : C} {a₁ : M} {a₂ : M} {a₃ : M} {a₁₂ : M} {a₂₃ : M} {a : M} (α : CategoryTheory.ShiftedHom X Y a₁) (β : CategoryTheory.ShiftedHom Y Z a₂) (γ : CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] {M : Type u_2} [AddMonoid M] [CategoryTheory.HasShift C M] {X : C} {Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) : CategoryTheory.ShiftedHom X Y m₀

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

Equations

• CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorZero' C m₀ hm₀).inv.app Y)

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShiftedHom.comp_add {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {M : Type u_2} [AddMonoid M] [CategoryTheory.HasShift C M] {X : C} {Y : C} {Z : C} [CategoryTheory.Preadditive C] [∀ (a : M), (CategoryTheory.shiftFunctor C a).Additive] {a : M} {b : M} {c : M} (α : CategoryTheory.ShiftedHom X Y a) (β₁ : CategoryTheory.ShiftedHom Y Z b) (β₂ : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c) : α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

@[simp]

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

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

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