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.
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_map_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
:
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₃ = F.map f.hom₃
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_map_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
:
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₂ = F.map f.hom₂
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_map_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
:
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₁ = F.map f.hom₁
@[simp]
theorem
CategoryTheory.Functor.mapTriangle_obj
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(T : CategoryTheory.Pretriangulated.Triangle C)
:
F.mapTriangle.obj T = CategoryTheory.Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂)
(CategoryTheory.CategoryStruct.comp (F.map T.mor₃) ((F.commShiftIso 1).hom.app T.obj₁))
def
CategoryTheory.Functor.mapTriangle
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.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
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Functor.instFaithfulTriangleMapTriangle
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[F.Faithful]
:
F.mapTriangle.Faithful
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[F.Full]
[F.Faithful]
:
F.mapTriangle.Full
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(n : ℤ)
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCommShiftIso n).inv.app X).hom₁ = (F.commShiftIso n).inv.app X.obj₁
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(n : ℤ)
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCommShiftIso n).hom.app X).hom₃ = (F.commShiftIso n).hom.app X.obj₃
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(n : ℤ)
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCommShiftIso n).inv.app X).hom₂ = (F.commShiftIso n).inv.app X.obj₂
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(n : ℤ)
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCommShiftIso n).hom.app X).hom₂ = (F.commShiftIso n).hom.app X.obj₂
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(n : ℤ)
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCommShiftIso n).inv.app X).hom₃ = (F.commShiftIso n).inv.app X.obj₃
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(n : ℤ)
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCommShiftIso n).hom.app X).hom₁ = (F.commShiftIso n).hom.app X.obj₁
noncomputable def
CategoryTheory.Functor.mapTriangleCommShiftIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(n : ℤ)
:
(CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).comp F.mapTriangle ≅ F.mapTriangle.comp (CategoryTheory.Pretriangulated.Triangle.shiftFunctor D n)
The functor F.mapTriangle commutes with the shift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
CategoryTheory.Functor.instCommShiftTriangleMapTriangleInt
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
:
F.mapTriangle.CommShift ℤ
Equations
- F.instCommShiftTriangleMapTriangleInt = { iso := F.mapTriangleCommShiftIso, zero := ⋯, add := ⋯ }
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleRotateIso.inv.app X).hom₃ = (F.commShiftIso 1).hom.app X.obj₁
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleRotateIso.hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleRotateIso.inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
@[simp]
theorem
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleRotateIso.hom.app X).hom₃ = (F.commShiftIso 1).inv.app X.obj₁
def
CategoryTheory.Functor.mapTriangleRotateIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
:
F.mapTriangle.comp (CategoryTheory.Pretriangulated.rotate D) ≅ (CategoryTheory.Pretriangulated.rotate C).comp F.mapTriangle
F.mapTriangle commutes with the rotation of triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleInvRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleInvRotateIso.hom.app X).hom₁ = (F.commShiftIso (-1)).inv.app X.obj₃
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleInvRotateIso.inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleInvRotateIso.inv.app X).hom₁ = (F.commShiftIso (-1)).hom.app X.obj₃
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleInvRotateIso.hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
@[simp]
theorem
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
(F.mapTriangleInvRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
noncomputable def
CategoryTheory.Functor.mapTriangleInvRotateIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[F.Additive]
:
F.mapTriangle.comp (CategoryTheory.Pretriangulated.invRotate D) ≅ (CategoryTheory.Pretriangulated.invRotate C).comp F.mapTriangle
F.mapTriangle commutes with the inverse of the rotation of triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.HasShift E ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(G : CategoryTheory.Functor D E)
[G.CommShift ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCompIso G).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.HasShift E ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(G : CategoryTheory.Functor D E)
[G.CommShift ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCompIso G).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.HasShift E ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(G : CategoryTheory.Functor D E)
[G.CommShift ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCompIso G).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.HasShift E ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(G : CategoryTheory.Functor D E)
[G.CommShift ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCompIso G).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.HasShift E ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(G : CategoryTheory.Functor D E)
[G.CommShift ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCompIso G).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
@[simp]
theorem
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.HasShift E ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(G : CategoryTheory.Functor D E)
[G.CommShift ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((F.mapTriangleCompIso G).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
def
CategoryTheory.Functor.mapTriangleCompIso
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.HasShift E ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
(G : CategoryTheory.Functor D E)
[G.CommShift ℤ]
:
(F.comp G).mapTriangle ≅ F.mapTriangle.comp G.mapTriangle
The canonical isomorphism (F ⋙ G).mapTriangle ≅ F.mapTriangle ⋙ G.mapTriangle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[CategoryTheory.NatTrans.CommShift e.hom ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₃ = e.inv.app X.obj₃
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[CategoryTheory.NatTrans.CommShift e.hom ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₂ = e.inv.app X.obj₂
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[CategoryTheory.NatTrans.CommShift e.hom ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₁ = e.inv.app X.obj₁
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[CategoryTheory.NatTrans.CommShift e.hom ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₁ = e.hom.app X.obj₁
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[CategoryTheory.NatTrans.CommShift e.hom ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₂ = e.hom.app X.obj₂
@[simp]
theorem
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[CategoryTheory.NatTrans.CommShift e.hom ℤ]
(X : CategoryTheory.Pretriangulated.Triangle C)
:
((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₃ = e.hom.app X.obj₃
def
CategoryTheory.Functor.mapTriangleIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F₁ : CategoryTheory.Functor C D}
{F₂ : CategoryTheory.Functor C D}
(e : F₁ ≅ F₂)
[F₁.CommShift ℤ]
[F₂.CommShift ℤ]
[CategoryTheory.NatTrans.CommShift e.hom ℤ]
:
F₁.mapTriangle ≅ F₂.mapTriangle
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
- One or more equations did not get rendered due to their size.
Instances For
class
CategoryTheory.Functor.IsTriangulated
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
:
A functor which commutes with the shift by ℤ is triangulated if
it sends distinguished triangles to distinguished triangles.
- map_distinguished : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
Instances
theorem
CategoryTheory.Functor.IsTriangulated.map_distinguished
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
{F : CategoryTheory.Functor C D}
[F.CommShift ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
[self : F.IsTriangulated]
(T : CategoryTheory.Pretriangulated.Triangle C)
:
theorem
CategoryTheory.Functor.map_distinguished
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
[F.IsTriangulated]
(T : CategoryTheory.Pretriangulated.Triangle C)
(hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
:
F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
@[instance 100]
instance
CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
[F.IsTriangulated]
:
F.PreservesZeroMorphisms
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.map_m₃
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
{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).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₁₃)
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
:
(h.map F).m₃ = F.map h.m₃
@[simp]
theorem
CategoryTheory.Triangulated.Octahedron.map_m₁
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
{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).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₁₃)
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
:
(h.map F).m₁ = F.map h.m₁
def
CategoryTheory.Triangulated.Octahedron.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
{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).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₁₃)
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
:
The image of an octahedron by a triangulated functor.
Equations
- h.map F = { m₁ := F.map h.m₁, m₃ := F.map h.m₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯, comm₄ := ⋯, mem := ⋯ }
Instances For
theorem
CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Pretriangulated D]
(F : CategoryTheory.Functor C D)
[F.CommShift ℤ]
[F.IsTriangulated]
[(F.mapComposableArrows 2).EssSurj]
[CategoryTheory.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.