English
For f ∈ A, the basic open in the projective spectrum equals the supremum of the basic opens of the projections GradedAlgebra.proj 𝒜 i f.
Русский
Для f ∈ A базовое открытое множество в проективном спектре равно супремусу базовых открытых после проекции на степень i.
LaTeX
$$$\operatorname{basicOpen} 𝒜 f = \bigsqcup_{i \in \mathbb{N}} \operatorname{basicOpen} 𝒜 (\operatorname{GradedAlgebra.proj} 𝒜 i f)$$$
Lean4
theorem basicOpen_eq_union_of_projection (f : A) : basicOpen 𝒜 f = ⨆ i : ℕ, basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f) :=
TopologicalSpace.Opens.ext <|
Set.ext fun z => by
rw [mem_coe_basicOpen, mem_coe, iSup, TopologicalSpace.Opens.mem_sSup]
constructor <;> intro hz
· rcases
show ∃ i, GradedAlgebra.proj 𝒜 i f ∉ z.asHomogeneousIdeal
by
contrapose! hz with H
classical
rw [← DirectSum.sum_support_decompose 𝒜 f]
apply Ideal.sum_mem _ fun i _ => H i with
⟨i, hi⟩
exact ⟨basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩
· obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
exact fun rid => hz (z.1.2 i rid)
