English
Let R be a commutative semiring, A a semiring with an R-algebra structure, A_s a localization of A with respect to S, and IsScalarTower linking R, A, A_s. Then IsLocalizedModule S (IsScalarTower.toAlgHom R A A_s).toLinearMap holds if and only if IsLocalization (Algebra.algebraMapSubmonoid A S) A_s holds.
Русский
Пусть R — коммутативная полугруппа, A — полугруппа с R-алгеброй, A_s — локализация A по S, и имеется связь через IsScalarTower между R, A и A_s. Тогда IsLocalizedModule S (IsScalarTower.toAlgHom R A A_s).toLinearMap эквивалентно IsLocalization (Algebra.algebraMapSubmonoid A S) A_s.
LaTeX
$$$\\IsLocalizedModule S\\big(\\IsScalarTower.toAlgHom\\,R\\,A\\,A_s\\big).toLinearMap \\iff \\IsLocalization\\big(\\mathsf{algebraMapSubmonoid}\\,A\\,S\\big) A_s.$$$
Lean4
theorem isLocalizedModule_iff_isLocalization :
IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔
IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ :=
by
rw [isLocalizedModule_iff, isLocalization_iff]
refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))
·
simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall, Algebra.algebraMapSubmonoid, ←
SetLike.mem_coe, Submonoid.coe_map, Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
· simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid]
simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm]
· congr!; simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]; simp [Algebra.smul_def]
