English
If X is reduced and the underlying space is irreducible, then X is integral.
Русский
Если X редуцирована и основанное пространство неприводимо, то X интегральна.
LaTeX
$$$\text{IsReduced}(X) \wedge \operatorname{IrreducibleSpace}( |X| ) \Rightarrow \text{IsIntegral}(X)$$$
Lean4
instance irreducibleSpace_of_isIntegral [IsIntegral X] : IrreducibleSpace X :=
by
by_contra H
replace H : ¬IsPreirreducible (⊤ : Set X) := fun h =>
H { toPreirreducibleSpace := ⟨h⟩
toNonempty := inferInstance }
simp_rw [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at H
rcases H with ⟨S, T, hS, hT, h₁, h₂, h₃⟩
rw [Set.not_top_subset] at h₂ h₃
haveI : Nonempty (⟨Sᶜ, hS.1⟩ : X.Opens) := ⟨⟨_, h₂.choose_spec⟩⟩
haveI : Nonempty (⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, h₃.choose_spec⟩⟩
haveI : Nonempty (⟨Sᶜ, hS.1⟩ ⊔ ⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, Or.inl h₂.choose_spec⟩⟩
let e : Γ(X, _) ≅ CommRingCat.of _ :=
(X.sheaf.isProductOfDisjoint ⟨_, hS.1⟩ ⟨_, hT.1⟩ ?_).conePointUniqueUpToIso (CommRingCat.prodFanIsLimit _ _)
· have : IsDomain (Γ(X, ⟨Sᶜ, hS.1⟩) × Γ(X, ⟨Tᶜ, hT.1⟩)) := e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
exact false_of_nontrivial_of_product_domain Γ(X, ⟨Sᶜ, hS.1⟩) Γ(X, ⟨Tᶜ, hT.1⟩)
· ext x
constructor
· rintro ⟨hS, hT⟩
rcases h₁ (show x ∈ ⊤ by trivial) with h | h
exacts [hS h, hT h]
· simp
