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

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

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
@[ext]

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  ───> X1
                        
  a      b      c       a1⟧'
  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
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
@[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₁
@[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₃
@[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₂
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
@[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₃
@[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 _ _ _