English
Under the given localizations and algebras, the two natural maps obtained by composing algebra maps and localization equivalences are equal.
Русский
При заданных локализациях и алгебрах две естественные композиции отображений согласуются и совпадают.
LaTeX
$$$(\text{algEquiv } N S_n S_n') \circ (\text{algebraMap } R_m S_n) = (\text{algebraMap } R_m' S_n') \circ (\text{algEquiv } M R_m R_m')$$$
Lean4
theorem algEquiv_comp_algebraMap :
(algEquiv N Sₙ Sₙ' : _ →+* Sₙ').comp (algebraMap Rₘ Sₙ) = (algebraMap Rₘ' Sₙ').comp (algEquiv M Rₘ Rₘ') :=
by
refine IsLocalization.ringHom_ext M (RingHom.ext fun x => ?_)
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes]
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply, ← AlgEquiv.restrictScalars_apply R,
AlgEquiv.commutes]
