English
The Jacobson radical of the bottom ideal in a polynomial ring is bounded above by the infimum of the images of Jacobson radicals under the C-map from the base ring to polynomials.
Русский
Радикал Якобсона нуля в кольце многочленов сверху ограничен инфимумом образов радикалов Якобсона под отображением C из базового кольца в полиномы.
LaTeX
$$jacobson (⊥ : Ideal R[X]) ≤ sInf (map (C : R →+* R[X]) '' {J : Ideal R | J.IsMaximal})$$
Lean4
theorem jacobson_bot_polynomial_le_sInf_map_maximal :
jacobson (⊥ : Ideal R[X]) ≤ sInf (map (C : R →+* R[X]) '' {J : Ideal R | J.IsMaximal}) :=
by
refine le_sInf fun J => exists_imp.2 fun j hj => ?_
haveI : j.IsMaximal := hj.1
refine Trans.trans (jacobson_mono bot_le) (le_of_eq ?_ : J.jacobson ≤ J)
suffices t : (⊥ : Ideal (Polynomial (R ⧸ j))).jacobson = ⊥
by
rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
rwa [map_jacobson_of_bijective _, map_bot] at t
exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)
refine eq_bot_iff.2 fun f hf => ?_
have r1 : (X : (R ⧸ j)[X]) ≠ 0 := ne_of_apply_ne (coeff · 1) <| by simp
simpa [r1] using eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit ((mem_jacobson_bot.1 hf) X))
