Pretriangulated

📁 Source: Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

Statistics

Metric	Count
Definitions Pretriangulated, binaryBiproductData, completeDistinguishedTriangleMorphism, distinguishedTriangles, isoTriangleOfIso₁₂, isoTriangleOfIso₁₃, shortComplexOfDistTriangle, shortComplexOfDistTriangleIsoOfIso, termDistTriang_	9
Theorems coyoneda_exact₁, coyoneda_exact₂, coyoneda_exact₃, distinguished_iff_of_isZero₁, distinguished_iff_of_isZero₂, distinguished_iff_of_isZero₃, epi₁, epi₂, epi₃, isZero₁_iff, isZero₁_iff_isIso₂, isZero₁_of_isIso₂, isZero₁_of_isZero₂₃, isZero₂_iff, isZero₂_iff_isIso₃, isZero₂_of_isIso₃, isZero₂_of_isZero₁₃, isZero₃_iff, isZero₃_iff_isIso₁, isZero₃_of_isIso₁, isZero₃_of_isZero₁₂, mono₁, mono₂, mono₃, mor₁_eq_zero_iff_epi₃, mor₁_eq_zero_iff_mono₂, mor₁_eq_zero_of_epi₃, mor₁_eq_zero_of_mono₂, mor₂_eq_zero_iff_epi₁, mor₂_eq_zero_iff_mono₃, mor₂_eq_zero_of_epi₁, mor₂_eq_zero_of_mono₃, mor₃_eq_zero_iff_epi₂, mor₃_eq_zero_iff_mono₁, mor₃_eq_zero_of_epi₂, mor₃_eq_zero_of_mono₁, shift_distinguished, shift_distinguished_iff, yoneda_exact₂, yoneda_exact₃, binaryBiproductData_bicone_fst, binaryBiproductData_bicone_inl, binaryBiproductData_bicone_inr, binaryBiproductData_bicone_pt, binaryBiproductData_bicone_snd, binaryBiproductData_isBilimit, binaryBiproductTriangle_distinguished, binaryProductTriangle_distinguished, comp_distTriang_mor_zero₁₂, comp_distTriang_mor_zero₁₂_assoc, comp_distTriang_mor_zero₂₃, comp_distTriang_mor_zero₂₃_assoc, comp_distTriang_mor_zero₃₁, comp_distTriang_mor_zero₃₁_assoc, completeDistinguishedTriangleMorphism_hom₁, completeDistinguishedTriangleMorphism_hom₂, complete_distinguished_triangle_morphism, complete_distinguished_triangle_morphism₁, complete_distinguished_triangle_morphism₂, contractible_distinguished, contractible_distinguished₁, contractible_distinguished₂, distinguished_cocone_triangle, distinguished_cocone_triangle₁, distinguished_cocone_triangle₂, distinguished_iff_of_iso, exists_iso_binaryBiproduct_of_distTriang, exists_iso_of_arrow_iso, instHasBinaryBiproducts, instHasFiniteBiproducts, instHasFiniteCoproducts, instHasFiniteProducts, instSplitEpiCategory, instSplitMonoCategory, inv_rot_of_distTriang, isIso₁_of_isIso₂₃, isIso₂_of_isIso₁₃, isIso₃_of_isIso₁₂, isoTriangleOfIso₁₂_hom_hom₁, isoTriangleOfIso₁₂_hom_hom₂, isoTriangleOfIso₁₂_inv_hom₁, isoTriangleOfIso₁₂_inv_hom₂, isoTriangleOfIso₁₃_hom_hom₁, isoTriangleOfIso₁₃_hom_hom₃, isoTriangleOfIso₁₃_inv_hom₁, isoTriangleOfIso₁₃_inv_hom₃, isomorphic_distinguished, productTriangle_distinguished, rot_of_distTriang, rotate_distinguished_triangle, shortComplexOfDistTriangleIsoOfIso_hom_τ₁, shortComplexOfDistTriangleIsoOfIso_hom_τ₂, shortComplexOfDistTriangleIsoOfIso_hom_τ₃, shortComplexOfDistTriangleIsoOfIso_inv_τ₁, shortComplexOfDistTriangleIsoOfIso_inv_τ₂, shortComplexOfDistTriangleIsoOfIso_inv_τ₃, shortComplexOfDistTriangle_X₁, shortComplexOfDistTriangle_X₂, shortComplexOfDistTriangle_X₃, shortComplexOfDistTriangle_f, shortComplexOfDistTriangle_g	101
Total	110

CategoryTheory

Definitions

Name	Category	Theorems
Pretriangulated 📖	CompData	—

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
binaryBiproductData 📖	CompOp	6 math math: binaryBiproductData_bicone_pt, binaryBiproductData_isBilimit, binaryBiproductData_bicone_inl, binaryBiproductData_bicone_fst, binaryBiproductData_bicone_snd, binaryBiproductData_bicone_inr
completeDistinguishedTriangleMorphism 📖	CompOp	2 math math: completeDistinguishedTriangleMorphism_hom₂, completeDistinguishedTriangleMorphism_hom₁
distinguishedTriangles 📖	CompOp	31 math math: Opposite.mem_distinguishedTriangles_iff, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished, CategoryTheory.Functor.distTriang_iff, Triangle.distinguished_iff_of_isZero₃, CategoryTheory.Functor.map_distinguished_iff, Triangle.distinguished_iff_of_isZero₁, HomotopyCategory.mappingCone_triangleh_distinguished, CategoryTheory.Triangulated.TStructure.exists_triangle, Triangle.distinguished_iff_of_isZero₂, Triangle.shift_distinguished_iff, contractible_distinguished₂, distinguished_cocone_triangle₂, mem_distTriang_op_iff, binaryProductTriangle_distinguished, mem_distTriang_op_iff', distinguished_cocone_triangle, CategoryTheory.Triangulated.TStructure.exists_triangle_zero_one, CategoryTheory.Triangulated.SpectralObject.distinguished', distinguished_cocone_triangle₁, distinguished_iff_of_iso, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, DerivedCategory.triangleOfSES_distinguished, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, contractible_distinguished, DerivedCategory.mem_distTriang_iff, contractible_distinguished₁, HomotopyCategory.mappingConeCompTriangleh_distinguished, rotate_distinguished_triangle, CategoryTheory.Triangulated.SpectralObject.triangle_distinguished, binaryBiproductTriangle_distinguished
isoTriangleOfIso₁₂ 📖	CompOp	4 math math: isoTriangleOfIso₁₂_hom_hom₂, isoTriangleOfIso₁₂_hom_hom₁, isoTriangleOfIso₁₂_inv_hom₂, isoTriangleOfIso₁₂_inv_hom₁
isoTriangleOfIso₁₃ 📖	CompOp	4 math math: isoTriangleOfIso₁₃_hom_hom₁, isoTriangleOfIso₁₃_hom_hom₃, isoTriangleOfIso₁₃_inv_hom₁, isoTriangleOfIso₁₃_inv_hom₃
shortComplexOfDistTriangle 📖	CompOp	15 math math: shortComplexOfDistTriangle_X₂, shortComplexOfDistTriangle_X₁, shortComplexOfDistTriangle_f, shortComplexOfDistTriangleIsoOfIso_hom_τ₃, shortComplexOfDistTriangle_g, shortComplexOfDistTriangleIsoOfIso_inv_τ₁, CategoryTheory.Functor.map_distinguished_exact, shortComplexOfDistTriangle_X₃, CategoryTheory.Functor.IsHomological.exact, shortComplexOfDistTriangleIsoOfIso_inv_τ₂, shortComplexOfDistTriangleIsoOfIso_hom_τ₁, shortComplexOfDistTriangleIsoOfIso_hom_τ₂, preadditiveYoneda_map_distinguished, CategoryTheory.Functor.map_distinguished_op_exact, shortComplexOfDistTriangleIsoOfIso_inv_τ₃
shortComplexOfDistTriangleIsoOfIso 📖	CompOp	6 math math: shortComplexOfDistTriangleIsoOfIso_hom_τ₃, shortComplexOfDistTriangleIsoOfIso_inv_τ₁, shortComplexOfDistTriangleIsoOfIso_inv_τ₂, shortComplexOfDistTriangleIsoOfIso_hom_τ₁, shortComplexOfDistTriangleIsoOfIso_hom_τ₂, shortComplexOfDistTriangleIsoOfIso_inv_τ₃
termDistTriang_ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binaryBiproductData_bicone_fst 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.comp Triangle.obj₂ Triangle.mor₂ CategoryTheory.CategoryStruct.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Triangle.mor₁	CategoryTheory.Limits.BinaryBicone.fst CategoryTheory.Limits.BinaryBiproductData.bicone binaryBiproductData	—	—
binaryBiproductData_bicone_inl 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.comp Triangle.obj₂ Triangle.mor₂ CategoryTheory.CategoryStruct.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Triangle.mor₁	CategoryTheory.Limits.BinaryBicone.inl CategoryTheory.Limits.BinaryBiproductData.bicone binaryBiproductData	—	—
binaryBiproductData_bicone_inr 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.comp Triangle.obj₂ Triangle.mor₂ CategoryTheory.CategoryStruct.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Triangle.mor₁	CategoryTheory.Limits.BinaryBicone.inr CategoryTheory.Limits.BinaryBiproductData.bicone binaryBiproductData	—	—
binaryBiproductData_bicone_pt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.comp Triangle.obj₂ Triangle.mor₂ CategoryTheory.CategoryStruct.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Triangle.mor₁	CategoryTheory.Limits.BinaryBicone.pt CategoryTheory.Limits.BinaryBiproductData.bicone binaryBiproductData	—	—
binaryBiproductData_bicone_snd 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.comp Triangle.obj₂ Triangle.mor₂ CategoryTheory.CategoryStruct.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Triangle.mor₁	CategoryTheory.Limits.BinaryBicone.snd CategoryTheory.Limits.BinaryBiproductData.bicone binaryBiproductData	—	—
binaryBiproductData_isBilimit 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.comp Triangle.obj₂ Triangle.mor₂ CategoryTheory.CategoryStruct.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Triangle.mor₁	CategoryTheory.Limits.BinaryBiproductData.isBilimit binaryBiproductData CategoryTheory.Limits.isBinaryBilimitOfTotal Triangle.mono₁ comp_distTriang_mor_zero₁₂	—	Triangle.mono₁ comp_distTriang_mor_zero₁₂
binaryBiproductTriangle_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles binaryBiproductTriangle CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct instHasBinaryBiproducts	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct instHasBinaryBiproducts distinguished_cocone_triangle₂ exists_iso_binaryBiproduct_of_distTriang isomorphic_distinguished CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id CategoryTheory.Limits.comp_zero
binaryProductTriangle_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles binaryProductTriangle CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct instHasBinaryBiproducts	—	isomorphic_distinguished CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct instHasBinaryBiproducts binaryBiproductTriangle_distinguished CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair
comp_distTriang_mor_zero₁₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.obj₃ Triangle.mor₁ Triangle.mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	complete_distinguished_triangle_morphism contractible_distinguished CategoryTheory.Limits.zero_comp
comp_distTriang_mor_zero₁₂_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁ Triangle.obj₃ Triangle.mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_distTriang_mor_zero₁₂
comp_distTriang_mor_zero₂₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₂ Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₂ Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	comp_distTriang_mor_zero₁₂ rot_of_distTriang
comp_distTriang_mor_zero₂₃_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₂ Triangle.obj₃ Triangle.mor₂ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_distTriang_mor_zero₂₃
comp_distTriang_mor_zero₃₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.obj₂ Triangle.mor₃ CategoryTheory.Functor.map Triangle.mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	rot_of_distTriang CategoryTheory.Preadditive.comp_neg comp_distTriang_mor_zero₁₂
comp_distTriang_mor_zero₃₁_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₃ Triangle.obj₂ CategoryTheory.Functor.map Triangle.mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_distTriang_mor_zero₃₁
completeDistinguishedTriangleMorphism_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁	TriangleMorphism.hom₁ completeDistinguishedTriangleMorphism	—	—
completeDistinguishedTriangleMorphism_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁	TriangleMorphism.hom₂ completeDistinguishedTriangleMorphism	—	—
complete_distinguished_triangle_morphism 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁	Triangle.obj₃ Triangle.mor₂ CategoryTheory.Functor.obj Triangle.mor₃ CategoryTheory.Functor.map	—	—
complete_distinguished_triangle_morphism₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₂ Triangle.obj₃ Triangle.mor₂	Triangle.obj₁ Triangle.mor₁ CategoryTheory.Functor.obj Triangle.mor₃ CategoryTheory.Functor.map	—	complete_distinguished_triangle_morphism rot_of_distTriang CategoryTheory.Functor.IsEquivalence.full CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.Functor.map_injective CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_preimage CategoryTheory.Preadditive.comp_neg CategoryTheory.Preadditive.neg_comp
complete_distinguished_triangle_morphism₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₃ CategoryTheory.Functor.map	Triangle.obj₂ Triangle.mor₁ Triangle.mor₂	—	complete_distinguished_triangle_morphism inv_rot_of_distTriang add_neg_cancel CategoryTheory.Preadditive.neg_comp CategoryTheory.Category.assoc CategoryTheory.Preadditive.comp_neg CategoryTheory.Functor.map_comp CategoryTheory.shift_shift_neg' CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.NatIso.inv_app_isIso neg_add_cancel CategoryTheory.shift_neg_shift' CategoryTheory.Iso.inv_hom_id_app_assoc
contractible_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles contractibleTriangle CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
contractible_distinguished₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.Limits.HasZeroObject.zero' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj	—	isomorphic_distinguished inv_rot_of_distTriang contractible_distinguished CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.comp_id add_neg_cancel CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_comp neg_zero CategoryTheory.Limits.comp_zero
contractible_distinguished₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.Limits.HasZeroObject.zero' CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.id	—	isomorphic_distinguished inv_rot_of_distTriang contractible_distinguished₁ CategoryTheory.Limits.id_zero CategoryTheory.Limits.comp_zero add_neg_cancel CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.zero_comp neg_zero CategoryTheory.Category.comp_id CategoryTheory.shift_shiftFunctorCompIsoId_inv_app CategoryTheory.Category.id_comp
distinguished_cocone_triangle 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles	—	—
distinguished_cocone_triangle₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles	—	distinguished_cocone_triangle inv_rot_of_distTriang
distinguished_cocone_triangle₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles	—	distinguished_cocone_triangle isomorphic_distinguished inv_rot_of_distTriang add_neg_cancel CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Preadditive.comp_neg CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.shift_shiftFunctorCompIsoId_inv_app
distinguished_iff_of_iso 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles	—	isomorphic_distinguished
exists_iso_binaryBiproduct_of_distTriang 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp Triangle.obj₂ CategoryTheory.Limits.biprod CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct instHasBinaryBiproducts Triangle.mor₁ CategoryTheory.Iso.hom CategoryTheory.Limits.biprod.inl Triangle.mor₂ CategoryTheory.Limits.biprod.snd	—	Triangle.epi₂ CategoryTheory.isSplitEpi_of_epi instSplitEpiCategory CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct instHasBinaryBiproducts Triangle.coyoneda_exact₂ CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.IsSplitEpi.id CategoryTheory.Category.comp_id sub_self sub_add_cancel CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Limits.BinaryBicone.inl_fst CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Limits.BinaryBicone.inl_snd
exists_iso_of_arrow_iso 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	TriangleMorphism.hom₁ CategoryTheory.Iso.hom triangleCategory CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id Triangle.obj₁ Triangle.obj₂ Triangle.mor₁ CategoryTheory.Arrow CategoryTheory.instCategoryArrow TriangleMorphism.hom₂ CategoryTheory.CommaMorphism.right	—	CategoryTheory.CommaMorphism.w CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_hom CategoryTheory.Arrow.isIso_right isIso₃_of_isIso₁₂ Triangle.isIso_of_isIsos
instHasBinaryBiproducts 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.HasBinaryBiproducts CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	distinguished_cocone_triangle₂ Triangle.coyoneda_exact₃ CategoryTheory.Limits.comp_zero Triangle.coyoneda_exact₂ CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Category.comp_id sub_self sub_add_cancel
instHasFiniteBiproducts 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.HasFiniteBiproducts CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts instHasFiniteProducts
instHasFiniteCoproducts 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.HasFiniteCoproducts	—	CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial CategoryTheory.Limits.hasBinaryCoproducts_of_hasBinaryBiproducts instHasBinaryBiproducts CategoryTheory.Limits.HasZeroObject.hasInitial
instHasFiniteProducts 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.HasFiniteProducts	—	CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal CategoryTheory.Limits.hasBinaryProducts_of_hasBinaryBiproducts instHasBinaryBiproducts CategoryTheory.Limits.HasZeroObject.hasTerminal
instSplitEpiCategory 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.SplitEpiCategory	—	distinguished_cocone_triangle Triangle.coyoneda_exact₂ Triangle.mor₂_eq_zero_of_epi₁ CategoryTheory.Limits.comp_zero
instSplitMonoCategory 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.SplitMonoCategory	—	distinguished_cocone_triangle₁ Triangle.yoneda_exact₂ Triangle.mor₁_eq_zero_of_mono₂ CategoryTheory.Limits.zero_comp
inv_rot_of_distTriang 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	Triangle.invRotate	—	rotate_distinguished_triangle isomorphic_distinguished
isIso₁_of_isIso₂₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.IsIso Triangle.obj₁ TriangleMorphism.hom₁	—	isIso₂_of_isIso₁₃ inv_rot_of_distTriang CategoryTheory.Functor.map_isIso
isIso₂_of_isIso₁₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.IsIso Triangle.obj₂ TriangleMorphism.hom₂	—	CategoryTheory.Preadditive.mono_iff_cancel_zero Triangle.coyoneda_exact₂ CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Category.assoc TriangleMorphism.comm₂ Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp inv_rot_of_distTriang TriangleMorphism.comm₁ CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.inv_hom_id_assoc comp_distTriang_mor_zero₁₂ CategoryTheory.Limits.comp_zero CategoryTheory.isIso_of_yoneda_map_bijective CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id Triangle.coyoneda_exact₃ CategoryTheory.Functor.map_mono CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.instIsEquivalenceShiftFunctor TriangleMorphism.comm₃ comp_distTriang_mor_zero₂₃ CategoryTheory.Preadditive.sub_comp sub_self CategoryTheory.Preadditive.add_comp add_sub_cancel
isIso₃_of_isIso₁₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.IsIso Triangle.obj₃ TriangleMorphism.hom₃	—	isIso₂_of_isIso₁₃ rot_of_distTriang CategoryTheory.Functor.map_isIso
isoTriangleOfIso₁₂_hom_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁ CategoryTheory.Iso.hom	TriangleMorphism.hom₁ triangleCategory isoTriangleOfIso₁₂	—	—
isoTriangleOfIso₁₂_hom_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁ CategoryTheory.Iso.hom	TriangleMorphism.hom₂ triangleCategory isoTriangleOfIso₁₂	—	—
isoTriangleOfIso₁₂_inv_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁ CategoryTheory.Iso.hom	TriangleMorphism.hom₁ CategoryTheory.Iso.inv triangleCategory isoTriangleOfIso₁₂	—	—
isoTriangleOfIso₁₂_inv_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ Triangle.obj₂ Triangle.mor₁ CategoryTheory.Iso.hom	TriangleMorphism.hom₂ CategoryTheory.Iso.inv triangleCategory isoTriangleOfIso₁₂	—	—
isoTriangleOfIso₁₃_hom_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₃ CategoryTheory.Functor.map CategoryTheory.Iso.hom	TriangleMorphism.hom₁ triangleCategory isoTriangleOfIso₁₃	—	—
isoTriangleOfIso₁₃_hom_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₃ CategoryTheory.Functor.map CategoryTheory.Iso.hom	TriangleMorphism.hom₃ triangleCategory isoTriangleOfIso₁₃	—	—
isoTriangleOfIso₁₃_inv_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₃ CategoryTheory.Functor.map CategoryTheory.Iso.hom	TriangleMorphism.hom₁ CategoryTheory.Iso.inv triangleCategory isoTriangleOfIso₁₃	—	—
isoTriangleOfIso₁₃_inv_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Functor.obj Triangle.obj₁ Triangle.mor₃ CategoryTheory.Functor.map CategoryTheory.Iso.hom	TriangleMorphism.hom₃ CategoryTheory.Iso.inv triangleCategory isoTriangleOfIso₁₃	—	—
isomorphic_distinguished 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	—	—	—
productTriangle_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	productTriangle	—	distinguished_cocone_triangle CategoryTheory.Limits.Pi.map_π CategoryTheory.Limits.Pi.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.id_comp CategoryTheory.IsIso.id CategoryTheory.isIso_of_yoneda_map_bijective CategoryTheory.Preadditive.mono_iff_cancel_zero CategoryTheory.cancel_mono CategoryTheory.Functor.map_mono CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Limits.zero_comp CategoryTheory.Category.assoc TriangleMorphism.comm₃ Mathlib.Tactic.Reassoc.eq_whisker' Triangle.coyoneda_exact₃ TriangleMorphism.comm₂_assoc Triangle.coyoneda_exact₂ CategoryTheory.Limits.limit.lift_map comp_distTriang_mor_zero₁₂ CategoryTheory.Limits.comp_zero CategoryTheory.Functor.map_comp TriangleMorphism.comm₁ productTriangle.zero₃₁ comp_distTriang_mor_zero₃₁ Triangle.coyoneda_exact₁ CategoryTheory.Preadditive.sub_comp TriangleMorphism.comm₃_assoc sub_eq_zero CategoryTheory.Functor.map_id CategoryTheory.Preadditive.add_comp TriangleMorphism.comm₂ add_sub_cancel Triangle.isIso_of_isIsos isomorphic_distinguished
rot_of_distTriang 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	Triangle.rotate	—	rotate_distinguished_triangle
rotate_distinguished_triangle 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Triangle Set Set.instMembership distinguishedTriangles Triangle.rotate	—	—
shortComplexOfDistTriangleIsoOfIso_hom_τ₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory isomorphic_distinguished CategoryTheory.Iso.symm triangleCategory shortComplexOfDistTriangleIsoOfIso TriangleMorphism.hom₁	—	isomorphic_distinguished
shortComplexOfDistTriangleIsoOfIso_hom_τ₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory isomorphic_distinguished CategoryTheory.Iso.symm triangleCategory shortComplexOfDistTriangleIsoOfIso TriangleMorphism.hom₂	—	isomorphic_distinguished
shortComplexOfDistTriangleIsoOfIso_hom_τ₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory isomorphic_distinguished CategoryTheory.Iso.symm triangleCategory shortComplexOfDistTriangleIsoOfIso TriangleMorphism.hom₃	—	isomorphic_distinguished
shortComplexOfDistTriangleIsoOfIso_inv_τ₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory isomorphic_distinguished CategoryTheory.Iso.symm triangleCategory shortComplexOfDistTriangleIsoOfIso TriangleMorphism.hom₁	—	isomorphic_distinguished
shortComplexOfDistTriangleIsoOfIso_inv_τ₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory isomorphic_distinguished CategoryTheory.Iso.symm triangleCategory shortComplexOfDistTriangleIsoOfIso TriangleMorphism.hom₂	—	isomorphic_distinguished
shortComplexOfDistTriangleIsoOfIso_inv_τ₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory isomorphic_distinguished CategoryTheory.Iso.symm triangleCategory shortComplexOfDistTriangleIsoOfIso TriangleMorphism.hom₃	—	isomorphic_distinguished
shortComplexOfDistTriangle_X₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle Triangle.obj₁	—	—
shortComplexOfDistTriangle_X₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle Triangle.obj₂	—	—
shortComplexOfDistTriangle_X₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle Triangle.obj₃	—	—
shortComplexOfDistTriangle_f 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle Triangle.mor₁	—	—
shortComplexOfDistTriangle_g 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms shortComplexOfDistTriangle Triangle.mor₂	—	—

CategoryTheory.Pretriangulated.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coyoneda_exact₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj obj₁ obj₂ CategoryTheory.Functor.map mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	obj₃ mor₃	—	coyoneda_exact₂ CategoryTheory.Pretriangulated.rot_of_distTriang CategoryTheory.Preadditive.comp_neg neg_zero
coyoneda_exact₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj₂ obj₃ mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	obj₁ mor₁	—	CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁ CategoryTheory.Pretriangulated.contractible_distinguished CategoryTheory.Limits.comp_zero CategoryTheory.Category.id_comp
coyoneda_exact₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj₃ CategoryTheory.Functor.obj obj₁ mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	obj₂ mor₂	—	coyoneda_exact₂ CategoryTheory.Pretriangulated.rot_of_distTriang
distinguished_iff_of_isZero₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.IsZero obj₁	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.IsIso obj₂ obj₃ mor₂	—	CategoryTheory.Pretriangulated.rotate_distinguished_triangle distinguished_iff_of_isZero₃ CategoryTheory.Functor.map_isZero CategoryTheory.Functor.preservesZeroMorphisms_of_additive
distinguished_iff_of_isZero₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.IsZero obj₂	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.IsIso obj₃ CategoryTheory.Functor.obj obj₁ mor₃	—	CategoryTheory.Pretriangulated.rotate_distinguished_triangle distinguished_iff_of_isZero₁
distinguished_iff_of_isZero₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.IsZero obj₃	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.IsIso obj₁ obj₂ mor₁	—	isZero₃_iff_isIso₁ CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Pretriangulated.contractible_distinguished CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.isZero_zero CategoryTheory.Limits.IsZero.eq_of_src
epi₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Epi obj₁ mor₁	—	mor₂_eq_zero_iff_epi₁
epi₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₃ CategoryTheory.Functor.obj obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Epi obj₂ mor₂	—	mor₃_eq_zero_iff_epi₂
epi₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Epi obj₃ CategoryTheory.Functor.obj mor₃	—	mor₁_eq_zero_iff_epi₃
isZero₁_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₁ mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mor₃ obj₃ CategoryTheory.Functor.obj	—	isZero₂_iff CategoryTheory.Pretriangulated.inv_rot_of_distTriang add_neg_cancel CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor
isZero₁_iff_isIso₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₁ CategoryTheory.IsIso obj₂ obj₃ mor₂	—	isZero₁_iff epi₂ yoneda_exact₂ CategoryTheory.Limits.zero_comp CategoryTheory.cancel_epi CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mor₁_eq_zero_iff_mono₂ mor₃_eq_zero_iff_epi₂ CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso
isZero₁_of_isIso₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₁	—	isZero₁_iff_isIso₂
isZero₁_of_isZero₂₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Limits.IsZero obj₂ obj₃	obj₁	—	isZero₁_iff CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.IsZero.eq_of_src
isZero₂_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₂ mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mor₂ obj₃	—	CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.IsZero.eq_of_src coyoneda_exact₂ CategoryTheory.Limits.comp_zero CategoryTheory.Limits.IsZero.iff_id_eq_zero
isZero₂_iff_isIso₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₂ CategoryTheory.IsIso obj₃ CategoryTheory.Functor.obj obj₁ mor₃	—	isZero₁_iff_isIso₂ CategoryTheory.Pretriangulated.rot_of_distTriang
isZero₂_of_isIso₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₂	—	isZero₂_iff_isIso₃
isZero₂_of_isZero₁₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Limits.IsZero obj₁ obj₃	obj₂	—	isZero₂_iff CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.IsZero.eq_of_tgt
isZero₃_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₃ mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mor₃ CategoryTheory.Functor.obj obj₁	—	isZero₂_iff CategoryTheory.Pretriangulated.rot_of_distTriang
isZero₃_iff_isIso₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₃ CategoryTheory.IsIso obj₁ obj₂ mor₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor isZero₁_iff_isIso₂ CategoryTheory.Pretriangulated.inv_rot_of_distTriang
isZero₃_of_isIso₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Limits.IsZero obj₃	—	isZero₃_iff_isIso₁
isZero₃_of_isZero₁₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Limits.IsZero obj₁ obj₂	obj₃	—	isZero₂_of_isZero₁₃ CategoryTheory.Pretriangulated.rot_of_distTriang CategoryTheory.Functor.map_id CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mono₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₃ CategoryTheory.Functor.obj obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Mono obj₂ mor₁	—	mor₃_eq_zero_iff_mono₁
mono₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Mono obj₃ mor₂	—	mor₁_eq_zero_iff_mono₂
mono₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Mono CategoryTheory.Functor.obj obj₁ mor₃	—	mor₂_eq_zero_iff_mono₃
mor₁_eq_zero_iff_epi₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Epi obj₃ CategoryTheory.Functor.obj mor₃	—	mor₃_eq_zero_iff_epi₂ CategoryTheory.Pretriangulated.rot_of_distTriang neg_eq_zero CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_eq_zero_iff CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor
mor₁_eq_zero_iff_mono₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Mono obj₃ mor₂	—	CategoryTheory.Preadditive.mono_iff_cancel_zero coyoneda_exact₂ CategoryTheory.Limits.comp_zero CategoryTheory.cancel_mono CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ CategoryTheory.Limits.zero_comp
mor₁_eq_zero_of_epi₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mor₁_eq_zero_iff_epi₃
mor₁_eq_zero_of_mono₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mor₁_eq_zero_iff_mono₂
mor₂_eq_zero_iff_epi₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Epi obj₁ mor₁	—	mor₃_eq_zero_iff_epi₂ CategoryTheory.Pretriangulated.inv_rot_of_distTriang add_neg_cancel CategoryTheory.Preadditive.IsIso.comp_right_eq_zero CategoryTheory.NatIso.inv_app_isIso
mor₂_eq_zero_iff_mono₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Mono CategoryTheory.Functor.obj obj₁ mor₃	—	mor₁_eq_zero_iff_mono₂ CategoryTheory.Pretriangulated.rot_of_distTriang
mor₂_eq_zero_of_epi₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mor₂_eq_zero_iff_epi₁
mor₂_eq_zero_of_mono₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₂ obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mor₂_eq_zero_iff_mono₃
mor₃_eq_zero_iff_epi₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₃ CategoryTheory.Functor.obj obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Epi obj₂ mor₂	—	CategoryTheory.Preadditive.epi_iff_cancel_zero yoneda_exact₃ CategoryTheory.Limits.zero_comp CategoryTheory.cancel_epi CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃ CategoryTheory.Limits.comp_zero
mor₃_eq_zero_iff_mono₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₃ CategoryTheory.Functor.obj obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Mono obj₂ mor₁	—	mor₁_eq_zero_iff_mono₂ CategoryTheory.Pretriangulated.inv_rot_of_distTriang add_neg_cancel neg_eq_zero CategoryTheory.Preadditive.IsIso.comp_right_eq_zero CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_eq_zero_iff CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor
mor₃_eq_zero_of_epi₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₃ CategoryTheory.Functor.obj obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mor₃_eq_zero_iff_epi₂
mor₃_eq_zero_of_mono₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₃ CategoryTheory.Functor.obj obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mor₃_eq_zero_iff_mono₁
shift_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory instHasShiftInt	—	CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Pretriangulated.rot_of_distTriang CategoryTheory.Pretriangulated.inv_rot_of_distTriang
shift_distinguished_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory instHasShiftInt	—	CategoryTheory.Pretriangulated.isomorphic_distinguished shift_distinguished
yoneda_exact₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj₁ obj₂ mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	obj₃ mor₂	—	CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism CategoryTheory.Pretriangulated.contractible_distinguished₁ CategoryTheory.Limits.comp_zero CategoryTheory.Category.comp_id
yoneda_exact₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj₂ obj₃ mor₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Functor.obj obj₁ mor₃	—	yoneda_exact₂ CategoryTheory.Pretriangulated.rot_of_distTriang

---

← Back to Index