ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c<VAR>i j : ι<GOAL>X.unop.d i j = (X.d j i).unop
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c<VAR>i : ι<GOAL>X.unop.X i = Opposite.unop (X.X i)
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c.symm<VAR>i j : ι<GOAL>X.unopSymm.d i j = (X.d j i).unop
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c.symm<VAR>i : ι<GOAL>X.unopSymm.X i = Opposite.unop (X.X i)
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>∀ {X Y : (HomologicalComplex V c)ᵒᵖ} (f : X ⟶ Y) (i : ι), ((HomologicalComplex.opFunctor V c).map f).f i = (f.unop.f i).op
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : (HomologicalComplex V c)ᵒᵖ<GOAL>(HomologicalComplex.opFunctor V c).obj X = (Opposite.unop X).op
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>∀ {X Y : HomologicalComplex Vᵒᵖ c.symm} (f : X ⟶ Y), (HomologicalComplex.opInverse V c).map f = Quiver.Hom.op { f := fun i => (f.f i).unop, comm' := ⋯ }
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c.symm<GOAL>(HomologicalComplex.opInverse V c).obj X = Opposite.op X.unopSymm
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.opEquivalence V c).functor = HomologicalComplex.opFunctor V c
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.opEquivalence V c).unitIso = HomologicalComplex.opUnitIso V c
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.opEquivalence V c).inverse = HomologicalComplex.opInverse V c
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.opEquivalence V c).counitIso = HomologicalComplex.opCounitIso V c
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ<GOAL>(HomologicalComplex.unopFunctor V c).obj X = (Opposite.unop X).unop
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>∀ {X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ} (f : X ⟶ Y) (i : ι), ((HomologicalComplex.unopFunctor V c).map f).f i = (f.unop.f i).unop
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V c.symm<GOAL>(HomologicalComplex.unopInverse V c).obj X = Opposite.op X.opSymm
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>∀ {X Y : HomologicalComplex V c.symm} (f : X ⟶ Y), (HomologicalComplex.unopInverse V c).map f = Quiver.Hom.op { f := fun i => (f.f i).op, comm' := ⋯ }
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.unopEquivalence V c).functor = HomologicalComplex.unopFunctor V c
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.unopEquivalence V c).counitIso = HomologicalComplex.unopCounitIso V c
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.unopEquivalence V c).unitIso = HomologicalComplex.unopUnitIso V c
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.unopEquivalence V c).inverse = HomologicalComplex.unopInverse V c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<GOAL>CategoryTheory.HasExt C ↔ ∀ (X Y : C) (n : ℤ), Small.{w, w'} ((DerivedCategory.singleFunctor C 0).obj X ⟶ (CategoryTheory.shiftFunctor (DerivedCategory C) n).obj ((DerivedCategory.singleFunctor C 0).obj Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<GOAL>CategoryTheory.HasExt C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y a₁<VAR>β : CategoryTheory.Abelian.Ext Y Z a₂<VAR>γ : CategoryTheory.Abelian.Ext Z T a₃<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h : a₁ + a₂ + a₃ = a<GOAL>(α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z : C<VAR>HasDerivedCategory C<VAR>a b : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y a<VAR>β : CategoryTheory.Abelian.Ext Y Z b<VAR>c : ℕ<VAR>h : a + b = c<GOAL>(α.comp β h).hom = α.hom.comp β.hom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>HasDerivedCategory C<VAR>n : ℕ<VAR>α β : CategoryTheory.Abelian.Ext X Y n<VAR>h : α.hom = β.hom<GOAL>α = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>HasDerivedCategory C<VAR>n : ℕ<VAR>α β : CategoryTheory.Abelian.Ext X Y n<GOAL>α = β ↔ α.hom = β.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>HasDerivedCategory C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.Ext.mk₀ f).hom = CategoryTheory.ShiftedHom.mk₀ ↑0 ⋯ ((DerivedCategory.singleFunctor C 0).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Abelian.Ext.mk₀ f).comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯ = CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext Z T n<GOAL>(CategoryTheory.Abelian.Ext.mk₀ f).comp ((CategoryTheory.Abelian.Ext.mk₀ g).comp α ⋯) ⋯ = (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.comp f g)).comp α ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>α β : CategoryTheory.Abelian.Ext X Y n<GOAL>(α + β).hom' = α.hom' + β.hom'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y n<GOAL>(-α).hom' = -α.hom'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<GOAL>CategoryTheory.Abelian.Ext.hom' 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z : C<VAR>n : ℕ<VAR>α₁ α₂ : CategoryTheory.Abelian.Ext X Y n<VAR>m : ℕ<VAR>β : CategoryTheory.Abelian.Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<GOAL>(α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z : C<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y n<VAR>m : ℕ<VAR>β₁ β₂ : CategoryTheory.Abelian.Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<GOAL>α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z : C<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y n<VAR>m : ℕ<VAR>β : CategoryTheory.Abelian.Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<GOAL>(-α).comp β h = -α.comp β h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z : C<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y n<VAR>m : ℕ<VAR>β : CategoryTheory.Abelian.Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<GOAL>α.comp (-β) h = -α.comp β h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X : C<VAR>Y Z : C<VAR>n : ℕ<VAR>m : ℕ<VAR>β : CategoryTheory.Abelian.Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<GOAL>CategoryTheory.Abelian.Ext.comp 0 β h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y n<VAR>Z : C<VAR>m p : ℕ<VAR>h : n + m = p<GOAL>α.comp 0 h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y n<GOAL>(CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.id X)).comp α ⋯ = α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>α : CategoryTheory.Abelian.Ext X Y n<GOAL>α.comp (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.id Y)) ⋯ = α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<GOAL>CategoryTheory.Abelian.Ext.mk₀ 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>HasDerivedCategory C<GOAL>CategoryTheory.Abelian.Ext.hom 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>Y : C<VAR>n : ℕ<VAR>X₁ X₂ : C<VAR>α β : CategoryTheory.Abelian.Ext (X₁ ⊞ X₂) Y n<VAR>h₁ : (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp α ⋯ = (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp β ⋯<VAR>h₂ : (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp α ⋯ = (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp β ⋯<GOAL>α = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>HasDerivedCategory C<VAR>α β : CategoryTheory.Abelian.Ext X Y n<GOAL>(α + β).hom = α.hom + β.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>HasDerivedCategory C<VAR>α : CategoryTheory.Abelian.Ext X Y n<GOAL>(-α).hom = -α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y : C<VAR>n : ℕ<VAR>HasDerivedCategory C<VAR>α : CategoryTheory.Abelian.Ext X Y n<GOAL>CategoryTheory.Abelian.Ext.homAddEquiv α = α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X Y Z : C<VAR>a b c : ℕ<VAR>h : a + b = c<VAR>α : CategoryTheory.Abelian.Ext X Y a<VAR>β : CategoryTheory.Abelian.Ext Y Z b<GOAL>((CategoryTheory.Abelian.Ext.bilinearComp X Y Z a b c h) α) β = α.comp β h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X : C<VAR>n : ℕ<GOAL>∀ {X_1 Y : C} (f : X_1 ⟶ Y), (CategoryTheory.Abelian.extFunctorObj X n).map f = AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ f).postcomp X ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>X : C<VAR>n : ℕ<VAR>Y : C<GOAL>(CategoryTheory.Abelian.extFunctorObj X n).obj Y = AddCommGrp.of (CategoryTheory.Abelian.Ext X Y n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>n : ℕ<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Abelian.extFunctor n).obj X = CategoryTheory.Abelian.extFunctorObj (Opposite.unop X) n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasExt C<VAR>n : ℕ<VAR>X₁ X₂ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>Y : C<GOAL>((CategoryTheory.Abelian.extFunctor n).map f).app Y = AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (CategoryTheory.Abelian.Ext.mk₀ f.unop).comp α ⋯) ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.ShortExact<GOAL>CategoryTheory.Mono S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.ShortExact<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.ShortExact<GOAL>CategoryTheory.Epi S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<GOAL>CategoryTheory.Mono S.f → CategoryTheory.Epi S.g → S.ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<GOAL>S₂.ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<GOAL>S₁.ShortExact ↔ S₂.ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.ShortExact<GOAL>S.op.ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.ShortExact<GOAL>S.unop.ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.ShortExact ↔ S.op.ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.ShortExact ↔ S.unop.ShortExact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.ShortExact<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<VAR>CategoryTheory.Mono (F.map S.f)<VAR>CategoryTheory.Epi (F.map S.g)<GOAL>(S.map F).ShortExact
<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>hS : S.ShortExact<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<GOAL>(S.map F).ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<VAR>CategoryTheory.Balanced C<GOAL>CategoryTheory.IsIso S.f ↔ CategoryTheory.Limits.IsZero S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<VAR>CategoryTheory.Balanced C<GOAL>CategoryTheory.IsIso S.g ↔ CategoryTheory.Limits.IsZero S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Balanced C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>CategoryTheory.IsIso φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₃<GOAL>CategoryTheory.IsIso φ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Balanced C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<GOAL>CategoryTheory.IsIso φ.τ₁ → CategoryTheory.IsIso φ.τ₃ → CategoryTheory.IsIso φ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>S.ShortExact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>(CategoryTheory.forget₂ C Ab).PreservesZeroMorphisms<VAR>S : CategoryTheory.ShortComplex C<VAR>x : ↑((CategoryTheory.forget₂ C Ab).obj S.X₁)<GOAL>((CategoryTheory.forget₂ C Ab).map S.g) (((CategoryTheory.forget₂ C Ab).map S.f) x) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑((CategoryTheory.forget₂ C Ab).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ Function.Injective ((CategoryTheory.forget C).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑((CategoryTheory.forget₂ C Ab).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ((CategoryTheory.forget C).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ (S.map (CategoryTheory.forget₂ C Ab)).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ ∀ (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂)), ((CategoryTheory.forget₂ C Ab).map S.g) x₂ = 0 → ∃ x₁, ((CategoryTheory.forget₂ C Ab).map S.f) x₁ = x₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>Function.Injective ⇑((CategoryTheory.forget₂ C Ab).map S.f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>Function.Surjective ⇑((CategoryTheory.forget₂ C Ab).map S.g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Preadditive C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂)<VAR>hx₂ : ((CategoryTheory.forget₂ C Ab).map S.g) x₂ = 0<GOAL>((CategoryTheory.forget₂ C Ab).map S.iCycles) (S.cyclesMk x₂ hx₂) = x₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Abelian C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>D : CategoryTheory.ShortComplex.SnakeInput C<VAR>x₃ : (CategoryTheory.forget C).obj D.L₀.X₃<VAR>x₂ : (CategoryTheory.forget C).obj D.L₁.X₂<VAR>x₁ : (CategoryTheory.forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Abelian C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>D : CategoryTheory.ShortComplex.SnakeInput C<VAR>x₃ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₀.X₃)<VAR>x₂ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₁.X₂)<VAR>x₁ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₂.X₁)<VAR>h₂ : ((CategoryTheory.forget₂ C Ab).map D.L₁.g) x₂ = ((CategoryTheory.forget₂ C Ab).map D.v₀₁.τ₃) x₃<VAR>h₁ : ((CategoryTheory.forget₂ C Ab).map D.L₂.f) x₁ = ((CategoryTheory.forget₂ C Ab).map D.v₁₂.τ₂) x₂<GOAL>((CategoryTheory.forget₂ C Ab).map D.δ) x₃ = ((CategoryTheory.forget₂ C Ab).map D.v₂₃.τ₁) x₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℤ<VAR>K : CochainComplex C ℤ<VAR>i j : ℤ<GOAL>((CochainComplex.shiftFunctor C n).obj K).d i j = n.negOnePow • K.d (i + n) (j + n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℤ<VAR>K : CochainComplex C ℤ<VAR>i : ℤ<GOAL>((CochainComplex.shiftFunctor C n).obj K).X i = K.X (i + n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℤ<GOAL>∀ {X Y : CochainComplex C ℤ} (φ : X ⟶ Y) (i : ℤ), ((CochainComplex.shiftFunctor C n).map φ).f i = φ.f (i + n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℤ<VAR>h : n = 0<VAR>X : CochainComplex C ℤ<VAR>i : ℤ<GOAL>((CochainComplex.shiftFunctorZero' C n h).hom.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℤ<VAR>h : n = 0<VAR>X : CochainComplex C ℤ<VAR>i : ℤ<GOAL>((CochainComplex.shiftFunctorZero' C n h).inv.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).inv