Documentation Verification Report

Triangulated

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

Statistics

Metric	Count
Definitions `essImageDistTriang`, `IsCompatibleWithTriangulation`, `instPretriangulatedLocalization`, `instPretriangulatedLocalization'`, `pretriangulated`	5
Theorems `complete_distinguished_essImageDistTriang_morphism`, `contractible_mem_essImageDistTriang`, `distTriang_iff`, `essImageDistTriang_mem_of_iso`, `rotate_essImageDistTriang`, `compatible_with_triangulation`, `toIsCompatibleWithShift`, `complete_distinguished_triangle_morphism`, `distinguished_cocone_triangle`, `instAdditiveLocalization'ShiftFunctorInt`, `instAdditiveLocalizationShiftFunctorInt`, `instIsTriangulatedLocalization`, `instIsTriangulatedLocalization'`, `isTriangulated`, `isTriangulated_functor`	15
Total	20

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`essImageDistTriang` 📖	CompOp	4 math math: `distTriang_iff`, `rotate_essImageDistTriang`, `CategoryTheory.Triangulated.Localization.distinguished_cocone_triangle`, `contractible_mem_essImageDistTriang`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complete_distinguished_essImageDistTriang_morphism` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.TriangleMorphism.hom₁` `obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `mapTriangle` `CategoryTheory.Pretriangulated.TriangleMorphism.hom₂` `Set` `Set.instMembership` `essImageDistTriang` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁`	`CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Pretriangulated.Triangle.mor₃` `map`	—	`CategoryTheory.Pretriangulated.TriangleMorphism.comm₁` `CategoryTheory.Pretriangulated.TriangleMorphism.comm₂` `CategoryTheory.Pretriangulated.TriangleMorphism.comm₃` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc` `CategoryTheory.Iso.hom_inv_id_triangle_hom₃` `CategoryTheory.Category.comp_id` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₃` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc` `CategoryTheory.cancel_mono` `map_mono` `preservesMonomorphisms_of_isRightAdjoint` `isRightAdjoint_of_isEquivalence` `CategoryTheory.instIsEquivalenceShiftFunctor` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₁` `CategoryTheory.Iso.isIso_hom` `map_comp`
`contractible_mem_essImageDistTriang` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `essImageDistTriang` `CategoryTheory.Pretriangulated.contractibleTriangle`	—	`CategoryTheory.Category.comp_id` `map_id` `CategoryTheory.Limits.comp_zero` `map_zero` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Pretriangulated.contractible_distinguished`
`distTriang_iff` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `essImageDistTriang`	—	`CategoryTheory.Pretriangulated.distinguished_cocone_triangle` `CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso` `map_distinguished` `CategoryTheory.Pretriangulated.isomorphic_distinguished`
`essImageDistTriang_mem_of_iso` 📖	—	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `essImageDistTriang`	—	—	—
`rotate_essImageDistTriang` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `essImageDistTriang` `CategoryTheory.Pretriangulated.Triangle.rotate`	—	`CategoryTheory.Pretriangulated.rot_of_distTriang` `CategoryTheory.Pretriangulated.inv_rot_of_distTriang`

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsCompatibleWithTriangulation` 📖	CompData	1 math math: `CategoryTheory.ObjectProperty.instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated`

CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatible_with_triangulation` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Pretriangulated.Triangle.mor₁`	`CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle.mor₃` `CategoryTheory.Functor.map`	—	—
`toIsCompatibleWithShift` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.MorphismProperty.IsCompatibleWithShift`	—	—

CategoryTheory.Triangulated.Localization

Definitions

Name	Category	Theorems
`instPretriangulatedLocalization` 📖	CompOp	1 math math: `instIsTriangulatedLocalization`
`instPretriangulatedLocalization'` 📖	CompOp	1 math math: `instIsTriangulatedLocalization'`
`pretriangulated` 📖	CompOp	1 math math: `isTriangulated_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complete_distinguished_triangle_morphism` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Functor.essImageDistTriang` `CategoryTheory.CategoryStruct.comp` `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.Functor.complete_distinguished_essImageDistTriang_morphism` `CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction` `CategoryTheory.MorphismProperty.map_eq_iff_postcomp` `CategoryTheory.Functor.map_comp` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `CategoryTheory.Category.assoc` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc` `CategoryTheory.Pretriangulated.distinguished_cocone_triangle` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.compatible_with_triangulation` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Pretriangulated.Triangle.isIso_of_isIsos` `CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₁` `CategoryTheory.Pretriangulated.comp_hom₁` `CategoryTheory.IsIso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₂` `CategoryTheory.Pretriangulated.comp_hom₂`
`distinguished_cocone_triangle` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Functor.essImageDistTriang`	—	`CategoryTheory.Localization.essSurj_mapArrow` `CategoryTheory.Pretriangulated.distinguished_cocone_triangle` `CategoryTheory.CommaMorphism.w` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`
`instAdditiveLocalization'ShiftFunctorInt` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.MorphismProperty.Localization'` `CategoryTheory.MorphismProperty.instCategoryLocalization'` `CategoryTheory.Localization.instPreadditiveLocalization'` `CategoryTheory.HasShift.localization'` `CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift`	—	`CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift` `CategoryTheory.Localization.functor_additive_iff` `CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'` `CategoryTheory.Localization.instAdditiveLocalization'Q'` `CategoryTheory.Functor.additive_of_iso` `CategoryTheory.Functor.instAdditiveComp`
`instAdditiveLocalizationShiftFunctorInt` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Localization.instPreadditiveLocalization` `CategoryTheory.HasShift.localization` `CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift`	—	`CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift` `CategoryTheory.Localization.functor_additive_iff` `CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Localization.instAdditiveLocalizationQ` `CategoryTheory.Functor.additive_of_iso` `CategoryTheory.Functor.instAdditiveComp`
`instIsTriangulatedLocalization` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.IsTriangulated` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Localization.instPreadditiveLocalization` `CategoryTheory.Localization.instHasZeroObjectLocalization` `CategoryTheory.HasShift.localization` `CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift` `instAdditiveLocalizationShiftFunctorInt` `instPretriangulatedLocalization`	—	`isTriangulated` `CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift` `CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Localization.instHasZeroObjectLocalization` `instAdditiveLocalizationShiftFunctorInt` `isTriangulated_functor` `CategoryTheory.Localization.instAdditiveLocalizationQ`
`instIsTriangulatedLocalization'` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.IsTriangulated` `CategoryTheory.MorphismProperty.Localization'` `CategoryTheory.MorphismProperty.instCategoryLocalization'` `CategoryTheory.Localization.instPreadditiveLocalization'` `CategoryTheory.Localization.instHasZeroObjectLocalization'` `CategoryTheory.HasShift.localization'` `CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift` `instAdditiveLocalization'ShiftFunctorInt` `instPretriangulatedLocalization'`	—	`isTriangulated` `CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift` `CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'` `CategoryTheory.Localization.instHasZeroObjectLocalization'` `instAdditiveLocalization'ShiftFunctorInt` `isTriangulated_functor` `CategoryTheory.Localization.instAdditiveLocalization'Q'`
`isTriangulated` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.IsTriangulated`	—	`CategoryTheory.Localization.essSurj_mapComposableArrows` `CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two`
`isTriangulated_functor` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.IsTriangulated` `pretriangulated`	—	—

---

← Back to Index