mathlib3 documentation

category_theory.triangulated.basic

Triangles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the definition of triangles in an additive category with an additive shift. It also defines morphisms between these triangles.

TODO: generalise this to n-angles in n-angulated categories as in https://arxiv.org/abs/1006.4592

source
structure category_theory.pretriangulated.triangle (C : Type u) [category_theory.category C] [category_theory.has_shift C ℤ] :
Type (max u v)

A triangle in C is a sextuple (X,Y,Z,f,g,h) where X,Y,Z are objects of C, and f : X ⟶ Y, g : Y ⟶ Z, h : Z ⟶ X⟦1⟧ are morphisms in C. See https://stacks.math.columbia.edu/tag/0144.

Instances for category_theory.pretriangulated.triangle
source
@[simp]
theorem category_theory.pretriangulated.triangle.mk_mor₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X) :
(category_theory.pretriangulated.triangle.mk f g h).mor₂ = g
source
@[simp]
theorem category_theory.pretriangulated.triangle.mk_mor₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X) :
(category_theory.pretriangulated.triangle.mk f g h).mor₁ = f
source
@[simp]
theorem category_theory.pretriangulated.triangle.mk_obj₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X) :
(category_theory.pretriangulated.triangle.mk f g h).obj₂ = Y
source
@[simp]
theorem category_theory.pretriangulated.triangle.mk_obj₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X) :
(category_theory.pretriangulated.triangle.mk f g h).obj₁ = X
source
def category_theory.pretriangulated.triangle.mk {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X) :
category_theory.pretriangulated.triangle C

A triangle (X,Y,Z,f,g,h) in C is defined by the morphisms f : X ⟶ Y, g : Y ⟶ Z and h : Z ⟶ X⟦1⟧.

Equations
source
@[simp]
theorem category_theory.pretriangulated.triangle.mk_mor₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X) :
(category_theory.pretriangulated.triangle.mk f g h).mor₃ = h
source
@[simp]
theorem category_theory.pretriangulated.triangle.mk_obj₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X) :
(category_theory.pretriangulated.triangle.mk f g h).obj₃ = Z
source
@[protected, instance]
noncomputable def category_theory.pretriangulated.triangle.inhabited {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] :
inhabited (category_theory.pretriangulated.triangle C)
Equations
source
noncomputable def category_theory.pretriangulated.contractible_triangle {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.pretriangulated.triangle C

For each object in C, there is a triangle of the form (X,X,0,𝟙 X,0,0)

Equations
source
@[simp]
theorem category_theory.pretriangulated.contractible_triangle_obj₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.pretriangulated.contractible_triangle X).obj₁ = X
source
@[simp]
theorem category_theory.pretriangulated.contractible_triangle_obj₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.pretriangulated.contractible_triangle X).obj₃ = 0
source
@[simp]
theorem category_theory.pretriangulated.contractible_triangle_obj₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.pretriangulated.contractible_triangle X).obj₂ = X
source
@[simp]
theorem category_theory.pretriangulated.contractible_triangle_mor₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.pretriangulated.contractible_triangle X).mor₃ = 0
source
@[simp]
theorem category_theory.pretriangulated.contractible_triangle_mor₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.pretriangulated.contractible_triangle X).mor₂ = 0
source
@[simp]
theorem category_theory.pretriangulated.contractible_triangle_mor₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.pretriangulated.contractible_triangle X).mor₁ = 𝟙 X
source
@[ext]
structure category_theory.pretriangulated.triangle_morphism {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (T₁ T₂ : category_theory.pretriangulated.triangle C) :
Type v

A morphism of triangles (X,Y,Z,f,g,h) ⟶ (X',Y',Z',f',g',h') in C is a triple of morphisms a : X ⟶ X', b : Y ⟶ Y', c : Z ⟶ Z' such that a ≫ f' = f ≫ b, b ≫ g' = g ≫ c, and a⟦1⟧' ≫ h = h' ≫ c. In other words, we have a commutative diagram:

     f      g      h
  X  ───> Y  ───> Z  ───> X⟦1⟧
  │       │       │        │
  │a      │b      │c       │a⟦1⟧'
  V       V       V        V
  X' ───> Y' ───> Z' ───> X'⟦1⟧
     f'     g'     h'

See https://stacks.math.columbia.edu/tag/0144.

Instances for category_theory.pretriangulated.triangle_morphism
source
theorem category_theory.pretriangulated.triangle_morphism.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.has_shift C ℤ} {T₁ T₂ : category_theory.pretriangulated.triangle C} (x y : category_theory.pretriangulated.triangle_morphism T₁ T₂) :
x = y ↔ x.hom₁ = y.hom₁ ∧ x.hom₂ = y.hom₂ ∧ x.hom₃ = y.hom₃
source
theorem category_theory.pretriangulated.triangle_morphism.ext {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.has_shift C ℤ} {T₁ T₂ : category_theory.pretriangulated.triangle C} (x y : category_theory.pretriangulated.triangle_morphism T₁ T₂) (h : x.hom₁ = y.hom₁) (h_1 : x.hom₂ = y.hom₂) (h_2 : x.hom₃ = y.hom₃) :
x = y
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comm₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.pretriangulated.triangle C} (self : category_theory.pretriangulated.triangle_morphism T₁ T₂) :
T₁.mor₁ ≫ self.hom₂ = self.hom₁ ≫ T₂.mor₁
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comm₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.pretriangulated.triangle C} (self : category_theory.pretriangulated.triangle_morphism T₁ T₂) :
T₁.mor₂ ≫ self.hom₃ = self.hom₂ ≫ T₂.mor₂
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comm₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.pretriangulated.triangle C} (self : category_theory.pretriangulated.triangle_morphism T₁ T₂) :
T₁.mor₃ ≫ (category_theory.shift_functor C 1).map self.hom₁ = self.hom₃ ≫ T₂.mor₃
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comm₃_assoc {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.pretriangulated.triangle C} (self : category_theory.pretriangulated.triangle_morphism T₁ T₂) {X' : C} (f' : (category_theory.shift_functor C 1).obj T₂.obj₁ ⟶ X') :
T₁.mor₃ ≫ (category_theory.shift_functor C 1).map self.hom₁ ≫ f' = self.hom₃ ≫ T₂.mor₃ ≫ f'
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comm₂_assoc {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.pretriangulated.triangle C} (self : category_theory.pretriangulated.triangle_morphism T₁ T₂) {X' : C} (f' : T₂.obj₃ ⟶ X') :
T₁.mor₂ ≫ self.hom₃ ≫ f' = self.hom₂ ≫ T₂.mor₂ ≫ f'
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comm₁_assoc {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ : category_theory.pretriangulated.triangle C} (self : category_theory.pretriangulated.triangle_morphism T₁ T₂) {X' : C} (f' : T₂.obj₂ ⟶ X') :
T₁.mor₁ ≫ self.hom₂ ≫ f' = self.hom₁ ≫ T₂.mor₁ ≫ f'
source
def category_theory.pretriangulated.triangle_morphism_id {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (T : category_theory.pretriangulated.triangle C) :
category_theory.pretriangulated.triangle_morphism T T

The identity triangle morphism.

Equations
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism_id_hom₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (T : category_theory.pretriangulated.triangle C) :
(category_theory.pretriangulated.triangle_morphism_id T).hom₃ = 𝟙 T.obj₃
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism_id_hom₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (T : category_theory.pretriangulated.triangle C) :
(category_theory.pretriangulated.triangle_morphism_id T).hom₂ = 𝟙 T.obj₂
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism_id_hom₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (T : category_theory.pretriangulated.triangle C) :
(category_theory.pretriangulated.triangle_morphism_id T).hom₁ = 𝟙 T.obj₁
source
@[protected, instance]
def category_theory.pretriangulated.triangle_morphism.inhabited {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (T : category_theory.pretriangulated.triangle C) :
inhabited (category_theory.pretriangulated.triangle_morphism T T)
Equations
source
def category_theory.pretriangulated.triangle_morphism.comp {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ T₃ : category_theory.pretriangulated.triangle C} (f : category_theory.pretriangulated.triangle_morphism T₁ T₂) (g : category_theory.pretriangulated.triangle_morphism T₂ T₃) :
category_theory.pretriangulated.triangle_morphism T₁ T₃

Composition of triangle morphisms gives a triangle morphism.

Equations
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comp_hom₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ T₃ : category_theory.pretriangulated.triangle C} (f : category_theory.pretriangulated.triangle_morphism T₁ T₂) (g : category_theory.pretriangulated.triangle_morphism T₂ T₃) :
(f.comp g).hom₂ = f.hom₂ ≫ g.hom₂
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comp_hom₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ T₃ : category_theory.pretriangulated.triangle C} (f : category_theory.pretriangulated.triangle_morphism T₁ T₂) (g : category_theory.pretriangulated.triangle_morphism T₂ T₃) :
(f.comp g).hom₁ = f.hom₁ ≫ g.hom₁
source
@[simp]
theorem category_theory.pretriangulated.triangle_morphism.comp_hom₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] {T₁ T₂ T₃ : category_theory.pretriangulated.triangle C} (f : category_theory.pretriangulated.triangle_morphism T₁ T₂) (g : category_theory.pretriangulated.triangle_morphism T₂ T₃) :
(f.comp g).hom₃ = f.hom₃ ≫ g.hom₃
source
@[simp]
theorem category_theory.pretriangulated.triangle_category_comp {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B C_1 : category_theory.pretriangulated.triangle C) (f : A ⟶ B) (g : B ⟶ C_1) :
f ≫ g = category_theory.pretriangulated.triangle_morphism.comp f g
source
@[protected, instance]
def category_theory.pretriangulated.triangle_category {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] :
category_theory.category (category_theory.pretriangulated.triangle C)

Triangles with triangle morphisms form a category.

Equations
source
@[simp]
theorem category_theory.pretriangulated.triangle_category_id {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A : category_theory.pretriangulated.triangle C) :
𝟙 A = category_theory.pretriangulated.triangle_morphism_id A
source
def category_theory.pretriangulated.triangle.hom_mk {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B : category_theory.pretriangulated.triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : A.mor₁ ≫ hom₂ = hom₁ ≫ B.mor₁) (comm₂ : A.mor₂ ≫ hom₃ = hom₂ ≫ B.mor₂) (comm₃ : A.mor₃ ≫ (category_theory.shift_functor C 1).map hom₁ = hom₃ ≫ B.mor₃) :
A ⟶ B

a constructor for morphisms of triangles

Equations
source
@[simp]
theorem category_theory.pretriangulated.triangle.hom_mk_hom₁ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B : category_theory.pretriangulated.triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : A.mor₁ ≫ hom₂ = hom₁ ≫ B.mor₁) (comm₂ : A.mor₂ ≫ hom₃ = hom₂ ≫ B.mor₂) (comm₃ : A.mor₃ ≫ (category_theory.shift_functor C 1).map hom₁ = hom₃ ≫ B.mor₃) :
(A.hom_mk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₁ = hom₁
source
@[simp]
theorem category_theory.pretriangulated.triangle.hom_mk_hom₃ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B : category_theory.pretriangulated.triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : A.mor₁ ≫ hom₂ = hom₁ ≫ B.mor₁) (comm₂ : A.mor₂ ≫ hom₃ = hom₂ ≫ B.mor₂) (comm₃ : A.mor₃ ≫ (category_theory.shift_functor C 1).map hom₁ = hom₃ ≫ B.mor₃) :
(A.hom_mk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₃ = hom₃
source
@[simp]
theorem category_theory.pretriangulated.triangle.hom_mk_hom₂ {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B : category_theory.pretriangulated.triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : A.mor₁ ≫ hom₂ = hom₁ ≫ B.mor₁) (comm₂ : A.mor₂ ≫ hom₃ = hom₂ ≫ B.mor₂) (comm₃ : A.mor₃ ≫ (category_theory.shift_functor C 1).map hom₁ = hom₃ ≫ B.mor₃) :
(A.hom_mk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₂ = hom₂
source
def category_theory.pretriangulated.triangle.iso_mk {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B : category_theory.pretriangulated.triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂) (iso₃ : A.obj₃ ≅ B.obj₃) (comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) (comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) (comm₃ : A.mor₃ ≫ (category_theory.shift_functor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) :
A ≅ B

a constructor for isomorphisms of triangles

Equations
source
@[simp]
theorem category_theory.pretriangulated.triangle.iso_mk_hom {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B : category_theory.pretriangulated.triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂) (iso₃ : A.obj₃ ≅ B.obj₃) (comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) (comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) (comm₃ : A.mor₃ ≫ (category_theory.shift_functor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) :
(A.iso_mk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = A.hom_mk B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃
source
@[simp]
theorem category_theory.pretriangulated.triangle.iso_mk_inv {C : Type u} [category_theory.category C] [category_theory.has_shift C ℤ] (A B : category_theory.pretriangulated.triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂) (iso₃ : A.obj₃ ≅ B.obj₃) (comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) (comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) (comm₃ : A.mor₃ ≫ (category_theory.shift_functor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) :
(A.iso_mk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = B.hom_mk A iso₁.inv iso₂.inv iso₃.inv _ _ _