Triangle

📁 Source: Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean

Statistics

Metric	Count
Definitions Triangle, counitIso, functor, inverse, unitIso, triangleOpEquivalence	6
Theorems counitIso_hom_app_hom₁, counitIso_hom_app_hom₂, counitIso_hom_app_hom₃, counitIso_inv_app_hom₁, counitIso_inv_app_hom₂, counitIso_inv_app_hom₃, functor_map_hom₁, functor_map_hom₂, functor_map_hom₃, functor_obj, inverse_map, inverse_obj, unitIso_hom_app, unitIso_inv_app, triangleOpEquivalence_counitIso, triangleOpEquivalence_functor, triangleOpEquivalence_inverse, triangleOpEquivalence_unitIso	18
Total	24

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
Triangle 📖	CompData	375 math math: rotCompInvRot_hom_app_hom₃, CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc, HomotopyCategory.spectralObjectMappingCone_δ'_app, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₃, Triangle.π₂_map, CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃, CategoryTheory.Triangulated.Octahedron.mem, triangleRotation_counitIso, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₂, 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.TStructure.triangleω₁δ_obj_obj₂, 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, CategoryTheory.Functor.distTriang_iff, contractibleTriangleFunctor_map_hom₂, CategoryTheory.Iso.inv_hom_id_triangle_hom₂, CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₃, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂, Opposite.mem_distinguishedTriangles_iff', CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₂, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_distinguished, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Triangulated.Octahedron'.mem, Triangle.functorHomMk'_app_hom₁, Triangle.shift_distinguished, Triangle.shiftFunctor_obj, Triangle.functorHomMk_app_hom₂, 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.Triangulated.TStructure.triangleω₁δ_map_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₂, CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂, Triangle.shiftFunctorAdd_eq, CategoryTheory.Iso.inv_hom_id_triangle_hom₂_assoc, CategoryTheory.Triangulated.AbelianSubcategory.exists_distinguished_triangle_of_epi, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₁, TriangleOpEquivalence.functor_map_hom₂, Triangle.π₃_map, CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished, Triangle.functorMk_map_hom₃, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂, Triangle.shiftFunctorZero_eq, Triangle.functorMk_map_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, Opposite.contractibleTriangleIso_hom_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, Triangle.eqToHom_hom₃, Triangle.functorIsoMk'_hom_app_hom₃, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₃, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₁, CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₁, DerivedCategory.mappingCone_triangle_distinguished, Triangle.smul_hom₂, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃, CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_iff, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂, Triangle.eqToHom_hom₁, Triangle.distinguished_iff_of_isZero₃, Opposite.contractibleTriangleIso_hom_hom₁, Triangle.functorIsoMk'_hom_app_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₁, Triangle.isoMk_inv, CategoryTheory.Triangulated.TStructure.triangleω₁δ_distinguished, CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₃, 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.Triangulated.TStructure.triangleLTLTGELT_obj_obj₃, CategoryTheory.Iso.hom_inv_id_triangle_hom₂, TriangleOpEquivalence.unitIso_hom_app, CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc, Triangle.distinguished_iff_of_isZero₁, isoTriangleOfIso₁₂_hom_hom₁, Triangle.isIso_of_isIsos, CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₁, TriangleOpEquivalence.counitIso_hom_app_hom₁, CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₂, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, TriangleOpEquivalence.counitIso_inv_app_hom₃, HomotopyCategory.mappingCone_triangleh_distinguished, Triangle.sub_hom₁, CategoryTheory.Triangulated.TStructure.exists_triangle, 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₃, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃, Triangle.distinguished_iff_of_isZero₂, binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₃, Triangle.shift_distinguished_iff, contractibleTriangleFunctor_map_hom₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₃, invRotate_map_hom₁, triangleRotation_unitIso, CategoryTheory.Functor.mapTriangle_map_hom₁, contractible_distinguished₂, preadditiveYoneda_homologySequenceδ_apply, Triangle.functorHomMk_app_hom₃, 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, Opposite.contractible_distinguished, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃, op_distinguished, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₃, distinguished_cocone_triangle₂, HomotopyCategory.Pretriangulated.distinguished_cocone_triangle, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₁, mem_distTriang_op_iff, contractibleTriangleFunctor_obj, HomotopyCategory.Pretriangulated.contractible_distinguished, TriangleOpEquivalence.counitIso_inv_app_hom₂, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂, Triangle.functorHomMk_app_hom₁, Triangle.zero_hom₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₃, triangleOpEquivalence_counitIso, triangleOpEquivalence_functor, shortComplexOfDistTriangleIsoOfIso_hom_τ₃, CategoryTheory.ObjectProperty.trW_iff', rotCompInvRot_inv_app_hom₃, contractibleTriangleFunctor_map_hom₃, binaryProductTriangle_distinguished, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁, rotate_map_hom₂, invRotCompRot_hom_app_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃, invRotCompRot_inv_app_hom₁, CategoryTheory.ObjectProperty.hasInducedTStructure_iff, rotate_map_hom₃, mem_distTriang_op_iff', CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₂, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃, comp_hom₂_assoc, CategoryTheory.ObjectProperty.extensionProduct_iff, CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₂, id_hom₂, TriangleOpEquivalence.unitIso_inv_app, Triangle.functorIsoMk'_hom_app_hom₂, distinguished_cocone_triangle, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁, CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃, CategoryTheory.Triangulated.TStructure.exists_triangle_zero_one, 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.Triangulated.SpectralObject.distinguished', CategoryTheory.Iso.hom_inv_id_triangle_hom₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₁, distinguished_cocone_triangle₁, Triangle.π₃Toπ₁_app, CategoryTheory.Triangulated.TStructure.isIso_truncGT_map_iff, Triangle.shiftFunctorZero_hom_app_hom₃, Triangle.shiftFunctorZero_hom_app_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, isoTriangleOfIso₁₃_hom_hom₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_distinguished, CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁, CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₃, CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₁, 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, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₁, Triangle.shiftFunctorAdd'_hom_app_hom₃, Triangle.shiftFunctor_eq, isomorphic_distinguished, Opposite.distinguished_cocone_triangle, CategoryTheory.Triangulated.TStructure.instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, Triangle.π₁_obj, comp_hom₂, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂, Triangle.add_hom₂, rotCompInvRot_inv_app_hom₁, CategoryTheory.Triangulated.TStructure.triangleLEGT_distinguished, Triangle.zero_hom₃, Triangle.add_hom₃, TriangleOpEquivalence.inverse_obj, distinguished_iff_of_iso, CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_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₁, CategoryTheory.Functor.rotate_essImageDistTriang, CategoryTheory.Triangulated.TStructure.isIso_truncLE_map_iff, triangleCategory_comp, inv_rot_of_distTriang, CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₂, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, Triangle.functorIsoMk_hom, HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, Triangle.shiftFunctor_map_hom₃, rotate_map_hom₁, Triangle.shiftFunctorAdd'_eq, CategoryTheory.Triangulated.TStructure.triangle_map_exists, Triangle.π₂_obj, Triangle.π₃_obj, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₃, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁, Triangle.add_hom₁, CategoryTheory.Functor.essImageDistTriang_mem_of_iso, CategoryTheory.ObjectProperty.HasInducedTStructure.exists_triangle_zero_one, Triangle.shiftFunctorAdd'_hom_app_hom₁, DerivedCategory.triangleOfSES_distinguished, CategoryTheory.Functor.instFaithfulTriangleMapTriangle, isoTriangleOfIso₁₂_inv_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₂, productTriangle_distinguished, Triangle.smul_hom₃, CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂, Triangle.sub_hom₃, Opposite.contractibleTriangleIso_inv_hom₂, CategoryTheory.Triangulated.Localization.distinguished_cocone_triangle, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_refl, invRotCompRot_hom_app_hom₃, Triangle.functorIsoMk_inv, isoTriangleOfIso₁₃_inv_hom₁, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₂, comp_hom₃, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle', 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₃, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle, exists_iso_of_arrow_iso, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂, comp_hom₁, rot_of_distTriang, CategoryTheory.Functor.contractible_mem_essImageDistTriang, Triangle.shiftFunctor_map_hom₂, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₃, shortComplexOfDistTriangleIsoOfIso_inv_τ₂, TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₂, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂, Triangle.shiftFunctorZero_inv_app_hom₂, CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₃, Triangle.shiftFunctorAdd'_hom_app_hom₂, contractible_distinguished, TriangleOpEquivalence.counitIso_hom_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle', HomotopyCategory.Pretriangulated.isomorphic_distinguished, shortComplexOfDistTriangleIsoOfIso_hom_τ₁, shortComplexOfDistTriangleIsoOfIso_hom_τ₂, invRotate_map_hom₃, Triangle.isoMk_hom, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, triangleRotation_inverse, CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₂, triangleRotation_functor, CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₂, CategoryTheory.Iso.inv_hom_id_triangle_hom₃, DerivedCategory.mem_distTriang_iff, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂, CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₂, DerivedCategory.mappingCocone_triangle_distinguished, CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₃, Triangle.shiftFunctorZero_hom_app_hom₂, contractible_distinguished₁, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₃, invRotCompRot_inv_app_hom₂, Opposite.rotate_distinguished_triangle, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₃, 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.Triangulated.TStructure.triangleLEGE_obj_mor₁, CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂, CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₂, CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished, HomotopyCategory.mappingConeCompTriangleh_distinguished, rotate_distinguished_triangle, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, CategoryTheory.Triangulated.SpectralObject.triangle_distinguished, CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₃, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₂, CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₁, binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_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, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₂, binaryBiproductTriangle_distinguished, 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, Opposite.isomorphic_distinguished, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_trans, Triangle.zero_hom₂, CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_iff, instIsEquivalenceTriangleInvRotate, CategoryTheory.ObjectProperty.trW_iff, instIsEquivalenceTriangleRotate, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃
triangleOpEquivalence 📖	CompOp	24 math math: Opposite.mem_distinguishedTriangles_iff, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, Opposite.mem_distinguishedTriangles_iff', CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, triangleOpEquivalence_unitIso, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, Opposite.contractibleTriangleIso_hom_hom₂, Opposite.contractibleTriangleIso_hom_hom₁, Opposite.contractibleTriangleIso_inv_hom₃, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, Opposite.contractibleTriangleIso_hom_hom₃, preadditiveYoneda_homologySequenceδ_apply, Opposite.contractibleTriangleIso_inv_hom₁, op_distinguished, mem_distTriang_op_iff, triangleOpEquivalence_counitIso, triangleOpEquivalence_functor, mem_distTriang_op_iff', CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, unop_distinguished, Opposite.contractibleTriangleIso_inv_hom₂, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, triangleOpEquivalence_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
triangleOpEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite Triangle CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt triangleCategory triangleOpEquivalence TriangleOpEquivalence.counitIso	—	—
triangleOpEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite Triangle CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt triangleCategory triangleOpEquivalence TriangleOpEquivalence.functor	—	—
triangleOpEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite Triangle CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt triangleCategory triangleOpEquivalence TriangleOpEquivalence.inverse	—	—
triangleOpEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite Triangle CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt triangleCategory triangleOpEquivalence TriangleOpEquivalence.unitIso	—	—

CategoryTheory.Pretriangulated.TriangleOpEquivalence

Definitions

Name	Category	Theorems
counitIso 📖	CompOp	7 math math: counitIso_hom_app_hom₁, counitIso_inv_app_hom₃, counitIso_inv_app_hom₂, CategoryTheory.Pretriangulated.triangleOpEquivalence_counitIso, counitIso_hom_app_hom₂, counitIso_hom_app_hom₃, counitIso_inv_app_hom₁
functor 📖	CompOp	13 math math: functor_map_hom₂, functor_map_hom₃, unitIso_hom_app, counitIso_hom_app_hom₁, counitIso_inv_app_hom₃, counitIso_inv_app_hom₂, CategoryTheory.Pretriangulated.triangleOpEquivalence_functor, unitIso_inv_app, functor_obj, counitIso_hom_app_hom₂, functor_map_hom₁, counitIso_hom_app_hom₃, counitIso_inv_app_hom₁
inverse 📖	CompOp	11 math math: unitIso_hom_app, counitIso_hom_app_hom₁, counitIso_inv_app_hom₃, counitIso_inv_app_hom₂, unitIso_inv_app, inverse_obj, counitIso_hom_app_hom₂, counitIso_hom_app_hom₃, inverse_map, counitIso_inv_app_hom₁, CategoryTheory.Pretriangulated.triangleOpEquivalence_inverse
unitIso 📖	CompOp	3 math math: CategoryTheory.Pretriangulated.triangleOpEquivalence_unitIso, unitIso_hom_app, unitIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counitIso_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
counitIso_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
counitIso_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
counitIso_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
counitIso_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
counitIso_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
functor_map_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Opposite.op CategoryTheory.Pretriangulated.Triangle.obj₃ Opposite.unop CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Pretriangulated.triangleCategory functor CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Quiver.Hom.unop	—	—
functor_map_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Opposite.op CategoryTheory.Pretriangulated.Triangle.obj₃ Opposite.unop CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Pretriangulated.triangleCategory functor Quiver.Hom.unop	—	—
functor_map_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Opposite.op CategoryTheory.Pretriangulated.Triangle.obj₃ Opposite.unop CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Pretriangulated.triangleCategory functor CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Quiver.Hom.unop	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Pretriangulated.Triangle CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt functor Opposite.op CategoryTheory.Pretriangulated.Triangle.obj₃ Opposite.unop CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃	—	—
inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Pretriangulated.triangleCategory inverse Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₁ Quiver.Hom.unop CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₁	—	—
inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Pretriangulated.triangleCategory inverse Opposite.op Opposite.unop CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₁ Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃	—	—
unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Pretriangulated.Triangle CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt functor inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ Opposite.unop CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.op Quiver.Hom.unop CategoryTheory.Functor.op CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Equivalence.counitIso CategoryTheory.Pretriangulated.Triangle.homMk CategoryTheory.CategoryStruct.id	—	—
unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Pretriangulated.Triangle CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt functor inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.op Quiver.Hom.unop CategoryTheory.Functor.op CategoryTheory.Equivalence.unitIso CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Equivalence.counitIso CategoryTheory.Pretriangulated.Triangle.homMk CategoryTheory.CategoryStruct.id CategoryTheory.Iso.refl	—	—

---

← Back to Index