English
Let 𝒜 be a graded algebra generated by homogeneous elements v_i with degrees dv_i, and let f have degree d with f ∈ 𝒜 d. Then the algebra adjoin over 𝒜0 of the set { Away.mk 𝒜 hf a (∏ i v_i^{a_i}) } with the relation ∑ a_i dv_i = a d, and a_i ≤ d for all i, equals the whole algebra.
Русский
Пусть 𝒜 — градуированная алгебра, порождаемая над 𝒜0 гомогенными элементами v_i степеней dv_i, и пусть f имеет степень d. Тогда алгебра, порождаемая над 𝒜0 множеством элементов вида (∏_i v_i^{a_i}) / f^a с условием ∑ a_i dv_i = a d и дополнительно a_i ≤ d для всех i, порождает всю алгебру.
LaTeX
$$$$ \\text{Let } 𝒜 \\text{ be graded with } v_i \\in 𝒜_{dv_i} \\text{ and } f \\in 𝒜_d. \\\\ \\text{Then } \\operatorname{adjoin}_{𝒜_0}\\{\\text{Away.mk } 𝒜 hf a (\\prod_i v_i^{a_i}) \\,|\, (a:\\mathbb{N}), (a_i: ι' → \\mathbb{N}), (hai : \\sum_i a_i dv_i = a d), (∀ i, a_i ≤ d)\\} = 𝒜. $$$$
Lean4
/-- Let `𝒜` be a graded algebra, finitely generated (as an algebra) over `𝒜₀` by `{ vᵢ }`,
where `vᵢ` has degree `dvᵢ`.
If `f : A` has degree `d`, then `𝒜_(f)` is generated (as an algebra) over `𝒜₀` by
elements of the form `(∏ i, vᵢ ^ aᵢ) / fᵃ` such that `∑ aᵢ • dvᵢ = a • d` and `∀ i, aᵢ ≤ d`.
-/
theorem adjoin_mk_prod_pow_eq_top {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) (ι' : Type*) [Fintype ι'] (v : ι' → A)
(hx : Algebra.adjoin (𝒜 0) (Set.range v) = ⊤) (dv : ι' → ℕ) (hxd : ∀ i, v i ∈ 𝒜 (dv i)) :
Algebra.adjoin (𝒜 0)
{Away.mk 𝒜 hf a (∏ i, v i ^ ai i) (hai ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i) | (a : ℕ) (ai :
ι' → ℕ) (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ i, ai i ≤ d)} =
⊤ :=
by
classical
let s := Finset.univ.filter (0 < dv ·)
have :=
Away.adjoin_mk_prod_pow_eq_top_of_pos hf (ι' := s) (v ∘ Subtype.val) ?_ (dv ∘ Subtype.val) (fun _ ↦ hxd _)
(by simp [s])
swap
· rw [← top_le_iff, ← hx, Algebra.adjoin_le_iff, Set.range_subset_iff]
intro i
rcases (dv i).eq_zero_or_pos with hi | hi
· exact algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩
exact Algebra.subset_adjoin ⟨⟨i, by simpa [s] using hi⟩, rfl⟩
rw [← top_le_iff, ← this]
apply Algebra.adjoin_mono
rintro _ ⟨a, ai, hai : ∑ x ∈ s.attach, _ = _, h, rfl⟩
refine ⟨a, fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0, ?_, ?_, ?_⟩
· simpa [Finset.sum_attach_eq_sum_dite] using hai
· simp [apply_dite, dite_apply, h]
· congr 1
change _ = ∏ x ∈ s.attach, _
simp [Finset.prod_attach_eq_prod_dite]
