English
Let f:R1 →+* R2, g:R2 →+* R3 be ring homomorphisms and gf: R1 →+* R3 with hgf: gf = g ∘ f. For any M,N in ModuleCat R3 and any φ: M → N, the canonical comparison between the two ways of restricting scalars along f and g commutes with φ; i.e., the naturality square for the App component of restrictScalarsApp is commutative.
Русский
Пусть f: R1 → R2 и g: R2 → R3 — кольцевые гомоморфизмы, gf: R1 → R3 и hgf: gf = g ∘ f. Пусть M,N — объекты в категории модулей над R3, и φ: M → N — гомоморфизм модулей над R3. Тогда каноническое сравнение между двумя способами ограничения скаляров по f и по g сменится естественно по φ; диаграмма естественности компоненты App для restrictScalars пересечение коммутирует.
LaTeX
$$$ (\text{restrictScalars } gf).map \phi \; \gg \; (\text{restrictScalarsComp'App } f g gf hgf N).hom = (\text{restrictScalarsComp'App } f g gf hgf M).hom \; \gg \; (\text{restrictScalars } f).map ((\text{restrictScalars } g).map \phi) $$$
Lean4
@[reassoc]
theorem restrictScalarsComp'App_hom_naturality {M N : ModuleCat R₃} (φ : M ⟶ N) :
(restrictScalars gf).map φ ≫ (restrictScalarsComp'App f g gf hgf N).hom =
(restrictScalarsComp'App f g gf hgf M).hom ≫ (restrictScalars f).map ((restrictScalars g).map φ) :=
(restrictScalarsComp' f g gf hgf).hom.naturality φ
