isReduced_of_isReduced_stalk — Mathlib

English

The carrier of a scheme carries a T0 space structure.

Русский

Носитель схемы несёт структуру T0-пространства.

LaTeX

$$T0Space X.carrier.carrier$$

Lean4

theorem isReduced_of_isReduced_stalk [∀ x : X, _root_.IsReduced (X.presheaf.stalk x)] : IsReduced X :=
  by
  refine ⟨fun U => ⟨fun s hs => ?_⟩⟩
  apply Presheaf.section_ext X.sheaf U s 0
  intro x hx
  change (X.sheaf.presheaf.germ U x hx) s = (X.sheaf.presheaf.germ U x hx) 0
  rw [RingHom.map_zero]
  change X.presheaf.germ U x hx s = 0
  exact (hs.map _).eq_zero

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