English
In a graded algebra with finite type, there exists a finite set of elements s in S such that S is generated by s over the base 𝒜0 and every element of s is homogeneous.
Русский
В градуированной алгебре с конечным типом существует конечный набор элементов в S, такой что S порождается над базой 𝒜0 набором этих элементов, и каждый элемент множества является однородным.
LaTeX
$$$\\exists s: Finset\,S,\\ Algebra.adjoin (A:=S) (𝒜 0) s = ⊤ \\wedge \\forall i \\in s,\\ SetLike.IsHomogeneousElem\\ 𝒜 i$$$
Lean4
theorem exists_finset_adjoin_eq_top_and_homogeneous :
∃ s : Finset S, Algebra.adjoin (A := S) (𝒜 0) s = ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i := by
classical
obtain ⟨F, hF⟩ := Algebra.FiniteType.out (R := 𝒜 0) (A := S)
let ι₀ := Σ (x : F), (DirectSum.decompose 𝒜 x.1).support
let x (i : ι₀) : S := ((DirectSum.decompose 𝒜) i.1 i.2).1
refine ⟨Finset.univ.image x, ?_, by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩⟩
rw [← top_le_iff, ← hF, Algebra.adjoin_le_iff]
intro s hs
rw [← DirectSum.sum_support_decompose 𝒜 s]
exact sum_mem fun n hn ↦ Algebra.subset_adjoin (by simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩)
