Triangulated

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

Statistics

Metric	Count
Definitions IsTriangulated, Octahedron, m₁, m₃, ofIso, triangle, triangleMorphism₁, triangleMorphism₂, someOctahedron, someOctahedron'	10
Theorems mk', octahedron_axiom, comm₁, comm₁_assoc, comm₂, comm₂_assoc, comm₃, comm₃_assoc, comm₄, comm₄_assoc, mem, triangleMorphism₁_hom₁, triangleMorphism₁_hom₂, triangleMorphism₁_hom₃, triangleMorphism₂_hom₁, triangleMorphism₂_hom₂, triangleMorphism₂_hom₃, triangle_mor₁, triangle_mor₂, triangle_mor₃, triangle_obj₁, triangle_obj₂, triangle_obj₃, instNonemptyOctahedron	24
Total	34

CategoryTheory

Definitions

Name	Category	Theorems
IsTriangulated 📖	CompData	10 math math: IsTriangulated.of_fully_faithful_triangulated_functor, DerivedCategory.instIsTriangulated, Triangulated.Localization.isTriangulated, HomotopyCategory.instIsTriangulatedIntUp, Triangulated.Localization.instIsTriangulatedLocalization, IsTriangulated.mk', Triangulated.Localization.instIsTriangulatedLocalization', ObjectProperty.instIsTriangulatedFullSubcategory, Pretriangulated.Opposite.instIsTriangulatedOpposite, isTriangulated_of_essSurj_mapComposableArrows_two

CategoryTheory.IsTriangulated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Triangulated.Octahedron CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.IsTriangulated	—	—
octahedron_axiom 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Triangulated.Octahedron	—	—

CategoryTheory.Triangulated

Definitions

Name	Category	Theorems
Octahedron 📖	CompData	2 math math: instNonemptyOctahedron, CategoryTheory.IsTriangulated.octahedron_axiom
someOctahedron 📖	CompOp	—
someOctahedron' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonemptyOctahedron 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Octahedron CategoryTheory.Limits.HasZeroObject.zero' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.comp_id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.contractible_distinguished	—	CategoryTheory.Category.comp_id CategoryTheory.Pretriangulated.contractible_distinguished Unique.instSubsingleton CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Limits.id_zero CategoryTheory.Limits.comp_zero CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive

CategoryTheory.Triangulated.Octahedron

Definitions

Name	Category	Theorems
m₁ 📖	CompOp	8 math math: mem, triangle_mor₁, comm₁, map_m₁, triangleMorphism₁_hom₃, comm₂, comm₁_assoc, comm₂_assoc
m₃ 📖	CompOp	8 math math: mem, comm₃_assoc, comm₄_assoc, map_m₃, triangleMorphism₂_hom₃, triangle_mor₂, comm₃, comm₄
ofIso 📖	CompOp	—
triangle 📖	CompOp	6 math math: triangle_mor₁, triangle_mor₃, triangle_mor₂, triangle_obj₁, triangle_obj₂, triangle_obj₃
triangleMorphism₁ 📖	CompOp	3 math math: triangleMorphism₁_hom₁, triangleMorphism₁_hom₃, triangleMorphism₁_hom₂
triangleMorphism₂ 📖	CompOp	3 math math: triangleMorphism₂_hom₃, triangleMorphism₂_hom₁, triangleMorphism₂_hom₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	m₁	—	—
comm₁_assoc 📖	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.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₁
comm₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Functor.obj m₁	—	—
comm₂_assoc 📖	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.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₂
comm₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	m₃	—	—
comm₃_assoc 📖	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.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₃
comm₄ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Functor.obj CategoryTheory.Functor.map m₃	—	—
comm₄_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Functor.obj CategoryTheory.Functor.map m₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₄
mem 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	m₁ m₃ CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
triangleMorphism₁_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ triangleMorphism₁ CategoryTheory.CategoryStruct.id	—	—
triangleMorphism₁_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ triangleMorphism₁	—	—
triangleMorphism₁_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ triangleMorphism₁ m₁	—	—
triangleMorphism₂_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ triangleMorphism₂	—	—
triangleMorphism₂_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ triangleMorphism₂ CategoryTheory.CategoryStruct.id	—	—
triangleMorphism₂_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ triangleMorphism₂ m₃	—	—
triangle_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.mor₁ triangle m₁	—	—
triangle_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.mor₂ triangle m₃	—	—
triangle_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.mor₃ triangle CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
triangle_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.obj₁ triangle	—	—
triangle_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.obj₂ triangle	—	—
triangle_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.obj₃ triangle	—	—

---

← Back to Index