English
If S generates an additive monoid M, the lift from FreeAlgebra on S to MonoidAlgebra R M is surjective.
Русский
Если S порождает аддитивный моноид M, то отображение FreeAlgebra(R,S) → MonoidAlgebra(R,M) сюръективно.
LaTeX
$$$\\mathrm{FreeAlgebra.lift}\\;\\Rightarrow\\mathrm{surjective}$$$
Lean4
/-- If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra,
`R[M]`. -/
theorem freeAlgebra_lift_of_surjective_of_closure [CommSemiring R] {S : Set M} (hS : closure S = ⊤) :
Function.Surjective (FreeAlgebra.lift R fun s : S => of R M ↑s : FreeAlgebra R S → 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 ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
· 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 _ _ _⟩
