English
If R is Jacobson, then the polynomial ring R[X] is Jacobson.
Русский
Если R — кольцо Якобсона, то кольцо полиномов R[X] также является кольцом Якобсона.
LaTeX
$$$IsJacobsonRing(R) \\Rightarrow IsJacobsonRing(R[X])$$$
Lean4
/-- If `f : R → S` descends to an integral map in the localization at `x`,
and `R` is a Jacobson ring, then the intersection of all maximal ideals in `S` is trivial -/
theorem jacobson_bot_of_integral_localization {R : Type*} [CommRing R] [IsDomain R] [IsJacobsonRing R] (Rₘ Sₘ : Type*)
[CommRing Rₘ] [CommRing Sₘ] (φ : R →+* S) (hφ : Function.Injective ↑φ) (x : R) (hx : x ≠ 0) [Algebra R Rₘ]
[IsLocalization.Away x Rₘ] [Algebra S Sₘ] [IsLocalization ((Submonoid.powers x).map φ : Submonoid S) Sₘ]
(hφ' : RingHom.IsIntegral (IsLocalization.map Sₘ φ (Submonoid.powers x).le_comap_map : Rₘ →+* Sₘ)) :
(⊥ : Ideal S).jacobson = (⊥ : Ideal S) :=
by
have hM : ((Submonoid.powers x).map φ : Submonoid S) ≤ nonZeroDivisors S :=
map_le_nonZeroDivisors_of_injective φ hφ (powers_le_nonZeroDivisors_of_noZeroDivisors hx)
letI : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors _ hM
let φ' : Rₘ →+* Sₘ := IsLocalization.map _ φ (Submonoid.powers x).le_comap_map
suffices ∀ I : Ideal Sₘ, I.IsMaximal → (I.comap (algebraMap S Sₘ)).IsMaximal
by
have hϕ' : comap (algebraMap S Sₘ) (⊥ : Ideal Sₘ) = (⊥ : Ideal S) :=
by
rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
exact IsLocalization.injective Sₘ hM
have hRₘ : IsJacobsonRing Rₘ := isJacobsonRing_localization x
have hSₘ : IsJacobsonRing Sₘ := isJacobsonRing_of_isIntegral' φ' hφ'
refine eq_bot_iff.mpr (le_trans ?_ (le_of_eq hϕ'))
rw [← hSₘ.out isRadical_bot_of_noZeroDivisors, comap_jacobson]
exact
sInf_le_sInf fun j hj =>
⟨bot_le,
let ⟨J, hJ⟩ := hj
hJ.2 ▸ this J hJ.1.2⟩
intro I hI
have : (I.comap (algebraMap S Sₘ)).IsPrime := comap_isPrime _ I
have : (I.comap φ').IsPrime := comap_isPrime φ' I
have : (⊥ : Ideal (S ⧸ I.comap (algebraMap S Sₘ))).IsPrime := bot_prime
have hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ := IsLocalization.map_comp _
let f := quotientMap (I.comap (algebraMap S Sₘ)) φ le_rfl
let g := quotientMap I (algebraMap S Sₘ) le_rfl
have := isMaximal_comap_of_isIntegral_of_isMaximal' φ' hφ' I
have := ((IsLocalization.isMaximal_iff_isMaximal_disjoint Rₘ x _).1 this).left
have : ((I.comap (algebraMap S Sₘ)).comap φ).IsMaximal := by rwa [comap_comap, hcomm, ← comap_comap] at this
rw [← bot_quotient_isMaximal_iff] at this ⊢
refine
isMaximal_of_isIntegral_of_isMaximal_comap' f ?_ ⊥
((eq_bot_iff.2 (comap_bot_le_of_injective f quotientMap_injective)).symm ▸ this)
exact
RingHom.IsIntegral.tower_bot f g quotientMap_injective
((comp_quotientMap_eq_of_comp_eq hcomm I).symm ▸
(RingHom.isIntegral_of_surjective _
(IsLocalization.surjective_quotientMap_of_maximal_of_localization (Submonoid.powers x) Rₘ
(by rwa [comap_comap, hcomm, ← bot_quotient_isMaximal_iff]))).trans
_ _ (hφ'.quotient _))
