English
The localized module LocalizedModule S A carries a natural structure of an R-algebra, defined so that its algebra map is built from the localizations of R and A in a compatible way; in particular, the commuting and smul definitions are arranged to satisfy the axioms of an algebra over R.
Русский
Локализованный модуль LocalizedModule S A естественным образом является R-алгеброй; отображение алгебры строится из локализаций R и A совместно, чтобы удовлетворять аксиомам алгебры над R (коммутативная).
LaTeX
$$$\\mathrm{LocalizedModule}(S,A)\\text{ is an }R\\text{-algebra with }\\mathrm{algebraMap}_R^{\\mathrm{Loc}} = \\mathrm{Localization}.algebraMap \\circ \\mathrm{algebraMap}_R$.$$
Lean4
noncomputable instance algebra' {A : Type*} [Semiring A] [Algebra R A] : Algebra R (LocalizedModule S A)
where
algebraMap := (algebraMap (Localization S) (LocalizedModule S A)).comp (algebraMap R <| Localization S)
commutes' := by
intro r x
induction x using induction_on with
| _ a s => _
dsimp
rw [← Localization.mk_one_eq_algebraMap, algebraMap_mk, mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]
smul_def' := by
intro r x
induction x using induction_on with
| _ a s => _
dsimp
rw [← Localization.mk_one_eq_algebraMap, algebraMap_mk, mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]
