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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
(h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
(h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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).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).map v₁₂)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
Instances For
instance
CategoryTheory.Triangulated.instNonemptyOctahedron
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(X : C)
:
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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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).obj X₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp w₁₃
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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).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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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)
:
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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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
- h.triangle = CategoryTheory.Pretriangulated.Triangle.mk h.m₁ h.m₃ (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂))
Instances For
@[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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangle.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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangle.mor₃ = CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)
@[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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangle.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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangle.mor₂ = h.m₃
@[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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangle.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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangle.obj₃ = Z₂₃
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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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
- h.triangleMorphism₁ = { hom₁ := CategoryTheory.CategoryStruct.id X₁, hom₂ := u₂₃, hom₃ := h.m₁, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangleMorphism₁.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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangleMorphism₁.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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangleMorphism₁.hom₁ = CategoryTheory.CategoryStruct.id X₁
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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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
- h.triangleMorphism₂ = { hom₁ := u₁₂, hom₂ := CategoryTheory.CategoryStruct.id X₃, hom₃ := h.m₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangleMorphism₂.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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangleMorphism₂.hom₂ = CategoryTheory.CategoryStruct.id X₃
@[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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
{h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
(h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
:
h.triangleMorphism₂.hom₃ = h.m₃
def
CategoryTheory.Triangulated.Octahedron.ofIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
(h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
(h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
(h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C}
(u₁₂' : X₁' ⟶ X₂')
(u₂₃' : X₂' ⟶ X₃')
(u₁₃' : X₁' ⟶ X₃')
(comm' : CategoryTheory.CategoryStruct.comp u₁₂' u₂₃' = u₁₃')
(e₁ : X₁ ≅ X₁')
(e₂ : X₂ ≅ X₂')
(e₃ : X₃ ≅ X₃')
(comm₁₂ : CategoryTheory.CategoryStruct.comp u₁₂ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom u₁₂')
(comm₂₃ : CategoryTheory.CategoryStruct.comp u₂₃ e₃.hom = CategoryTheory.CategoryStruct.comp e₂.hom u₂₃')
(v₁₂' : X₂' ⟶ Z₁₂')
(w₁₂' : Z₁₂' ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁')
(h₁₂' :
CategoryTheory.Pretriangulated.Triangle.mk u₁₂' v₁₂' w₁₂' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(v₂₃' : X₃' ⟶ Z₂₃')
(w₂₃' : Z₂₃' ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂')
(h₂₃' :
CategoryTheory.Pretriangulated.Triangle.mk u₂₃' v₂₃' w₂₃' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(v₁₃' : X₃' ⟶ Z₁₃')
(w₁₃' : Z₁₃' ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁')
(h₁₃' :
CategoryTheory.Pretriangulated.Triangle.mk u₁₃' v₁₃' w₁₃' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(H : CategoryTheory.Triangulated.Octahedron comm' h₁₂' h₂₃' h₁₃')
:
CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃
When two diagrams are isomorphic, an octahedron for one gives an octahedron for the other.
Equations
- One or more equations did not get rendered due to their size.
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.shiftFunctor C n).Additive]
[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).obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
{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).obj X₁}
{h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
{h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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 = ⋯.some
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.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.IsTriangulated C]
{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).obj X₁}
(h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
(h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).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
Instances For
theorem
CategoryTheory.IsTriangulated.mk'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasShift C ℤ]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
(h :
∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃'),
∃ (X₁ : C) (X₂ : C) (X₃ : C) (Z₁₂ : C) (Z₂₃ : C) (Z₁₃ : C) (u₁₂ : X₁ ⟶ X₂) (u₂₃ : X₂ ⟶ X₃) (e₁ : X₁' ≅ X₁) (e₂ :
X₂' ≅ X₂) (e₃ : X₃' ≅ X₃) (_ :
CategoryTheory.CategoryStruct.comp u₁₂' e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom u₁₂) (_ :
CategoryTheory.CategoryStruct.comp u₂₃' e₃.hom = CategoryTheory.CategoryStruct.comp e₂.hom u₂₃) (v₁₂ : X₂ ⟶ Z₁₂)
(w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁) (h₁₂ :
CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(v₂₃ : X₃ ⟶ Z₂₃) (w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂) (h₂₃ :
CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(v₁₃ : X₃ ⟶ Z₁₃) (w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁) (h₁₃ :
CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.comp u₁₂ u₂₃) v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
Nonempty (CategoryTheory.Triangulated.Octahedron ⋯ h₁₂ h₂₃ h₁₃))
:
Constructor for IsTriangulated C which shows that it suffices to obtain an octahedron
for a suitable isomorphic diagram instead of the given diagram.