English
A variant of the zero-shift inverse composes with the pullback iso to give the inverse in the shifted setting φ 0.
Русский
Вариант обратного компонента нулевого сдвига сочетается с каноническим изоморфизмом pullbackShift и дает обратный компонент в сдвинутой системе φ 0.
LaTeX
$$$ (shiftFunctorZero\; (PullbackShift\; C\; \varphi))^{-1}_{X} = (shiftFunctorZero'\; C\; (\varphi\ 0)\ (by\ rw[map_zero]))^{-1}_{X} \circ (pullbackShiftIso\; C\; \varphi\ 0\ (\varphi\ 0)\ rfl)^{-1}_{X} $$$
Lean4
theorem pullbackShiftFunctorZero'_inv_app :
(shiftFunctorZero _ A).inv.app X =
(shiftFunctorZero' C (φ 0) (by rw [map_zero])).inv.app X ≫ (pullbackShiftIso C φ 0 (φ 0) rfl).inv.app X :=
by
rw [pullbackShiftFunctorZero_inv_app]
simp only [Functor.id_obj, pullbackShiftIso, eqToIso.inv, eqToHom_app, shiftFunctorZero', Iso.trans_inv,
NatTrans.comp_app, eqToIso_refl, Iso.refl_inv, NatTrans.id_app, assoc]
erw [comp_id]
