Graded algebras of finite type

We show that graded algebras of finite type are generated by homogeneous elements of positive degree.

theorem GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous {R₀ : Type u_1} {ι : Type u_2} {S : Type u_3} [DecidableEq ι] [AddCommMonoid ι] [CommRing R₀] [CommRing S] [Algebra R₀ S] (𝒜 : ι → Submodule R₀ S) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) S] : ∃ (s : Finset S), Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i

theorem GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero {R₀ : Type u_1} {ι : Type u_2} {S : Type u_3} [DecidableEq ι] [AddCommMonoid ι] [CommRing R₀] [CommRing S] [Algebra R₀ S] (𝒜 : ι → Submodule R₀ S) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) S] : ∃ (s : Finset S), Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n