English
Let f: X → Y be an open immersion, Y integral, and X nonempty. Then X is integral.
Русский
Пусть f: X → Y является открытым вложением, Y интегральна и X непусто. Тогда X интегральна.
LaTeX
$$$\text{IsOpenImmersion}(f) \wedge \text{IsIntegral}(Y) \wedge \text{Nonempty}(X) \Rightarrow \text{IsIntegral}(X)$$$
Lean4
theorem isIntegral_of_irreducibleSpace_of_isReduced [IsReduced X] [H : IrreducibleSpace X] : IsIntegral X :=
by
constructor; · infer_instance
intro U hU
haveI := (@LocallyRingedSpace.component_nontrivial X.toLocallyRingedSpace U hU).1
have : NoZeroDivisors (X.toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.obj (op U)) :=
by
refine ⟨fun {a b} e => ?_⟩
simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]
by_contra! h
obtain ⟨x, ⟨hxU, hx₁⟩, _, hx₂⟩ := nonempty_preirreducible_inter (X.basicOpen a).2 (X.basicOpen b).2 h.1 h.2
replace e := congr_arg (X.presheaf.germ U x hxU) e
rw [RingHom.map_mul, RingHom.map_zero] at e
refine zero_ne_one' (X.presheaf.stalk x) (isUnit_zero_iff.1 ?_)
convert hx₁.mul hx₂
exact e.symm
exact NoZeroDivisors.to_isDomain _