iSup_basicOpen_eq_top — Mathlib

English

If a finite family of elements are irrelevant, their D₊-opens cover Proj 𝒜.

Русский

Если конечная совокупность элементов порождает нерелевантную идеалу, их D₊-открытые покрывают Proj 𝒜.

LaTeX

$$iSup_basicOpen_eq_top : ⨆ i, Proj.basicOpen 𝒜 (f i) = ⊤$$

Lean4

/-- If `{ xᵢ }` spans the irrelevant ideal of `A`, then `D₊(xᵢ)` covers `Proj A`. -/
theorem iSup_basicOpen_eq_top {ι : Type*} (f : ι → A)
    (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)) : ⨆ i, Proj.basicOpen 𝒜 (f i) = ⊤ := by
  classical
  refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
  by_contra! H
  simp only [mem_basicOpen, Decidable.not_not] at H
  refine x.not_irrelevant_le (hf.trans ?_)
  rwa [Ideal.span_le, Set.range_subset_iff]

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