English
Explicit formula for the component of the inverse of the isomorphism (in the LeftAdjointCommShift setting) at an object Y in C, expressed as a long composite of maps coming from F, G, unit, counit, and shift isomorphisms.
Русский
Явная формула компоненты обратного изоморфизма (в контексте LeftAdjointCommShift) на объекте Y в C, представляемая как композиция отображений из F, G, единицы, counit и изоморфизмов сдвигов.
LaTeX
$$$(\\text{(iso adj a).inv})_Y = \\text{long composition involving }F, G, \\text{shift iso, unit, counit}$$$
Lean4
@[reassoc]
theorem iso_inv_app (Y : C) :
(iso adj a).inv.app Y =
(F.map ((shiftFunctorCompIsoId C a b h).inv.app Y))⟦a⟧' ≫
(F.map ((adj.unit.app (Y⟦a⟧))⟦b⟧'))⟦a⟧' ≫
(F.map ((G.commShiftIso b).inv.app (F.obj (Y⟦a⟧))))⟦a⟧' ≫
(adj.counit.app ((F.obj (Y⟦a⟧))⟦b⟧))⟦a⟧' ≫
(shiftFunctorCompIsoId D b a (by simp [eq_neg_of_add_eq_zero_left h])).hom.app (F.obj (Y⟦a⟧)) :=
by
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
simp [iso, iso', shiftEquiv']
