English
If S generates an additive monoid M, then the evaluation map from the free polynomial algebra on S to R[M] is surjective.
Русский
Если S порождает аддитивный моноид M, то диагональная (aeval) карта из свободной полиномиальной алгебры на S в R[M] сюръективна.
LaTeX
$$$\\mathrm{mvPolynomial\\_aeval}\\;\\text{surjective}\\;\\text{given } closure(S)=\\top$$$
Lean4
/-- If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra,
`R[M]`. -/
theorem mvPolynomial_aeval_of_surjective_of_closure [AddCommMonoid M] [CommSemiring R] {S : Set M}
(hS : closure S = ⊤) : Function.Surjective (MvPolynomial.aeval fun s : S => of' R M ↑s : MvPolynomial S R → R[M]) :=
by
intro f
induction f using induction_on with
| hM m =>
have : m ∈ closure S := hS.symm ▸ mem_top _
refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
· exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
· exact ⟨1, map_one _⟩
· rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
exact ⟨P₁ * P₂, by rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]; rfl⟩
| hadd f g ihf ihg =>
rcases ihf with ⟨P, rfl⟩
rcases ihg with ⟨Q, rfl⟩
exact ⟨P + Q, map_add _ _ _⟩
| hsmul r f ih =>
rcases ih with ⟨P, rfl⟩
exact ⟨r • P, map_smul _ _ _⟩
