English
The inv component satisfies naturality with respect to a morphism f, i.e., the inverse component at X corresponds to the inverse of the corresponding composed iso at Y.
Русский
Компонента обратного естественным образом совместима с морфизмом f: inv.app X соответствует обратному изоморфизму на Y.
LaTeX
$$$ ((\\mathrm{shiftFunctorCompIsoId} \\ C n m h).inv.app X) = ((\\mathrm{shiftFunctorCompIsoId} \\ C m n (..)).inv.app (X⟦n⟧)) $$$
Lean4
theorem shift_shiftFunctorCompIsoId_inv_app (n m : A) (h : n + m = 0) (X : C) :
((shiftFunctorCompIsoId C n m h).inv.app X)⟦n⟧' =
((shiftFunctorCompIsoId C m n (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel])).inv.app (X⟦n⟧)) :=
by
rw [← cancel_mono (((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧'), ← Functor.map_comp, Iso.inv_hom_id_app,
Functor.map_id, shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app]
rfl
