projIsoSpec — Mathlib

English

There is a canonical isomorphism between the projective spectrum restricted to a basic open D(f) and the affine scheme Spec of A⁰_f.

Русский

Существует канонический изоморфизм между ограниченным проективным спектром на D(f) и аффинным спектром Spec(A⁰_f).

LaTeX

$$$$(\mathrm{Proj}\;|\;pbo\;f) \cong \mathrm{Spec}(A⁰_f)$$$$

Lean4

/-- If `f ∈ A` is a homogeneous element of positive degree, then the projective spectrum restricted to
`D(f)` as a locally ringed space is isomorphic to `Spec A⁰_f`.
-/
def projIsoSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : (Proj| pbo f) ≅ (Spec (A⁰_ f)) :=
  @asIso _ _ _ _ (f := toSpec 𝒜 f) (isIso_toSpec 𝒜 f f_deg hm)

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