Preimages of finitely generated additive submonoids

The preimage of a finitely generated additive submonoid under a homomorphism from a finitely generated commutative monoid is finitely generated, provided the target is cancellative. In particular, finitely many integral linear inequalities on a finitely generated abelian group define a finitely generated additive submonoid: nonnegative integer vectors are the image of a finite product of naturals under coordinatewise casting.

The construction uses Mathlib's AddSubmonoid.fg_iff_exists_fin_addMonoidHom to parametrize both monoids by finite products of naturals, and AddSubmonoid.fg_eqLocusM to impose equality of their images. This is the slack-variable form of Gordan's lemma.

References

• D. Cox, J. Little and H. Schenck, Toric Varieties, §1.2, Gordan's lemma.

theorem AddSubmonoid.FG.comap {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommMonoid G] [IsCancelAdd G] [AddMonoid.FG M] {P : AddSubmonoid G} (hP : P.FG) (f : M →+ G) : (AddSubmonoid.comap f P).FG

The preimage of a finitely generated additive submonoid of a cancellative commutative monoid is finitely generated when the source monoid is finitely generated.