finiteType_iff_fg — Mathlib

English

A monoid M is finitely generated iff MonoidAlgebra R M is of finite type.

Русский

Моноид M конечен порождён тогда и только тогда, когда MonoidAlgebra R M конечного типа.

LaTeX

$$$\\mathrm{FiniteType}(R,\\mathrm{MonoidAlgebra}(R,M)) \\iff \\mathrm{FG}(M)$$$

Lean4

/-- A monoid `M` is finitely generated if and only if `MonoidAlgebra R M` is of finite type. -/
theorem finiteType_iff_fg [CommRing R] [Nontrivial R] : FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M :=
  ⟨fun h => Monoid.fg_iff_add_fg.2 <| AddMonoidAlgebra.finiteType_iff_fg.1 <| h.equiv <| toAdditiveAlgEquiv R M,
    fun h => @MonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩

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