basicOpen

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Proj.basicOpen

English

The basicOpenToSpec map from basicOpen 𝒜 f to Spec Away 𝒜 f is a natural morphism of schemes.

Русский

Гомоморфизм basicOpenToSpec является morphism-ом схемы между D₊(f) и Spec Away f.

LaTeX

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

Lean4

/-- The basic open set `D₊(f)` associated to `f : A`. -/
def basicOpen : (Proj 𝒜).Opens :=
  ProjectiveSpectrum.basicOpen 𝒜 f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru