toΓSpecCBasicOpens — Mathlib

English

The preimage of the zero locus under the canonical map to Spec Γ(X) agrees with the zero locus in X.

Русский

Предобраз нулевой локус under канонического отображения совпадает с нулевой локус в X.

LaTeX

$$$X.toΓSpec.base^{-1} (PrimeSpectrum.zeroLocus(s)) = X.toRingedSpace.zeroLocus(s)$$$

Lean4

/-- The sheaf hom on all basic opens, commuting with restrictions. -/
@[simps app]
def toΓSpecCBasicOpens :
    (inducedFunctor basicOpen).op ⋙ (structureSheaf (Γ.obj (op X))).1 ⟶
      (inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward _ X.toΓSpecBase).obj X.𝒪).1
    where
  app r := X.toΓSpecCApp r.unop
  naturality r s
    f := by
    apply (StructureSheaf.to_basicOpen_epi (Γ.obj (op X)) r.unop).1
    simp only [← Category.assoc]
    rw [X.toΓSpecCApp_spec r.unop]
    convert X.toΓSpecCApp_spec s.unop
    symm
    apply X.presheaf.map_comp

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