iso_inv_app — Mathlib

English

The inv component of the commShiftOfLocalization iso is given by a specific composite mirroring the hom case, but with inv arrows.

Русский

Обратный компонент изоморфизма commShiftOfLocalization задан через соответствующую композицию, аналогично случаю гомов, но с inv.

LaTeX

$$$ (commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X) = (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) \gg (F.commShiftIso a).inv.app X \gg (Lifting.iso L W F F').inv.app (X⟦a⟧) \gg F'.map ((L.commShiftIso a).hom.app X) $$$

Lean4

@[simp, reassoc]
theorem iso_inv_app (a : A) (X : C) :
    (commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X) =
      (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
        (F.commShiftIso a).inv.app X ≫ (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫ F'.map ((L.commShiftIso a).hom.app X) :=
  by simp [commShiftOfLocalization.iso]

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