commShiftIso_add' — Mathlib

English

For composed functors F and G, the hom component of the composed commShiftIso is given by composing the maps through the intermediate shift and the isoAdd structure.

Русский

Для композиции функторов F и G гомоморфизм соответствующего сдвигового изоморфизма задаётся через композицию через промежуточный сдвиг и структуру isoAdd.

LaTeX

$$$ (commShiftIso (F ⋙ G) a).hom.app X = G.map ((commShiftIso F a).hom.app X) ≫ (commShiftIso G a).hom.app (F.obj X) $$$

Lean4

theorem commShiftIso_add' {a b c : A} (h : a + b = c) :
    F.commShiftIso c = CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b) :=
  by
  subst h
  simp only [commShiftIso_add, CommShift.isoAdd]

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