mapTriangleRotateIso — Mathlib

English

There is a natural isomorphism between applying rotate to triangles after mapTriangle and applying rotate before mapTriangle.

Русский

Существ́ует естественное изоморождение между поворотом треугольников после mapTriangle и поворотом до mapTriangle.

LaTeX

$$$\\mathrm{mapTriangle}.\\circ\\mathrm{rotate}_D \\cong \\mathrm{rotate}_C \\circ \\mathrm{mapTriangle}$$$

Lean4

/-- `F.mapTriangle` commutes with the rotation of triangles. -/
@[simps!]
def mapTriangleRotateIso : F.mapTriangle ⋙ Pretriangulated.rotate D ≅ Pretriangulated.rotate C ⋙ F.mapTriangle :=
  NatIso.ofComponents
    (fun T =>
      Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) ((F.commShiftIso (1 : ℤ)).symm.app _) (by simp) (by simp) (by simp))
    (by cat_disch)

Похожие утверждения