English
The affine open cover of Proj 𝒜 is constructed from a spanning set of the irrelevant ideal via basic opens on graded projections.
Русский
Аффинное открытое покрытие Proj 𝒜 строится из порождающего набора неррелевантного идеала через базовые открытые множества проекций градуированной алгебры.
LaTeX
$$AffineOpenCover 𝒜 := affineOpenCoverOfIrrelevantLESpan 𝒜 ...$$
Lean4
/-- `Proj A` is covered by `Spec (A_f)₀` for all homogeneous elements of positive degree. -/
noncomputable def affineOpenCover : (Proj 𝒜).AffineOpenCover :=
affineOpenCoverOfIrrelevantLESpan 𝒜 (ι := Σ i : PNat, 𝒜 i) (m := fun i ↦ i.1) (fun i ↦ i.2) (fun i ↦ i.2.2)
(fun i ↦ i.1.2) <|
by
classical
intro z hz
rw [← DirectSum.sum_support_decompose 𝒜 z]
refine
Ideal.sum_mem _ fun c hc ↦
if hc0 : c = 0 then ?_ else Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩
convert Ideal.zero_mem _
subst hc0
exact hz
