induced_shiftIso_hom_app_obj — Mathlib

English

For the induced shiftIso, its hom component at L X equals the composite (F' a).map inv, (e' a).hom, (G.shiftIso), and (e' a').inv evaluated at X.

Русский

Для индуцированного shiftIso гомоморфизм в точке L X равен композиции (F' a).map inv, (e' a).hom, (G.shiftIso) и (e' a').inv в X.

LaTeX

$$$ (shiftIso\ L\ G\ M\ F'\ e'\ n\ a\ a'\ ha').hom.app\ (L.obj\ X) = (F'\ a).map ((L.commShiftIso\ n).inv.app\ X) \gg (e'\ a).hom.app\ (X\langle n \rangle) \gg (G.shiftIso\ n\ a\ a'\ ha').hom.app\ X \gg (e'\ a').inv.app\ X $$$

Lean4

@[simp, reassoc]
theorem induced_shiftIso_hom_app_obj (n a a' : M) (ha' : n + a = a') (X : C) :
    letI := (induced e M F' e')
    (F.shiftIso n a a' ha').hom.app (L.obj X) =
      (F.shift a).map ((L.commShiftIso n).inv.app X) ≫
        (e' a).hom.app (X⟦n⟧) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X :=
  by apply induced.shiftIso_hom_app_obj

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