English
Same as mapTriangleRotateIso in spirit: a natural isomorphism between rotated triangles and mapped triangles.
Русский
То же самое, что и mapTriangleRotateIso, но в другой форме: естественное изоморождение между повернутыми треугольниками и отображёнными треугольниками.
LaTeX
$$$F.mapTriangle \\circ \\mathrm{rotate}_D \\cong \\mathrm{rotate}_C \\circ F.mapTriangle$$$
Lean4
/-- Two isomorphic functors `F₁` and `F₂` induce isomorphic functors
`F₁.mapTriangle` and `F₂.mapTriangle` if the isomorphism `F₁ ≅ F₂` is compatible
with the shifts. -/
@[simps!]
def mapTriangleIso {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] :
F₁.mapTriangle ≅ F₂.mapTriangle :=
NatIso.ofComponents
(fun T =>
Triangle.isoMk _ _ (e.app _) (e.app _) (e.app _) (by simp) (by simp)
(by
dsimp
simp only [assoc, NatTrans.shift_app_comm e.hom (1 : ℤ) T.obj₁, NatTrans.naturality_assoc]))
(by cat_disch)
