English
An integral domain is a DVR iff it is a PID with a unique non-zero prime ideal.
Русский
Цельная область является DVR тогда и только тогда, когда она является PID с уникальным ненулевым простым идеалом.
LaTeX
$$$IsDiscreteValuationRing R \;\iff\; IsPrincipalIdealRing R \land \exists! P: Ideal R, P \neq \bot \land IsPrime P$$$
Lean4
/-- An integral domain is a DVR iff it's a PID with a unique non-zero prime ideal. -/
theorem iff_pid_with_one_nonzero_prime (R : Type u) [CommRing R] [IsDomain R] :
IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ IsPrime P :=
by
constructor
· intro RDVR
rcases id RDVR with ⟨Rlocal⟩
constructor
· assumption
use IsLocalRing.maximalIdeal R
constructor
· exact ⟨Rlocal, inferInstance⟩
· rintro Q ⟨hQ1, hQ2⟩
obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1
have hq : q ≠ 0 := by
rintro rfl
apply hQ1
simp
rw [submodule_span_eq, span_singleton_prime hq] at hQ2
replace hQ2 := hQ2.irreducible
rw [irreducible_iff_uniformizer] at hQ2
exact hQ2.symm
· rintro ⟨RPID, Punique⟩
haveI : IsLocalRing R := IsLocalRing.of_unique_nonzero_prime Punique
refine { not_a_field' := ?_ }
rcases Punique with ⟨P, ⟨hP1, hP2⟩, _⟩
have hPM : P ≤ maximalIdeal R := le_maximalIdeal hP2.1
intro h
rw [h, le_bot_iff] at hPM
exact hP1 hPM
