Documentation

Mathlib.Algebra.AffineMonoid.Embedding

Affine monoids embed into ℤⁿ #

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

source
🔸 coverage
@[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
    Instances For
      source
      🔸 coverage
      noncomputable def AffineAddMonoid.embedding (M : Type u_1) [AddCancelCommMonoid M] [AddMonoid.FG M] [IsAddTorsionFree M] :
      M →+ FreeAbelianGroup (Fin (dim M))

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

      Equations
        Instances For
          source
          📐 coverage
          theorem AffineAddMonoid.embedding_injective {M : Type u_1} [AddCancelCommMonoid M] [AddMonoid.FG M] [IsAddTorsionFree M] :
          Function.Injective ⇑(embedding M)