basicOpenToSpec — Mathlib

English

The canonical map D₊(f) → Spec Away 𝒜 f is defined and is a morphism of schemes.

Русский

Канонический отображение D₊(f) → Spec Away 𝒜 f задано и является морфизмом схем.

LaTeX

$$basicOpenToSpec : (basicOpen 𝒜 f).toScheme ⟶ Spec (.of <| Away 𝒜 f)$$

Lean4

/-- The canonical map `Proj A |_ D₊(f) ⟶ Spec (A_f)₀`.
This is an isomorphism when `f` is homogeneous of positive degree. See `basicOpenIsoSpec` below. -/
noncomputable def basicOpenToSpec : (basicOpen 𝒜 f).toScheme ⟶ Spec (.of <| Away 𝒜 f) :=
  (basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f)

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