English
Let M, M' be monoids. If P ≤ M is FG and e: M →* M' is injective and (P.map e) is FG, then P is FG.
Русский
Пусть M, M' — моноиды. Если P — FG подмножество M и e: M →* M' инъективен, а P.map e — FG, то P — FG.
LaTeX
$$$\forall M M' [Monoid M'] {P : Submonoid M} (e : M \rightarrow* M') (he : Function.Injective e) (h : (P.map e).FG), P.FG$$$
Lean4
@[to_additive]
theorem map_injective {M' : Type*} [Monoid M'] {P : Submonoid M} (e : M →* M') (he : Function.Injective e)
(h : (P.map e).FG) : P.FG := by
obtain ⟨s, hs⟩ := h
use s.preimage e he.injOn
apply Submonoid.map_injective_of_injective he
rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
congr
rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs, MonoidHom.mrange_eq_map e]
exact Submonoid.monotone_map le_top
