Documentation Verification Report

Pretriangulated

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

Statistics

Metric	Count
Definitions `contractibleTriangleIso`, `distinguishedTriangles`, `instOpposite`, `rotateTriangleOpEquivalenceInverseObjRotateUnopIso`	4
Theorems `map_distinguished_op_exact`, `complete_distinguished_triangle_morphism`, `contractibleTriangleIso_hom_hom₁`, `contractibleTriangleIso_hom_hom₂`, `contractibleTriangleIso_hom_hom₃`, `contractibleTriangleIso_inv_hom₁`, `contractibleTriangleIso_inv_hom₂`, `contractibleTriangleIso_inv_hom₃`, `contractible_distinguished`, `distinguished_cocone_triangle`, `isomorphic_distinguished`, `mem_distinguishedTriangles_iff`, `mem_distinguishedTriangles_iff'`, `rotate_distinguished_triangle`, `mem_distTriang_op_iff`, `mem_distTriang_op_iff'`, `op_distinguished`, `unop_distinguished`	18
Total	22

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_distinguished_op_exact` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.ShortComplex.op` `CategoryTheory.Pretriangulated.shortComplexOfDistTriangle` `IsHomological.toPreservesZeroMorphisms` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.instPreadditiveOpposite` `CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt` `CategoryTheory.Pretriangulated.Opposite.instOpposite`	—	`CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt` `map_distinguished_exact` `CategoryTheory.Pretriangulated.op_distinguished`

CategoryTheory.Pretriangulated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_distTriang_op_iff` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`Triangle` `Opposite` `CategoryTheory.Category.opposite` `Opposite.instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.instPreadditiveOpposite` `Opposite.instAdditiveOppositeShiftFunctorInt` `Opposite.instOpposite` `Opposite.unop` `CategoryTheory.Functor.obj` `triangleCategory` `CategoryTheory.Equivalence.inverse` `triangleOpEquivalence`	—	`CategoryTheory.Limits.hasZeroObject_op` `Opposite.instAdditiveOppositeShiftFunctorInt`
`mem_distTriang_op_iff'` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`Triangle` `Opposite` `CategoryTheory.Category.opposite` `Opposite.instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.instPreadditiveOpposite` `Opposite.instAdditiveOppositeShiftFunctorInt` `Opposite.instOpposite` `CategoryTheory.Iso` `triangleCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.functor` `triangleOpEquivalence` `Opposite.op`	—	`Opposite.mem_distinguishedTriangles_iff'`
`op_distinguished` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `Triangle` `Set` `Set.instMembership` `distinguishedTriangles`	`Opposite` `CategoryTheory.Category.opposite` `Opposite.instHasShiftOppositeInt` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.instPreadditiveOpposite` `Opposite.instAdditiveOppositeShiftFunctorInt` `Opposite.instOpposite` `CategoryTheory.Functor.obj` `triangleCategory` `CategoryTheory.Equivalence.functor` `triangleOpEquivalence` `Opposite.op`	—	`CategoryTheory.Limits.hasZeroObject_op` `Opposite.instAdditiveOppositeShiftFunctorInt` `mem_distTriang_op_iff'`
`unop_distinguished` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `Triangle` `Opposite` `CategoryTheory.Category.opposite` `Opposite.instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.instPreadditiveOpposite` `Opposite.instAdditiveOppositeShiftFunctorInt` `Opposite.instOpposite`	`Opposite.unop` `CategoryTheory.Functor.obj` `triangleCategory` `CategoryTheory.Equivalence.inverse` `triangleOpEquivalence`	—	`CategoryTheory.Limits.hasZeroObject_op` `Opposite.instAdditiveOppositeShiftFunctorInt`

CategoryTheory.Pretriangulated.Opposite

Definitions

Name	Category	Theorems
`contractibleTriangleIso` 📖	CompOp	6 math math: `contractibleTriangleIso_hom_hom₂`, `contractibleTriangleIso_hom_hom₁`, `contractibleTriangleIso_inv_hom₃`, `contractibleTriangleIso_hom_hom₃`, `contractibleTriangleIso_inv_hom₁`, `contractibleTriangleIso_inv_hom₂`
`distinguishedTriangles` 📖	CompOp	5 math math: `mem_distinguishedTriangles_iff`, `mem_distinguishedTriangles_iff'`, `contractible_distinguished`, `distinguished_cocone_triangle`, `rotate_distinguished_triangle`
`instOpposite` 📖	CompOp	12 math math: `CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOpEquivalence`, `CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOp`, `CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda`, `CategoryTheory.Pretriangulated.op_distinguished`, `CategoryTheory.Pretriangulated.mem_distTriang_op_iff`, `CategoryTheory.Pretriangulated.mem_distTriang_op_iff'`, `functor_isTriangulated_op`, `CategoryTheory.Functor.op_isTriangulated_iff`, `instIsTriangulatedOpposite`, `CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished`, `CategoryTheory.Functor.map_distinguished_op_exact`, `CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop`
`rotateTriangleOpEquivalenceInverseObjRotateUnopIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complete_distinguished_triangle_morphism` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.opposite` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁`	`CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle.mor₃` `CategoryTheory.Functor.map`	—	`CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁` `mem_distinguishedTriangles_iff` `CategoryTheory.whisker_eq` `CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.IsEquivalence.faithful` `CategoryTheory.instIsEquivalenceShiftFunctor` `CategoryTheory.unop_comp` `CategoryTheory.Functor.map_comp` `Quiver.Hom.unop_op` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.unop_hom_inv_id_app_assoc` `CategoryTheory.unop_comp_assoc` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`contractibleTriangleIso_hom_hom₁` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₁` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `CategoryTheory.Pretriangulated.contractibleTriangle` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.triangleOpEquivalence` `Opposite.op` `CategoryTheory.Pretriangulated.Triangle.invRotate` `Opposite.unop` `CategoryTheory.Iso.hom` `contractibleTriangleIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Limits.hasZeroObject_op`
`contractibleTriangleIso_hom_hom₂` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₂` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `CategoryTheory.Pretriangulated.contractibleTriangle` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.triangleOpEquivalence` `Opposite.op` `CategoryTheory.Pretriangulated.Triangle.invRotate` `Opposite.unop` `CategoryTheory.Iso.hom` `contractibleTriangleIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Limits.hasZeroObject_op`
`contractibleTriangleIso_hom_hom₃` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₃` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `CategoryTheory.Pretriangulated.contractibleTriangle` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.triangleOpEquivalence` `Opposite.op` `CategoryTheory.Pretriangulated.Triangle.invRotate` `Opposite.unop` `CategoryTheory.Iso.hom` `contractibleTriangleIso` `CategoryTheory.Limits.HasZeroObject.zero'` `CategoryTheory.Limits.IsZero.iso`	—	`CategoryTheory.Limits.hasZeroObject_op`
`contractibleTriangleIso_inv_hom₁` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₁` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.triangleOpEquivalence` `Opposite.op` `CategoryTheory.Pretriangulated.Triangle.invRotate` `CategoryTheory.Pretriangulated.contractibleTriangle` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Opposite.unop` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Iso.inv` `contractibleTriangleIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Limits.hasZeroObject_op`
`contractibleTriangleIso_inv_hom₂` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₂` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.triangleOpEquivalence` `Opposite.op` `CategoryTheory.Pretriangulated.Triangle.invRotate` `CategoryTheory.Pretriangulated.contractibleTriangle` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Opposite.unop` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Iso.inv` `contractibleTriangleIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Limits.hasZeroObject_op`
`contractibleTriangleIso_inv_hom₃` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₃` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.triangleOpEquivalence` `Opposite.op` `CategoryTheory.Pretriangulated.Triangle.invRotate` `CategoryTheory.Pretriangulated.contractibleTriangle` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Opposite.unop` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Iso.inv` `contractibleTriangleIso` `CategoryTheory.Limits.HasZeroObject.zero'` `CategoryTheory.Limits.IsZero.iso`	—	`CategoryTheory.Limits.hasZeroObject_op`
`contractible_distinguished` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.Pretriangulated.contractibleTriangle` `CategoryTheory.Limits.hasZeroObject_op` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`CategoryTheory.Limits.hasZeroObject_op` `mem_distinguishedTriangles_iff'` `CategoryTheory.Pretriangulated.inv_rot_of_distTriang` `CategoryTheory.Pretriangulated.contractible_distinguished`
`distinguished_cocone_triangle` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles`	—	`CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁` `CategoryTheory.Pretriangulated.isomorphic_distinguished` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.assoc` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality` `CategoryTheory.Iso.hom_inv_id_app_assoc`
`isomorphic_distinguished` 📖	—	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles`	—	—	`CategoryTheory.Pretriangulated.isomorphic_distinguished`
`mem_distinguishedTriangles_iff` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.Pretriangulated.distinguishedTriangles` `Opposite.unop` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Pretriangulated.triangleOpEquivalence`	—	—
`mem_distinguishedTriangles_iff'` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.Iso` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.triangleOpEquivalence` `Opposite.op`	—	`mem_distinguishedTriangles_iff` `CategoryTheory.Pretriangulated.isomorphic_distinguished`
`rotate_distinguished_triangle` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Opposite` `CategoryTheory.Category.opposite` `instHasShiftOppositeInt` `Set` `Set.instMembership` `distinguishedTriangles` `CategoryTheory.Pretriangulated.Triangle.rotate` `CategoryTheory.instPreadditiveOpposite`	—	`CategoryTheory.Pretriangulated.rotate_distinguished_triangle` `CategoryTheory.Pretriangulated.distinguished_iff_of_iso`

---

← Back to Index