English
A variant where the f_i generate modulo the zero-degree part; the supremum equals the top open.
Русский
Вариант, где f_i порождают порождающее посредством нулевого града; верхняя граница покрывает Proj.
LaTeX
$$iSup_basicOpen_eq_top' : ... equals top under hypotheses.$$
Lean4
/-- If `{ xᵢ }` are homogeneous and span `A` as an `A₀` algebra, then `D₊(xᵢ)` covers `Proj A`. -/
theorem iSup_basicOpen_eq_top' {ι : Type*} (f : ι → A) (hfn : ∀ i, ∃ n, f i ∈ 𝒜 n)
(hf : Algebra.adjoin (𝒜 0) (Set.range f) = ⊤) : ⨆ i, Proj.basicOpen 𝒜 (f i) = ⊤ := by
classical
apply Proj.iSup_basicOpen_eq_top
intro x hx
convert_to x - GradedRing.projZeroRingHom 𝒜 x ∈ _
·
rw [GradedRing.projZeroRingHom_apply, ← GradedRing.proj_apply, (HomogeneousIdeal.mem_irrelevant_iff _ _).mp hx,
sub_zero]
clear hx
have := (eq_iff_iff.mp congr(x ∈ $hf)).mpr trivial
induction this using Algebra.adjoin_induction with
| mem x hx =>
obtain ⟨i, rfl⟩ := hx
obtain ⟨n, hn⟩ := hfn i
rw [GradedRing.projZeroRingHom_apply]
by_cases hn' : n = 0
· rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]
exact zero_mem _
· rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]
exact Ideal.subset_span ⟨_, rfl⟩
| algebraMap r =>
convert zero_mem (Ideal.span _)
rw [sub_eq_zero]
exact (DirectSum.decompose_of_mem_same 𝒜 r.2).symm
| add x y hx hy _ _ =>
rw [map_add, add_sub_add_comm]
exact add_mem ‹_› ‹_›
| mul x y hx hy hx'
hy' =>
convert add_mem (Ideal.mul_mem_left _ x hy') (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx') using 1
rw [map_mul]
ring
