ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₂ = CategoryTheory.CategoryStruct.id S.L₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁.Hom S₂<VAR>g : S₂.Hom S₃<GOAL>(f.comp g).f₃ = CategoryTheory.CategoryStruct.comp f.f₃ g.f₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁.Hom S₂<VAR>g : S₂.Hom S₃<GOAL>(f.comp g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁.Hom S₂<VAR>g : S₂.Hom S₃<GOAL>(f.comp g).f₂ = CategoryTheory.CategoryStruct.comp f.f₂ g.f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁.Hom S₂<VAR>g : S₂.Hom S₃<GOAL>(f.comp g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.CategoryStruct.id S).f₀ = CategoryTheory.CategoryStruct.id S.L₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.CategoryStruct.id S).f₁ = CategoryTheory.CategoryStruct.id S.L₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.CategoryStruct.id S).f₂ = CategoryTheory.CategoryStruct.id S.L₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.CategoryStruct.id S).f₃ = CategoryTheory.CategoryStruct.id S.L₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁ ⟶ S₂<VAR>g : S₂ ⟶ S₃<GOAL>(CategoryTheory.CategoryStruct.comp f g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁ ⟶ S₂<VAR>g : S₂ ⟶ S₃<GOAL>(CategoryTheory.CategoryStruct.comp f g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁ ⟶ S₂<VAR>g : S₂ ⟶ S₃<GOAL>(CategoryTheory.CategoryStruct.comp f g).f₂ = CategoryTheory.CategoryStruct.comp f.f₂ g.f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁ ⟶ S₂<VAR>g : S₂ ⟶ S₃<GOAL>(CategoryTheory.CategoryStruct.comp f g).f₃ = CategoryTheory.CategoryStruct.comp f.f₃ g.f₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₀.map f = f.f₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.functorL₀.obj S = S.L₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.functorL₁.obj S = S.L₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₁.map f = f.f₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.functorL₂.obj S = S.L₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₂.map f = f.f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.functorL₃.obj S = S.L₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₃.map f = f.f₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorP.map f = CategoryTheory.Limits.pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.functorP.obj S = S.P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.φ₂ f.f₂.τ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) S₂.φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.φ₁ f.f₂.τ₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) S₂.φ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C<VAR>f : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.δ f.f₃.τ₁ = CategoryTheory.CategoryStruct.comp f.f₀.τ₃ S₂.δ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₃ = f.f₃.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.functorL₁'.obj S = S.L₁'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₁ = f.f₀.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₂ = f.f₀.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₃ = f.f₃.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₁ = f.f₀.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₂ = f.f₃.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.functorL₂'.obj S = S.L₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.obj S = S.composableArrows
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.map f = CategoryTheory.ComposableArrows.homMk₅ f.f₀.τ₁ f.f₀.τ₂ f.f₀.τ₃ f.f₃.τ₁ f.f₃.τ₂ f.f₃.τ₃ ⋯ ⋯ ⋯ ⋯ ⋯
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<GOAL>((HomotopyCategory.quotient V c).obj C).as = C
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomotopyCategory V c<VAR>f : C ⟶ D<GOAL>(HomotopyCategory.quotient V c).map (Quot.out f) = f
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : C ⟶ D<GOAL>Quot.mk (CategoryTheory.Quotient.CompClosure (homotopic V c)) f = (HomotopyCategory.quotient V c).map f
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h : Homotopy f g<GOAL>(HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomotopyCategory V c<VAR>f : C ⟶ D<VAR>g : D ⟶ E<GOAL>(HomotopyCategory.quotient V c).map (Quot.out f ≫ Quot.out g) = f ≫ g
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : HomotopyEquiv C D<GOAL>(HomotopyCategory.isoOfHomotopyEquiv f).inv = (HomotopyCategory.quotient V c).map f.inv
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : HomotopyEquiv C D<GOAL>(HomotopyCategory.isoOfHomotopyEquiv f).hom = (HomotopyCategory.quotient V c).map f.hom
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<GOAL>(HomologicalComplex.homotopyEquivalences V c).IsInvertedBy (HomotopyCategory.quotient V c)
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<GOAL>CategoryTheory.Limits.IsZero ((HomotopyCategory.quotient V c).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0)
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>W : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} W<VAR>CategoryTheory.Preadditive W<VAR>F : V ⥤ W<VAR>F.Additive<VAR>c : ComplexShape ι<VAR>a : CategoryTheory.Quotient (homotopic V c)<GOAL>(F.mapHomotopyCategory c).obj a = (HomotopyCategory.quotient W c).obj ((F.mapHomologicalComplex c).obj a.as)
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>W : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} W<VAR>CategoryTheory.Preadditive W<VAR>F : V ⥤ W<VAR>F.Additive<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex V c<VAR>f : K ⟶ L<GOAL>(F.mapHomotopyCategory c).map ((HomotopyCategory.quotient V c).map f) = (HomotopyCategory.quotient W c).map ((F.mapHomologicalComplex c).map f)
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>W : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} W<VAR>CategoryTheory.Preadditive W<VAR>F G : V ⥤ W<VAR>F.Additive<VAR>G.Additive<VAR>α : F ⟶ G<VAR>c : ComplexShape ι<VAR>C : HomotopyCategory V c<GOAL>(CategoryTheory.NatTrans.mapHomotopyCategory α c).app C = (HomotopyCategory.quotient W c).map ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C.as)
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>W : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} W<VAR>CategoryTheory.Preadditive W<VAR>c : ComplexShape ι<VAR>F : V ⥤ W<VAR>F.Additive<GOAL>CategoryTheory.NatTrans.mapHomotopyCategory (𝟙 F) c = 𝟙 (F.mapHomotopyCategory c)
<VAR>ι : Type u_2<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>W : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} W<VAR>CategoryTheory.Preadditive W<VAR>c : ComplexShape ι<VAR>F G H : V ⥤ W<VAR>F.Additive<VAR>G.Additive<VAR>H.Additive<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>CategoryTheory.NatTrans.mapHomotopyCategory (α ≫ β) c = CategoryTheory.NatTrans.mapHomotopyCategory α c ≫ CategoryTheory.NatTrans.mapHomotopyCategory β c
<VAR>n : ℤ<VAR>self : CochainComplex.HomComplex.Triplet n<GOAL>self.p + n = self.q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(CochainComplex.HomComplex.Cochain.mk v).v p q hpq = v p q hpq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cochain F G n<VAR>h : z₁ = z₂<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>z₁.v p q hpq = z₂.v p q hpq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cochain F G n<VAR>h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cochain F G 0<VAR>h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>CochainComplex.HomComplex.Cochain.v 0 p q hpq = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(z₁ + z₂).v p q hpq = z₁.v p q hpq + z₂.v p q hpq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(z₁ - z₂).v p q hpq = z₁.v p q hpq - z₂.v p q hpq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z : CochainComplex.HomComplex.Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(-z).v p q hpq = -z.v p q hpq
<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>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>k : R<VAR>z : CochainComplex.HomComplex.Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(k • z).v p q hpq = k • z.v p q hpq
<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>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>k : Rˣ<VAR>z : CochainComplex.HomComplex.Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(k • z).v p q hpq = k • z.v p q hpq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p : ℤ<GOAL>(CochainComplex.HomComplex.Cochain.ofHoms ψ).v p p ⋯ = ψ p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<GOAL>(CochainComplex.HomComplex.Cochain.ofHoms fun p => 0) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p q q' : ℤ<VAR>hpq : p + 0 = q<GOAL>(CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq ≫ G.d q q' = ψ p ≫ G.d p q'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p' p q : ℤ<VAR>hpq : p + 0 = q<GOAL>F.d p' p ≫ (CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<GOAL>CochainComplex.HomComplex.Cochain.ofHom 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>p : ℤ<GOAL>(CochainComplex.HomComplex.Cochain.ofHom φ).v p p ⋯ = φ.f p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>p q q' : ℤ<VAR>hpq : p + 0 = q<GOAL>(CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>p' p q : ℤ<VAR>hpq : p + 0 = q<GOAL>F.d p' p ≫ (CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq = F.d p' q ≫ φ.f q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ₁ φ₂ : F ⟶ G<GOAL>CochainComplex.HomComplex.Cochain.ofHom (φ₁ + φ₂) = CochainComplex.HomComplex.Cochain.ofHom φ₁ + CochainComplex.HomComplex.Cochain.ofHom φ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ₁ φ₂ : F ⟶ G<GOAL>CochainComplex.HomComplex.Cochain.ofHom (φ₁ - φ₂) = CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<GOAL>CochainComplex.HomComplex.Cochain.ofHom (-φ) = -CochainComplex.HomComplex.Cochain.ofHom φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : φ₁ = φ₂<GOAL>CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.ofEq h) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<GOAL>CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.refl φ) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain F G n<VAR>p q q' : ℤ<VAR>hpq : p + n = q<VAR>hq' : q = q'<GOAL>γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain F G n<VAR>p q q' : ℤ<VAR>hpq : p + n = q<VAR>hq' : q' = q<GOAL>γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁ : p₁ + n₁ = p₂<VAR>h₂ : p₂ + n₂ = p₃<GOAL>(z₁.comp z₂ h).v p₁ p₃ ⋯ = z₁.v p₁ p₂ h₁ ≫ z₂.v p₂ p₃ h₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n<VAR>z₂ : CochainComplex.HomComplex.Cochain G K 0<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(z₁.comp z₂ ⋯).v p q hpq = z₁.v p q hpq ≫ z₂.v q q ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G 0<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(z₁.comp z₂ ⋯).v p q hpq = z₁.v p p ⋯ ≫ z₂.v p q hpq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K L : CochainComplex C ℤ<VAR>n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>z₃ : CochainComplex.HomComplex.Cochain K L n₃<VAR>h₁₂ : n₁ + n₂ = n₁₂<VAR>h₂₃ : n₂ + n₃ = n₂₃<VAR>h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃<GOAL>(z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K L : CochainComplex C ℤ<VAR>n₂ n₃ n₂₃ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G 0<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>z₃ : CochainComplex.HomComplex.Cochain K L n₃<VAR>h₂₃ : n₂ + n₃ = n₂₃<GOAL>(z₁.comp z₂ ⋯).comp z₃ h₂₃ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K L : CochainComplex C ℤ<VAR>n₁ n₃ n₁₃ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K 0<VAR>z₃ : CochainComplex.HomComplex.Cochain K L n₃<VAR>h₁₃ : n₁ + n₃ = n₁₃<GOAL>(z₁.comp z₂ ⋯).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ ⋯) h₁₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K L : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>z₃ : CochainComplex.HomComplex.Cochain K L 0<VAR>h₁₂ : n₁ + n₂ = n₁₂<GOAL>(z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) h₁₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K L : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K (-n₂)<VAR>z₃ : CochainComplex.HomComplex.Cochain K L n₂<VAR>h₁₂ : n₁ + -n₂ = n₁₂<GOAL>(z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>CochainComplex.HomComplex.Cochain.comp 0 z₂ h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ z₁' : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>(z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ z₁' : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>(z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>(-z₁).comp z₂ h = -z₁.comp z₂ h
<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>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>k : R<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>(k • z₁).comp z₂ h = k • z₁.comp z₂ h
<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>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>k : Rˣ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>(k • z₁).comp z₂ h = k • z₁.comp z₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₂ : CochainComplex.HomComplex.Cochain F G n<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (𝟙 F)).comp z₂ ⋯ = z₂