Basic

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

Statistics

Metric	Count
Definitions functorHomMk, functorHomMk', functorIsoMk, functorIsoMk', functorMk, homMk, instAddCommGroupHom, instAddHom, instLinear, instModuleHom, instNegHom, instPreadditive, instSMulHom, instSubHom, instZeroHom, isoMk, mk, mor₁, mor₂, mor₃, obj₁, obj₂, obj₃, π₁, π₁Toπ₂, π₂, π₂Toπ₃, π₃, π₃Toπ₁, TriangleMorphism, comp, hom₁, hom₂, hom₃, binaryBiproductTriangle, binaryProductTriangle, binaryProductTriangleIsoBinaryBiproductTriangle, contractibleTriangle, contractibleTriangleFunctor, instInhabitedTriangle, instInhabitedTriangleMorphism, productTriangle, fan, isLimitFan, π, triangleCategory, triangleMorphismId	47
Theorems hom_inv_id_triangle_hom₁, hom_inv_id_triangle_hom₁_assoc, hom_inv_id_triangle_hom₂, hom_inv_id_triangle_hom₂_assoc, hom_inv_id_triangle_hom₃, hom_inv_id_triangle_hom₃_assoc, inv_hom_id_triangle_hom₁, inv_hom_id_triangle_hom₁_assoc, inv_hom_id_triangle_hom₂, inv_hom_id_triangle_hom₂_assoc, inv_hom_id_triangle_hom₃, inv_hom_id_triangle_hom₃_assoc, add_hom₁, add_hom₂, add_hom₃, eqToHom_hom₁, eqToHom_hom₂, eqToHom_hom₃, functorHomMk'_app_hom₁, functorHomMk'_app_hom₂, functorHomMk'_app_hom₃, functorHomMk_app_hom₁, functorHomMk_app_hom₂, functorHomMk_app_hom₃, functorIsoMk'_hom_app_hom₁, functorIsoMk'_hom_app_hom₂, functorIsoMk'_hom_app_hom₃, functorIsoMk'_inv_app_hom₁, functorIsoMk'_inv_app_hom₂, functorIsoMk'_inv_app_hom₃, functorIsoMk_hom, functorIsoMk_inv, functorMk_map_hom₁, functorMk_map_hom₂, functorMk_map_hom₃, functorMk_obj, homMk_hom₁, homMk_hom₂, homMk_hom₃, hom_ext, hom_ext_iff, instIsIsoHom₁, instIsIsoHom₂, instIsIsoHom₃, isIso_of_isIsos, isoMk_hom, isoMk_inv, mk_mor₁, mk_mor₂, mk_mor₃, mk_obj₁, mk_obj₂, mk_obj₃, neg_hom₁, neg_hom₂, neg_hom₃, smul_hom₁, smul_hom₂, smul_hom₃, sub_hom₁, sub_hom₂, sub_hom₃, zero_hom₁, zero_hom₂, zero_hom₃, π₁Toπ₂_app, π₁_map, π₁_obj, π₂Toπ₃_app, π₂_map, π₂_obj, π₃Toπ₁_app, π₃_map, π₃_obj, comm₁, comm₁_assoc, comm₂, comm₂_assoc, comm₃, comm₃_assoc, comp_hom₁, comp_hom₂, comp_hom₃, ext, ext_iff, binaryBiproductTriangle_mor₁, binaryBiproductTriangle_mor₂, binaryBiproductTriangle_mor₃, binaryBiproductTriangle_obj₁, binaryBiproductTriangle_obj₂, binaryBiproductTriangle_obj₃, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃, binaryProductTriangle_mor₁, binaryProductTriangle_mor₂, binaryProductTriangle_mor₃, binaryProductTriangle_obj₁, binaryProductTriangle_obj₂, binaryProductTriangle_obj₃, comp_hom₁, comp_hom₁_assoc, comp_hom₂, comp_hom₂_assoc, comp_hom₃, comp_hom₃_assoc, contractibleTriangleFunctor_map_hom₁, contractibleTriangleFunctor_map_hom₂, contractibleTriangleFunctor_map_hom₃, contractibleTriangleFunctor_obj, contractibleTriangle_mor₁, contractibleTriangle_mor₂, contractibleTriangle_mor₃, contractibleTriangle_obj₁, contractibleTriangle_obj₂, contractibleTriangle_obj₃, id_hom₁, id_hom₂, id_hom₃, lift_hom₁, lift_hom₂, lift_hom₃, zero₃₁, π_hom₁, π_hom₂, π_hom₃, productTriangle_mor₁, productTriangle_mor₂, productTriangle_mor₃, productTriangle_obj₁, productTriangle_obj₂, productTriangle_obj₃, triangleCategory_comp, triangleCategory_id, triangleMorphismId_hom₁, triangleMorphismId_hom₂, triangleMorphismId_hom₃	140
Total	187

CategoryTheory.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id_triangle_hom₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Pretriangulated.comp_hom₁ hom_inv_id CategoryTheory.Pretriangulated.id_hom₁
hom_inv_id_triangle_hom₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_triangle_hom₁
hom_inv_id_triangle_hom₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Pretriangulated.comp_hom₂ hom_inv_id CategoryTheory.Pretriangulated.id_hom₂
hom_inv_id_triangle_hom₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_triangle_hom₂
hom_inv_id_triangle_hom₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Pretriangulated.comp_hom₃ hom_inv_id CategoryTheory.Pretriangulated.id_hom₃
hom_inv_id_triangle_hom₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_triangle_hom₃
inv_hom_id_triangle_hom₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Pretriangulated.comp_hom₁ inv_hom_id CategoryTheory.Pretriangulated.id_hom₁
inv_hom_id_triangle_hom₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_triangle_hom₁
inv_hom_id_triangle_hom₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Pretriangulated.comp_hom₂ inv_hom_id CategoryTheory.Pretriangulated.id_hom₂
inv_hom_id_triangle_hom₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_triangle_hom₂
inv_hom_id_triangle_hom₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Pretriangulated.comp_hom₃ inv_hom_id CategoryTheory.Pretriangulated.id_hom₃
inv_hom_id_triangle_hom₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_triangle_hom₃

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
TriangleMorphism 📖	CompData	—
binaryBiproductTriangle 📖	CompOp	13 math math: binaryBiproductTriangle_mor₁, binaryBiproductTriangle_mor₂, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, binaryBiproductTriangle_obj₃, binaryBiproductTriangle_obj₂, binaryBiproductTriangle_obj₁, binaryBiproductTriangle_mor₃, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁, binaryBiproductTriangle_distinguished
binaryProductTriangle 📖	CompOp	13 math math: binaryProductTriangle_obj₂, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, binaryProductTriangle_mor₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, binaryProductTriangle_mor₁, binaryProductTriangle_distinguished, binaryProductTriangle_mor₃, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃, binaryProductTriangle_obj₃, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁, binaryProductTriangle_obj₁, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁
binaryProductTriangleIsoBinaryBiproductTriangle 📖	CompOp	6 math math: binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁
contractibleTriangle 📖	CompOp	20 math math: contractibleTriangle_obj₂, contractibleTriangleFunctor_map_hom₂, Opposite.contractibleTriangleIso_hom_hom₂, Opposite.contractibleTriangleIso_hom_hom₁, Opposite.contractibleTriangleIso_inv_hom₃, contractibleTriangle_mor₂, Opposite.contractibleTriangleIso_hom_hom₃, contractibleTriangleFunctor_map_hom₁, Opposite.contractibleTriangleIso_inv_hom₁, Opposite.contractible_distinguished, contractibleTriangleFunctor_obj, HomotopyCategory.Pretriangulated.contractible_distinguished, contractibleTriangleFunctor_map_hom₃, contractibleTriangle_obj₃, contractibleTriangle_mor₁, contractibleTriangle_obj₁, contractibleTriangle_mor₃, Opposite.contractibleTriangleIso_inv_hom₂, CategoryTheory.Functor.contractible_mem_essImageDistTriang, contractible_distinguished
contractibleTriangleFunctor 📖	CompOp	4 math math: contractibleTriangleFunctor_map_hom₂, contractibleTriangleFunctor_map_hom₁, contractibleTriangleFunctor_obj, contractibleTriangleFunctor_map_hom₃
instInhabitedTriangle 📖	CompOp	—
instInhabitedTriangleMorphism 📖	CompOp	—
productTriangle 📖	CompOp	14 math math: productTriangle.π_hom₁, productTriangle_mor₂, productTriangle.π_hom₃, productTriangle.π_hom₂, productTriangle.lift_hom₁, productTriangle_obj₃, productTriangle.lift_hom₃, productTriangle_mor₃, productTriangle_mor₁, productTriangle_distinguished, productTriangle_obj₁, productTriangle.lift_hom₂, productTriangle_obj₂, productTriangle.zero₃₁
triangleCategory 📖	CompOp	258 math math: rotCompInvRot_hom_app_hom₃, CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc, HomotopyCategory.spectralObjectMappingCone_δ'_app, Triangle.π₂_map, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃, triangleRotation_counitIso, Opposite.mem_distinguishedTriangles_iff, Triangle.shiftFunctorZero_inv_app_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished, rotCompInvRot_inv_app_hom₂, Triangle.shiftFunctor_map_hom₁, Triangle.π₁_map, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂, CategoryTheory.Triangulated.TStructure.triangle_iso_exists, contractibleTriangleFunctor_map_hom₂, CategoryTheory.Iso.inv_hom_id_triangle_hom₂, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂, Opposite.mem_distinguishedTriangles_iff', CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, Triangle.functorHomMk'_app_hom₁, Triangle.shift_distinguished, Triangle.shiftFunctor_obj, invRotCompRot_inv_app_hom₃, comp_hom₁_assoc, Triangle.eqToHom_hom₂, isoTriangleOfIso₁₂_hom_hom₂, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁, CategoryTheory.Iso.inv_hom_id_triangle_hom₁, Triangle.functorIsoMk'_inv_app_hom₂, triangleOpEquivalence_unitIso, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂, Triangle.shiftFunctorAdd_eq, CategoryTheory.Iso.inv_hom_id_triangle_hom₂_assoc, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₁, TriangleOpEquivalence.functor_map_hom₂, Triangle.π₃_map, Triangle.functorMk_map_hom₃, Triangle.shiftFunctorZero_eq, Triangle.functorMk_map_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, Opposite.contractibleTriangleIso_hom_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, Triangle.eqToHom_hom₃, Triangle.functorIsoMk'_hom_app_hom₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₃, Triangle.smul_hom₂, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, Triangle.eqToHom_hom₁, Opposite.contractibleTriangleIso_hom_hom₁, Triangle.functorIsoMk'_hom_app_hom₁, Triangle.isoMk_inv, TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Functor.map_distinguished_iff, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁, id_hom₃, Triangle.functorHomMk'_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃, CategoryTheory.Iso.hom_inv_id_triangle_hom₂, TriangleOpEquivalence.unitIso_hom_app, CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc, isoTriangleOfIso₁₂_hom_hom₁, Triangle.isIso_of_isIsos, TriangleOpEquivalence.counitIso_hom_app_hom₁, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, TriangleOpEquivalence.counitIso_inv_app_hom₃, Triangle.sub_hom₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, Opposite.contractibleTriangleIso_inv_hom₃, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, Opposite.contractibleTriangleIso_hom_hom₃, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, Triangle.shift_distinguished_iff, contractibleTriangleFunctor_map_hom₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, invRotate_map_hom₁, triangleRotation_unitIso, CategoryTheory.Functor.mapTriangle_map_hom₁, preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.Triangulated.TStructure.instIsGEObj₃ObjTriangleTriangleLTGE, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, Opposite.contractibleTriangleIso_inv_hom₁, Triangle.neg_hom₁, Triangle.shiftFunctorZero_inv_app_hom₃, Triangle.π₁Toπ₂_app, comp_hom₃_assoc, Triangle.neg_hom₃, Triangle.π₂Toπ₃_app, isoTriangleOfIso₁₂_inv_hom₂, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃, triangleCategory_id, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃, op_distinguished, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₃, mem_distTriang_op_iff, contractibleTriangleFunctor_obj, TriangleOpEquivalence.counitIso_inv_app_hom₂, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂, Triangle.zero_hom₁, triangleOpEquivalence_counitIso, triangleOpEquivalence_functor, shortComplexOfDistTriangleIsoOfIso_hom_τ₃, rotCompInvRot_inv_app_hom₃, contractibleTriangleFunctor_map_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁, rotate_map_hom₂, invRotCompRot_hom_app_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃, invRotCompRot_inv_app_hom₁, rotate_map_hom₃, mem_distTriang_op_iff', CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃, comp_hom₂_assoc, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₂, id_hom₂, TriangleOpEquivalence.unitIso_inv_app, Triangle.functorIsoMk'_hom_app_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃, invRotate_map_hom₂, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, Triangle.shiftFunctorAdd'_inv_app_hom₂, TriangleOpEquivalence.functor_obj, CategoryTheory.Iso.hom_inv_id_triangle_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, shortComplexOfDistTriangleIsoOfIso_inv_τ₁, CategoryTheory.Iso.hom_inv_id_triangle_hom₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₁, Triangle.π₃Toπ₁_app, Triangle.shiftFunctorZero_hom_app_hom₃, Triangle.shiftFunctorZero_hom_app_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, isoTriangleOfIso₁₃_hom_hom₁, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁, Triangle.functorMk_map_hom₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃, Triangle.shiftFunctorAdd'_inv_app_hom₁, CategoryTheory.Functor.IsTriangulated.map_distinguished, CategoryTheory.Functor.mapTriangle_map_hom₃, Triangle.neg_hom₂, unop_distinguished, Triangle.shiftFunctorAdd'_hom_app_hom₃, Triangle.shiftFunctor_eq, CategoryTheory.Triangulated.TStructure.instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, Triangle.π₁_obj, comp_hom₂, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂, Triangle.add_hom₂, rotCompInvRot_inv_app_hom₁, Triangle.zero_hom₃, Triangle.add_hom₃, TriangleOpEquivalence.inverse_obj, TriangleOpEquivalence.counitIso_hom_app_hom₂, CategoryTheory.Iso.inv_hom_id_triangle_hom₁_assoc, isoTriangleOfIso₁₃_hom_hom₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁, triangleCategory_comp, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, Triangle.shiftFunctor_map_hom₃, rotate_map_hom₁, Triangle.shiftFunctorAdd'_eq, Triangle.π₂_obj, Triangle.π₃_obj, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁, Triangle.add_hom₁, Triangle.shiftFunctorAdd'_hom_app_hom₁, CategoryTheory.Functor.instFaithfulTriangleMapTriangle, isoTriangleOfIso₁₂_inv_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₂, Triangle.smul_hom₃, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂, Triangle.sub_hom₃, Opposite.contractibleTriangleIso_inv_hom₂, invRotCompRot_hom_app_hom₃, isoTriangleOfIso₁₃_inv_hom₁, comp_hom₃, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁, rotate_obj, Triangle.sub_hom₂, Triangle.functorHomMk'_app_hom₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, CategoryTheory.Iso.hom_inv_id_triangle_hom₃_assoc, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂, rotCompInvRot_hom_app_hom₂, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₁, Triangle.shiftFunctorAdd'_inv_app_hom₃, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃, exists_iso_of_arrow_iso, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂, comp_hom₁, Triangle.shiftFunctor_map_hom₂, shortComplexOfDistTriangleIsoOfIso_inv_τ₂, TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂, Triangle.shiftFunctorZero_inv_app_hom₂, CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful, Triangle.shiftFunctorAdd'_hom_app_hom₂, TriangleOpEquivalence.counitIso_hom_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, shortComplexOfDistTriangleIsoOfIso_hom_τ₁, shortComplexOfDistTriangleIsoOfIso_hom_τ₂, invRotate_map_hom₃, Triangle.isoMk_hom, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, triangleRotation_inverse, triangleRotation_functor, CategoryTheory.Iso.inv_hom_id_triangle_hom₃, DerivedCategory.mem_distTriang_iff, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₂, Triangle.shiftFunctorZero_hom_app_hom₂, invRotCompRot_inv_app_hom₂, TriangleOpEquivalence.inverse_map, CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁, CategoryTheory.Functor.map_distinguished, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂, CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃, isoTriangleOfIso₁₃_inv_hom₃, TriangleOpEquivalence.counitIso_inv_app_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, shortComplexOfDistTriangleIsoOfIso_inv_τ₃, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁, rotCompInvRot_hom_app_hom₁, Triangle.functorMk_obj, Triangle.smul_hom₁, invRotate_obj, HomotopyCategory.Pretriangulated.shift_distinguished_triangle, invRotCompRot_hom_app_hom₁, Triangle.functorIsoMk'_inv_app_hom₁, Triangle.functorIsoMk'_inv_app_hom₃, id_hom₁, CategoryTheory.Functor.mapTriangle_map_hom₂, triangleOpEquivalence_inverse, Triangle.zero_hom₂, instIsEquivalenceTriangleInvRotate, instIsEquivalenceTriangleRotate, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃
triangleMorphismId 📖	CompOp	4 math math: triangleMorphismId_hom₃, triangleCategory_id, triangleMorphismId_hom₂, triangleMorphismId_hom₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binaryBiproductTriangle_mor₁ 📖	mathematical	—	Triangle.mor₁ binaryBiproductTriangle CategoryTheory.Limits.biprod.inl	—	—
binaryBiproductTriangle_mor₂ 📖	mathematical	—	Triangle.mor₂ binaryBiproductTriangle CategoryTheory.Limits.biprod.snd	—	—
binaryBiproductTriangle_mor₃ 📖	mathematical	—	Triangle.mor₃ binaryBiproductTriangle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
binaryBiproductTriangle_obj₁ 📖	mathematical	—	Triangle.obj₁ binaryBiproductTriangle	—	—
binaryBiproductTriangle_obj₂ 📖	mathematical	—	Triangle.obj₂ binaryBiproductTriangle CategoryTheory.Limits.biprod	—	—
binaryBiproductTriangle_obj₃ 📖	mathematical	—	Triangle.obj₃ binaryBiproductTriangle	—	—
binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ binaryProductTriangle CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair binaryBiproductTriangle CategoryTheory.Iso.hom Triangle triangleCategory binaryProductTriangleIsoBinaryBiproductTriangle CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair
binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ binaryProductTriangle CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair binaryBiproductTriangle CategoryTheory.Iso.hom Triangle triangleCategory binaryProductTriangleIsoBinaryBiproductTriangle CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	CategoryTheory.Limits.biprod.isoProd_inv
binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ binaryProductTriangle CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair binaryBiproductTriangle CategoryTheory.Iso.hom Triangle triangleCategory binaryProductTriangleIsoBinaryBiproductTriangle CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair
binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ binaryBiproductTriangle binaryProductTriangle CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair CategoryTheory.Iso.inv Triangle triangleCategory binaryProductTriangleIsoBinaryBiproductTriangle CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair
binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ binaryBiproductTriangle binaryProductTriangle CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair CategoryTheory.Iso.inv Triangle triangleCategory binaryProductTriangleIsoBinaryBiproductTriangle CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd	—	CategoryTheory.Limits.biprod.isoProd_hom
binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ binaryBiproductTriangle binaryProductTriangle CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair CategoryTheory.Iso.inv Triangle triangleCategory binaryProductTriangleIsoBinaryBiproductTriangle CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair
binaryProductTriangle_mor₁ 📖	mathematical	—	Triangle.mor₁ binaryProductTriangle CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
binaryProductTriangle_mor₂ 📖	mathematical	—	Triangle.mor₂ binaryProductTriangle CategoryTheory.Limits.prod.snd	—	—
binaryProductTriangle_mor₃ 📖	mathematical	—	Triangle.mor₃ binaryProductTriangle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
binaryProductTriangle_obj₁ 📖	mathematical	—	Triangle.obj₁ binaryProductTriangle	—	—
binaryProductTriangle_obj₂ 📖	mathematical	—	Triangle.obj₂ binaryProductTriangle CategoryTheory.Limits.prod	—	—
binaryProductTriangle_obj₃ 📖	mathematical	—	Triangle.obj₃ binaryProductTriangle	—	—
comp_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ CategoryTheory.CategoryStruct.comp Triangle CategoryTheory.Category.toCategoryStruct triangleCategory Triangle.obj₁	—	—
comp_hom₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₁ TriangleMorphism.hom₁ Triangle triangleCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom₁
comp_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ CategoryTheory.CategoryStruct.comp Triangle CategoryTheory.Category.toCategoryStruct triangleCategory Triangle.obj₂	—	—
comp_hom₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₂ TriangleMorphism.hom₂ Triangle triangleCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom₂
comp_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ CategoryTheory.CategoryStruct.comp Triangle CategoryTheory.Category.toCategoryStruct triangleCategory Triangle.obj₃	—	—
comp_hom₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.obj₃ TriangleMorphism.hom₃ Triangle triangleCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom₃
contractibleTriangleFunctor_map_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ contractibleTriangle CategoryTheory.Functor.map Triangle triangleCategory contractibleTriangleFunctor	—	—
contractibleTriangleFunctor_map_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ contractibleTriangle CategoryTheory.Functor.map Triangle triangleCategory contractibleTriangleFunctor	—	—
contractibleTriangleFunctor_map_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ contractibleTriangle CategoryTheory.Functor.map Triangle triangleCategory contractibleTriangleFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Triangle.obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
contractibleTriangleFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Triangle triangleCategory contractibleTriangleFunctor contractibleTriangle	—	—
contractibleTriangle_mor₁ 📖	mathematical	—	Triangle.mor₁ contractibleTriangle CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
contractibleTriangle_mor₂ 📖	mathematical	—	Triangle.mor₂ contractibleTriangle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroObject.zero' CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
contractibleTriangle_mor₃ 📖	mathematical	—	Triangle.mor₃ contractibleTriangle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroObject.zero' CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
contractibleTriangle_obj₁ 📖	mathematical	—	Triangle.obj₁ contractibleTriangle	—	—
contractibleTriangle_obj₂ 📖	mathematical	—	Triangle.obj₂ contractibleTriangle	—	—
contractibleTriangle_obj₃ 📖	mathematical	—	Triangle.obj₃ contractibleTriangle CategoryTheory.Limits.HasZeroObject.zero'	—	—
id_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ CategoryTheory.CategoryStruct.id Triangle CategoryTheory.Category.toCategoryStruct triangleCategory Triangle.obj₁	—	—
id_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ CategoryTheory.CategoryStruct.id Triangle CategoryTheory.Category.toCategoryStruct triangleCategory Triangle.obj₂	—	—
id_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ CategoryTheory.CategoryStruct.id Triangle CategoryTheory.Category.toCategoryStruct triangleCategory Triangle.obj₃	—	—
productTriangle_mor₁ 📖	mathematical	—	Triangle.mor₁ productTriangle CategoryTheory.Limits.Pi.map Triangle.obj₁ Triangle.obj₂	—	—
productTriangle_mor₂ 📖	mathematical	—	Triangle.mor₂ productTriangle CategoryTheory.Limits.Pi.map Triangle.obj₂ Triangle.obj₃	—	—
productTriangle_mor₃ 📖	mathematical	—	Triangle.mor₃ productTriangle CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.piObj Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Triangle.obj₁ CategoryTheory.Limits.Pi.map CategoryTheory.inv CategoryTheory.Limits.piComparison	—	—
productTriangle_obj₁ 📖	mathematical	—	Triangle.obj₁ productTriangle CategoryTheory.Limits.piObj	—	—
productTriangle_obj₂ 📖	mathematical	—	Triangle.obj₂ productTriangle CategoryTheory.Limits.piObj	—	—
productTriangle_obj₃ 📖	mathematical	—	Triangle.obj₃ productTriangle CategoryTheory.Limits.piObj	—	—
triangleCategory_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Triangle CategoryTheory.Category.toCategoryStruct triangleCategory TriangleMorphism.comp	—	—
triangleCategory_id 📖	mathematical	—	CategoryTheory.CategoryStruct.id Triangle CategoryTheory.Category.toCategoryStruct triangleCategory triangleMorphismId	—	—
triangleMorphismId_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ triangleMorphismId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₁	—	—
triangleMorphismId_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ triangleMorphismId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₂	—	—
triangleMorphismId_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ triangleMorphismId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₃	—	—

CategoryTheory.Pretriangulated.Triangle

Definitions

Name	Category	Theorems
functorHomMk 📖	CompOp	5 math math: functorHomMk_app_hom₂, functorHomMk_app_hom₃, functorHomMk_app_hom₁, functorIsoMk_hom, functorIsoMk_inv
functorHomMk' 📖	CompOp	3 math math: functorHomMk'_app_hom₁, functorHomMk'_app_hom₃, functorHomMk'_app_hom₂
functorIsoMk 📖	CompOp	2 math math: functorIsoMk_hom, functorIsoMk_inv
functorIsoMk' 📖	CompOp	6 math math: functorIsoMk'_inv_app_hom₂, functorIsoMk'_hom_app_hom₃, functorIsoMk'_hom_app_hom₁, functorIsoMk'_hom_app_hom₂, functorIsoMk'_inv_app_hom₁, functorIsoMk'_inv_app_hom₃
functorMk 📖	CompOp	13 math math: functorHomMk'_app_hom₁, functorIsoMk'_inv_app_hom₂, functorMk_map_hom₃, functorMk_map_hom₁, functorIsoMk'_hom_app_hom₃, functorIsoMk'_hom_app_hom₁, functorHomMk'_app_hom₃, functorIsoMk'_hom_app_hom₂, functorMk_map_hom₂, functorHomMk'_app_hom₂, functorMk_obj, functorIsoMk'_inv_app_hom₁, functorIsoMk'_inv_app_hom₃
homMk 📖	CompOp	7 math math: homMk_hom₃, isoMk_inv, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, homMk_hom₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, homMk_hom₂, isoMk_hom
instAddCommGroupHom 📖	CompOp	—
instAddHom 📖	CompOp	3 math math: add_hom₂, add_hom₃, add_hom₁
instLinear 📖	CompOp	—
instModuleHom 📖	CompOp	—
instNegHom 📖	CompOp	3 math math: neg_hom₁, neg_hom₃, neg_hom₂
instPreadditive 📖	CompOp	—
instSMulHom 📖	CompOp	3 math math: smul_hom₂, smul_hom₃, smul_hom₁
instSubHom 📖	CompOp	3 math math: sub_hom₁, sub_hom₃, sub_hom₂
instZeroHom 📖	CompOp	3 math math: zero_hom₁, zero_hom₃, zero_hom₂
isoMk 📖	CompOp	2 math math: isoMk_inv, isoMk_hom
mk 📖	CompOp	—
mor₁ 📖	CompOp	90 math math: CochainComplex.mappingConeCompTriangleh_comm₁_assoc, coyoneda_exact₂, shiftFunctor_map_hom₁, CochainComplex.mappingCone.triangle_mor₁, CategoryTheory.Triangulated.Octahedron.triangle_mor₁, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Functor.homologySequence_comp_assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, shiftFunctor_obj, CategoryTheory.Functor.homologySequence_comp, CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₁, mor₁_eq_zero_of_mono₂, DerivedCategory.HomologySequence.exact₂, mk_mor₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, DerivedCategory.triangleOfSES_mor₁, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, distinguished_iff_of_isZero₃, CategoryTheory.ObjectProperty.trW_iff_of_distinguished, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁_assoc, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, rotate_mor₃, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_f, CategoryTheory.Triangulated.Octahedron.map_m₃, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.Functor.mapTriangle_map_hom₁, CategoryTheory.Functor.homologySequenceδ_comp_assoc, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, mono₁, isZero₃_iff_isIso₁, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁, π₁Toπ₂_app, DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, invRotate_mor₁, CochainComplex.mappingConeCompTriangle_mor₁, CategoryTheory.Pretriangulated.binaryProductTriangle_mor₁, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, mor₂_eq_zero_iff_epi₁, rotate_mor₁, CategoryTheory.Triangulated.Octahedron.map_m₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Pretriangulated.contractibleTriangle_mor₁, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CategoryTheory.Triangulated.SpectralObject.triangle_mor₁, DerivedCategory.HomologySequence.exact₁, isZero₂_iff, CategoryTheory.Functor.mapTriangle_map_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, CategoryTheory.Functor.homologySequence_exact₁, CategoryTheory.Pretriangulated.productTriangle_mor₁, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc, shiftFunctor_map_hom₃, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, mor₁_eq_zero_iff_epi₃, CategoryTheory.ObjectProperty.trW.mk, CochainComplex.triangleOfDegreewiseSplit_mor₁, mor₁_eq_zero_iff_mono₂, mor₁_eq_zero_of_epi₃, CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang, CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso, shiftFunctor_map_hom₂, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁, epi₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, isZero₁_iff, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, CochainComplex.mappingConeCompTriangleh_comm₁, mor₃_eq_zero_iff_mono₁, DerivedCategory.HomologySequence.δ_comp_assoc, DerivedCategory.HomologySequence.δ_comp, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc, CochainComplex.mappingCone.triangleRotateShortComplex_f, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Functor.homologySequenceδ_comp, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, CategoryTheory.Functor.mapTriangle_map_hom₂, invRotate_mor₂
mor₂ 📖	CompOp	89 math math: CochainComplex.mappingConeCompTriangleh_comm₁_assoc, invRotate_mor₃, shiftFunctor_map_hom₁, DerivedCategory.HomologySequence.comp_δ, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Functor.homologySequence_comp_assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, shiftFunctor_obj, CategoryTheory.Functor.homologySequence_comp, CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₂, DerivedCategory.HomologySequence.exact₂, CategoryTheory.Pretriangulated.productTriangle_mor₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, yoneda_exact₂, epi₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Pretriangulated.binaryProductTriangle_mor₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, distinguished_iff_of_isZero₁, HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism, mor₂_eq_zero_of_mono₃, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, CategoryTheory.Triangulated.Localization.complete_distinguished_triangle_morphism, CategoryTheory.Pretriangulated.contractibleTriangle_mor₂, CategoryTheory.Triangulated.Octahedron.map_m₃, mor₂_eq_zero_of_epi₁, DerivedCategory.HomologySequence.comp_δ_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.Functor.mapTriangle_map_hom₁, coyoneda_exact₃, CategoryTheory.Triangulated.Octahedron.triangle_mor₂, π₂Toπ₃_app, CategoryTheory.ObjectProperty.trW.mk', DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, CategoryTheory.Functor.comp_homologySequenceδ, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, CochainComplex.triangleOfDegreewiseSplit_mor₂, CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism, mk_mor₂, CategoryTheory.Functor.homologySequence_exact₃, CochainComplex.mappingCone.triangle_mor₂, CategoryTheory.Triangulated.SpectralObject.triangle_mor₂, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, mor₂_eq_zero_iff_epi₁, rotate_mor₁, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂, CategoryTheory.Triangulated.Octahedron.map_m₁, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_g, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc, CategoryTheory.ObjectProperty.trW_iff_of_distinguished', isZero₂_iff, CategoryTheory.Functor.mapTriangle_map_hom₃, mor₃_eq_zero_iff_epi₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, shiftFunctor_map_hom₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₂, CochainComplex.mappingCone.triangleRotateShortComplex_g, mor₁_eq_zero_iff_mono₂, rotate_mor₂, CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, isZero₃_iff, shiftFunctor_map_hom₂, CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.compatible_with_triangulation, DerivedCategory.triangleOfSES_mor₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, mor₂_eq_zero_iff_mono₃, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc, CochainComplex.mappingConeCompTriangle_mor₂, CochainComplex.mappingConeCompTriangleh_comm₁, CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂, DerivedCategory.HomologySequence.exact₃, mono₂, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, isZero₁_iff_isIso₂, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, CategoryTheory.Functor.comp_homologySequenceδ_assoc, CategoryTheory.Functor.mapTriangle_map_hom₂, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff, invRotate_mor₂
mor₃ 📖	CompOp	87 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, invRotate_mor₃, shiftFunctor_map_hom₁, CategoryTheory.Functor.mapTriangle_obj, shiftFunctor_obj, CochainComplex.mappingConeCompTriangle_mor₃, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CochainComplex.mappingCone.inr_triangleδ, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CategoryTheory.Triangulated.SpectralObject.triangle_mor₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism, rotate_mor₃, CategoryTheory.Triangulated.Localization.complete_distinguished_triangle_morphism, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.Triangulated.Octahedron.triangle_mor₃, CategoryTheory.Triangulated.Octahedron.map_m₃, distinguished_iff_of_isZero₂, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, mor₃_eq_zero_of_epi₂, CategoryTheory.Functor.mapTriangle_map_hom₁, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, isZero₂_iff_isIso₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₃, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, invRotate_mor₁, CochainComplex.mappingCone.inr_triangleδ_assoc, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, CategoryTheory.Triangulated.Octahedron.map_m₁, CategoryTheory.Pretriangulated.binaryProductTriangle_mor₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃_assoc, π₃Toπ₁_app, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₃, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, CategoryTheory.Functor.mapTriangle_map_hom₃, mor₃_eq_zero_iff_epi₂, mono₃, CategoryTheory.Pretriangulated.productTriangle_mor₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, DerivedCategory.triangleOfSES_mor₃, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc, epi₃, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, CategoryTheory.Pretriangulated.contractibleTriangle_mor₃, shiftFunctor_map_hom₃, CochainComplex.triangleOfDegreewiseSplit_mor₃, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, mor₁_eq_zero_iff_epi₃, rotate_mor₂, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, isZero₃_iff, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, mor₃_eq_zero_of_mono₁, shiftFunctor_map_hom₂, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁, CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.compatible_with_triangulation, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, mor₂_eq_zero_iff_mono₃, isZero₁_iff, mor₃_eq_zero_iff_mono₁, mk_mor₃, CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, coyoneda_exact₁, CategoryTheory.Functor.mapTriangle_map_hom₂, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, yoneda_exact₃, CochainComplex.mappingCone.map_δ
obj₁ 📖	CompOp	190 math math: CochainComplex.triangleOfDegreewiseSplit_obj₁, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, shiftFunctorZero_inv_app_hom₁, coyoneda_exact₂, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁, invRotate_obj₁, shiftFunctor_map_hom₁, CategoryTheory.Pretriangulated.productTriangle.π_hom₁, DerivedCategory.HomologySequence.comp_δ, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.homologySequence_comp_assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, shiftFunctor_obj, CategoryTheory.Pretriangulated.comp_hom₁_assoc, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁, CategoryTheory.Iso.inv_hom_id_triangle_hom₁, CategoryTheory.Functor.homologySequence_comp, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, mor₁_eq_zero_of_mono₂, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₁, DerivedCategory.HomologySequence.exact₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, CategoryTheory.Functor.homologySequenceδ_naturality, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CochainComplex.mappingCone.inr_triangleδ, rotate_obj₁, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, eqToHom_hom₁, distinguished_iff_of_isZero₃, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.ObjectProperty.trW_iff_of_distinguished, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁_assoc, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₁, rotate_mor₃, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, sub_hom₁, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.Triangulated.Octahedron.map_m₃, distinguished_iff_of_isZero₂, DerivedCategory.HomologySequence.comp_δ_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.ext₁', CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, mor₃_eq_zero_of_epi₂, CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.Functor.mapTriangle_map_hom₁, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.homologySequenceδ_comp_assoc, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, isZero₂_iff_isIso₃, isZero₃_iff_isIso₁, neg_hom₁, CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₁, DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, CategoryTheory.Functor.comp_homologySequenceδ, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, invRotate_mor₁, CochainComplex.mappingCone.inr_triangleδ_assoc, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, DerivedCategory.triangleOfSES_obj₁, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂, zero_hom₁, CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, mor₂_eq_zero_iff_epi₁, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃, CategoryTheory.Triangulated.Octahedron.map_m₁, CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₁, CategoryTheory.Pretriangulated.rotate_map_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, instIsIsoHom₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Iso.hom_inv_id_triangle_hom₁, CategoryTheory.Pretriangulated.productTriangle.lift_hom₁, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃_assoc, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, CategoryTheory.Triangulated.Octahedron.triangle_obj₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₁, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, CategoryTheory.ObjectProperty.trW_iff_of_distinguished', rotate_obj₃, CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₁, shiftFunctorZero_hom_app_hom₁, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, DerivedCategory.HomologySequence.exact₁, isZero₂_iff, shiftFunctorAdd'_inv_app_hom₁, CategoryTheory.Functor.mapTriangle_map_hom₃, mor₃_eq_zero_iff_epi₂, CategoryTheory.Triangulated.TStructure.instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, π₁_obj, mono₃, CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₁, CategoryTheory.Pretriangulated.contractibleTriangle_obj₁, CategoryTheory.Pretriangulated.productTriangle_mor₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, CategoryTheory.Iso.inv_hom_id_triangle_hom₁_assoc, CategoryTheory.Functor.homologySequence_exact₁, CategoryTheory.Pretriangulated.productTriangle_mor₁, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, shiftFunctor_map_hom₃, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁, add_hom₁, shiftFunctorAdd'_hom_app_hom₁, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, invRotate_obj₂, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, mor₁_eq_zero_iff_epi₃, CategoryTheory.Pretriangulated.productTriangle_obj₁, CategoryTheory.ObjectProperty.trW.mk, CategoryTheory.Pretriangulated.triangleMorphismId_hom₁, mor₁_eq_zero_iff_mono₂, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁, mor₁_eq_zero_of_epi₃, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, isZero₃_iff, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃, CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, isZero₁_of_isZero₂₃, CategoryTheory.Pretriangulated.comp_hom₁, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, CategoryTheory.Functor.homologySequenceδ_naturality_assoc, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁', mor₃_eq_zero_of_mono₁, shiftFunctor_map_hom₂, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁, isZero₁_of_isIso₂, epi₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.Triangulated.SpectralObject.triangle_obj₁, mor₂_eq_zero_iff_mono₃, isZero₁_iff, CategoryTheory.Pretriangulated.binaryProductTriangle_obj₁, CochainComplex.mappingConeCompTriangleh_comm₁, mor₃_eq_zero_iff_mono₁, DerivedCategory.HomologySequence.δ_comp_assoc, DerivedCategory.HomologySequence.δ_comp, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂, DerivedCategory.HomologySequence.exact₃, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁, isZero₁_iff_isIso₂, CategoryTheory.Functor.homologySequenceδ_comp, mk_obj₁, CategoryTheory.Pretriangulated.isIso₁_of_isIso₂₃, CochainComplex.mappingCone.triangle_obj₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₁, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₁, smul_hom₁, CategoryTheory.Functor.comp_homologySequenceδ_assoc, CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₁, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, CategoryTheory.Pretriangulated.id_hom₁, CategoryTheory.Functor.mapTriangle_map_hom₂, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, CochainComplex.mappingConeCompTriangle_obj₁, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff, yoneda_exact₃, CochainComplex.mappingCone.map_δ
obj₂ 📖	CompOp	165 math math: CategoryTheory.Pretriangulated.contractibleTriangle_obj₂, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, CategoryTheory.Pretriangulated.binaryProductTriangle_obj₂, CochainComplex.mappingConeCompTriangle_obj₂, CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₂, invRotate_mor₃, CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₂, instIsIsoHom₂, shiftFunctor_map_hom₁, CategoryTheory.Triangulated.TStructure.triangle_iso_exists, CategoryTheory.Iso.inv_hom_id_triangle_hom₂, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂, DerivedCategory.HomologySequence.comp_δ, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Functor.homologySequence_comp_assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, shiftFunctor_obj, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₂, eqToHom_hom₂, CategoryTheory.Functor.homologySequence_comp, mor₁_eq_zero_of_mono₂, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂, CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.ext₂', CategoryTheory.Iso.inv_hom_id_triangle_hom₂_assoc, DerivedCategory.HomologySequence.exact₂, CategoryTheory.Pretriangulated.productTriangle_mor₂, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, isZero₂_of_isZero₁₃, epi₂, rotate_obj₁, smul_hom₂, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, distinguished_iff_of_isZero₃, CategoryTheory.ObjectProperty.trW_iff_of_distinguished, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁_assoc, CochainComplex.triangleOfDegreewiseSplit_obj₂, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃, CategoryTheory.Iso.hom_inv_id_triangle_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc, distinguished_iff_of_isZero₁, mor₂_eq_zero_of_mono₃, CategoryTheory.Triangulated.SpectralObject.triangle_obj₂, rotate_mor₃, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, CochainComplex.mappingCone.triangleRotateShortComplex_X₂, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂, CategoryTheory.Triangulated.Octahedron.map_m₃, mor₂_eq_zero_of_epi₁, DerivedCategory.HomologySequence.comp_δ_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, invRotate_obj₃, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.Functor.mapTriangle_map_hom₁, CategoryTheory.Functor.homologySequenceδ_comp_assoc, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, coyoneda_exact₃, mono₁, isZero₂_iff_isIso₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂, isZero₃_iff_isIso₁, CategoryTheory.ObjectProperty.trW.mk', DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, CategoryTheory.Functor.comp_homologySequenceδ, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, CategoryTheory.Pretriangulated.productTriangle.π_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₂, CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, mor₂_eq_zero_iff_epi₁, CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₂, CategoryTheory.Triangulated.Octahedron.map_m₁, CategoryTheory.Pretriangulated.comp_hom₂_assoc, CategoryTheory.Pretriangulated.id_hom₂, CategoryTheory.Pretriangulated.triangleMorphismId_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁, shiftFunctorAdd'_inv_app_hom₂, isZero₂_of_isIso₃, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc, CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₂, CategoryTheory.ObjectProperty.trW_iff_of_distinguished', CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, DerivedCategory.HomologySequence.exact₁, isZero₂_iff, CategoryTheory.Functor.mapTriangle_map_hom₃, neg_hom₂, mor₃_eq_zero_iff_epi₂, CategoryTheory.Pretriangulated.comp_hom₂, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂, add_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₂, CategoryTheory.Functor.homologySequence_exact₁, CategoryTheory.Pretriangulated.productTriangle_mor₁, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc, shiftFunctor_map_hom₃, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, π₂_obj, mk_obj₂, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, invRotate_obj₂, mor₁_eq_zero_iff_epi₃, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂, CategoryTheory.ObjectProperty.trW.mk, mor₁_eq_zero_iff_mono₂, CategoryTheory.Triangulated.Octahedron.triangle_obj₂, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂, sub_hom₂, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂', mor₁_eq_zero_of_epi₃, CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang, rotate_obj₂, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂, isZero₃_iff, CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₂, DerivedCategory.triangleOfSES_obj₂, CategoryTheory.Pretriangulated.productTriangle.lift_hom₂, CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂, shiftFunctor_map_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂, shiftFunctorZero_inv_app_hom₂, mor₂_eq_zero_iff_mono₃, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc, shiftFunctorAdd'_hom_app_hom₂, CategoryTheory.Pretriangulated.productTriangle_obj₂, isZero₁_iff, CochainComplex.mappingCone.triangle_obj₂, CochainComplex.mappingConeCompTriangleh_comm₁, mor₃_eq_zero_iff_mono₁, DerivedCategory.HomologySequence.δ_comp_assoc, DerivedCategory.HomologySequence.δ_comp, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₂, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂, DerivedCategory.HomologySequence.exact₃, shiftFunctorZero_hom_app_hom₂, CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₂, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, isZero₁_iff_isIso₂, CategoryTheory.Functor.homologySequenceδ_comp, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, CategoryTheory.Functor.comp_homologySequenceδ_assoc, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, CategoryTheory.Functor.mapTriangle_map_hom₂, zero_hom₂, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff
obj₃ 📖	CompOp	179 math math: CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₃, CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃, isZero₃_of_isIso₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, invRotate_mor₃, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃, invRotate_obj₁, shiftFunctor_map_hom₁, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃', DerivedCategory.HomologySequence.comp_δ, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.homologySequence_comp_assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, shiftFunctor_obj, CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₃, CategoryTheory.Functor.homologySequence_comp, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, DerivedCategory.HomologySequence.exact₂, CategoryTheory.Pretriangulated.productTriangle_mor₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, yoneda_exact₂, CategoryTheory.Functor.homologySequenceδ_naturality, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, eqToHom_hom₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₃, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.ObjectProperty.trW_iff_of_distinguished, CategoryTheory.Pretriangulated.triangleMorphismId_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Pretriangulated.id_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, distinguished_iff_of_isZero₁, HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism, mor₂_eq_zero_of_mono₃, DerivedCategory.triangleOfSES_obj₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₃, CategoryTheory.Triangulated.Localization.complete_distinguished_triangle_morphism, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃, CategoryTheory.Triangulated.Octahedron.map_m₃, distinguished_iff_of_isZero₂, mor₂_eq_zero_of_epi₁, DerivedCategory.HomologySequence.comp_δ_assoc, invRotate_obj₃, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, CategoryTheory.Pretriangulated.invRotate_map_hom₁, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, mor₃_eq_zero_of_epi₂, CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.Functor.mapTriangle_map_hom₁, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.homologySequenceδ_comp_assoc, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, CategoryTheory.Pretriangulated.isIso₃_of_isIso₁₂, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.Triangulated.TStructure.instIsGEObj₃ObjTriangleTriangleLTGE, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂, isZero₂_iff_isIso₃, isZero₃_iff_isIso₁, shiftFunctorZero_inv_app_hom₃, CategoryTheory.Pretriangulated.productTriangle.π_hom₃, CategoryTheory.Pretriangulated.comp_hom₃_assoc, neg_hom₃, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃, CategoryTheory.ObjectProperty.trW.mk', instIsIsoHom₃, DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃, CategoryTheory.Functor.comp_homologySequenceδ, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, invRotate_mor₁, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism, CochainComplex.triangleOfDegreewiseSplit_obj₃, CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, mor₂_eq_zero_iff_epi₁, CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₃, CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁, CategoryTheory.Triangulated.Octahedron.map_m₁, CategoryTheory.Pretriangulated.contractibleTriangle_obj₃, CochainComplex.mappingConeCompTriangle_obj₃, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₃, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃_assoc, CategoryTheory.Iso.hom_inv_id_triangle_hom₃, CategoryTheory.ObjectProperty.trW_iff_of_distinguished', shiftFunctorZero_hom_app_hom₃, rotate_obj₃, CategoryTheory.Pretriangulated.productTriangle_obj₃, DerivedCategory.HomologySequence.exact₁, isZero₂_iff, CategoryTheory.Functor.mapTriangle_map_hom₃, mor₃_eq_zero_iff_epi₂, shiftFunctorAdd'_hom_app_hom₃, CategoryTheory.Pretriangulated.productTriangle.lift_hom₃, zero_hom₃, add_hom₃, CategoryTheory.Pretriangulated.productTriangle_mor₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, CategoryTheory.Functor.homologySequence_exact₁, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc, CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.ext₃', epi₃, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, CategoryTheory.Pretriangulated.binaryProductTriangle_obj₃, shiftFunctor_map_hom₃, π₃_obj, smul_hom₃, mor₁_eq_zero_iff_epi₃, sub_hom₃, CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₃, mor₁_eq_zero_iff_mono₂, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₃, CategoryTheory.Pretriangulated.comp_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, rotate_obj₂, CategoryTheory.Iso.hom_inv_id_triangle_hom₃_assoc, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, isZero₃_iff, CategoryTheory.Triangulated.SpectralObject.triangle_obj₃, shiftFunctorAdd'_inv_app_hom₃, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, CategoryTheory.Functor.homologySequenceδ_naturality_assoc, mor₃_eq_zero_of_mono₁, shiftFunctor_map_hom₂, CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.compatible_with_triangulation, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, mor₂_eq_zero_iff_mono₃, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc, isZero₁_iff, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁, CochainComplex.mappingConeCompTriangleh_comm₁, mor₃_eq_zero_iff_mono₁, DerivedCategory.HomologySequence.δ_comp_assoc, DerivedCategory.HomologySequence.δ_comp, CategoryTheory.Iso.inv_hom_id_triangle_hom₃, CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂, CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₃, DerivedCategory.HomologySequence.exact₃, isZero₃_of_isZero₁₂, mono₂, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, mk_obj₃, isZero₁_iff_isIso₂, CategoryTheory.Functor.homologySequenceδ_comp, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, CategoryTheory.Functor.comp_homologySequenceδ_assoc, CategoryTheory.Triangulated.Octahedron.triangle_obj₃, coyoneda_exact₁, CategoryTheory.Functor.mapTriangle_map_hom₂, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, CochainComplex.mappingCone.triangle_obj₃, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃, CochainComplex.mappingCone.map_δ
π₁ 📖	CompOp	7 math math: π₁_map, functorHomMk'_app_hom₁, functorIsoMk'_hom_app_hom₁, π₁Toπ₂_app, π₃Toπ₁_app, π₁_obj, functorIsoMk'_inv_app_hom₁
π₁Toπ₂ 📖	CompOp	1 math math: π₁Toπ₂_app
π₂ 📖	CompOp	7 math math: π₂_map, functorIsoMk'_inv_app_hom₂, π₁Toπ₂_app, π₂Toπ₃_app, functorIsoMk'_hom_app_hom₂, π₂_obj, functorHomMk'_app_hom₂
π₂Toπ₃ 📖	CompOp	1 math math: π₂Toπ₃_app
π₃ 📖	CompOp	7 math math: π₃_map, functorIsoMk'_hom_app_hom₃, functorHomMk'_app_hom₃, π₂Toπ₃_app, π₃Toπ₁_app, π₃_obj, functorIsoMk'_inv_app_hom₃
π₃Toπ₁ 📖	CompOp	1 math math: π₃Toπ₁_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instAddHom obj₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instAddHom obj₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instAddHom obj₃ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
eqToHom_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.eqToHom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory obj₁	—	—
eqToHom_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.eqToHom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory obj₂	—	—
eqToHom_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.eqToHom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory obj₃	—	—
functorHomMk'_app_hom₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app functorHomMk' π₁	—	—
functorHomMk'_app_hom₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app functorHomMk' π₂	—	—
functorHomMk'_app_hom₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app functorHomMk' π₃	—	—
functorHomMk_app_hom₁ 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ π₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerLeft π₁Toπ₂ π₃ π₂Toπ₃ CategoryTheory.shiftFunctor Int.instAddMonoid π₃Toπ₁ CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.NatTrans.app functorHomMk	—	—
functorHomMk_app_hom₂ 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ π₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerLeft π₁Toπ₂ π₃ π₂Toπ₃ CategoryTheory.shiftFunctor Int.instAddMonoid π₃Toπ₁ CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.NatTrans.app functorHomMk	—	—
functorHomMk_app_hom₃ 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ π₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerLeft π₁Toπ₂ π₃ π₂Toπ₃ CategoryTheory.shiftFunctor Int.instAddMonoid π₃Toπ₁ CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.NatTrans.app functorHomMk	—	—
functorIsoMk'_hom_app_hom₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app functorIsoMk' π₁	—	—
functorIsoMk'_hom_app_hom₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app functorIsoMk' π₂	—	—
functorIsoMk'_hom_app_hom₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app functorIsoMk' π₃	—	—
functorIsoMk'_inv_app_hom₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app CategoryTheory.Iso.inv functorIsoMk' π₁	—	—
functorIsoMk'_inv_app_hom₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app CategoryTheory.Iso.inv functorIsoMk' π₂	—	—
functorIsoMk'_inv_app_hom₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskerRight	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app CategoryTheory.Iso.inv functorIsoMk' π₃	—	—
functorIsoMk_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ π₂ CategoryTheory.Functor.whiskerLeft π₁Toπ₂ CategoryTheory.Iso.hom π₃ π₂Toπ₃ CategoryTheory.shiftFunctor Int.instAddMonoid π₃Toπ₁ CategoryTheory.Functor.whiskerRight	functorIsoMk functorHomMk	—	—
functorIsoMk_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ π₂ CategoryTheory.Functor.whiskerLeft π₁Toπ₂ CategoryTheory.Iso.hom π₃ π₂Toπ₃ CategoryTheory.shiftFunctor Int.instAddMonoid π₃Toπ₁ CategoryTheory.Functor.whiskerRight	CategoryTheory.Iso.inv functorIsoMk functorHomMk	—	—
functorMk_map_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk	—	—
functorMk_map_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk	—	—
functorMk_map_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk	—	—
functorMk_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory functorMk CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid	—	—
homMk_hom₁ 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.CategoryStruct.comp mor₁ obj₃ mor₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid mor₃ CategoryTheory.Functor.map	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ homMk	—	—
homMk_hom₂ 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.CategoryStruct.comp mor₁ obj₃ mor₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid mor₃ CategoryTheory.Functor.map	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ homMk	—	—
homMk_hom₃ 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.CategoryStruct.comp mor₁ obj₃ mor₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid mor₃ CategoryTheory.Functor.map	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ homMk	—	—
hom_ext 📖	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃	—	—	CategoryTheory.Pretriangulated.TriangleMorphism.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃	—	hom_ext
instIsIsoHom₁ 📖	mathematical	—	CategoryTheory.IsIso obj₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₁	—	CategoryTheory.Functor.map_isIso
instIsIsoHom₂ 📖	mathematical	—	CategoryTheory.IsIso obj₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂	—	CategoryTheory.Functor.map_isIso
instIsIsoHom₃ 📖	mathematical	—	CategoryTheory.IsIso obj₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃	—	CategoryTheory.Functor.map_isIso
isIso_of_isIsos 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory	—	CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ CategoryTheory.Pretriangulated.TriangleMorphism.comm₃ CategoryTheory.Iso.isIso_hom
isoMk_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.CategoryStruct.comp mor₁ CategoryTheory.Iso.hom obj₃ mor₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid mor₃ CategoryTheory.Functor.map	CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory isoMk homMk	—	—
isoMk_inv 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj₁ obj₂ CategoryTheory.CategoryStruct.comp mor₁ CategoryTheory.Iso.hom obj₃ mor₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid mor₃ CategoryTheory.Functor.map	CategoryTheory.Iso.inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory isoMk homMk	—	—
mk_mor₁ 📖	mathematical	—	mor₁	—	—
mk_mor₂ 📖	mathematical	—	mor₂	—	—
mk_mor₃ 📖	mathematical	—	mor₃	—	—
mk_obj₁ 📖	mathematical	—	obj₁	—	—
mk_obj₂ 📖	mathematical	—	obj₂	—	—
mk_obj₃ 📖	mathematical	—	obj₃	—	—
neg_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instNegHom obj₁ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instNegHom obj₂ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instNegHom obj₃ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
smul_hom₁ 📖	mathematical	CategoryTheory.Functor.Linear CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instSMulHom obj₁ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	—
smul_hom₂ 📖	mathematical	CategoryTheory.Functor.Linear CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instSMulHom obj₂ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	—
smul_hom₃ 📖	mathematical	CategoryTheory.Functor.Linear CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instSMulHom obj₃ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	—
sub_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instSubHom obj₁ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
sub_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instSubHom obj₂ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
sub_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instSubHom obj₃ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
zero_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instZeroHom obj₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
zero_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instZeroHom obj₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
zero_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory instZeroHom obj₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
π₁Toπ₂_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ π₂ π₁Toπ₂ mor₁	—	—
π₁_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ CategoryTheory.Pretriangulated.TriangleMorphism.hom₁	—	—
π₁_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₁ obj₁	—	—
π₂Toπ₃_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₂ π₃ π₂Toπ₃ mor₂	—	—
π₂_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂	—	—
π₂_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₂ obj₂	—	—
π₃Toπ₁_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₃ CategoryTheory.Functor.comp π₁ CategoryTheory.shiftFunctor Int.instAddMonoid π₃Toπ₁ mor₃	—	—
π₃_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃	—	—
π₃_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory π₃ obj₃	—	—

CategoryTheory.Pretriangulated.TriangleMorphism

Definitions

Name	Category	Theorems
comp 📖	CompOp	4 math math: comp_hom₂, comp_hom₁, CategoryTheory.Pretriangulated.triangleCategory_comp, comp_hom₃
hom₁ 📖	CompOp	88 math math: CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁, CategoryTheory.Pretriangulated.Triangle.π₁_map, CategoryTheory.Pretriangulated.productTriangle.π_hom₁, CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₁, CategoryTheory.Pretriangulated.comp_hom₁_assoc, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁, CategoryTheory.Iso.inv_hom_id_triangle_hom₁, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁, CategoryTheory.Functor.homologySequenceδ_naturality, CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₁, comm₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₁, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₁, CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₁, comm₁_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_hom₁, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₁, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, CategoryTheory.Pretriangulated.Triangle.sub_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₁, CategoryTheory.Pretriangulated.invRotate_map_hom₁, CategoryTheory.Functor.mapTriangle_map_hom₁, CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₁, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₁, CategoryTheory.Pretriangulated.Triangle.neg_hom₁, CategoryTheory.Pretriangulated.Triangle.homMk_hom₁, comp_hom₁, CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₁, CategoryTheory.Pretriangulated.Triangle.zero_hom₁, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁, CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₁, CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₁, CategoryTheory.Pretriangulated.rotate_map_hom₃, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁, CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₁, CategoryTheory.Pretriangulated.invRotate_map_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.Iso.hom_inv_id_triangle_hom₁, CategoryTheory.Pretriangulated.productTriangle.lift_hom₁, comm₃_assoc, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₁, CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₁, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃_hom_hom₁, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁, CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₁, CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₁, CategoryTheory.Iso.inv_hom_id_triangle_hom₁_assoc, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CategoryTheory.Pretriangulated.rotate_map_hom₁, comm₁, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁, CategoryTheory.Pretriangulated.Triangle.add_hom₁, CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₁, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₁, CategoryTheory.Pretriangulated.triangleMorphismId_hom₁, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃_inv_hom₁, ext_iff, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁, CochainComplex.mappingCone.triangleMap_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₁, CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso, CategoryTheory.Pretriangulated.comp_hom₁, CategoryTheory.Functor.homologySequenceδ_naturality_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₁, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₁, CategoryTheory.Pretriangulated.Triangle.hom_ext_iff, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁, CategoryTheory.Pretriangulated.isIso₁_of_isIso₂₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₁, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁, CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₁, CategoryTheory.Pretriangulated.Triangle.smul_hom₁, CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₁, CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₁, CategoryTheory.Pretriangulated.id_hom₁
hom₂ 📖	CompOp	85 math math: CategoryTheory.Pretriangulated.Triangle.π₂_map, comp_hom₂, CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₂, CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₂, CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂, CategoryTheory.Triangulated.TStructure.triangle_iso_exists, CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₂, CategoryTheory.Iso.inv_hom_id_triangle_hom₂, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂, CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₂, CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₂, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_hom₂, CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₂, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂, CategoryTheory.Iso.inv_hom_id_triangle_hom₂_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₂, CategoryTheory.Pretriangulated.Triangle.smul_hom₂, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, comm₁_assoc, CategoryTheory.Iso.hom_inv_id_triangle_hom₂, CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc, CochainComplex.mappingCone.triangleMap_hom₂, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₂, CategoryTheory.Pretriangulated.productTriangle.π_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₂, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂, CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃, CategoryTheory.Pretriangulated.rotate_map_hom₂, CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₂, CategoryTheory.Pretriangulated.comp_hom₂_assoc, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₂, CategoryTheory.Pretriangulated.id_hom₂, CategoryTheory.Pretriangulated.triangleMorphismId_hom₂, CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₂, CategoryTheory.Pretriangulated.invRotate_map_hom₂, CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₂, CategoryTheory.Pretriangulated.Triangle.homMk_hom₂, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₂, CategoryTheory.Pretriangulated.Triangle.neg_hom₂, CategoryTheory.Pretriangulated.comp_hom₂, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂, CategoryTheory.Pretriangulated.Triangle.add_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₂, CategoryTheory.Pretriangulated.rotate_map_hom₁, comm₁, CategoryTheory.Triangulated.TStructure.triangle_map_exists, CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₂, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₂, ext_iff, CategoryTheory.Pretriangulated.Triangle.sub_hom₂, CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂, CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₂, CategoryTheory.Pretriangulated.productTriangle.lift_hom₂, CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₂, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂, CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₂, comm₂_assoc, CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₂, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₂, CategoryTheory.Pretriangulated.invRotate_map_hom₃, CategoryTheory.Pretriangulated.Triangle.hom_ext_iff, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂, comm₂, CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₂, CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₂, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, CategoryTheory.Functor.mapTriangle_map_hom₂, CategoryTheory.Pretriangulated.Triangle.zero_hom₂, CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₂
hom₃ 📖	CompOp	84 math math: CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₃, CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃, CategoryTheory.Pretriangulated.Triangle.homMk_hom₃, CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₃, CategoryTheory.Pretriangulated.Triangle.π₃_map, CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₃, CategoryTheory.Functor.homologySequenceδ_naturality, comm₃, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₃, CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃, CategoryTheory.Pretriangulated.triangleMorphismId_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Pretriangulated.id_hom₃, CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₃, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃, CategoryTheory.Pretriangulated.invRotate_map_hom₁, CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₃, CategoryTheory.Pretriangulated.isIso₃_of_isIso₁₂, CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₃, CategoryTheory.Pretriangulated.productTriangle.π_hom₃, CategoryTheory.Pretriangulated.comp_hom₃_assoc, CategoryTheory.Pretriangulated.Triangle.neg_hom₃, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃, CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₃, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₃, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₃, CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₃, CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₃, CategoryTheory.Pretriangulated.rotate_map_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃, CategoryTheory.Pretriangulated.rotate_map_hom₃, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃, comm₃_assoc, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, CategoryTheory.Iso.hom_inv_id_triangle_hom₃, CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₃, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃, CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₃, CategoryTheory.Functor.mapTriangle_map_hom₃, CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₃, CategoryTheory.Pretriangulated.productTriangle.lift_hom₃, CategoryTheory.Pretriangulated.Triangle.zero_hom₃, CategoryTheory.Pretriangulated.Triangle.add_hom₃, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃_hom_hom₃, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃, CategoryTheory.Pretriangulated.Triangle.smul_hom₃, CategoryTheory.Pretriangulated.Triangle.sub_hom₃, CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₃, CategoryTheory.Pretriangulated.comp_hom₃, ext_iff, CategoryTheory.Iso.hom_inv_id_triangle_hom₃_assoc, CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₃, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃, CategoryTheory.Functor.homologySequenceδ_naturality_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, comm₂_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₃, CochainComplex.mappingCone.triangleMap_hom₃, CategoryTheory.Pretriangulated.invRotate_map_hom₃, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, CategoryTheory.Pretriangulated.Triangle.hom_ext_iff, CategoryTheory.Iso.inv_hom_id_triangle_hom₃, comm₂, comp_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃_inv_hom₃, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₃, CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.mor₁ hom₂ hom₁	—	—
comm₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.mor₁ hom₂ hom₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₁
comm₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₂ hom₃ hom₂	—	—
comm₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₂ hom₃ hom₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₂
comm₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.map hom₁ hom₃	—	—
comm₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.map hom₁ hom₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₃
comp_hom₁ 📖	mathematical	—	hom₁ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
comp_hom₂ 📖	mathematical	—	hom₂ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
comp_hom₃ 📖	mathematical	—	hom₃ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
ext 📖	—	hom₁ hom₂ hom₃	—	—	—
ext_iff 📖	mathematical	—	hom₁ hom₂ hom₃	—	ext

CategoryTheory.Pretriangulated.productTriangle

Definitions

Name	Category	Theorems
fan 📖	CompOp	—
isLimitFan 📖	CompOp	—
π 📖	CompOp	3 math math: π_hom₁, π_hom₃, π_hom₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Pretriangulated.productTriangle lift CategoryTheory.Limits.Pi.lift CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
lift_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Pretriangulated.productTriangle lift CategoryTheory.Limits.Pi.lift CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
lift_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Pretriangulated.productTriangle lift CategoryTheory.Limits.Pi.lift CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
zero₃₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Pretriangulated.productTriangle	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Limits.instIsIsoPiComparison CategoryTheory.Limits.zero_comp CategoryTheory.Limits.Pi.hom_ext CategoryTheory.Limits.map_lift_piComparison CategoryTheory.Functor.map_comp CategoryTheory.Limits.limit.lift_π CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.Limits.limMap_π_assoc CategoryTheory.Limits.comp_zero
π_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Pretriangulated.productTriangle π CategoryTheory.Limits.Pi.π CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
π_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Pretriangulated.productTriangle π CategoryTheory.Limits.Pi.π CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
π_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Pretriangulated.productTriangle π CategoryTheory.Limits.Pi.π CategoryTheory.Pretriangulated.Triangle.obj₃	—	—

---

← Back to Index