Documentation

Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

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.

References #

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

Equations
Instances For
    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') :
    (γ.rightShift a n' hn').v p q hpq = CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a q p' ).inv

    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.
    Instances For
      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) :
      (γ.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')

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

      Equations
      Instances For
        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') :
        (γ.rightUnshift n hn).v p q hpq = CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a p' q ).hom

        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.
        Instances For
          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) :
          (γ.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 )

          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.
          Instances For
            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) :
            (γ.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {a : } {n' : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {a : } {n' : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ₁ : CochainComplex.HomComplex.Cochain K L n) (γ₂ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ₁ : CochainComplex.HomComplex.Cochain K L n) (γ₂ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ₁ : CochainComplex.HomComplex.Cochain K L n) (γ₂ : CochainComplex.HomComplex.Cochain K L n) (a : ) :
            (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a

            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.
            Instances For

              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.
              Instances For
                @[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) :
                (-γ).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 : CochainComplex C } {L : CochainComplex C } {n' : } {a : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n' : } {a : } (γ : CochainComplex.HomComplex.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.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) :
                (γ₁ + γ₂).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 : 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') :
                (γ₁ + γ₂).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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.Cochain K L n) (a : ) (n' : ) (hn' : n + a = n') (x : R) :
                (x γ).leftShift a n' hn' = x γ.leftShift a n' hn'
                @[simp]

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

                Equations
                Instances For

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

                  Equations
                  Instances For

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

                    Equations
                    Instances For
                      @[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ˣ) :
                      (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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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.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) :
                      (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 : 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ˣ) :
                      (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 : 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) :
                      (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 : 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ˣ) :
                      (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 : 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') :
                      (γ.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 : 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') :
                      (γ.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 : 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) :
                      (γ.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 : 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' (γ.rightShift a n' hn') = a.negOnePow (CochainComplex.HomComplex.δ n m γ).rightShift 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 (γ.rightUnshift n hn) = a.negOnePow (CochainComplex.HomComplex.δ n' m' γ).rightUnshift 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' (γ.leftShift a n' hn') = a.negOnePow (CochainComplex.HomComplex.δ n m γ).leftShift 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 (γ.leftUnshift n hn) = a.negOnePow (CochainComplex.HomComplex.δ n' m' γ).leftUnshift m hm'
                      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) :
                      (γ.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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 : CochainComplex C } {L : CochainComplex C } {n : } (γ : CochainComplex.HomComplex.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.

                      @[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) :
                      (γ.rightShift a n' hn') = (↑γ).rightShift a n' hn'

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

                      Equations
                      Instances For
                        @[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) :
                        (γ.rightUnshift n hn) = (↑γ).rightUnshift n hn

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

                        Equations
                        Instances For
                          @[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') :
                          (γ.leftShift a n' hn') = (↑γ).leftShift a n' hn'

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

                          Equations
                          Instances For
                            @[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') :
                            (γ.leftUnshift n hn) = (↑γ).leftUnshift n hn

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

                            Equations
                            Instances For

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

                              Equations
                              Instances For