ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>G.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<VAR>G.PreservesRightHomologyOf S<VAR>S.HasHomology<VAR>τ : F ⟶ G<GOAL>CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ) = CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).hom (CategoryTheory.CategoryStruct.comp (τ.app S.homology) (S.mapHomologyIso G).inv)
<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>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>ψl : CategoryTheory.ShortComplex.LeftHomologyMapData φ hl₁ hl₂<VAR>(F.mapShortComplex.obj S₁).HasHomology<VAR>(F.mapShortComplex.obj S₂).HasHomology<VAR>hl₁.IsPreservedBy F<VAR>hl₂.IsPreservedBy F<GOAL>CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.IsIso (F.map ψl.φ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>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hr₁ : S₁.RightHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>ψr : CategoryTheory.ShortComplex.RightHomologyMapData φ hr₁ hr₂<VAR>(F.mapShortComplex.obj S₁).HasHomology<VAR>(F.mapShortComplex.obj S₂).HasHomology<VAR>hr₁.IsPreservedBy F<VAR>hr₂.IsPreservedBy F<GOAL>CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.IsIso (F.map ψr.φ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>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>(F.mapShortComplex.obj S₁).HasHomology<VAR>(F.mapShortComplex.obj S₂).HasHomology<VAR>F.PreservesLeftHomologyOf S₁<VAR>F.PreservesLeftHomologyOf S₂<VAR>F.ReflectsIsomorphisms<GOAL>CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
<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>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>(F.mapShortComplex.obj S₁).HasHomology<VAR>(F.mapShortComplex.obj S₂).HasHomology<VAR>F.PreservesRightHomologyOf S₁<VAR>F.PreservesRightHomologyOf S₂<VAR>F.ReflectsIsomorphisms<GOAL>CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
<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>F G : CategoryTheory.Functor C D<VAR>τ : F ⟶ G<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>G.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<VAR>G.PreservesRightHomologyOf S<GOAL>τ.app S.homology = CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ)) (S.mapHomologyIso G).hom)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<VAR>n : ℤ<GOAL>(CochainComplex.homOfDegreewiseSplit S σ).f n = (↑(CochainComplex.cocycleOfDegreewiseSplit S σ)).v n (n + 1) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<GOAL>(CochainComplex.triangleOfDegreewiseSplit S σ).mor₁ = S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<GOAL>(CochainComplex.triangleOfDegreewiseSplit S σ).mor₂ = S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<GOAL>(CochainComplex.triangleOfDegreewiseSplit S σ).mor₃ = CochainComplex.homOfDegreewiseSplit S σ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<GOAL>(CochainComplex.triangleOfDegreewiseSplit S σ).obj₁ = S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<GOAL>(CochainComplex.triangleOfDegreewiseSplit S σ).obj₃ = S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<GOAL>(CochainComplex.triangleOfDegreewiseSplit S σ).obj₂ = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>i : ℤ<GOAL>(CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).hom.f i = (CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>i : ℤ<GOAL>(CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv.f i = (CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<GOAL>(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f ≫ (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv = -CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<GOAL>(CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv ≫ (CochainComplex.mappingCone.triangle (CochainComplex.homOfDegreewiseSplit S σ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangleRotateShortComplex φ).X₁ = (CochainComplex.mappingCone.triangle φ).rotate.obj₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangleRotateShortComplex φ).g = (CochainComplex.mappingCone.triangle φ).rotate.mor₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangleRotateShortComplex φ).X₃ = (CochainComplex.mappingCone.triangle φ).rotate.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangleRotateShortComplex φ).X₂ = (CochainComplex.mappingCone.triangle φ).rotate.obj₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangleRotateShortComplex φ).f = (CochainComplex.mappingCone.triangle φ).rotate.mor₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n : ℤ<GOAL>(CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ n).r = (CochainComplex.mappingCone.snd φ).v n n ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n : ℤ<GOAL>(CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ n).s = -(CochainComplex.mappingCone.inl φ).v (n + 1) n ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p : ℤ<GOAL>(↑(CochainComplex.cocycleOfDegreewiseSplit (CochainComplex.mappingCone.triangleRotateShortComplex φ) (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ))).v p (p + 1) ⋯ = -φ.f (p + { as := 1 }.as)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>self : QuasiIsoAt f i<GOAL>CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>QuasiIsoAt f i ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>L.HasHomology j<VAR>(K.sc' i j k).HasHomology<VAR>(L.sc' i j k).HasHomology<GOAL>QuasiIsoAt f j ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C c i j k).map f)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>QuasiIsoAt f i ↔ CategoryTheory.IsIso (HomologicalComplex.homologyMap f i)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>hK : K.ExactAt i<GOAL>QuasiIsoAt f i ↔ L.ExactAt i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>hL : L.ExactAt i<GOAL>QuasiIsoAt f i ↔ K.ExactAt i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>QuasiIsoAt f i<GOAL>(isoOfQuasiIsoAt f i).hom = HomologicalComplex.homologyMap f i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>QuasiIsoAt f i<GOAL>HomologicalComplex.homologyMap f i ≫ (isoOfQuasiIsoAt f i).inv = 𝟙 (K.homology i)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>QuasiIsoAt f i<GOAL>(isoOfQuasiIsoAt f i).inv ≫ HomologicalComplex.homologyMap f i = 𝟙 (L.homology i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : CochainComplex C ℕ<VAR>f : K ⟶ L<VAR>HomologicalComplex.HasHomology K 0<VAR>HomologicalComplex.HasHomology L 0<VAR>(HomologicalComplex.sc' K 0 0 1).HasHomology<VAR>(HomologicalComplex.sc' L 0 0 1).HasHomology<GOAL>QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : ChainComplex C ℕ<VAR>f : K ⟶ L<VAR>HomologicalComplex.HasHomology K 0<VAR>HomologicalComplex.HasHomology L 0<VAR>(HomologicalComplex.sc' K 1 0 0).HasHomology<VAR>(HomologicalComplex.sc' L 1 0 0).HasHomology<GOAL>QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map f)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>self : QuasiIso f<VAR>i : ι<GOAL>QuasiIsoAt f i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<GOAL>QuasiIso f ↔ ∀ (i : ι), QuasiIsoAt f i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>M.HasHomology i<VAR>hφ : QuasiIsoAt φ i<VAR>hφφ' : QuasiIsoAt (φ ≫ φ') i<GOAL>QuasiIsoAt φ' i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>M.HasHomology i<VAR>hφ : QuasiIsoAt φ i<GOAL>QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ' i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ<GOAL>QuasiIso (φ ≫ φ') ↔ QuasiIso φ'
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso φ'
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>M.HasHomology i<VAR>hφ' : QuasiIsoAt φ' i<VAR>hφφ' : QuasiIsoAt (φ ≫ φ') i<GOAL>QuasiIsoAt φ i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>M.HasHomology i<VAR>hφ' : QuasiIsoAt φ' i<GOAL>QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>∀ (i : ι), M.HasHomology i<VAR>hφ' : QuasiIso φ'<GOAL>QuasiIso (φ ≫ φ') ↔ QuasiIso φ
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ'<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso φ
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : K' ⟶ L'<VAR>e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ'<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>∀ (i : ι), K'.HasHomology i<VAR>∀ (i : ι), L'.HasHomology i<GOAL>QuasiIso φ ↔ QuasiIso φ'
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : K' ⟶ L'<VAR>e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ'<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>∀ (i : ι), K'.HasHomology i<VAR>∀ (i : ι), L'.HasHomology i<VAR>hφ : QuasiIso φ<GOAL>QuasiIso φ'
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>CategoryTheory.Category.{u_4, u_2} C₁<VAR>CategoryTheory.Category.{u_5, u_3} C₂<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Preadditive C₂<VAR>K L : HomologicalComplex C₁ c<VAR>φ : K ⟶ L<VAR>F : C₁ ⥤ C₂<VAR>F.Additive<VAR>F.PreservesHomology<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>((F.mapHomologicalComplex c).obj K).HasHomology i<VAR>((F.mapHomologicalComplex c).obj L).HasHomology i<VAR>F.ReflectsIsomorphisms<GOAL>QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>CategoryTheory.Category.{u_4, u_2} C₁<VAR>CategoryTheory.Category.{u_5, u_3} C₂<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Preadditive C₂<VAR>K L : HomologicalComplex C₁ c<VAR>φ : K ⟶ L<VAR>F : C₁ ⥤ C₂<VAR>F.Additive<VAR>F.PreservesHomology<VAR>∀ (i : ι), K.HasHomology i<VAR>∀ (i : ι), L.HasHomology i<VAR>∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i<VAR>∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i<VAR>F.ReflectsIsomorphisms<GOAL>QuasiIso ((F.mapHomologicalComplex c).map φ) ↔ QuasiIso φ
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>CategoryTheory.CategoryWithHomology C<VAR>f : K ⟶ L<GOAL>HomologicalComplex.quasiIso C c f ↔ QuasiIso f
<VAR>ι : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>CategoryTheory.CategoryWithHomology C<GOAL>HomologicalComplex.homotopyEquivalences C c ≤ HomologicalComplex.quasiIso C c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>self : HomologicalComplex.HasHomotopyCofiber φ<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i : ι<GOAL>HomologicalComplex.homotopyCofiber.inrX φ i ≫ HomologicalComplex.homotopyCofiber.sndX φ i = 𝟙 (G.X i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<GOAL>HomologicalComplex.homotopyCofiber.sndX φ i ≫ HomologicalComplex.homotopyCofiber.inrX φ i = 𝟙 (HomologicalComplex.homotopyCofiber.X φ i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>HomologicalComplex.homotopyCofiber.inlX φ i j hij ≫ HomologicalComplex.homotopyCofiber.fstX φ j i hij = 𝟙 (F.X i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>HomologicalComplex.homotopyCofiber.inlX φ i j hij ≫ HomologicalComplex.homotopyCofiber.sndX φ j = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>HomologicalComplex.homotopyCofiber.inrX φ i ≫ HomologicalComplex.homotopyCofiber.fstX φ i j hij = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>f g : A ⟶ HomologicalComplex.homotopyCofiber.X φ i<VAR>h₁ : f ≫ HomologicalComplex.homotopyCofiber.fstX φ i j hij = g ≫ HomologicalComplex.homotopyCofiber.fstX φ i j hij<VAR>h₂ : f ≫ HomologicalComplex.homotopyCofiber.sndX φ i = g ≫ HomologicalComplex.homotopyCofiber.sndX φ i<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<VAR>A : C<VAR>f g : A ⟶ HomologicalComplex.homotopyCofiber.X φ i<VAR>h : f ≫ HomologicalComplex.homotopyCofiber.sndX φ i = g ≫ HomologicalComplex.homotopyCofiber.sndX φ i<GOAL>f = g