ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 : ι<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₃ = f.f (c.next 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 : ι<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₁ = f.f (c.prev 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 : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor C c i).obj K).g = K.d i (c.next 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 : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor C c i).obj K).X₃ = K.X (c.next 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 : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor C c i).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 : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor C c i).obj K).f = K.d (c.prev i) 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 : ι<VAR>K : HomologicalComplex C c<GOAL>((HomologicalComplex.shortComplexFunctor C c i).obj K).X₁ = K.X (c.prev 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 : ι<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).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>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>X : HomologicalComplex C c<GOAL>((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₃ = (X.XIsoOfEq hk).inv
<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>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>X : HomologicalComplex C c<GOAL>((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₂ = 𝟙 (X.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>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>X : HomologicalComplex C c<GOAL>((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₂ = 𝟙 (X.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>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>X : HomologicalComplex C c<GOAL>((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₁ = (X.XIsoOfEq hi).hom
<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>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>X : HomologicalComplex C c<GOAL>((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₁ = (X.XIsoOfEq hi).inv
<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>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>X : HomologicalComplex C c<GOAL>((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₃ = (X.XIsoOfEq hk).hom
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>A : C<VAR>k : A ⟶ K.X i<VAR>j : ι<VAR>hj : c.next i = j<VAR>hk : k ≫ K.d i j = 0<GOAL>K.liftCycles k j hj hk ≫ K.iCycles i = 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<GOAL>K.iCycles i ≫ K.d i j = 0
<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>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology j<GOAL>K.toCycles i j ≫ K.iCycles j = 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>K : HomologicalComplex C c<VAR>i j k : ι<VAR>K.HasHomology k<GOAL>K.d i j ≫ K.toCycles j k = 0
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>A' A : C<VAR>k : A ⟶ K.X i<VAR>j : ι<VAR>hj : c.next i = j<VAR>hk : k ≫ K.d i j = 0<VAR>α : A' ⟶ A<GOAL>α ≫ K.liftCycles k j hj hk = K.liftCycles (α ≫ k) j hj ⋯
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>A : C<VAR>k : A ⟶ K.X i<VAR>j : ι<VAR>hj : c.next i = j<VAR>i' : ι<VAR>x : A ⟶ K.X i'<VAR>hx : k = x ≫ K.d i' i<GOAL>K.liftCycles k j hj ⋯ ≫ K.homologyπ i = 0
<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>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology j<GOAL>K.toCycles i j ≫ K.homologyπ j = 0
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>A : C<VAR>k : K.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>hk : K.d j i ≫ k = 0<GOAL>K.pOpcycles i ≫ K.descOpcycles k j hj hk = 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<VAR>K.HasHomology j<GOAL>K.d i j ≫ K.pOpcycles j = 0
<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>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<GOAL>K.pOpcycles i ≫ K.fromOpcycles i j = 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>K : HomologicalComplex C c<VAR>i j k : ι<VAR>K.HasHomology i<GOAL>K.fromOpcycles i j ≫ K.d j k = 0
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>A A' : C<VAR>k : K.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>hk : K.d j i ≫ k = 0<VAR>α : A ⟶ A'<GOAL>K.descOpcycles k j hj hk ≫ α = K.descOpcycles (k ≫ α) j hj ⋯
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>A : C<VAR>k : K.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>i' : ι<VAR>x : K.X i' ⟶ A<VAR>hx : k = K.d i i' ≫ x<GOAL>K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0
<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>K : HomologicalComplex C c<VAR>i j : ι<VAR>K.HasHomology i<GOAL>K.homologyι i ≫ K.fromOpcycles i j = 0
<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>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.cyclesMap φ i ≫ L.iCycles i = K.iCycles i ≫ φ.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>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>K.pOpcycles i ≫ HomologicalComplex.opcyclesMap φ i = φ.f i ≫ L.pOpcycles 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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<GOAL>HomologicalComplex.homologyMap (𝟙 K) i = 𝟙 (K.homology 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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<GOAL>HomologicalComplex.cyclesMap (𝟙 K) i = 𝟙 (K.cycles 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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<GOAL>HomologicalComplex.opcyclesMap (𝟙 K) i = 𝟙 (K.opcycles 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>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<GOAL>HomologicalComplex.homologyMap (φ ≫ ψ) i = HomologicalComplex.homologyMap φ i ≫ HomologicalComplex.homologyMap ψ 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>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<GOAL>HomologicalComplex.cyclesMap (φ ≫ ψ) i = HomologicalComplex.cyclesMap φ i ≫ HomologicalComplex.cyclesMap ψ 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>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<GOAL>HomologicalComplex.opcyclesMap (φ ≫ ψ) i = HomologicalComplex.opcyclesMap φ i ≫ HomologicalComplex.opcyclesMap ψ 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>K L : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.homologyMap 0 i = 0
<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>K L : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.cyclesMap 0 i = 0
<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>K L : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.opcyclesMap 0 i = 0
<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>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>K.homologyπ i ≫ HomologicalComplex.homologyMap φ i = HomologicalComplex.cyclesMap φ i ≫ L.homologyπ 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>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.homologyMap φ i ≫ L.homologyι i = K.homologyι i ≫ HomologicalComplex.opcyclesMap φ 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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<GOAL>K.homologyπ i ≫ K.homologyι i = K.iCycles i ≫ K.pOpcycles 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>K L : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>A : C<VAR>k : L.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>hk : L.d j i ≫ k = 0<VAR>φ : K ⟶ L<GOAL>HomologicalComplex.opcyclesMap φ i ≫ L.descOpcycles k j hj hk = K.descOpcycles (φ.f i ≫ k) j hj ⋯
<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>K L : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>A : C<VAR>k : A ⟶ K.X i<VAR>j : ι<VAR>hj : c.next i = j<VAR>hk : k ≫ K.d i j = 0<VAR>φ : K ⟶ L<GOAL>K.liftCycles k j hj hk ≫ HomologicalComplex.cyclesMap φ i = L.liftCycles (k ≫ φ.f i) j hj ⋯
<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 : ι<VAR>CategoryTheory.CategoryWithHomology C<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), (HomologicalComplex.homologyFunctor C c i).map f = HomologicalComplex.homologyMap 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<GOAL>(HomologicalComplex.homologyFunctor C c i).obj K = K.homology 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>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<VAR>i : ι<GOAL>(HomologicalComplex.gradedHomologyFunctor C c).obj K i = K.homology 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>CategoryTheory.CategoryWithHomology C<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y) (i : ι), (HomologicalComplex.gradedHomologyFunctor C c).map f i = HomologicalComplex.homologyMap 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<GOAL>(HomologicalComplex.cyclesFunctor C c i).obj K = K.cycles 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), (HomologicalComplex.cyclesFunctor C c i).map f = HomologicalComplex.cyclesMap 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<GOAL>∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), (HomologicalComplex.opcyclesFunctor C c i).map f = HomologicalComplex.opcyclesMap 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<GOAL>(HomologicalComplex.opcyclesFunctor C c i).obj K = K.opcycles 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<GOAL>(HomologicalComplex.natTransHomologyπ C c i).app K = K.homologyπ 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : HomologicalComplex C c<GOAL>(HomologicalComplex.natTransHomologyι C c i).app K = K.homologyι 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>X : HomologicalComplex C c<GOAL>(HomologicalComplex.homologyFunctorIso C c i).inv.app X = 𝟙 (X.homology 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 : ι<VAR>CategoryTheory.CategoryWithHomology C<VAR>X : HomologicalComplex C c<GOAL>(HomologicalComplex.homologyFunctorIso C c i).hom.app X = 𝟙 (X.homology 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>CategoryTheory.IsIso (K.iCycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>(K.iCyclesIso i j hj h).hom = K.iCycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>K.iCycles i ≫ (K.iCyclesIso i j hj h).inv = 𝟙 (K.cycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>(K.iCyclesIso i j hj h).inv ≫ K.iCycles i = 𝟙 (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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>CategoryTheory.IsIso (K.homologyι 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>(K.isoHomologyι i j hj h).hom = K.homologyι 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>K.homologyι i ≫ (K.isoHomologyι i j hj h).inv = 𝟙 (K.homology 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hj : c.next i = j<VAR>h : K.d i j = 0<VAR>K.HasHomology i<GOAL>(K.isoHomologyι i j hj h).inv ≫ K.homologyι i = 𝟙 (K.opcycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>CategoryTheory.IsIso (K.pOpcycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>(K.pOpcyclesIso i j hi h).hom = K.pOpcycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>K.pOpcycles j ≫ (K.pOpcyclesIso i j hi h).inv = 𝟙 (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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>(K.pOpcyclesIso i j hi h).inv ≫ K.pOpcycles j = 𝟙 (K.opcycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>CategoryTheory.IsIso (K.homologyπ 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>(K.isoHomologyπ i j hi h).hom = K.homologyπ 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>K.homologyπ j ≫ (K.isoHomologyπ i j hi h).inv = 𝟙 (K.cycles 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>K : HomologicalComplex C c<VAR>i j : ι<VAR>hi : c.prev j = i<VAR>h : K.d i j = 0<VAR>K.HasHomology j<GOAL>(K.isoHomologyπ i j hi h).inv ≫ K.homologyπ j = 𝟙 (K.homology 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>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<VAR>CategoryTheory.Epi (φ.f i)<VAR>hi : ∀ (j : ι), ¬c.Rel i j<GOAL>CategoryTheory.Epi (HomologicalComplex.homologyMap φ 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>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>j : ι<VAR>K.HasHomology j<VAR>L.HasHomology j<VAR>CategoryTheory.Mono (φ.f j)<VAR>hj : ∀ (i : ι), ¬c.Rel i j<GOAL>CategoryTheory.Mono (HomologicalComplex.homologyMap φ 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>K : HomologicalComplex C c<VAR>i : ι<GOAL>K.ExactAt i ↔ (K.sc i).Exact
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>hK : K.ExactAt i<VAR>L : HomologicalComplex C c<VAR>e : K ≅ L<GOAL>L.ExactAt 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>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<GOAL>K.ExactAt j ↔ (K.sc' i j k).Exact
<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>K : HomologicalComplex C c<VAR>i : ι<VAR>K.HasHomology i<GOAL>K.ExactAt i ↔ CategoryTheory.Limits.IsZero (K.homology i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : ChainComplex C ℕ<VAR>φ : K ⟶ L<VAR>HomologicalComplex.HasHomology K 0<VAR>HomologicalComplex.HasHomology L 0<GOAL>K.isoHomologyι₀.inv ≫ HomologicalComplex.homologyMap φ 0 = HomologicalComplex.opcyclesMap φ 0 ≫ L.isoHomologyι₀.inv