English
For any A with a commutative semiring structure and an algebra structure A → R, and any m ∈ A, the localization element mk (algebraMap A R m) 1 equals algebraMap A (Localization M) m. This expresses compatibility of mk with algebra maps.
Русский
Для любого кольца A с коммутативной полугруппой и алгебраическим отображением A → R и любого m ∈ A, локализационный элемент mk (algebraMap A R m) 1 равен algebraMap A (Localization M) m. Это выражает совместимость mk с алгебраическими отображениями.
LaTeX
$$$\\forall {A}\\ [\\text{CommSemiring } A]\\ [\\text{Algebra } A R]\\ (m:\\, A),\\ \n \\mathrm{Localization.mk}(\\mathrm{algebraMap}\ A\\ R\\ m)\\ 1 = \\mathrm{algebraMap}\\ A\\ (\\mathrm{Localization}\\ M)\\ m$$
Lean4
theorem mk_algebraMap {A : Type*} [CommSemiring A] [Algebra A R] (m : A) :
mk (algebraMap A R m) 1 = algebraMap A (Localization M) m := by
rw [mk_eq_mk', mk'_eq_iff_eq_mul, Submonoid.coe_one, map_one, mul_one]; rfl
