mapTriangleCommShiftIso — Mathlib

English

For every integer n, there is a natural isomorphism between applying the shift functor first and then mapTriangle, and applying mapTriangle first and then the shift functor.

Русский

Для каждого целого n существует естественное изоморование между последовательностью сдвига сначала и затем mapTriangle и последовательностью mapTriangle сначала и затем сдвиг.

LaTeX

$$$\\triangleShiftC(n) \\circ F.mapTriangle \\cong F.mapTriangle \\circ \\triangleShiftD(n)$$$

Lean4

/-- The functor `F.mapTriangle` commutes with the shift. -/
noncomputable def mapTriangleCommShiftIso (n : ℤ) :
    Triangle.shiftFunctor C n ⋙ F.mapTriangle ≅ F.mapTriangle ⋙ Triangle.shiftFunctor D n :=
  NatIso.ofComponents
    (fun T =>
      Triangle.isoMk _ _ ((F.commShiftIso n).app _) ((F.commShiftIso n).app _) ((F.commShiftIso n).app _) (by simp)
        (by simp)
        (by
          dsimp
          simp only [map_units_smul, map_comp, Linear.units_smul_comp, assoc, Linear.comp_units_smul,
            ← F.commShiftIso_hom_naturality_assoc]
          rw [F.map_shiftFunctorComm_hom_app T.obj₁ 1 n]
          simp only [comp_obj, assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp, Iso.inv_hom_id_app, map_id,
            comp_id]))
    (by cat_disch)

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