English
In the same setting as above, the inverse components satisfy a naturality relation: the naturality of the App inverse with respect to φ, i.e., the two ways of transporting φ and then applying the isomorphism on the opposite side agree.
Русский
В той же постановке утверждается естественность обратной составляющей преобразования: естественность для обратного компонента при отображении φ.
LaTeX
$$$ (\text{restrictScalars } f).map ((\text{restrictScalars } g).map \phi) \; \gg \; (\text{restrictScalarsComp'App } f g gf hgf N).inv = (\text{restrictScalarsComp'App } f g gf hgf M).inv \; \gg \; (\text{restrictScalars } gf).map \phi $$$
Lean4
@[reassoc]
theorem restrictScalarsComp'App_inv_naturality {M N : ModuleCat R₃} (φ : M ⟶ N) :
(restrictScalars f).map ((restrictScalars g).map φ) ≫ (restrictScalarsComp'App f g gf hgf N).inv =
(restrictScalarsComp'App f g gf hgf M).inv ≫ (restrictScalars gf).map φ :=
(restrictScalarsComp' f g gf hgf).inv.naturality φ
