Shifting cochains

Let C be a preadditive category. Given two cochain complexes (indexed by ℤ), the type of cochains HomComplex.Cochain K L n of degree n was introduced in Mathlib.Algebra.Homology.HomotopyCategory.HomComplex. In this file, we study how these cochains behave with respect to the shift on the complexes K and L.

When n, a, n' are integers such that h : n' + a = n, we obtain rightShiftAddEquiv K L n a n' h : Cochain K L n ≃+ Cochain K (L⟦a⟧) n'. This definition does not involve signs, but the analogous definition of leftShiftAddEquiv K L n a n' h' : Cochain K L n ≃+ Cochain (K⟦a⟧) L n' when h' : n + a = n' does involve signs, as we follow the conventions appearing in the introduction of [Brian Conrad's book Grothendieck duality and base change][conrad2000].

References

• [Brian Conrad, Grothendieck duality and base change][conrad2000]

def CochainComplex.HomComplex.Cochain.rightShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'

The map Cochain K L n → Cochain K (L⟦a⟧) n' when n' + a = n.

Equations

• γ.rightShift a n' hn' = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + n' = q) => CategoryTheory.CategoryStruct.comp (γ.v p (p + n) ⋯) (L.shiftFunctorObjXIso a q (p + n) ⋯).inv

theorem CochainComplex.HomComplex.Cochain.rightShift_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p + n = p') : (γ.rightShift a n' hn').v p q hpq = CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a q p' ⋯).inv

def CochainComplex.HomComplex.Cochain.leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'

The map Cochain K L n → Cochain (K⟦a⟧) L n' when n + a = n'.

Equations

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

theorem CochainComplex.HomComplex.Cochain.leftShift_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p' + n = q) : (γ.leftShift a n' hn').v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' ⋯).hom (γ.v p' q hp')

def CochainComplex.HomComplex.Cochain.rightUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) : Cochain K L n

The map Cochain K (L⟦a⟧) n' → Cochain K L n when n' + a = n.

Equations

• γ.rightUnshift n hn = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + n = q) => CategoryTheory.CategoryStruct.comp (γ.v p (p + n') ⋯) (L.shiftFunctorObjXIso a (p + n') q ⋯).hom

theorem CochainComplex.HomComplex.Cochain.rightUnshift_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p + n' = p') : (γ.rightUnshift n hn).v p q hpq = CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a p' q ⋯).hom

def CochainComplex.HomComplex.Cochain.leftUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') : Cochain K L n

The map Cochain (K⟦a⟧) L n' → Cochain K L n when n + a = n'.

Equations

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

theorem CochainComplex.HomComplex.Cochain.leftUnshift_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q) : (γ.leftUnshift n hn).v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p' p ⋯).inv (γ.v p' q ⋯)

def CochainComplex.HomComplex.Cochain.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a : ℤ) : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n

The map Cochain K L n → Cochain (K⟦a⟧) (L⟦a⟧) n.

Equations

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

theorem CochainComplex.HomComplex.Cochain.shift_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a p q : ℤ) (hpq : p + n = q) (p' q' : ℤ) (hp' : p' = p + a) (hq' : q' = q + a) : (γ.shift a).v p q hpq = CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' hp').hom (CategoryTheory.CategoryStruct.comp (γ.v p' q' ⋯) (L.shiftFunctorObjXIso a q q' hq').inv)

theorem CochainComplex.HomComplex.Cochain.shift_v' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a p q : ℤ) (hpq : p + n = q) : (γ.shift a).v p q hpq = γ.v (p + a) (q + a) ⋯

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightUnshift_rightShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) : (γ.rightShift a n' hn').rightUnshift n hn' = γ

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShift_rightUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn' : n' + a = n) : (γ.rightUnshift n hn').rightShift a n' hn' = γ

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftUnshift_leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') : (γ.leftShift a n' hn').leftUnshift n hn' = γ

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_leftUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn' : n + a = n') : (γ.leftUnshift n hn').leftShift a n' hn' = γ

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShift_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ₁ γ₂ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) : (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ₁ γ₂ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') : (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.shift_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ₁ γ₂ : Cochain K L n) (a : ℤ) : (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a

def CochainComplex.HomComplex.Cochain.rightShiftAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) : Cochain K L n ≃+ Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'

The additive equivalence Cochain K L n ≃+ Cochain K L⟦a⟧ n' when n' + a = n.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) (γ : Cochain K L n) : (rightShiftAddEquiv K L n a n' hn') γ = γ.rightShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') : (rightShiftAddEquiv K L n a n' hn').symm γ = γ.rightUnshift n hn'

def CochainComplex.HomComplex.Cochain.leftShiftAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n') : Cochain K L n ≃+ Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'

The additive equivalence Cochain K L n ≃+ Cochain (K⟦a⟧) L n' when n + a = n'.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n') (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') : (leftShiftAddEquiv K L n a n' hn').symm γ = γ.leftUnshift n hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n') (γ : Cochain K L n) : (leftShiftAddEquiv K L n a n' hn') γ = γ.leftShift a n' hn'

def CochainComplex.HomComplex.Cochain.shiftAddHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a : ℤ) : Cochain K L n →+ Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n

The additive map Cochain K L n →+ Cochain (K⟦a⟧) (L⟦a⟧) n.

Equations

• CochainComplex.HomComplex.Cochain.shiftAddHom K L n a = AddMonoidHom.mk' (fun (γ : CochainComplex.HomComplex.Cochain K L n) => γ.shift a) ⋯

@[simp]

theorem CochainComplex.HomComplex.Cochain.shiftAddHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a : ℤ) (γ : Cochain K L n) : (shiftAddHom K L n a) γ = γ.shift a

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) : rightShift 0 a n' hn' = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightUnshift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) : rightUnshift 0 n hn' = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n') : leftShift 0 a n' hn' = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftUnshift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n') : leftUnshift 0 n hn' = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.shift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n a : ℤ) : shift 0 a = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShift_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) : (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightUnshift_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) : (-γ).rightUnshift n hn = -γ.rightUnshift n hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') : (-γ).leftShift a n' hn' = -γ.leftShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftUnshift_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') : (-γ).leftUnshift n hn = -γ.leftUnshift n hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.shift_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a : ℤ) : (-γ).shift a = -γ.shift a

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightUnshift_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) : (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftUnshift_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ₁ γ₂ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') : (γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShift_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) (x : R) : (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (x : R) : (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.shift_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a : ℤ) (x : R) : (x • γ).shift a = x • γ.shift a

def CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) : Cochain K L n ≃ₗ[R] Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'

The linear equivalence Cochain K L n ≃+ Cochain K L⟦a⟧ n' when n' + a = n and the category is R-linear.

Equations

• CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn' = (CochainComplex.HomComplex.Cochain.rightShiftAddEquiv K L n a n' hn').toLinearEquiv ⋯

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) (a✝ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') : (rightShiftLinearEquiv R K L n a n' hn').symm a✝ = a✝.rightUnshift n hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n) (a✝ : Cochain K L n) : (rightShiftLinearEquiv R K L n a n' hn') a✝ = a✝.rightShift a n' hn'

def CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn : n + a = n') : Cochain K L n ≃ₗ[R] Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'

The additive equivalence Cochain K L n ≃+ Cochain (K⟦a⟧) L n' when n + a = n' and the category is R-linear.

Equations

• CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn = (CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn).toLinearEquiv ⋯

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn : n + a = n') (a✝ : Cochain K L n) : (leftShiftLinearEquiv R K L n a n' hn) a✝ = a✝.leftShift a n' hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn : n + a = n') (a✝ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') : (leftShiftLinearEquiv R K L n a n' hn).symm a✝ = a✝.leftUnshift n hn

def CochainComplex.HomComplex.Cochain.shiftLinearMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a : ℤ) : Cochain K L n →ₗ[R] Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n

The linear map Cochain K L n ≃+ Cochain (K⟦a⟧) (L⟦a⟧) n when the category is R-linear.

Equations

• CochainComplex.HomComplex.Cochain.shiftLinearMap R K L n a = { toAddHom := ↑(CochainComplex.HomComplex.Cochain.shiftAddHom K L n a), map_smul' := ⋯ }

@[simp]

theorem CochainComplex.HomComplex.Cochain.shiftLinearMap_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a : ℤ) (a✝ : Cochain K L n) : (shiftLinearMap R K L n a) a✝ = a✝.shift a

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShift_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) (x : Rˣ) : (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (x : Rˣ) : (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

@[simp]

theorem CochainComplex.HomComplex.Cochain.shift_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a : ℤ) (x : Rˣ) : (x • γ).shift a = x • γ.shift a

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightUnshift_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (x : R) : (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightUnshift_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (x : Rˣ) : (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftUnshift_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (x : R) : (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftUnshift_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (x : Rˣ) : (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

theorem CochainComplex.HomComplex.Cochain.rightUnshift_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L M : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) {m a : ℤ} (γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m) {nm : ℤ} (hnm : n + m = nm) (nm' : ℤ) (hnm' : nm + a = nm') (m' : ℤ) (hm' : m + a = m') : (γ.comp γ' hnm).rightUnshift nm' hnm' = γ.comp (γ'.rightUnshift m' hm') ⋯

theorem CochainComplex.HomComplex.Cochain.leftShift_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L M : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') {m t t' : ℤ} (γ' : Cochain L M m) (h : n + m = t) (ht' : t + a = t') : (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L M : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (γ' : Cochain L M 0) : (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯

theorem CochainComplex.HomComplex.Cochain.δ_rightShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = m) : δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

theorem CochainComplex.HomComplex.Cochain.δ_rightUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (m m' : ℤ) (hm' : m' + a = m) : δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'

theorem CochainComplex.HomComplex.Cochain.δ_leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' m' : ℤ) (hn' : n + a = n') (m : ℤ) (hm' : m + a = m') : δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'

theorem CochainComplex.HomComplex.Cochain.δ_leftUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (m m' : ℤ) (hm' : m + a = m') : δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'

@[simp]

theorem CochainComplex.HomComplex.Cochain.δ_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a m : ℤ) : δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

theorem CochainComplex.HomComplex.Cochain.leftShift_rightShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) : (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a

theorem CochainComplex.HomComplex.Cochain.rightShift_leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' : ℤ) (hn' : n + a = n') : (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a

theorem CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cochain K L n) (a n' n'' : ℤ) (hn' : n' + a = n) (hn'' : n + a = n'') : (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''

The left and right shift of cochains commute only up to a sign.

def CochainComplex.HomComplex.Cocycle.rightShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cocycle K L n) (a n' : ℤ) (hn' : n' + a = n) : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'

The map Cocycle K L n → Cocycle K (L⟦a⟧) n' when n' + a = n.

Equations

• γ.rightShift a n' hn' = CochainComplex.HomComplex.Cocycle.mk ((↑γ).rightShift a n' hn') (n' + 1) ⋯ ⋯

@[simp]

theorem CochainComplex.HomComplex.Cocycle.rightShift_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cocycle K L n) (a n' : ℤ) (hn' : n' + a = n) : ↑(γ.rightShift a n' hn') = (↑γ).rightShift a n' hn'

def CochainComplex.HomComplex.Cocycle.rightUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) : Cocycle K L n

The map Cocycle K (L⟦a⟧) n' → Cocycle K L n when n' + a = n.

Equations

• γ.rightUnshift n hn = CochainComplex.HomComplex.Cocycle.mk ((↑γ).rightUnshift n hn) (n + 1) ⋯ ⋯

@[simp]

theorem CochainComplex.HomComplex.Cocycle.rightUnshift_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) : ↑(γ.rightUnshift n hn) = (↑γ).rightUnshift n hn

def CochainComplex.HomComplex.Cocycle.leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cocycle K L n) (a n' : ℤ) (hn' : n + a = n') : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'

The map Cocycle K L n → Cocycle (K⟦a⟧) L n' when n + a = n'.

Equations

• γ.leftShift a n' hn' = CochainComplex.HomComplex.Cocycle.mk ((↑γ).leftShift a n' hn') (n' + 1) ⋯ ⋯

@[simp]

theorem CochainComplex.HomComplex.Cocycle.leftShift_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cocycle K L n) (a n' : ℤ) (hn' : n + a = n') : ↑(γ.leftShift a n' hn') = (↑γ).leftShift a n' hn'

def CochainComplex.HomComplex.Cocycle.leftUnshift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') : Cocycle K L n

The map Cocycle (K⟦a⟧) L n' → Cocycle K L n when n + a = n'.

Equations

• γ.leftUnshift n hn = CochainComplex.HomComplex.Cocycle.mk ((↑γ).leftUnshift n hn) (n + 1) ⋯ ⋯

@[simp]

theorem CochainComplex.HomComplex.Cocycle.leftUnshift_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') : ↑(γ.leftUnshift n hn) = (↑γ).leftUnshift n hn

def CochainComplex.HomComplex.Cocycle.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cocycle K L n) (a : ℤ) : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n

The map Cocycle K L n → Cocycle (K⟦a⟧) (L⟦a⟧) n.

Equations

• γ.shift a = CochainComplex.HomComplex.Cocycle.mk ((↑γ).shift a) (n + 1) ⋯ ⋯

@[simp]

theorem CochainComplex.HomComplex.Cocycle.shift_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : Cocycle K L n) (a : ℤ) : ↑(γ.shift a) = (↑γ).shift a