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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : CochainComplex.HomComplex.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

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

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

def CochainComplex.HomComplex.Cochain.leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n + a = n') : CochainComplex.HomComplex.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n + a = n') (p : ℤ) (q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p' + n = q) : (CochainComplex.HomComplex.Cochain.leftShift γ a n' hn').v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso K 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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n' : ℤ} {a : ℤ} (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) : CochainComplex.HomComplex.Cochain K L n

The map Cochain K (L⟦a⟧) 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.rightUnshift_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n' : ℤ} {a : ℤ} (γ : CochainComplex.HomComplex.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') : (CochainComplex.HomComplex.Cochain.rightUnshift γ n hn).v p q hpq = CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (CochainComplex.shiftFunctorObjXIso L a p' q ⋯).hom

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

def CochainComplex.HomComplex.Cochain.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) : CochainComplex.HomComplex.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (p : ℤ) (q : ℤ) (hpq : p + n = q) (p' : ℤ) (q' : ℤ) (hp' : p' = p + a) (hq' : q' = q + a) : (CochainComplex.HomComplex.Cochain.shift γ a).v p q hpq = CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso K a p p' hp').hom (CategoryTheory.CategoryStruct.comp (γ.v p' q' ⋯) (CochainComplex.shiftFunctorObjXIso L a q q' hq').inv)

theorem CochainComplex.HomComplex.Cochain.shift_v' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : CochainComplex.HomComplex.Cochain.rightUnshift (CochainComplex.HomComplex.Cochain.rightShift γ a n' hn') n hn' = γ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CochainComplex.HomComplex.Cochain.rightShiftAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : CochainComplex.HomComplex.Cochain K L n ≃+ CochainComplex.HomComplex.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.leftShiftAddEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n + a = n') (γ : CochainComplex.HomComplex.Cochain K L n) : (CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn') γ = CochainComplex.HomComplex.Cochain.leftShift γ a n' hn'

@[simp]

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

def CochainComplex.HomComplex.Cochain.leftShiftAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n + a = n') : CochainComplex.HomComplex.Cochain K L n ≃+ CochainComplex.HomComplex.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.shiftAddHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (γ : CochainComplex.HomComplex.Cochain K L n) : (CochainComplex.HomComplex.Cochain.shiftAddHom K L n a) γ = CochainComplex.HomComplex.Cochain.shift γ a

def CochainComplex.HomComplex.Cochain.shiftAddHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) : CochainComplex.HomComplex.Cochain K L n →+ CochainComplex.HomComplex.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) => CochainComplex.HomComplex.Cochain.shift γ a) ⋯

@[simp]

theorem CochainComplex.HomComplex.Cochain.rightShift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : CochainComplex.HomComplex.Cochain.rightUnshift 0 n hn' = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftShift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n + a = n') : CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n + a = n') : CochainComplex.HomComplex.Cochain.leftUnshift 0 n hn' = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.leftUnshift_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n' : ℤ} {a : ℤ} (γ₁ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (γ₂ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') : CochainComplex.HomComplex.Cochain.leftUnshift (γ₁ + γ₂) n hn = CochainComplex.HomComplex.Cochain.leftUnshift γ₁ n hn + CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) (x : R) : CochainComplex.HomComplex.Cochain.rightShift (x • γ) a n' hn' = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n + a = n') (x : R) : CochainComplex.HomComplex.Cochain.leftShift (x • γ) a n' hn' = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (x : R) : CochainComplex.HomComplex.Cochain.shift (x • γ) a = x • CochainComplex.HomComplex.Cochain.shift γ a

@[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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : ∀ (a_1 : CochainComplex.HomComplex.Cochain K L n), (CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn') a_1 = CochainComplex.HomComplex.Cochain.rightShift a_1 a n' hn'

@[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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : ∀ (a_1 : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'), (LinearEquiv.symm (CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn')) a_1 = CochainComplex.HomComplex.Cochain.rightUnshift a_1 n hn'

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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : CochainComplex.HomComplex.Cochain K L n ≃ₗ[R] CochainComplex.HomComplex.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' = AddEquiv.toLinearEquiv (CochainComplex.HomComplex.Cochain.rightShiftAddEquiv K L n a n' hn') ⋯

@[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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn : n + a = n') : ∀ (a_1 : CochainComplex.HomComplex.Cochain K L n), (CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn) a_1 = CochainComplex.HomComplex.Cochain.leftShift a_1 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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn : n + a = n') : ∀ (a_1 : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'), (LinearEquiv.symm (CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn)) a_1 = CochainComplex.HomComplex.Cochain.leftUnshift a_1 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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (n' : ℤ) (hn : n + a = n') : CochainComplex.HomComplex.Cochain K L n ≃ₗ[R] CochainComplex.HomComplex.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 = AddEquiv.toLinearEquiv (CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn) ⋯

@[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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) (a : CochainComplex.HomComplex.Cochain K L n) : (CochainComplex.HomComplex.Cochain.shiftLinearMap R K L n a✝) a = CochainComplex.HomComplex.Cochain.shift a a✝

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 : CochainComplex C ℤ) (L : CochainComplex C ℤ) (n : ℤ) (a : ℤ) : CochainComplex.HomComplex.Cochain K L n →ₗ[R] CochainComplex.HomComplex.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.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) (x : Rˣ) : CochainComplex.HomComplex.Cochain.rightShift (x • γ) a n' hn' = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (n' : ℤ) (hn' : n + a = n') (x : Rˣ) : CochainComplex.HomComplex.Cochain.leftShift (x • γ) a n' hn' = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (x : Rˣ) : CochainComplex.HomComplex.Cochain.shift (x • γ) a = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n' : ℤ} {a : ℤ} (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (x : R) : CochainComplex.HomComplex.Cochain.rightUnshift (x • γ) n hn = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n' : ℤ} {a : ℤ} (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (x : Rˣ) : CochainComplex.HomComplex.Cochain.rightUnshift (x • γ) n hn = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n' : ℤ} {a : ℤ} (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (x : R) : CochainComplex.HomComplex.Cochain.leftUnshift (x • γ) n hn = x • CochainComplex.HomComplex.Cochain.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 : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n' : ℤ} {a : ℤ} (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (x : Rˣ) : CochainComplex.HomComplex.Cochain.leftUnshift (x • γ) n hn = x • CochainComplex.HomComplex.Cochain.leftUnshift γ n hn

theorem CochainComplex.HomComplex.Cochain.rightUnshift_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {M : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) {m : ℤ} {a : ℤ} (γ' : CochainComplex.HomComplex.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') : CochainComplex.HomComplex.Cochain.rightUnshift (γ.comp γ' hnm) nm' hnm' = γ.comp (CochainComplex.HomComplex.Cochain.rightUnshift γ' m' hm') ⋯

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

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

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

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

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

@[simp]

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

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

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

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

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

@[simp]

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

def CochainComplex.HomComplex.Cocycle.rightShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cocycle K L n) (a : ℤ) (n' : ℤ) (hn' : n' + a = n) : CochainComplex.HomComplex.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

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

@[simp]

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

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

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

Equations

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

@[simp]

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

def CochainComplex.HomComplex.Cocycle.leftShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cocycle K L n) (a : ℤ) (n' : ℤ) (hn' : n + a = n') : CochainComplex.HomComplex.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

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

@[simp]

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

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

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

Equations

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

@[simp]

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

def CochainComplex.HomComplex.Cocycle.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cocycle K L n) (a : ℤ) : CochainComplex.HomComplex.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

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