commShiftIso_comp_inv_app — Mathlib

English

For two commShiftIso structures on F and G, the composed inverse component matches the expected composite given by applying G to F’s inverse and then composing with the inverse of the outer iso.

Русский

Для двух структур commShiftIso на F и G составной обратный компонент совпадает с ожидаемым композитом: применяется обратное F, затем компонуется с обратным внешнего изоморфизма.

LaTeX

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

Lean4

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

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