English
If R is Jacobson, then R[X] is Jacobson (alternative formulation).
Русский
Если R — кольцо Якобсона, то R[X] тоже Якобсон.
LaTeX
$$$IsJacobsonRing(R) \\Rightarrow IsJacobsonRing(R[X])$$$
Lean4
theorem isJacobsonRing_polynomial_of_isJacobsonRing (hR : IsJacobsonRing R) : IsJacobsonRing R[X] :=
by
rw [isJacobsonRing_iff_prime_eq]
intro I hI
let R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
let i : R →+* R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
have hi : Function.Surjective ↑i := ((Ideal.Quotient.mk I).comp C).rangeRestrict_surjective
have hi' : RingHom.ker (mapRingHom i) ≤ I := by
intro f hf
apply polynomial_mem_ideal_of_coeff_mem_ideal I f
intro n
replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf
change (Polynomial.map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf
rw [coeff_map, Subtype.ext_iff] at hf
rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
have R'_jacob : IsJacobsonRing R' := isJacobsonRing_of_surjective ⟨i, hi⟩
let J := I.map (mapRingHom i)
have h_surj : Function.Surjective (mapRingHom i) := Polynomial.map_surjective i hi
have : IsPrime J := map_isPrime_of_surjective h_surj hi'
suffices h : J.jacobson = J by
replace h := congrArg (comap (Polynomial.mapRingHom i)) h
rw [← map_jacobson_of_surjective h_surj hi', comap_map_of_surjective _ h_surj,
comap_map_of_surjective _ h_surj] at h
refine le_antisymm ?_ le_jacobson
exact le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi'))
apply isJacobsonRing_polynomial_of_domain R' J
exact eq_zero_of_polynomial_mem_map_range I
