isClosed_supportSet — Mathlib

English

The support set of an ideal sheaf is a closed subset of the scheme.

Русский

Поддержка идеального слоя является замкнутым подмножеством схемы.

LaTeX

$$IsClosed(I.suppportSet)$$

Lean4

theorem isClosed_supportSet (I : IdealSheafData X) : IsClosed I.supportSet :=
  by
  rw [TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage (iSup_affineOpens_eq_top X)]
  intro U
  refine ⟨(X.zeroLocus (U := U.1) (I.ideal U))ᶜ, (X.zeroLocus_isClosed _).isOpen_compl, ?_⟩
  simp only [Set.preimage_compl, compl_inj_iff]
  apply Subtype.val_injective.image_injective
  simp [Set.image_preimage_eq_inter_range, I.supportSet_inter]

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