English
If R,S have NoZeroDivisors and certain localization hypotheses hold, then the localized ring inherits the NoZeroDivisors property.
Русский
Если в R,S нет нулевых делителей и соблюдены условия локализации, то локализация сохраняет свойство без нулевых делителей.
LaTeX
$$$NoZeroSMulDivisors\\ R\\ S \\Rightarrow NoZeroSMulDivisors\\ R_{p} S_{p}$$$
Lean4
theorem _root_.NoZeroSMulDivisors_of_isLocalization (Rₚ Sₚ : Type*) [CommRing Rₚ] [CommRing Sₚ] [Algebra R Rₚ]
[Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] {M : Submonoid R}
(hM : M ≤ R⁰) [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [NoZeroSMulDivisors R S]
[IsDomain S] : NoZeroSMulDivisors Rₚ Sₚ :=
by
have e : Algebra.algebraMapSubmonoid S M ≤ S⁰ :=
Submonoid.map_le_of_le_comap _ <|
hM.trans (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective _ _))
have : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors _ e
have :
algebraMap Rₚ Sₚ =
IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) (Submonoid.le_comap_map M) :=
by
apply IsLocalization.ringHom_ext M
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
intro x hx
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x
simp only [IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff, Subtype.exists, exists_prop, this] at hx ⊢
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
simp only [← map_mul, (injective_iff_map_eq_zero' _).mp (FaithfulSMul.algebraMap_injective R S)] at H
exact ⟨a, ha, H⟩
