Triangulated Categories #
This file contains the definition of triangulated categories, which are pretriangulated categories which satisfy the octahedron axiom.
structure
CategoryTheory.Triangulated.Octahedron
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
(h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
(h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
(h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
:
Type u_2
An octahedron is a type of datum whose existence is asserted by the octahedron axiom (TR 4), see https://stacks.math.columbia.edu/tag/05QK
- m₁ : Z₁₂ ⟶ Z₁₃
- m₃ : Z₁₃ ⟶ Z₂₃
- comm₁ : CategoryTheory.CategoryStruct.comp v₁₂ self.m₁ = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃
- comm₂ : CategoryTheory.CategoryStruct.comp self.m₁ w₁₃ = w₁₂
- comm₃ : CategoryTheory.CategoryStruct.comp v₁₃ self.m₃ = v₂₃
- comm₄ : CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).toPrefunctor.map u₁₂) = CategoryTheory.CategoryStruct.comp self.m₃ w₂₃
- mem : CategoryTheory.Pretriangulated.Triangle.mk self.m₁ self.m₃ (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).toPrefunctor.map v₁₂)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
Instances For
instance
CategoryTheory.Triangulated.instNonemptyOctahedronIntOfNatToOfNat0Zero'IdToCategoryStructComp_idOfNatHomToQuiverToOfNat0ZeroPreadditiveHasZeroMorphismsObjToPrefunctorShiftFunctorInstAddMonoidIntOfNatInstOfNatContractible_distinguished
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
(X : C)
:
Nonempty
(CategoryTheory.Triangulated.Octahedron
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X)
(_ : CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(_ : CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(_ : CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles))
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Triangulated.Octahedron.comm₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
{comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃}
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
{Z : C}
(h : (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁ ⟶ Z)
:
theorem
CategoryTheory.Triangulated.Octahedron.comm₄_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
{comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃}
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
{Z : C}
(h : (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp w₁₃
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).toPrefunctor.map u₁₂) h) = CategoryTheory.CategoryStruct.comp self.m₃ (CategoryTheory.CategoryStruct.comp w₂₃ h)
theorem
CategoryTheory.Triangulated.Octahedron.comm₁_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
{comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃}
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
{Z : C}
(h : Z₁₃ ⟶ Z)
:
theorem
CategoryTheory.Triangulated.Octahedron.comm₃_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
{comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃}
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
{Z : C}
(h : Z₂₃ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangle_mor₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangle comm h).mor₃ = CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).toPrefunctor.map v₁₂)
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangle_mor₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangle comm h).mor₁ = h.m₁
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangle_obj₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangle comm h).obj₂ = Z₁₃
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangle_mor₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangle comm h).mor₂ = h.m₃
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangle_obj₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangle comm h).obj₁ = Z₁₂
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangle_obj₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangle comm h).obj₃ = Z₂₃
def
CategoryTheory.Triangulated.Octahedron.triangle
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
The triangle Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ ⟶ Z₁₂⟦1⟧ given by an octahedron.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ comm h).hom₂ = u₂₃
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ comm h).hom₃ = h.m₁
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
def
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ⟶ CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃
The first morphism of triangles given by an octahedron.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangleMorphism₂ comm h).hom₁ = u₁₂
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
(CategoryTheory.Triangulated.Octahedron.triangleMorphism₂ comm h).hom₃ = h.m₃
def
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ⟶ CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃
The second morphism of triangles given an octahedron.
Equations
Instances For
class
CategoryTheory.IsTriangulated
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
:
A triangulated category is a pretriangulated category which satisfies the octahedron axiom (TR 4), see https://stacks.math.columbia.edu/tag/05QK
- octahedron_axiom : ∀ {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁} (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
the octahedron axiom (TR 4)
Instances
def
CategoryTheory.Triangulated.someOctahedron'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
[CategoryTheory.IsTriangulated C]
:
CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃
A choice of octahedron given by the octahedron axiom.
Equations
- CategoryTheory.Triangulated.someOctahedron' comm = Nonempty.some (_ : Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃))
Instances For
def
CategoryTheory.Triangulated.someOctahedron
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.IsTriangulated C]
{X₁ : C}
{X₂ : C}
{X₃ : C}
{Z₁₂ : C}
{Z₂₃ : C}
{Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
(comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
(h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₂}
(h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X₁}
(h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
:
CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃
A choice of octahedron given by the octahedron axiom.
Equations
- CategoryTheory.Triangulated.someOctahedron comm h₁₂ h₂₃ h₁₃ = CategoryTheory.Triangulated.someOctahedron' comm