English
If a monoid M is contained in the non-zero-divisors and one localizes along M, the resulting fraction rings of the localized algebras are separable over each other.
Русский
Если моноид M содержится в множестве ненулевых делителей, и производится локализация по M, полученные дробные кольца локализаций алгебр являются разделимыми относительно друг друга.
LaTeX
$$$\text{Algebra.IsSeparable} \left( \FractionRing{R_m} \right) \left( \FractionRing{S_m} \right)$$$
Lean4
theorem isSeparable_of_isLocalization (hM : M ≤ R⁰) : Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ) :=
by
let M' := algebraMapSubmonoid S M
have hM' : algebraMapSubmonoid S M ≤ S⁰ := algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ hM
let f₁ : Rₘ →+* K := map _ (T := R⁰) (RingHom.id R) hM
let f₂ : Sₘ →+* L := map _ (T := S⁰) (RingHom.id S) hM'
algebraize [f₁, f₂]
have := localization_isScalarTower_of_submonoid_le Rₘ K _ _ hM
have := localization_isScalarTower_of_submonoid_le Sₘ L _ _ hM'
have := isFractionRing_of_isDomain_of_isLocalization M Rₘ K
have := isFractionRing_of_isDomain_of_isLocalization M' Sₘ L
have : IsDomain Rₘ := isDomain_of_le_nonZeroDivisors _ hM
apply
Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₘ K).symm.toRingEquiv
(FractionRing.algEquiv Sₘ L).symm.toRingEquiv
apply ringHom_ext R⁰
ext
simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, ← algebraMap_apply]
rw [algebraMap_apply R Rₘ (FractionRing R), AlgEquiv.coe_ringEquiv, AlgEquiv.commutes, algebraMap_apply R S L,
algebraMap_apply S Sₘ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]
simp only [← algebraMap_apply]
rw [algebraMap_apply R Rₘ (FractionRing Rₘ), ← algebraMap_apply Rₘ, ← algebraMap_apply]
