Functor

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

Statistics

Metric	Count
Definitions IsTriangulated, instCommShiftTriangleMapTriangleInt, mapTriangle, mapTriangleCommShiftIso, mapTriangleCompIso, mapTriangleIdIso, mapTriangleInvRotateIso, mapTriangleIso, mapTriangleRotateIso, map	10
Theorems instAdditive, instComp, instId, instPreservesLimitsOfShapeDiscreteWalkingPair, instPreservesZeroMorphisms, map_distinguished, instFaithfulTriangleMapTriangle, instFullTriangleMapTriangleOfFaithful, isTriangulated_iff_comp_right, isTriangulated_iff_of_iso, isTriangulated_of_iso, isTriangulated_of_precomp, isTriangulated_of_precomp_iso, mapTriangleCommShiftIso_hom_app_hom₁, mapTriangleCommShiftIso_hom_app_hom₂, mapTriangleCommShiftIso_hom_app_hom₃, mapTriangleCommShiftIso_inv_app_hom₁, mapTriangleCommShiftIso_inv_app_hom₂, mapTriangleCommShiftIso_inv_app_hom₃, mapTriangleCompIso_hom_app_hom₁, mapTriangleCompIso_hom_app_hom₂, mapTriangleCompIso_hom_app_hom₃, mapTriangleCompIso_inv_app_hom₁, mapTriangleCompIso_inv_app_hom₂, mapTriangleCompIso_inv_app_hom₃, mapTriangleIdIso_hom_app_hom₁, mapTriangleIdIso_hom_app_hom₂, mapTriangleIdIso_hom_app_hom₃, mapTriangleIdIso_inv_app_hom₁, mapTriangleIdIso_inv_app_hom₂, mapTriangleIdIso_inv_app_hom₃, mapTriangleInvRotateIso_hom_app_hom₁, mapTriangleInvRotateIso_hom_app_hom₂, mapTriangleInvRotateIso_hom_app_hom₃, mapTriangleInvRotateIso_inv_app_hom₁, mapTriangleInvRotateIso_inv_app_hom₂, mapTriangleInvRotateIso_inv_app_hom₃, mapTriangleIso_hom_app_hom₁, mapTriangleIso_hom_app_hom₂, mapTriangleIso_hom_app_hom₃, mapTriangleIso_inv_app_hom₁, mapTriangleIso_inv_app_hom₂, mapTriangleIso_inv_app_hom₃, mapTriangleRotateIso_hom_app_hom₁, mapTriangleRotateIso_hom_app_hom₂, mapTriangleRotateIso_hom_app_hom₃, mapTriangleRotateIso_inv_app_hom₁, mapTriangleRotateIso_inv_app_hom₂, mapTriangleRotateIso_inv_app_hom₃, mapTriangle_map_hom₁, mapTriangle_map_hom₂, mapTriangle_map_hom₃, mapTriangle_obj, map_distinguished, map_distinguished_iff, mem_mapTriangle_essImage_of_distinguished, of_fully_faithful_triangulated_functor, map_m₁, map_m₃, isTriangulated_of_essSurj_mapComposableArrows_two	60
Total	70

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTriangulated_of_essSurj_mapComposableArrows_two 📖	mathematical	Functor.Additive shiftFunctor Int.instAddMonoid	IsTriangulated	—	ComposableArrows.mk₂_surjective Pretriangulated.distinguished_cocone_triangle le_rfl ComposableArrows.naturality' Functor.map_distinguished

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsTriangulated 📖	CompData	26 math math: CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctor, isTriangulated_of_precomp_iso, CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOp, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, CategoryTheory.Triangulated.Localization.isTriangulated_functor, isTriangulated_of_op, instIsTriangulatedDerivedCategoryMapDerivedCategory, isTriangulated_iff_comp_right, isTriangulated_of_precomp, isTriangulated_iff_of_iso, CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryι, CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctorSymmOfInverse, CategoryTheory.Pretriangulated.Opposite.functor_isTriangulated_op, HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory, IsTriangulated.instId, CategoryTheory.Adjunction.IsTriangulated.leftAdjoint_isTriangulated, CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverseSymmOfFunctor, op_isTriangulated_iff, isTriangulated_of_iso, CategoryTheory.Adjunction.isTriangulated_rightAdjoint, CategoryTheory.Adjunction.IsTriangulated.rightAdjoint_isTriangulated, CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop, CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverse, CategoryTheory.Adjunction.isTriangulated_leftAdjoint, CategoryTheory.ObjectProperty.isTriangulated_lift, IsTriangulated.instComp
instCommShiftTriangleMapTriangleInt 📖	CompOp	—
mapTriangle 📖	CompOp	60 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, mapTriangleIdIso_inv_app_hom₃, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, mapTriangleIso_inv_app_hom₁, mapTriangleIso_inv_app_hom₃, mapTriangleRotateIso_inv_app_hom₂, mapTriangleCompIso_inv_app_hom₂, mapTriangle_obj, mapTriangleCommShiftIso_inv_app_hom₁, mapTriangleCompIso_hom_app_hom₂, mapTriangleRotateIso_inv_app_hom₁, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, DerivedCategory.mappingCone_triangle_distinguished, mapTriangleInvRotateIso_inv_app_hom₃, map_distinguished_iff, mapTriangleIso_hom_app_hom₁, mapTriangleInvRotateIso_hom_app_hom₃, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, mapTriangleIso_hom_app_hom₂, mapTriangleCompIso_inv_app_hom₃, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, mapTriangleCompIso_hom_app_hom₃, mapTriangle_map_hom₁, mapTriangleRotateIso_hom_app_hom₂, mapTriangleCommShiftIso_hom_app_hom₃, mapTriangleCommShiftIso_inv_app_hom₃, mapTriangleInvRotateIso_inv_app_hom₂, mapTriangleInvRotateIso_inv_app_hom₁, mapTriangleRotateIso_hom_app_hom₃, mapTriangleIdIso_hom_app_hom₃, mapTriangleRotateIso_hom_app_hom₁, mapTriangleIso_hom_app_hom₃, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, mapTriangleCompIso_inv_app_hom₁, IsTriangulated.map_distinguished, mapTriangle_map_hom₃, mapTriangleCommShiftIso_inv_app_hom₂, mapTriangleCompIso_hom_app_hom₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, mapTriangleCommShiftIso_hom_app_hom₁, instFaithfulTriangleMapTriangle, mapTriangleIso_inv_app_hom₂, mapTriangleIdIso_inv_app_hom₁, mapTriangleIdIso_inv_app_hom₂, mapTriangleRotateIso_inv_app_hom₃, mapTriangleCommShiftIso_hom_app_hom₂, instFullTriangleMapTriangleOfFaithful, mapTriangleInvRotateIso_hom_app_hom₁, DerivedCategory.mem_distTriang_iff, mapTriangleInvRotateIso_hom_app_hom₂, DerivedCategory.mappingCocone_triangle_distinguished, map_distinguished, mapTriangleIdIso_hom_app_hom₁, mapTriangleIdIso_hom_app_hom₂, mem_mapTriangle_essImage_of_distinguished, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, mapTriangle_map_hom₂
mapTriangleCommShiftIso 📖	CompOp	6 math math: mapTriangleCommShiftIso_inv_app_hom₁, mapTriangleCommShiftIso_hom_app_hom₃, mapTriangleCommShiftIso_inv_app_hom₃, mapTriangleCommShiftIso_inv_app_hom₂, mapTriangleCommShiftIso_hom_app_hom₁, mapTriangleCommShiftIso_hom_app_hom₂
mapTriangleCompIso 📖	CompOp	6 math math: mapTriangleCompIso_inv_app_hom₂, mapTriangleCompIso_hom_app_hom₂, mapTriangleCompIso_inv_app_hom₃, mapTriangleCompIso_hom_app_hom₃, mapTriangleCompIso_inv_app_hom₁, mapTriangleCompIso_hom_app_hom₁
mapTriangleIdIso 📖	CompOp	6 math math: mapTriangleIdIso_inv_app_hom₃, mapTriangleIdIso_hom_app_hom₃, mapTriangleIdIso_inv_app_hom₁, mapTriangleIdIso_inv_app_hom₂, mapTriangleIdIso_hom_app_hom₁, mapTriangleIdIso_hom_app_hom₂
mapTriangleInvRotateIso 📖	CompOp	6 math math: mapTriangleInvRotateIso_inv_app_hom₃, mapTriangleInvRotateIso_hom_app_hom₃, mapTriangleInvRotateIso_inv_app_hom₂, mapTriangleInvRotateIso_inv_app_hom₁, mapTriangleInvRotateIso_hom_app_hom₁, mapTriangleInvRotateIso_hom_app_hom₂
mapTriangleIso 📖	CompOp	6 math math: mapTriangleIso_inv_app_hom₁, mapTriangleIso_inv_app_hom₃, mapTriangleIso_hom_app_hom₁, mapTriangleIso_hom_app_hom₂, mapTriangleIso_hom_app_hom₃, mapTriangleIso_inv_app_hom₂
mapTriangleRotateIso 📖	CompOp	6 math math: mapTriangleRotateIso_inv_app_hom₂, mapTriangleRotateIso_inv_app_hom₁, mapTriangleRotateIso_hom_app_hom₂, mapTriangleRotateIso_hom_app_hom₃, mapTriangleRotateIso_hom_app_hom₁, mapTriangleRotateIso_inv_app_hom₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulTriangleMapTriangle 📖	mathematical	—	Faithful CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle	—	CategoryTheory.Pretriangulated.Triangle.hom_ext map_injective
instFullTriangleMapTriangleOfFaithful 📖	mathematical	—	Full CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle	—	map_injective map_comp map_preimage CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Category.assoc commShiftIso_hom_naturality CategoryTheory.Pretriangulated.TriangleMorphism.comm₃ CategoryTheory.Pretriangulated.Triangle.hom_ext
isTriangulated_iff_comp_right 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated	—	isTriangulated_iff_of_iso IsTriangulated.instComp map_distinguished_iff CategoryTheory.Pretriangulated.isomorphic_distinguished map_distinguished
isTriangulated_iff_of_iso 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated	—	isTriangulated_of_iso
isTriangulated_of_iso 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated	—	CategoryTheory.Pretriangulated.isomorphic_distinguished map_distinguished
isTriangulated_of_precomp 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated	—	mem_mapTriangle_essImage_of_distinguished CategoryTheory.Pretriangulated.isomorphic_distinguished map_distinguished
isTriangulated_of_precomp_iso 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated	—	isTriangulated_iff_of_iso isTriangulated_of_precomp
mapTriangleCommShiftIso_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.Triangle.shiftFunctor mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleCommShiftIso CategoryTheory.shiftFunctor Int.instAddMonoid CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleCommShiftIso_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.Triangle.shiftFunctor mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleCommShiftIso CategoryTheory.shiftFunctor Int.instAddMonoid CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleCommShiftIso_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.Triangle.shiftFunctor mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleCommShiftIso CategoryTheory.shiftFunctor Int.instAddMonoid CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleCommShiftIso_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.Triangle.shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleCommShiftIso CategoryTheory.shiftFunctor Int.instAddMonoid CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleCommShiftIso_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.Triangle.shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleCommShiftIso CategoryTheory.shiftFunctor Int.instAddMonoid CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleCommShiftIso_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.Triangle.shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleCommShiftIso CategoryTheory.shiftFunctor Int.instAddMonoid CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleCompIso_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle comp CommShift.comp Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleCompIso_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle comp CommShift.comp Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleCompIso_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle comp CommShift.comp Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleCompIso_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CommShift.comp Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleCompIso_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CommShift.comp Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleCompIso_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CommShift.comp Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleIdIso_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle id CommShift.id Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleIdIso_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle id CommShift.id Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleIdIso_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle id CommShift.id Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleIdIso_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory id mapTriangle CommShift.id Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleIdIso_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory id mapTriangle CommShift.id Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleIdIso_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory id mapTriangle CommShift.id Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleInvRotateIso_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.invRotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleInvRotateIso CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Iso.inv CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleInvRotateIso_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.invRotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleInvRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleInvRotateIso_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.invRotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleInvRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleInvRotateIso_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.invRotate mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleInvRotateIso CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Iso.hom CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleInvRotateIso_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.invRotate mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleInvRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleInvRotateIso_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.invRotate mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleInvRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleIso_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleIso CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleIso_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleIso CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleIso_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleIso CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleIso_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleIso CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleIso_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleIso CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleIso_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleIso CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleRotateIso_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.rotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleRotateIso_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.rotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleRotateIso_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp mapTriangle CategoryTheory.Pretriangulated.rotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapTriangleRotateIso CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Iso.inv CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleRotateIso_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.rotate mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleRotateIso_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.rotate mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleRotateIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleRotateIso_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory comp CategoryTheory.Pretriangulated.rotate mapTriangle CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapTriangleRotateIso CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Iso.hom CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangle_map_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ obj CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ map CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle	—	—
mapTriangle_map_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ obj CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ map CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle	—	—
mapTriangle_map_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ obj CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ map CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle	—	—
mapTriangle_obj 📖	mathematical	—	obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ map CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category CommShift.commShiftIso	—	—
map_distinguished 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles obj CategoryTheory.Pretriangulated.triangleCategory mapTriangle	—	IsTriangulated.map_distinguished
map_distinguished_iff 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles obj CategoryTheory.Pretriangulated.triangleCategory mapTriangle	—	CategoryTheory.Pretriangulated.distinguished_cocone_triangle CategoryTheory.Pretriangulated.isomorphic_distinguished instFullTriangleMapTriangleOfFaithful instFaithfulTriangleMapTriangle map_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mem_mapTriangle_essImage_of_distinguished 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Iso CategoryTheory.Pretriangulated.triangleCategory obj mapTriangle	—	CategoryTheory.CommaMorphism.w CategoryTheory.Pretriangulated.distinguished_cocone_triangle map_distinguished

CategoryTheory.Functor.IsTriangulated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditive 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.Additive	—	CategoryTheory.Functor.additive_of_preserves_binary_products CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Pretriangulated.instHasFiniteProducts Finite.of_fintype instPreservesLimitsOfShapeDiscreteWalkingPair instPreservesZeroMorphisms
instComp 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated CategoryTheory.Functor.comp CategoryTheory.Functor.CommShift.comp Int.instAddMonoid	—	CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Functor.map_distinguished
instId 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated CategoryTheory.Functor.id CategoryTheory.Functor.CommShift.id Int.instAddMonoid	—	CategoryTheory.Pretriangulated.isomorphic_distinguished
instPreservesLimitsOfShapeDiscreteWalkingPair 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory	—	CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Pretriangulated.instHasBinaryBiproducts CategoryTheory.Limits.prod.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.prodComparison_fst CategoryTheory.Functor.map_comp CategoryTheory.Limits.limit.lift_π CategoryTheory.Functor.map_id CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero CategoryTheory.Limits.prodComparison_snd CategoryTheory.Functor.map_zero instPreservesZeroMorphisms CategoryTheory.Limits.zero_comp CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃ CategoryTheory.Functor.map_distinguished CategoryTheory.Pretriangulated.binaryProductTriangle_distinguished CategoryTheory.IsIso.id CategoryTheory.Limits.PreservesLimitPair.of_iso_prod_comparison CategoryTheory.Limits.preservesLimit_of_iso_diagram
instPreservesZeroMorphisms 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Limits.id_zero CategoryTheory.Limits.comp_zero CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isIso₁ CategoryTheory.Functor.map_distinguished CategoryTheory.Pretriangulated.contractible_distinguished CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.id CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Limits.zero_comp
map_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.mapTriangle	—	—

CategoryTheory.IsTriangulated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_fully_faithful_triangulated_functor 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsTriangulated	—	CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_distinguished CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_preimage CategoryTheory.Triangulated.Octahedron.comm₁ CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Category.assoc CategoryTheory.Triangulated.Octahedron.comm₂ CategoryTheory.Triangulated.Octahedron.comm₃ CategoryTheory.Functor.commShiftIso_hom_naturality CategoryTheory.Triangulated.Octahedron.comm₄ CategoryTheory.Functor.map_distinguished_iff CategoryTheory.Triangulated.Octahedron.mem

CategoryTheory.Triangulated.Octahedron

Definitions

Name	Category	Theorems
map 📖	CompOp	2 math math: map_m₃, map_m₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_m₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	m₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Functor.map_distinguished map	—	CategoryTheory.Functor.map_distinguished
map_m₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	m₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Functor.map_distinguished map	—	CategoryTheory.Functor.map_distinguished

---

← Back to Index