fg_of_surjective — Mathlib

English

If f: M →* M' is a surjective monoid hom and M is finitely generated, then M' is finitely generated.

Русский

Если непрерывно отображающий моноид f: M →* M' сюръективен и M конечно порожден, то M' конечно порожден.

LaTeX

$$$\forall {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M \rightarrow* M') (hf : Function.Surjective f), Monoid.FG M'$$$

Lean4

@[to_additive]
theorem fg_of_surjective {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M') (hf : Function.Surjective f) :
    Monoid.FG M' := by
  classical
  obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
  use s.image f
  rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map, MonoidHom.mrange_eq_top]

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