English
The inverse of the iso for the RightAdjointCommShift is expressed via unit, shifted unit, and counit maps, mirroring the forward construction.
Русский
Обратный изоморфизм RightAdjointCommShift выражается через единицу, сдвиг единицы и кавитацию, повторяя прямую конструкцию.
LaTeX
$$$ (RightAdjointCommShift.iso(adj,a)).\mathrm{inv}_{Y} = \text{unit, shifted maps, counit composition}$$$
Lean4
@[reassoc]
theorem iso_hom_app (X : D) :
(iso adj a).hom.app X =
(shiftFunctorCompIsoId C b a h).inv.app (G.obj ((shiftFunctor D a).obj X)) ≫
(adj.unit.app ((shiftFunctor C b).obj (G.obj ((shiftFunctor D a).obj X))))⟦a⟧' ≫
(G.map ((F.commShiftIso b).hom.app (G.obj ((shiftFunctor D a).obj X))))⟦a⟧' ≫
(G.map ((shiftFunctor D b).map (adj.counit.app ((shiftFunctor D a).obj X))))⟦a⟧' ≫
(G.map
((shiftFunctorCompIsoId D a b (by rw [← add_left_inj a, add_assoc, h, zero_add, add_zero])).hom.app
X))⟦a⟧' :=
by
obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]
simp [iso, iso', shiftEquiv']
