commShiftIso_comp_hom_app — Mathlib

English

The map of the hom component of the shift functor commutativity under F is expressed by a combination of the commShiftIso and the shift functor morphisms on X and F.obj X.

Русский

Отображение гомоморфизма компонента коммутативности сдвига через F выражается через комбинацию commShiftIso и гомоморфизмов shiftFunctor на X и F.obj X.

LaTeX

$$$ F.map ((shiftFunctorComm C a b).hom.app X) = (F.commShiftIso b).hom.app (X⟦a⟧) ≫ ((F.commShiftIso a).hom.app X)⟦b⟧' ≫ (shiftFunctorComm D a b).hom.app (F.obj X) ≫ ((F.commShiftIso b).inv.app X)⟦a⟧' ≫ (F.commShiftIso a).inv.app (X⟦b⟧) $$$

Lean4

theorem commShiftIso_comp_hom_app [F.CommShift A] [G.CommShift A] (a : A) (X : C) :
    (commShiftIso (F ⋙ G) a).hom.app X = G.map ((commShiftIso F a).hom.app X) ≫ (commShiftIso G a).hom.app (F.obj X) :=
  by simp [commShiftIso, CommShift.iso]

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