Affine monoids embed into ℤⁿ

This file proves that finitely generated cancellative torsion-free commutative monoids embed into ℤⁿ for some n.

@[reducible, inline]

noncomputable abbrev AffineAddMonoid.dim (M : Type u_1) [AddCancelCommMonoid M] : ℕ

The dimension of an affine monoid M, namely the minimum n for which M embeds into ℤⁿ.

Equations

• AffineAddMonoid.dim M = Module.finrank ℤ (Algebra.GrothendieckAddGroup M)

noncomputable def AffineAddMonoid.embedding (M : Type u_1) [AddCancelCommMonoid M] [AddMonoid.FG M] [HasUniqueDiv M] : M →+ FreeAbelianGroup (Fin (dim M))

An arbitrary embedding of an affine monoid M into ℤ ^ dim M.

Equations

• One or more equations did not get rendered due to their size.

theorem AffineAddMonoid.embedding_injective {M : Type u_1} [AddCancelCommMonoid M] [AddMonoid.FG M] [HasUniqueDiv M] : Function.Injective ⇑(embedding M)