ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>n : ℕ<VAR>f : C ⟶ D<VAR>i : ι<GOAL>(n • f).f i = n • f.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>n : ℤ<VAR>f : C ⟶ D<VAR>i : ι<GOAL>(n • f).f i = n • f.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C₁ C₂ : HomologicalComplex V c<VAR>i : ι<VAR>f : C₁ ⟶ C₂<GOAL>(HomologicalComplex.Hom.fAddMonoidHom i) f = f.f i
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex W₁ c<VAR>i j : ι<GOAL>((F.mapHomologicalComplex c).obj C).d i j = F.map (C.d i j)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<GOAL>∀ {X Y : HomologicalComplex W₁ c} (f : X ⟶ Y) (i : ι), ((F.mapHomologicalComplex c).map f).f i = F.map (f.f i)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex W₁ c<VAR>i : ι<GOAL>((F.mapHomologicalComplex c).obj C).X i = F.obj (C.X i)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>c : ComplexShape ι<VAR>X : HomologicalComplex W₁ c<VAR>i : ι<GOAL>((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).hom.app X).f i = 𝟙 (X.X i)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>c : ComplexShape ι<VAR>X : HomologicalComplex W₁ c<VAR>i : ι<GOAL>((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).inv.app X).f i = 𝟙 (X.X i)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>F G : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>α : F ⟶ G<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex W₁ c<VAR>i : ι<GOAL>((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C).f i = α.app (C.X i)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>c : ComplexShape ι<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<GOAL>CategoryTheory.NatTrans.mapHomologicalComplex (𝟙 F) c = 𝟙 (F.mapHomologicalComplex c)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>c : ComplexShape ι<VAR>F G H : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>H.PreservesZeroMorphisms<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>CategoryTheory.NatTrans.mapHomologicalComplex (α ≫ β) c = CategoryTheory.NatTrans.mapHomologicalComplex α c ≫ CategoryTheory.NatTrans.mapHomologicalComplex β c
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>c : ComplexShape ι<VAR>F G : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>α : F ⟶ G<VAR>C D : HomologicalComplex W₁ c<VAR>f : C ⟶ D<GOAL>(F.mapHomologicalComplex c).map f ≫ (CategoryTheory.NatTrans.mapHomologicalComplex α c).app D = (CategoryTheory.NatTrans.mapHomologicalComplex α c).app C ≫ (G.mapHomologicalComplex c).map f
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>F G : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>α : F ≅ G<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex W₁ c<VAR>i : ι<GOAL>((CategoryTheory.NatIso.mapHomologicalComplex α c).hom.app C).f i = α.hom.app (C.X i)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>F G : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>α : F ≅ G<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex W₁ c<VAR>i : ι<GOAL>((CategoryTheory.NatIso.mapHomologicalComplex α c).inv.app C).f i = α.inv.app (C.X i)
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>e : W₁ ≌ W₂<VAR>e.functor.PreservesZeroMorphisms<VAR>c : ComplexShape ι<GOAL>(e.mapHomologicalComplex c).unitIso = (CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).symm ≪≫ CategoryTheory.NatIso.mapHomologicalComplex e.unitIso c
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>e : W₁ ≌ W₂<VAR>e.functor.PreservesZeroMorphisms<VAR>c : ComplexShape ι<GOAL>(e.mapHomologicalComplex c).functor = e.functor.mapHomologicalComplex c
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>e : W₁ ≌ W₂<VAR>e.functor.PreservesZeroMorphisms<VAR>c : ComplexShape ι<GOAL>(e.mapHomologicalComplex c).counitIso = CategoryTheory.NatIso.mapHomologicalComplex e.counitIso c ≪≫ CategoryTheory.Functor.mapHomologicalComplexIdIso W₂ c
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_5, u_3} W₁<VAR>CategoryTheory.Category.{u_6, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>e : W₁ ≌ W₂<VAR>e.functor.PreservesZeroMorphisms<VAR>c : ComplexShape ι<GOAL>(e.mapHomologicalComplex c).inverse = e.inverse.mapHomologicalComplex c
<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_6, u_3} W₁<VAR>CategoryTheory.Category.{u_7, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>α : Type u_5<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>X : α → W₁<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<GOAL>(F.mapHomologicalComplex (ComplexShape.down α)).obj (ChainComplex.of X d sq) = ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_6, u_3} W₁<VAR>CategoryTheory.Category.{u_5, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>CategoryTheory.Limits.HasZeroObject W₁<VAR>CategoryTheory.Limits.HasZeroObject W₂<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>DecidableEq ι<VAR>j : ι<VAR>X : W₁<GOAL>((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X).f j = F.map (HomologicalComplex.singleObjXSelf c j X).hom ≫ (HomologicalComplex.singleObjXSelf c j (F.obj X)).inv
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_6, u_3} W₁<VAR>CategoryTheory.Category.{u_5, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>CategoryTheory.Limits.HasZeroObject W₁<VAR>CategoryTheory.Limits.HasZeroObject W₂<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<VAR>X : W₁<GOAL>((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X).f i = 0
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_6, u_3} W₁<VAR>CategoryTheory.Category.{u_5, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>CategoryTheory.Limits.HasZeroObject W₁<VAR>CategoryTheory.Limits.HasZeroObject W₂<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>DecidableEq ι<VAR>j : ι<VAR>X : W₁<GOAL>((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X).f j = (HomologicalComplex.singleObjXSelf c j (F.obj X)).hom ≫ F.map (HomologicalComplex.singleObjXSelf c j X).inv
<VAR>ι : Type u_1<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>CategoryTheory.Category.{u_6, u_3} W₁<VAR>CategoryTheory.Category.{u_5, u_4} W₂<VAR>CategoryTheory.Limits.HasZeroMorphisms W₁<VAR>CategoryTheory.Limits.HasZeroMorphisms W₂<VAR>CategoryTheory.Limits.HasZeroObject W₁<VAR>CategoryTheory.Limits.HasZeroObject W₂<VAR>F : W₁ ⥤ W₂<VAR>F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<VAR>X : W₁<GOAL>((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X).f i = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>self : CategoryTheory.ShortComplex.QuasiIso φ<GOAL>CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₃.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ : CategoryTheory.ShortComplex.QuasiIso φ<VAR>hφφ' : CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')<GOAL>CategoryTheory.ShortComplex.QuasiIso φ'
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₃.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ : CategoryTheory.ShortComplex.QuasiIso φ<GOAL>CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ CategoryTheory.ShortComplex.QuasiIso φ'
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₃.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ' : CategoryTheory.ShortComplex.QuasiIso φ'<VAR>hφφ' : CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')<GOAL>CategoryTheory.ShortComplex.QuasiIso φ
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₃.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ' : CategoryTheory.ShortComplex.QuasiIso φ'<GOAL>CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ CategoryTheory.ShortComplex.QuasiIso φ
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₃.HasHomology<VAR>S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₃ ⟶ S₄<VAR>e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ'<VAR>hφ : CategoryTheory.ShortComplex.QuasiIso φ<GOAL>CategoryTheory.ShortComplex.QuasiIso φ'
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₃.HasHomology<VAR>S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₃ ⟶ S₄<VAR>e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ'<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.ShortComplex.QuasiIso φ'
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso γ.φH
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso γ.φH
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>CategoryTheory.ShortComplex.QuasiIso φ
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.ShortComplex.opMap φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>CategoryTheory.ShortComplex.QuasiIso φ<GOAL>CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.ShortComplex.opMap φ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₁.unop.HasHomology<VAR>S₂.unop.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>CategoryTheory.ShortComplex.QuasiIso φ<GOAL>CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.ShortComplex.unopMap φ)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (S₂.liftCycles φ.τ₂ ⋯)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (S₁.descOpcycles φ.τ₂ ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T) n₀ n₁ h = (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app T.obj₃ ≫ (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app T.obj₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<GOAL>CochainComplex.mappingCone.inr S.f ≫ CochainComplex.mappingCone.descShortComplex S = S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>n : ℤ<GOAL>(CochainComplex.mappingCone.inr S.f).f n ≫ (CochainComplex.mappingCone.descShortComplex S).f n = S.g.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>i j : ℤ<VAR>h : i + -1 = j<GOAL>(CochainComplex.mappingCone.inl S.f).v i j h ≫ (CochainComplex.mappingCone.descShortComplex S).f j = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ (CochainComplex.mappingCone.triangleh S.f) n₀ n₁ h = (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app (CochainComplex.mappingCone S.f) ≫ HomologicalComplex.homologyMap (CochainComplex.mappingCone.descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>QuasiIso (CochainComplex.mappingCone.descShortComplex S)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>self : c.Embedding c'<VAR>i₁ i₂ : ι<VAR>h : c.Rel i₁ i₂<GOAL>c'.Rel (self.f i₁) (self.f i₂)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>self : c.Embedding c'<GOAL>Function.Injective self.f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<GOAL>∀ (a : ι), e.op.f a = e.f a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>self : e.IsRelIff<VAR>i₁ i₂ : ι<VAR>h : c'.Rel (e.f i₁) (e.f i₂)<GOAL>c.Rel i₁ i₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i₁ i₂ : ι<GOAL>c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>iff : ∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)<GOAL>∀ (a : ι), (ComplexShape.Embedding.mk' c c' f hf iff).f a = f a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>self : e.IsTruncGE<VAR>j : ι<VAR>k' : ι'<VAR>h : c'.Rel (e.f j) k'<GOAL>∃ k, e.f k = k'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsTruncGE<VAR>j : ι<VAR>k' : ι'<VAR>h : c'.Rel (e.f j) k'<GOAL>∃ k, e.f k = k'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>self : e.IsTruncLE<VAR>i' : ι'<VAR>j : ι<VAR>h : c'.Rel i' (e.f j)<GOAL>∃ i, e.f i = i'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsTruncLE<VAR>i' : ι'<VAR>j : ι<VAR>h : c'.Rel i' (e.f j)<GOAL>∃ i, e.f i = i'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i : ι<VAR>i' : ι'<VAR>hi : e.f i = i'<GOAL>e.r i' = some i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i' : ι'<VAR>hi : ∀ (i : ι), e.f i ≠ i'<GOAL>e.r i' = none
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i : ι<GOAL>e.r (e.f i) = some i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i : ι<VAR>i' : ι'<VAR>hi : e.r i' = some i<GOAL>e.f i = i'
<VAR>n : ℕ<GOAL>ComplexShape.embeddingUpNat.f n = ↑n
<VAR>n : ℕ<GOAL>ComplexShape.embeddingDownNat.f n = -↑n
<VAR>p : ℤ<VAR>n : ℕ<GOAL>(ComplexShape.embeddingUpIntGE p).f n = p + ↑n
<VAR>p : ℤ<VAR>n : ℕ<GOAL>(ComplexShape.embeddingUpIntLE p).f n = p - ↑n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₁ = f.f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).f = K.d i j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₁ = K.X i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₂ = f.f j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₃ = K.X k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₃ = f.f k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₂ = K.X j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>i j k : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).g = K.d j k