English
The associativity of the extension of scalars isomorphisms expresses that extending along a composition of ring homs and then composing with intermediate extensions is canonically equal to first extending along one and then along the other, up to canonical whiskering and associator isomorphisms.
Русский
Сопряжённости расширения скаляров отображают ассоциативность: расширение по композиции гомоморфизмов равно поэтапному расширению через промежуточные шаги, с учётом естественных сопряжений и ассоциатора.
LaTeX
$$$$ (\extendScalarsComp (f_{23} \circ f_{12}) f_{34}).\mathrm{hom} \; = \; (\extendScalarsComp f_{12} f_{23}).\mathrm{hom} \circ \text{ whiskerLeft/Right } \circ (\text{ associator }).^{-1} \circ (\extendScalarsComp f_{12} (f_{34} \circ f_{23})).^{ -1} $$$$
Lean4
theorem homEquiv_extendScalarsComp (M : ModuleCat R₁) :
(extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv _ _ ((extendScalarsComp f₁₂ f₂₃).hom.app M) =
(extendRestrictScalarsAdj f₁₂).unit.app M ≫
(restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app _) ≫
(restrictScalarsComp f₁₂ f₂₃).inv.app _ :=
by
dsimp [extendScalarsComp, conjugateIsoEquiv, conjugateEquiv]
simp only [Category.assoc, Category.id_comp, Category.comp_id, Adjunction.comp_unit_app, Adjunction.homEquiv_unit,
Functor.map_comp, Adjunction.unit_naturality_assoc, Adjunction.right_triangle_components]
rfl
