isIntegral_of_irreducibleSpace_of_isReduced

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 _

Похожие утверждения