English
If S generates M, the lift from the free algebra on S to the monoid algebra R[M] is surjective.
Русский
Если S порождает M, то отображение из свободной алгебры на S в R[M] сюръективно.
LaTeX
$$$\\mathrm{FreeAlgebra.lift}\\;\\Rightarrow\\text{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 → 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 ⟨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]; 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 _ _ _⟩
