finiteType_of_fg — Mathlib

English

If the additive monoid M is finitely generated, then the monoid algebra R[M] is a finite type R-algebra.

Русский

Если аддитивный моноид M конечного типа, то моноидная алгебра R[M] конечного типа над R.

LaTeX

$$$\\text{FG}(M) \\Rightarrow \\mathrm{FiniteType}(R,R[M])$$$

Lean4

/-- If an additive monoid `M` is finitely generated then `R[M]` is of finite
type. -/
instance finiteType_of_fg [CommRing R] [h : AddMonoid.FG M] : FiniteType R R[M] :=
  by
  obtain ⟨S, hS⟩ := h.fg_top
  exact
    .of_surjective (FreeAlgebra.lift R fun s : (S : Set M) => of' R M ↑s) (freeAlgebra_lift_of_surjective_of_closure hS)

Похожие утверждения