finiteType_of_monoid_fg — Mathlib

English

If M is finitely generated as a monoid, then S is of finite type over R after localization.

Русский

Если M конечно порожден как моноид, то локализация S над R имеет конечный тип.

LaTeX

$$$[Monoid.FG M] \Rightarrow \ Algebra.FiniteType R S$$$

Lean4

theorem finiteType_of_monoid_fg [Monoid.FG M] : Algebra.FiniteType R S :=
  by
  have := Monoid.fg_of_surjective _ (toInvSubmonoid_surjective M S)
  rw [Monoid.fg_iff_submonoid_fg] at this
  rcases this with ⟨s, hs⟩
  refine ⟨⟨s, ?_⟩⟩
  rw [eq_top_iff]
  rintro x -
  change x ∈ (Subalgebra.toSubmodule (Algebra.adjoin R _ : Subalgebra R S) : Set S)
  rw [Algebra.adjoin_eq_span, hs, span_invSubmonoid]
  trivial

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