basicOpen_eq_iSup_proj — Mathlib

English

For a graded algebra 𝒜 and an element f ∈ A, the basic open in Proj 𝒜 associated to f equals the supremum over all degrees i of the basic opens corresponding to the graded projection of f to degree i.

Русский

Для градуированной алгебры 𝒜 и элемента f ∈ A верно: basicOpen 𝒜 f = ⨆ i, basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f).

LaTeX

$$$\\operatorname{basicOpen}\\ 𝒜 f = \\bigvee_{i:\\mathbb{N}} \\operatorname{basicOpen}\\ 𝒜 (\\operatorname{GradedAlgebra.proj} 𝒜 i\\ f)$$$

Lean4

theorem basicOpen_eq_iSup_proj (f : A) : basicOpen 𝒜 f = ⨆ i : ℕ, basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f) :=
  ProjectiveSpectrum.basicOpen_eq_union_of_projection ..

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