English
For a domain R, PrimeSpectrum(R) is T1 if and only if R is a field.
Русский
Для домена R спектр примар является T1 тогда и только тогда, когда R является полем.
LaTeX
$$$\\operatorname{T1Space}(\\operatorname{PrimeSpectrum}(R)) \\iff \\operatorname{IsField}(R)$$$
Lean4
theorem t1Space_iff_isField [IsDomain R] : T1Space (PrimeSpectrum R) ↔ IsField R :=
by
refine ⟨?_, fun h => ?_⟩
· intro h
have hbot : Ideal.IsPrime (⊥ : Ideal R) := Ideal.bot_prime
exact
Classical.not_not.1
(mt (Ring.ne_bot_of_isMaximal_of_not_isField <| (isClosed_singleton_iff_isMaximal _).1 (T1Space.t1 ⟨⊥, hbot⟩))
(by simp))
· refine ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩
by_cases hx : x.asIdeal = ⊥
· letI := h.toSemifield
exact hx.symm ▸ Ideal.bot_isMaximal
· exact absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)
