English
For a prime p, the existence of a nontrivial ideal I with CharP(R/I) p is equivalent to the existence of a maximal ideal M with CharP(R/M) p.
Русский
Для простого p существование не тривиального идеала I с CharP(R/I) p эквивалентно существованию максимального идеала M с CharP(R/M) p.
LaTeX
$$$\\exists I\\, (I \\neq \\top) \\land \\operatorname{CharP}(R/I,p) \\quad\\iff\\quad \\exists I\\, (I.\\IsMaximal) \\land \\operatorname{CharP}(R/I,p) $$$
Lean4
/-- Reduction to `I` prime ideal: When proving statements about mixed characteristic rings,
after we reduced to `p` prime, we can assume that the ideal `I` in the definition is maximal.
-/
theorem reduce_to_maximal_ideal {p : ℕ} (hp : Nat.Prime p) :
(∃ I : Ideal R, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I : Ideal R, I.IsMaximal ∧ CharP (R ⧸ I) p :=
by
constructor
· intro g
rcases g with
⟨I, ⟨hI_not_top, _⟩⟩
-- Krull's Thm: There exists a prime ideal `M` such that `I ≤ M`.
rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
use M
constructor
· exact hM_max
·
cases CharP.exists (R ⧸ M) with
| intro r hr =>
convert hr
have r_dvd_p : r ∣ p := by
rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
convert congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
symm
apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
exact CharP.char_ne_one (R ⧸ M) r
· intro ⟨I, hI_max, h_charP⟩
use I
exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩
