English
The two constructions IsLocalization.mk' A_s x s and IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A A_s).toLinearMap x s agree.
Русский
Эти две конструкторы mk' совпадают: IsLocalization.mk' и IsLocalizedModule.mk'.
LaTeX
$$$\\IsLocalization.mk' A_s x\\; s = \\IsLocalizedModule.mk'\\big( \\IsScalarTower.toAlgHom R A A_s\\big).toLinearMap x s.$$$
Lean4
/-- `IsLocalization.mk'` agrees with `IsLocalizedModule.mk'`. -/
theorem mk'_algebraMap_eq_mk' [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {x : A} {s : S} :
IsLocalization.mk' Aₛ x ⟨_, Algebra.mem_algebraMapSubmonoid_of_mem s⟩ =
IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x s :=
by
rw [← IsLocalizedModule.smul_inj (IsScalarTower.toAlgHom R A Aₛ).toLinearMap s, IsLocalizedModule.mk'_cancel',
Submonoid.smul_def, ← algebraMap_smul A]
exact IsLocalization.smul_mk'_self (m := ⟨_, _⟩)
