English
The image of m in MonoidAlgebra lies in the span of the image of S iff m ∈ S (MonoidAlgebra version).
Русский
Образ m в MonoidAlgebra лежит в span образов S тогда и только тогда, когда m ∈ S.
LaTeX
$$$\\mathrm{of}_R M m \\in \\operatorname{span}_R(\\mathrm{Set.image}(\\mathrm{MonoidHom.instFunLike.coe}(\\mathrm{MonoidAlgebra.of R M}), S)) \\iff m \\in S$$$
Lean4
/-- If a set `S` generates a monoid `M`, then the image of `M` generates, as algebra,
`MonoidAlgebra R M`. -/
theorem mvPolynomial_aeval_of_surjective_of_closure [CommMonoid M] [CommSemiring R] {S : Set M} (hS : closure S = ⊤) :
Function.Surjective (MvPolynomial.aeval fun s : S => of R M ↑s : MvPolynomial S R → MonoidAlgebra R M) :=
by
intro f
induction f using induction_on with
| hM m =>
have : m ∈ closure S := hS.symm ▸ mem_top _
refine Submonoid.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]⟩
| 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 _ _ _⟩
