Triangulated functors #
In this file, when C and D are categories equipped with a shift by ℤ and
F : C ⥤ D is a functor which commutes with the shift, we define the induced
functor F.mapTriangle : Triangle C ⥤ Triangle D on the categories of
triangles. When C and D are pretriangulated, a triangulated functor
is such a functor F which also sends distinguished triangles to
distinguished triangles: this defines the typeclass Functor.IsTriangulated.
def
CategoryTheory.Functor.mapTriangle
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
:
The functor Triangle C ⥤ Triangle D that is induced by a functor F : C ⥤ D
which commutes with shift by ℤ.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_map_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
{X✝ Y✝ : Pretriangulated.Triangle C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_map_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
{X✝ Y✝ : Pretriangulated.Triangle C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_obj
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(T : Pretriangulated.Triangle C)
:
F.mapTriangle.obj T = Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂)
(CategoryStruct.comp (F.map T.mor₃) ((F.commShiftIso 1).hom.app T.obj₁))
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_map_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
{X✝ Y✝ : Pretriangulated.Triangle C}
(f : X✝ ⟶ Y✝)
:
instance
CategoryTheory.Functor.instFaithfulTriangleMapTriangle
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[F.Faithful]
:
instance
CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[F.Full]
[F.Faithful]
:
noncomputable def
CategoryTheory.Functor.mapTriangleCommShiftIso
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(n : ℤ)
:
The functor F.mapTriangle commutes with the shift.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(n : ℤ)
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(n : ℤ)
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(n : ℤ)
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(n : ℤ)
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(n : ℤ)
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(n : ℤ)
(X : Pretriangulated.Triangle C)
:
noncomputable instance
CategoryTheory.Functor.instCommShiftTriangleMapTriangleInt
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
:
Equations
def
CategoryTheory.Functor.mapTriangleRotateIso
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
:
F.mapTriangle commutes with the rotation of triangles.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
noncomputable def
CategoryTheory.Functor.mapTriangleInvRotateIso
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
:
F.mapTriangle commutes with the inverse of the rotation of triangles.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Preadditive C]
[Preadditive D]
[F.Additive]
(X : Pretriangulated.Triangle C)
:
The canonical isomorphism (𝟭 C).mapTriangle ≅ 𝟭 (Triangle C).
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂
(C : Type u_1)
[Category.{u_4, u_1} C]
[HasShift C ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃
(C : Type u_1)
[Category.{u_4, u_1} C]
[HasShift C ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂
(C : Type u_1)
[Category.{u_4, u_1} C]
[HasShift C ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁
(C : Type u_1)
[Category.{u_4, u_1} C]
[HasShift C ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁
(C : Type u_1)
[Category.{u_4, u_1} C]
[HasShift C ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃
(C : Type u_1)
[Category.{u_4, u_1} C]
[HasShift C ℤ]
(X : Pretriangulated.Triangle C)
:
def
CategoryTheory.Functor.mapTriangleCompIso
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
:
The canonical isomorphism (F ⋙ G).mapTriangle ≅ F.mapTriangle ⋙ G.mapTriangle.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
(X : Pretriangulated.Triangle C)
:
def
CategoryTheory.Functor.mapTriangleIso
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
:
Two isomorphic functors F₁ and F₂ induce isomorphic functors
F₁.mapTriangle and F₂.mapTriangle if the isomorphism F₁ ≅ F₂ is compatible
with the shifts.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
(X : Pretriangulated.Triangle C)
:
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
(X : Pretriangulated.Triangle C)
:
class
CategoryTheory.Functor.IsTriangulated
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
:
A functor which commutes with the shift by ℤ is triangulated if
it sends distinguished triangles to distinguished triangles.
- map_distinguished (T : Pretriangulated.Triangle C) : T ∈ Pretriangulated.distinguishedTriangles → F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
Instances
theorem
CategoryTheory.Functor.map_distinguished
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[F.IsTriangulated]
(T : Pretriangulated.Triangle C)
(hT : T ∈ Pretriangulated.distinguishedTriangles)
:
@[instance 100]
instance
CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[F.IsTriangulated]
:
instance
CategoryTheory.Functor.IsTriangulated.instPreservesLimitsOfShapeDiscreteWalkingPair
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[F.IsTriangulated]
:
@[instance 100]
instance
CategoryTheory.Functor.IsTriangulated.instAdditive
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[F.IsTriangulated]
:
F.Additive
instance
CategoryTheory.Functor.IsTriangulated.instId
{C : Type u_1}
[Category.{u_4, u_1} C]
[HasShift C ℤ]
[Limits.HasZeroObject C]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
:
instance
CategoryTheory.Functor.IsTriangulated.instComp
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Limits.HasZeroObject E]
[Preadditive C]
[Preadditive D]
[Preadditive E]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[∀ (n : ℤ), (shiftFunctor E n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[Pretriangulated E]
[F.IsTriangulated]
[G.IsTriangulated]
:
(F.comp G).IsTriangulated
theorem
CategoryTheory.Functor.isTriangulated_of_iso
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
[F₁.IsTriangulated]
:
theorem
CategoryTheory.Functor.isTriangulated_iff_of_iso
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[NatTrans.CommShift e.hom ℤ]
:
theorem
CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
(F : Functor C D)
[F.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[F.IsTriangulated]
[F.mapArrow.EssSurj]
(T : Pretriangulated.Triangle D)
(hT : T ∈ Pretriangulated.distinguishedTriangles)
:
∃ (T' : Pretriangulated.Triangle C) (_ : T' ∈ Pretriangulated.distinguishedTriangles),
Nonempty (F.mapTriangle.obj T' ≅ T)
theorem
CategoryTheory.Functor.isTriangulated_of_precomp
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_6, u_2} D]
[Category.{u_5, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
(F : Functor C D)
[F.CommShift ℤ]
(G : Functor D E)
[G.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Limits.HasZeroObject E]
[Preadditive C]
[Preadditive D]
[Preadditive E]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[∀ (n : ℤ), (shiftFunctor E n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[Pretriangulated E]
[(F.comp G).IsTriangulated]
[F.IsTriangulated]
[F.mapArrow.EssSurj]
:
theorem
CategoryTheory.Functor.isTriangulated_of_precomp_iso
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_6, u_2} D]
[Category.{u_5, u_3} E]
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift E ℤ]
{F : Functor C D}
[F.CommShift ℤ]
{G : Functor D E}
[G.CommShift ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Limits.HasZeroObject E]
[Preadditive C]
[Preadditive D]
[Preadditive E]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[∀ (n : ℤ), (shiftFunctor E n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[Pretriangulated E]
{H : Functor C E}
(e : F.comp G ≅ H)
[H.CommShift ℤ]
[H.IsTriangulated]
[F.IsTriangulated]
[F.mapArrow.EssSurj]
[NatTrans.CommShift e.hom ℤ]
:
def
CategoryTheory.Triangulated.Octahedron.map
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
{comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃}
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁}
{h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂}
{h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁}
{h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles}
(h : Octahedron comm h₁₂ h₂₃ h₁₃)
(F : Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
:
Octahedron ⋯ ⋯ ⋯ ⋯
The image of an octahedron by a triangulated functor.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.map_m₁
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
{comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃}
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁}
{h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂}
{h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁}
{h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles}
(h : Octahedron comm h₁₂ h₂₃ h₁₃)
(F : Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
:
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.map_m₃
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
{u₁₂ : X₁ ⟶ X₂}
{u₂₃ : X₂ ⟶ X₃}
{u₁₃ : X₁ ⟶ X₃}
{comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃}
{v₁₂ : X₂ ⟶ Z₁₂}
{w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁}
{h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles}
{v₂₃ : X₃ ⟶ Z₂₃}
{w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂}
{h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles}
{v₁₃ : X₃ ⟶ Z₁₃}
{w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁}
{h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles}
(h : Octahedron comm h₁₂ h₂₃ h₁₃)
(F : Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
:
theorem
CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[HasShift C ℤ]
[HasShift D ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(F : Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
[(F.mapComposableArrows 2).EssSurj]
[IsTriangulated C]
:
If F : C ⥤ D is a triangulated functor from a triangulated category, then D
is also triangulated if tuples of composables arrows in D can be lifted to C.