English
If P is a prime ideal in R, then the image of P under the map C into R[X] is a prime ideal in R[X]; and conversely, P is prime iff its C-map is prime.
Русский
Если P — простой идеал в R, то образ P под включением C в R[X] является простым идеалом в R[X]; и наоборот, P прост iff его образ прост.
LaTeX
$$IsPrime (map C P) ≃ IsPrime P$$
Lean4
/-- If `P` is a prime ideal of `R`, then `P.R[x]` is a prime ideal of `R[x]`. -/
theorem isPrime_map_C_iff_isPrime (P : Ideal R) : IsPrime (map (C : R →+* R[X]) P : Ideal R[X]) ↔ IsPrime P := by
-- Note: the following proof avoids quotient rings
-- It can be golfed substantially by using something like
-- `(Quotient.isDomain_iff_prime (map C P : Ideal R[X]))`
constructor
· intro H
have := comap_isPrime C (map C P)
convert this using 1
ext x
simp only [mem_comap, mem_map_C_iff]
constructor
· rintro h (- | n)
· rwa [coeff_C_zero]
· simp only [coeff_C_ne_zero (Nat.succ_ne_zero _), Submodule.zero_mem]
· intro h
simpa only [coeff_C_zero] using h 0
· intro h
constructor
· rw [Ne, eq_top_iff_one, mem_map_C_iff, not_forall]
use 0
rw [coeff_one_zero, ← eq_top_iff_one]
exact h.1
· intro f g
simp only [mem_map_C_iff]
contrapose!
rintro ⟨hf, hg⟩
classical
let m := Nat.find hf
let n := Nat.find hg
refine ⟨m + n, ?_⟩
rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]
· apply mt h.2
rw [not_or]
exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
apply P.sum_mem
rintro ⟨i, j⟩ hij
rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
simp only [Ne, Prod.mk_inj, not_and_or] at hij
obtain hi | hj : i < m ∨ j < n := by cutsat
· rw [mul_comm]
apply P.mul_mem_left
exact Classical.not_not.1 (Nat.find_min hf hi)
· apply P.mul_mem_left
exact Classical.not_not.1 (Nat.find_min hg hj)
