shiftIso_hom_naturality — Mathlib

English

The naturality of shiftIso with respect to a morphism f is expressed: F.map(shiftFunctor C n).map f commutes with the iso after shifting by a'

Русский

Естественность сдвиг-изоморфизма по отношении к морморфизму f записывается как commuting условие после применения сдвига на n и a'.

LaTeX

$$$\text{(F.shiftIso n a a' ha').hom.naturality } f$$$

Lean4

@[reassoc (attr := simp)]
theorem shiftIso_hom_naturality {X Y : C} (n a a' : M) (ha' : n + a = a') (f : X ⟶ Y) :
    (shift F a).map (f⟦n⟧') ≫ (shiftIso F n a a' ha').hom.app Y =
      (shiftIso F n a a' ha').hom.app X ≫ (shift F a').map f :=
  (F.shiftIso n a a' ha').hom.naturality f

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