ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>d : D<GOAL>∀ {X Y : (CategoryTheory.CostructuredArrow F d)ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.CostructuredArrow.toStructuredArrow F d).map f = CategoryTheory.StructuredArrow.homMk f.unop.left.op ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>d : D<GOAL>∀ {X Y : (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.CostructuredArrow.toStructuredArrow' F d).map f = CategoryTheory.StructuredArrow.homMk f.unop.left.unop ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>d : D<VAR>X : (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ<GOAL>(CategoryTheory.CostructuredArrow.toStructuredArrow' F d).obj X = CategoryTheory.StructuredArrow.mk (Opposite.unop X).hom.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : W₁.MapFactorizationData W₂ f<GOAL>W₂ self.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : W₁.MapFactorizationData W₂ f<GOAL>W₁ self.i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : W₁.MapFactorizationData W₂ f<GOAL>CategoryTheory.CategoryStruct.comp self.i self.p = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>self : W₁.HasFactorization W₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Nonempty (W₁.MapFactorizationData W₂ f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<GOAL>W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>self : W₁.FunctorialFactorizationData W₂<VAR>f : CategoryTheory.Arrow C<GOAL>W₁ (self.i.app f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>self : W₁.FunctorialFactorizationData W₂<GOAL>CategoryTheory.CategoryStruct.comp self.i self.p = CategoryTheory.Arrow.leftToRight
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>self : W₁.FunctorialFactorizationData W₂<VAR>f : CategoryTheory.Arrow C<GOAL>W₂ (self.p.app f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>f : CategoryTheory.Arrow C<GOAL>CategoryTheory.CategoryStruct.comp (data.i.app f) (data.p.app f) = f.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<VAR>φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g<GOAL>CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (data.mapZ φ) = CategoryTheory.CategoryStruct.comp φ.left (data.factorizationData g).i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<VAR>φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g<GOAL>CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.factorizationData g).p = CategoryTheory.CategoryStruct.comp (data.factorizationData f).p φ.right
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>data.mapZ (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f)) = CategoryTheory.CategoryStruct.id (data.factorizationData f).Z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<VAR>φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g<VAR>X'' Y'' : C<VAR>h : X'' ⟶ Y''<VAR>ψ : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk h<GOAL>data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.mapZ ψ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} J<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Functor J C)} (τ : X ⟶ Y) (j : J), ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).map τ).app j = data.mapZ { left := τ.left.app j, right := τ.right.app j, w := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} J<VAR>f : CategoryTheory.Arrow (CategoryTheory.Functor J C)<VAR>j : J<GOAL>((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).obj j = (data.factorizationData (f.hom.app j)).Z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} J<VAR>f : CategoryTheory.Arrow (CategoryTheory.Functor J C)<GOAL>∀ {X Y : J} (φ : X ⟶ Y), ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).map φ = data.mapZ { left := f.left.map φ, right := f.right.map φ, w := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W₁ W₂ : CategoryTheory.MorphismProperty C<VAR>self : W₁.HasFunctorialFactorization W₂<GOAL>Nonempty (W₁.FunctorialFactorizationData W₂)
<VAR>C : Type u<VAR>X Y Z : CategoryTheory.FreeMonoidalCategory C<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>⟦f.comp g⟧ = CategoryTheory.CategoryStruct.comp ⟦f⟧ ⟦g⟧
<VAR>C : Type u<VAR>X₁ Y₁ X₂ Y₂ : CategoryTheory.FreeMonoidalCategory C<VAR>f : X₁.Hom Y₁<VAR>g : X₂.Hom Y₂<GOAL>⟦f.tensor g⟧ = CategoryTheory.MonoidalCategory.tensorHom ⟦f⟧ ⟦g⟧
<VAR>C : Type u<VAR>X : CategoryTheory.FreeMonoidalCategory C<VAR>Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C<VAR>f : Y₁.Hom Y₂<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f⟧ = CategoryTheory.MonoidalCategory.whiskerLeft X ⟦f⟧
<VAR>C : Type u<VAR>X₁ X₂ : CategoryTheory.FreeMonoidalCategory C<VAR>f : X₁.Hom X₂<VAR>Y : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦f.whiskerRight Y⟧ = CategoryTheory.MonoidalCategory.whiskerRight ⟦f⟧ Y
<VAR>C : Type u<VAR>X : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.id X⟧ = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>X Y Z : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z⟧ = (CategoryTheory.MonoidalCategory.associator X Y Z).hom
<VAR>C : Type u<VAR>X Y Z : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z⟧ = (CategoryTheory.MonoidalCategory.associator X Y Z).inv
<VAR>C : Type u<VAR>X : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X⟧ = (CategoryTheory.MonoidalCategory.rightUnitor X).hom
<VAR>C : Type u<VAR>X : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X⟧ = (CategoryTheory.MonoidalCategory.rightUnitor X).inv
<VAR>C : Type u<VAR>X : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.l_hom X⟧ = (CategoryTheory.MonoidalCategory.leftUnitor X).hom
<VAR>C : Type u<VAR>X : CategoryTheory.FreeMonoidalCategory C<GOAL>⟦CategoryTheory.FreeMonoidalCategory.Hom.l_inv X⟧ = (CategoryTheory.MonoidalCategory.leftUnitor X).inv
<VAR>C : Type u<VAR>X Y : CategoryTheory.FreeMonoidalCategory C<GOAL>X.tensor Y = CategoryTheory.MonoidalCategory.tensorObj X Y
<VAR>C : Type u<GOAL>CategoryTheory.FreeMonoidalCategory.unit = 𝟙_ (CategoryTheory.FreeMonoidalCategory C)
<VAR>C : Type u<VAR>motive : {X Y : CategoryTheory.FreeMonoidalCategory C} → (X ⟶ Y) → Prop<VAR>X Y : CategoryTheory.FreeMonoidalCategory C<VAR>t : X ⟶ Y<VAR>id : ∀ (X : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.CategoryStruct.id X)<VAR>α_hom : ∀ (X Y Z : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.MonoidalCategory.associator X Y Z).hom<VAR>α_inv : ∀ (X Y Z : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.MonoidalCategory.associator X Y Z).inv<VAR>l_hom : ∀ (X : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.MonoidalCategory.leftUnitor X).hom<VAR>l_inv : ∀ (X : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.MonoidalCategory.leftUnitor X).inv<VAR>ρ_hom : ∀ (X : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.MonoidalCategory.rightUnitor X).hom<VAR>ρ_inv : ∀ (X : CategoryTheory.FreeMonoidalCategory C), motive (CategoryTheory.MonoidalCategory.rightUnitor X).inv<VAR>comp : ∀ {X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (CategoryTheory.CategoryStruct.comp f g)<VAR>whiskerLeft : ∀ (X : CategoryTheory.FreeMonoidalCategory C) {Y Z : CategoryTheory.FreeMonoidalCategory C} (f : Y ⟶ Z), motive f → motive (CategoryTheory.MonoidalCategory.whiskerLeft X f)<VAR>whiskerRight : ∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y) (Z : CategoryTheory.FreeMonoidalCategory C), motive f → motive (CategoryTheory.MonoidalCategory.whiskerRight f Z)<GOAL>motive t
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>self : F.IsHomological<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.PreservesZeroMorphisms<VAR>hF : ∀ (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), ∃ T' e, ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T' ⋯).map F).Exact<GOAL>F.IsHomological
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F₁ F₂ : CategoryTheory.Functor C A<VAR>F₁.IsHomological<VAR>e : F₁ ≅ F₂<GOAL>F₂.IsHomological
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>X : C<GOAL>F.homologicalKernel.P X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((F.shift n).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated D<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>CategoryTheory.Abelian A<VAR>L : CategoryTheory.Functor C D<VAR>L.CommShift ℤ<VAR>L.IsTriangulated<VAR>L.mapArrow.EssSurj<VAR>F : CategoryTheory.Functor D A<VAR>G : CategoryTheory.Functor C A<VAR>e : L.comp F ≅ G<VAR>G.IsHomological<GOAL>F.IsHomological
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>F : CategoryTheory.Functor C A<VAR>F.ShiftSequence ℤ<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>CategoryTheory.CategoryStruct.comp ((F.shift n₀).map φ.hom₃) (F.homologySequenceδ T' n₀ n₁ h) = CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map φ.hom₁)
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) = 0
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) = 0
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ : ℤ<GOAL>CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) = 0
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ : ℤ<GOAL>(CategoryTheory.ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯).Exact
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(CategoryTheory.ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯).Exact
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(CategoryTheory.ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯).Exact
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ : ℤ<GOAL>CategoryTheory.Epi ((F.shift n₀).map T.mor₁) ↔ (F.shift n₀).map T.mor₂ = 0
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>CategoryTheory.Mono ((F.shift n₁).map T.mor₁) ↔ F.homologySequenceδ T n₀ n₁ h = 0
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>CategoryTheory.Epi ((F.shift n₀).map T.mor₂) ↔ F.homologySequenceδ T n₀ n₁ h = 0
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ : ℤ<GOAL>CategoryTheory.Mono ((F.shift n₀).map T.mor₂) ↔ (F.shift n₀).map T.mor₁ = 0
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.homologicalKernel.W f ↔ ∀ (n : ℤ), CategoryTheory.IsIso ((F.shift n).map f)
<VAR>C : Type u_1<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Category.{u_4, u_3} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor C A<VAR>F.IsHomological<VAR>F.ShiftSequence ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>n : ℕ<VAR>X : C<GOAL>(CategoryTheory.Tor C n).obj X = ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X).leftDerived n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>n : ℕ<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Tor C n).map f = CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f) n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>n : ℕ<VAR>k j : C<GOAL>((CategoryTheory.Tor' C n).obj k).obj j = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).obj k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>n : ℕ<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>((CategoryTheory.Tor' C n).map f).app Z = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj Z).leftDerived n).map f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>n : ℕ<VAR>X Y : C<VAR>Z : C<VAR>f : X ⟶ Y<GOAL>((CategoryTheory.Tor' C n).obj Z).map f = (CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringRight C).map f) n).app Z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>X Y : C<VAR>CategoryTheory.Projective Y<VAR>n : ℕ<GOAL>CategoryTheory.Limits.IsZero (((CategoryTheory.Tor C (n + 1)).obj X).obj Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>X Y : C<VAR>CategoryTheory.Projective X<VAR>n : ℕ<GOAL>CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' C (n + 1)).obj X).obj Y)