English
As above, the open cover defined by images of homogeneous elements of positive degree yields an open cover of X when the irrelevant ideal maps to the whole ring.
Русский
Как выше, открытое покрытие, заданное образами однородных элементов положительной степени, образует открытое покрытие X, когда нерелевантный идеал инвариантно отображается на все кольцо.
LaTeX
$$$ openCoverOfMapIrrelevantEqTop 𝒜 f hf : X.OpenCover $$$
Lean4
/-- Given a graded ring `A` and a map `f : A →+* Γ(X, ⊤)` such that the image of the
irrelevant ideal under `f` generates the whole ring, the set of `D(f(r))` for homogeneous `r`
of positive degree forms an open cover on `X`. -/
def openCoverOfMapIrrelevantEqTop : X.OpenCover :=
X.openCoverOfIsOpenCover (fun ir : Σ' i r, 0 < i ∧ r ∈ 𝒜 i ↦ X.basicOpen (f ir.2.1))
(by
classical
have H :
Ideal.span (Set.range fun x : Σ' i r, 0 < i ∧ r ∈ 𝒜 i ↦ x.2.1) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal :=
by
apply le_antisymm
· rw [Ideal.span_le, Set.range_subset_iff]
rintro ⟨i, r, hi0, hri⟩
simp [-ZeroMemClass.coe_eq_zero, DirectSum.decompose_of_mem_ne 𝒜 hri hi0.ne']
· intro x hx
rw [← DirectSum.sum_support_decompose 𝒜 x]
refine Ideal.sum_mem _ fun c hc ↦ ?_
have : c ≠ 0 := by contrapose! hc; simpa [hc] using hx
exact Ideal.subset_span ⟨⟨c, _, this.bot_lt, by simp⟩, rfl⟩
ext1
apply compl_injective
simp only [TopologicalSpace.Opens.coe_iSup, Set.compl_iUnion, ← Scheme.zeroLocus_singleton,
← Scheme.zeroLocus_iUnion, Set.iUnion_singleton_eq_range, TopologicalSpace.Opens.coe_top, Set.compl_univ]
rw [← Scheme.zeroLocus_span, Set.range_comp', ← Ideal.map_span, H, hf]
simp)
