ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : K ⟶ M<VAR>β : L ⟶ M<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inr.f i ≫ (CategoryTheory.Limits.biprod.desc α β).f i = β.f i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : M ⟶ K<VAR>β : M ⟶ L<VAR>i : ι<GOAL>(CategoryTheory.Limits.biprod.lift α β).f i ≫ CategoryTheory.Limits.biprod.fst.f i = α.f i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : M ⟶ K<VAR>β : M ⟶ L<VAR>i : ι<GOAL>(CategoryTheory.Limits.biprod.lift α β).f i ≫ CategoryTheory.Limits.biprod.snd.f i = β.f i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n' = q<VAR>p' : ℤ<VAR>hp' : p + n = p'<GOAL>(γ.rightShift a n' hn').v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a q p' ⋯).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n' = q<VAR>p' : ℤ<VAR>hp' : p' + n = q<GOAL>(γ.leftShift a n' hn').v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p p' ⋯).hom ≫ γ.v p' q hp'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n = q<VAR>p' : ℤ<VAR>hp' : p + n' = p'<GOAL>(γ.rightUnshift n hn).v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a p' q ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n = q<VAR>p' : ℤ<VAR>hp' : p' + n' = q<GOAL>(γ.leftUnshift n hn).v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p' p ⋯).inv ≫ γ.v p' q ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a p q : ℤ<VAR>hpq : p + n = q<VAR>p' q' : ℤ<VAR>hp' : p' = p + a<VAR>hq' : q' = q + a<GOAL>(γ.shift a).v p q hpq = (K.shiftFunctorObjXIso a p p' hp').hom ≫ γ.v p' q' ⋯ ≫ (L.shiftFunctorObjXIso a q q' hq').inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a p q : ℤ<VAR>hpq : p + n = q<GOAL>(γ.shift a).v p q hpq = γ.v (p + a) (q + a) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>(γ.rightShift a n' hn').rightUnshift n hn' = γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>a n' : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn' : n' + a = n<GOAL>(γ.rightUnshift n hn').rightShift a n' hn' = γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>(γ.leftShift a n' hn').leftUnshift n hn' = γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>a n' : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn' : n + a = n'<GOAL>(γ.leftUnshift n hn').leftShift a n' hn' = γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ₁ γ₂ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>(γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ₁ γ₂ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>(γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ₁ γ₂ : CochainComplex.HomComplex.Cochain K L n<VAR>a : ℤ<GOAL>(γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n' + a = n<VAR>γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<GOAL>(CochainComplex.HomComplex.Cochain.rightShiftAddEquiv K L n a n' hn').symm γ = γ.rightUnshift n hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n' + a = n<VAR>γ : CochainComplex.HomComplex.Cochain K L n<GOAL>(CochainComplex.HomComplex.Cochain.rightShiftAddEquiv K L n a n' hn') γ = γ.rightShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n + a = n'<VAR>γ : CochainComplex.HomComplex.Cochain K L n<GOAL>(CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn') γ = γ.leftShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n + a = n'<VAR>γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<GOAL>(CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn').symm γ = γ.leftUnshift n hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<GOAL>(CochainComplex.HomComplex.Cochain.shiftAddHom K L n a) γ = γ.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n' + a = n<GOAL>CochainComplex.HomComplex.Cochain.rightShift 0 a n' hn' = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n' + a = n<GOAL>CochainComplex.HomComplex.Cochain.rightUnshift 0 n hn' = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n + a = n'<GOAL>CochainComplex.HomComplex.Cochain.leftShift 0 a n' hn' = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n + a = n'<GOAL>CochainComplex.HomComplex.Cochain.leftUnshift 0 n hn' = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n a : ℤ<GOAL>CochainComplex.HomComplex.Cochain.shift 0 a = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>(-γ).rightShift a n' hn' = -γ.rightShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<GOAL>(-γ).rightUnshift n hn = -γ.rightUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>(-γ).leftShift a n' hn' = -γ.leftShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<GOAL>(-γ).leftUnshift n hn = -γ.leftUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a : ℤ<GOAL>(-γ).shift a = -γ.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ₁ γ₂ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<GOAL>(γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ₁ γ₂ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<GOAL>(γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>x : R<GOAL>(x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>x : R<GOAL>(x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a : ℤ<VAR>x : R<GOAL>(x • γ).shift a = x • γ.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n' + a = n<GOAL>∀ (a_1 : CochainComplex.HomComplex.Cochain K L n), (CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn') a_1 = a_1.rightShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn' : n' + a = n<GOAL>∀ (a_1 : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'), (CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn').symm a_1 = a_1.rightUnshift n hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn : n + a = n'<GOAL>∀ (a_1 : CochainComplex.HomComplex.Cochain K L n), (CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn) a_1 = a_1.leftShift a n' hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n a n' : ℤ<VAR>hn : n + a = n'<GOAL>∀ (a_1 : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'), (CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn).symm a_1 = a_1.leftUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n a : ℤ<GOAL>∀ (a_1 : CochainComplex.HomComplex.Cochain K L n), (CochainComplex.HomComplex.Cochain.shiftLinearMap R K L n a) a_1 = a_1.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>x : Rˣ<GOAL>(x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>x : Rˣ<GOAL>(x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a : ℤ<VAR>x : Rˣ<GOAL>(x • γ).shift a = x • γ.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>x : R<GOAL>(x • γ).rightUnshift n hn = x • γ.rightUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>x : Rˣ<GOAL>(x • γ).rightUnshift n hn = x • γ.rightUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<VAR>x : R<GOAL>(x • γ).leftUnshift n hn = x • γ.leftUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<VAR>x : Rˣ<GOAL>(x • γ).leftUnshift n hn = x • γ.leftUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>m a : ℤ<VAR>γ' : CochainComplex.HomComplex.Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m<VAR>nm : ℤ<VAR>hnm : n + m = nm<VAR>nm' : ℤ<VAR>hnm' : nm + a = nm'<VAR>m' : ℤ<VAR>hm' : m + a = m'<GOAL>(γ.comp γ' hnm).rightUnshift nm' hnm' = γ.comp (γ'.rightUnshift m' hm') ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>m t t' : ℤ<VAR>γ' : CochainComplex.HomComplex.Cochain L M m<VAR>h : n + m = t<VAR>ht' : t + a = t'<GOAL>(γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>γ' : CochainComplex.HomComplex.Cochain L M 0<GOAL>(γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' m' : ℤ<VAR>hn' : n' + a = n<VAR>m : ℤ<VAR>hm' : m' + a = m<GOAL>CochainComplex.HomComplex.δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).rightShift a m' hm'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>a n' : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>m m' : ℤ<VAR>hm' : m' + a = m<GOAL>CochainComplex.HomComplex.δ n m (γ.rightUnshift n hn) = a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).rightUnshift m hm'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' m' : ℤ<VAR>hn' : n + a = n'<VAR>m : ℤ<VAR>hm' : m + a = m'<GOAL>CochainComplex.HomComplex.δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).leftShift a m' hm'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>a n' : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<VAR>m m' : ℤ<VAR>hm' : m + a = m'<GOAL>CochainComplex.HomComplex.δ n m (γ.leftUnshift n hn) = a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).leftUnshift m hm'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a m : ℤ<GOAL>CochainComplex.HomComplex.δ n m (γ.shift a) = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>(γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>(γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain K L n<VAR>a n' n'' : ℤ<VAR>hn' : n' + a = n<VAR>hn'' : n + a = n''<GOAL>(γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cocycle K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>↑(γ.rightShift a n' hn') = (↑γ).rightShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<GOAL>↑(γ.rightUnshift n hn) = (↑γ).rightUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cocycle K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>↑(γ.leftShift a n' hn') = (↑γ).leftShift a n' hn'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n' a : ℤ<VAR>γ : CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<GOAL>↑(γ.leftUnshift n hn) = (↑γ).leftUnshift n hn
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cocycle K L n<VAR>a : ℤ<GOAL>↑(γ.shift a) = (↑γ).shift a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).i = F.map h.i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).K = F.obj h.K
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).H = F.obj h.H
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).π = F.map h.π
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).f' = F.map h.f'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h₁.IsPreservedBy F<VAR>h₂.IsPreservedBy F<GOAL>(ψ.map F).φH = F.map ψ.φH
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h₁.IsPreservedBy F<VAR>h₂.IsPreservedBy F<GOAL>(ψ.map F).φK = F.map ψ.φK
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).H = F.obj h.H