mapTriangleInvRotateIso — Mathlib

English

There is a natural isomorphism between mapTriangle and the inverse rotation: F.mapTriangle ≅ invRotate ∘ F.mapTriangle.

Русский

Существует естественное изоморождение между mapTriangle и обратной перестановкой вращения.

LaTeX

$$$\\mathrm{mapTriangle}\\;\\mathrm{InvRotate} \\cong \\mathrm{InvRotate}\\;\\mathrm{mapTriangle}$$$

Lean4

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

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