subschemeCover — Mathlib

English

simp version of the range equality: the closed-support description coincides with the range of the base map.

Русский

упрощённая версия равенства образа: замыкание поддержки совпадает с образом базового отображения.

LaTeX

$$$\text{Eq}(\operatorname{Top.closedSet} \text{(I.subschemeι.base)}) = \text{Supp}(I)$$$

Lean4

/-- The subscheme associated to an ideal sheaf `I` is covered by `Spec(Γ(X, U)/I(U))`. -/
noncomputable def subschemeCover : I.subscheme.AffineOpenCover
    where
  I₀ := X.affineOpens
  X U := .of <| Γ(X, U) ⧸ I.ideal U
  f U := I.glueData.ι U ≫ I.subschemeIso.inv
  idx x := (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X)).idx x.1
  covers
    x := by
    let U := (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X)).idx x.1
    obtain ⟨⟨y, hy : y ∈ U.1⟩, rfl : y = x.1⟩ := (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X)).covers x.1
    exact (I.opensRange_glueData_ι_subschemeIso_inv U).ge hy

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