Gordan's lemma for dual semigroups

The integral characters nonnegative on a lattice-rational cone form a finitely generated additive monoid. Neither salience nor regularity is needed. This gives finite monomial generating families for the coordinate rings of arbitrary affine toric cones.

A finite lattice generating family for the cone identifies its dual semigroup with the preimage of the nonnegative integer vectors under evaluation. The character lattice is finitely generated, and AddSubmonoid.FG.comap proves finite generation of this preimage using natural slack variables and Mathlib's equalizer form of Gordan's lemma.

Main declarations

• TauCeti.Toric.IsLatticeRational.fg_dualSemigroup: Gordan's lemma without salience.
• TauCeti.Toric.IsToricCone.fg_dualSemigroup: the dual semigroup of every toric cone is finitely generated.

References

• W. Fulton, Introduction to Toric Varieties, §1.2, Proposition 1.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §1.2, Proposition 1.2.17.

theorem TauCeti.Toric.IsLatticeRational.fg_dualSemigroup {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hσ : IsLatticeRational i σ) (hi : IsIntegralLattice i) : AddMonoid.FG ↥(dualSemigroup hi σ)

Gordan's lemma. The dual semigroup of a lattice-rational cone in an integral lattice is finitely generated. Salience is not required.

theorem TauCeti.Toric.IsToricCone.fg_dualSemigroup {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hσ : IsToricCone i σ) (hi : IsIntegralLattice i) : AddMonoid.FG ↥(dualSemigroup hi σ)

The dual semigroup of every toric cone in an integral lattice is finitely generated.