English
In a Dedekind domain, if P is a prime not equal to a maximal ideal and x ∈ P with x not in P^2, and x is not in any other prime, then P is generated by x.
Русский
В Дедекинд домене, если P — простый идеал, не равный мaкcимальному, и x ∈ P, x ∉ P^2, и x не лежит в любом другом простом, то P порожден порождением x.
LaTeX
$$$$P = \\operatorname{span}\\{x\\}$$$$
Lean4
/-- Let `P` be a prime ideal, `x ∈ P \ P²` and `x ∉ Q` for all prime ideals `Q ≠ P`.
Then `P` is generated by `x`. -/
theorem eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne {P : Ideal R} (hP : P.IsPrime) [IsDedekindDomain R]
{x : R} (x_mem : x ∈ P) (hxP2 : x ∉ P ^ 2) (hxQ : ∀ Q : Ideal R, IsPrime Q → Q ≠ P → x ∉ Q) :
P = Ideal.span { x } := by
letI := Classical.decEq (Ideal R)
have hx0 : x ≠ 0 := by
rintro rfl
exact hxP2 (zero_mem _)
by_cases hP0 : P = ⊥
· subst hP0
rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]
have hspan0 : span ({ x } : Set R) ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp hx0
have span_le := (Ideal.span_singleton_le_iff_mem _).mpr x_mem
refine
associated_iff_eq.mp
((associated_iff_normalizedFactors_eq_normalizedFactors hP0 hspan0).mpr
(le_antisymm ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 hspan0).mp ?_) ?_))
· rwa [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
simp only [normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, normalize_eq,
Multiset.le_iff_count, Multiset.count_singleton]
intro Q
split_ifs with hQ
· subst hQ
refine (Ideal.count_normalizedFactors_eq ?_ ?_).le <;> simp only [Ideal.span_singleton_le_iff_mem, pow_one] <;>
assumption
by_cases hQp : IsPrime Q
· refine (Ideal.count_normalizedFactors_eq ?_ ?_).le <;> simp [Ideal.span_singleton_le_iff_mem]
exact hxQ _ hQp hQ
·
exact
(Multiset.count_eq_zero.mpr fun hQi =>
hQp (isPrime_of_prime (irreducible_iff_prime.mp (irreducible_of_normalized_factor _ hQi)))).le
