awayToSection — Mathlib

English

Canonical map from the away- localization to global sections on Proj 𝒜 is defined.

Русский

Каноническое отображение из Away 𝒜 f в Γ(Proj 𝒜, D₊(f)) определено.

LaTeX

$$awayToSection : CommRingCat.of (Away 𝒜 f) ⟶ Γ(Proj 𝒜, basicOpen 𝒜 f)$$

Lean4

/-- The canonical map `(A_f)₀ ⟶ Γ(Proj A, D₊(f))`.
This is an isomorphism when `f` is homogeneous of positive degree. See `basicOpenIsoAway` below. -/
def awayToSection : CommRingCat.of (Away 𝒜 f) ⟶ Γ(Proj 𝒜, basicOpen 𝒜 f) :=
  ProjectiveSpectrum.Proj.awayToSection ..

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