English
There exists a finite set of homogeneous generators such that each generator lies in some nonzero homogeneous component 𝒜n with n ≠ 0.
Русский
Существует конечный набор однородных порождающих, каждый элемент которого лежит в некотором ненулевом однородном компоненте 𝒜n при n ≠ 0.
LaTeX
$$$\\exists s: Finset\,S,\\ Algebra.adjoin (A:=S) (𝒜 0) s = ⊤ \\wedge \\forall i\\in s,\\ \\exists n \\neq 0,\\ i\\in 𝒜 n$$$
Lean4
theorem exists_finset_adjoin_eq_top_and_homogeneous_ne_zero :
∃ s : Finset S, Algebra.adjoin (A := S) (𝒜 0) s = ⊤ ∧ ∀ i ∈ s, ∃ n ≠ 0, i ∈ 𝒜 n :=
by
obtain ⟨s, h₁, h₂⟩ := exists_finset_adjoin_eq_top_and_homogeneous 𝒜
choose! n hn using h₂
refine ⟨s.filter (n · ≠ 0), ?_, by simpa using fun i hi hin ↦ ⟨n i, hin, hn i hi⟩⟩
rw [← top_le_iff, ← h₁, Algebra.adjoin_le_iff]
rintro i hi
by_cases hi0 : n i = 0
· exact Subalgebra.algebraMap_mem (Algebra.adjoin (𝒜 0) (s.filter (n · ≠ 0)).toSet) ⟨i, hi0 ▸ hn i hi⟩
· exact Algebra.subset_adjoin (by simpa [hi0] using hi)
