awayι — Mathlib

English

There is an open immersion of schemes from Spec Away 𝒜 f into Proj 𝒜, realized by the basic open embedding.

Русский

Существует открытое вложение схемs из Spec Away 𝒜 f в Proj 𝒜, реализованное базовым открытым вложением.

LaTeX

$$$\operatorname{Spec} (\mathrm{Away}\, 𝒜 f) \hookrightarrow \operatorname{Proj}(\mathcal{A})$$$

Lean4

/-- The open immersion `Spec (A_f)₀ ⟶ Proj A`. -/
noncomputable def awayι : Spec (.of <| Away 𝒜 f) ⟶ Proj 𝒜 :=
  (basicOpenIsoSpec 𝒜 f f_deg hm).inv ≫ (Proj.basicOpen 𝒜 f).ι

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