jacobson_bot_polynomial_of_jacobson_bot

English

If jacobson(⊥) in R is 0, then jacobson(⊥) in R[X] is also 0.

Русский

Если jacobson(⊥) в R равно 0, то jacobson(⊥) в R[X] тоже равно 0.

LaTeX

$$jacobson(⊥ : Ideal R) = ⊥ \Rightarrow jacobson(⊥ : Ideal R[X]) = ⊥$$

Lean4

theorem jacobson_bot_polynomial_of_jacobson_bot (h : jacobson (⊥ : Ideal R) = ⊥) : jacobson (⊥ : Ideal R[X]) = ⊥ :=
  by
  refine eq_bot_iff.2 (le_trans jacobson_bot_polynomial_le_sInf_map_maximal ?_)
  refine fun f hf =>
    (Submodule.mem_bot R[X]).2 <| Polynomial.ext fun n => Trans.trans (?_ : coeff f n = 0) (coeff_zero n).symm
  suffices f.coeff n ∈ Ideal.jacobson ⊥ by rwa [h, Submodule.mem_bot] at this
  exact mem_sInf.2 fun j hj => (mem_map_C_iff.1 ((mem_sInf.1 hf) ⟨j, ⟨hj.2, rfl⟩⟩)) n

Похожие утверждения