isAffineOpen_basicOpen — Mathlib

English

Each basic open D_+(f) is an affine open subset of Proj 𝒜 when f is homogeneous of positive degree.

Русский

Каждый базовый открытый D_+(f) является аффинной открытой подсистемой Proj 𝒜, когда f однороден и имеет положительную степень.

LaTeX

$$IsAffineOpen (basicOpen 𝒜 f)$$

Lean4

theorem isAffineOpen_basicOpen : IsAffineOpen (basicOpen 𝒜 f) :=
  by
  rw [← opensRange_awayι 𝒜 f f_deg hm]
  exact isAffineOpen_opensRange (awayι _ _ _ _)

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