Toric ideals and the binomial presentation of semigroup algebras

Let a : ι → M be a family in an additive commutative monoid, and write A u = ∑ i, u i • a i (Finsupp.linearCombination ℕ a u) for the exponent map ℕ^(ι) → M. The toric ideal TauCeti.toricIdeal R a is the kernel of the R-algebra map MvPolynomial ι R → R[M] sending X i to the basis element single (a i) 1; this map sends the monomial c X^u to single (A u) c.

Over every commutative ring R, the toric ideal is generated by the binomials X^u - X^v with A u = A v. It is unchanged when M is replaced by a larger monoid, and its formation commutes with change of coefficients. If the a i generate M, then MvPolynomial ι R ⧸ toricIdeal R a is the semigroup algebra R[M]; in general it is the semigroup algebra of the submonoid AddSubmonoid.closure (Set.range a) generated by the a i. For finitely many exponents, a single finite family of binomials, with exponent pairs independent of R, generates the toric ideal over every commutative ring: such a family is selected over ℤ by noetherianity and transported to R by change of coefficients.

Main declarations

• TauCeti.coeff_aeval_single_linearCombination, TauCeti.coeff_aeval_single_of_notMem_range: the substitution X i ↦ single (a i) 1 moves the coefficient at u to A u when A is injective, and its coefficients vanish outside the image of A.
• TauCeti.toricIdeal: the kernel of X i ↦ single (a i) 1.
• TauCeti.toricIdeal_eq_span: it is generated by the binomials X^u - X^v with A u = A v.
• TauCeti.monomial_sub_monomial_mem_toricIdeal_iff: over a nontrivial ring, X^u - X^v lies in the toric ideal exactly when A u = A v.
• TauCeti.toricIdeal_comp_of_injective: the toric ideal does not depend on the ambient monoid.
• TauCeti.toricIdeal_eq_ker_aeval_monomial: for exponents in σ →₀ ℕ, the toric ideal is the kernel of X i ↦ X ^ (a i) into MvPolynomial σ R.
• TauCeti.map_toricIdeal: the toric ideal over S is the extension of the toric ideal over R along any ring homomorphism R →+* S.
• TauCeti.quotientToricIdealAlgEquiv: if the a i generate M, the quotient by the toric ideal is R[M].
• TauCeti.quotientToricIdealAlgEquivClosure: the quotient by the toric ideal is the semigroup algebra of the submonoid generated by the a i.
• TauCeti.exists_finset_toricIdeal_eq_span: for finite ι, finitely many binomials, with exponent pairs independent of the coefficient ring, generate the toric ideal over every commutative ring.

References

• B. Sturmfels, Gröbner Bases and Convex Polytopes, University Lecture Series 8, AMS, 1996, Chapter 4, Lemma 4.1.
• E. Miller and B. Sturmfels, Combinatorial Commutative Algebra, GTM 227, Springer, 2005, Chapter 7.

theorem TauCeti.aeval_single_eq_mapDomainAlgHom {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommSemiring R] (a : ι → M) : (MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single (a i) 1) = AddMonoidAlgebra.mapDomainAlgHom R R (Finsupp.linearCombination ℕ a).toAddMonoidHom

The R-algebra map MvPolynomial ι R → R[M] sending X i to single (a i) 1 is the map of monoid algebras induced by the exponent map u ↦ ∑ i, u i • a i.

@[simp]

theorem TauCeti.aeval_single_monomial {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommSemiring R] (a : ι → M) (u : ι →₀ ℕ) (c : R) : (MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single (a i) 1) ((MvPolynomial.monomial u) c) = AddMonoidAlgebra.single ((Finsupp.linearCombination ℕ a) u) c

The image of the monomial c X^u under X i ↦ single (a i) 1 is single (A u) c, where A u = ∑ i, u i • a i.

theorem TauCeti.coeff_aeval_single_linearCombination {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {R : Type u_4} [CommSemiring R] {a : ι → M} (ha : Function.Injective ⇑(Finsupp.linearCombination ℕ a)) (p : MvPolynomial ι R) (u : ι →₀ ℕ) : ((MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single (a i) 1) p).coeff ((Finsupp.linearCombination ℕ a) u) = p.coeff u

The substitution X i ↦ single (a i) 1 has coefficient p.coeff u at A u when A is injective.

theorem TauCeti.coeff_aeval_single_of_notMem_range {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {R : Type u_4} [CommSemiring R] {a : ι → M} (p : MvPolynomial ι R) {m : M} (hm : m ∉ Set.range ⇑(Finsupp.linearCombination ℕ a)) : ((MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single (a i) 1) p).coeff m = 0

The substitution X i ↦ single (a i) 1 has coefficient zero outside the image of A.

theorem TauCeti.aeval_single_surjective {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommSemiring R] {a : ι → M} (ha : AddSubmonoid.closure (Set.range a) = ⊤) : Function.Surjective ⇑(MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single (a i) 1)

If the a i generate M, then X i ↦ single (a i) 1 is surjective onto R[M]. This is AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, for the variables indexed by the family a rather than by the set of its values.

noncomputable def TauCeti.toricIdeal {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommSemiring R] (a : ι → M) : Ideal (MvPolynomial ι R)

The toric ideal of a family a : ι → M: the kernel of the R-algebra map MvPolynomial ι R → R[M] sending X i to the basis element single (a i) 1.

theorem TauCeti.mem_toricIdeal_iff {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {R : Type u_4} [CommSemiring R] {a : ι → M} {p : MvPolynomial ι R} : p ∈ toricIdeal R a ↔ (MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single (a i) 1) p = 0

A polynomial lies in the toric ideal exactly when it vanishes under X i ↦ single (a i) 1.

theorem TauCeti.toricIdeal_comp_of_injective {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] (R : Type u_4) [CommSemiring R] (a : ι → M) {g : M →+ N} (hg : Function.Injective ⇑g) : toricIdeal R (⇑g ∘ a) = toricIdeal R a

The toric ideal does not depend on the ambient monoid: it is unchanged by an injective additive homomorphism g : M →+ N.

theorem TauCeti.toricIdeal_eq_ker_aeval_monomial {ι : Type u_1} (R : Type u_4) [CommSemiring R] {σ : Type u_5} (a : ι → σ →₀ ℕ) : toricIdeal R a = RingHom.ker (MvPolynomial.aeval fun (i : ι) => (MvPolynomial.monomial (a i)) 1)

For exponents a i : σ →₀ ℕ, the toric ideal is the kernel of the map MvPolynomial ι R → MvPolynomial σ R sending X i to the monomial X ^ (a i), since MvPolynomial σ R is the semigroup algebra R[σ →₀ ℕ].

theorem TauCeti.toricIdeal_eq_span {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommRing R] (a : ι → M) : toricIdeal R a = Ideal.span {p : MvPolynomial ι R | ∃ (u : ι →₀ ℕ) (v : ι →₀ ℕ), (Finsupp.linearCombination ℕ a) u = (Finsupp.linearCombination ℕ a) v ∧ p = (MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1}

Binomial generation of toric ideals. Over any commutative ring, the toric ideal of a : ι → M is generated by the binomials X^u - X^v with ∑ i, u i • a i = ∑ i, v i • a i.

theorem TauCeti.monomial_sub_monomial_mem_toricIdeal {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {R : Type u_4} [CommRing R] {a : ι → M} {u v : ι →₀ ℕ} (h : (Finsupp.linearCombination ℕ a) u = (Finsupp.linearCombination ℕ a) v) : (MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1 ∈ toricIdeal R a

A binomial X^u - X^v with ∑ i, u i • a i = ∑ i, v i • a i lies in the toric ideal.

@[simp]

theorem TauCeti.monomial_sub_monomial_mem_toricIdeal_iff {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {R : Type u_4} [CommRing R] [Nontrivial R] {a : ι → M} {u v : ι →₀ ℕ} : (MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1 ∈ toricIdeal R a ↔ (Finsupp.linearCombination ℕ a) u = (Finsupp.linearCombination ℕ a) v

Over a nontrivial ring, a binomial X^u - X^v lies in the toric ideal exactly when ∑ i, u i • a i = ∑ i, v i • a i.

theorem TauCeti.map_toricIdeal {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommRing R] {S : Type u_5} [CommRing S] (f : R →+* S) (a : ι → M) : Ideal.map (MvPolynomial.map f) (toricIdeal R a) = toricIdeal S a

The formation of toric ideals commutes with change of coefficients: the toric ideal over S is generated by the image of the toric ideal over R, for any ring homomorphism R →+* S.

noncomputable def TauCeti.quotientToricIdealAlgEquiv {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommRing R] {a : ι → M} (ha : AddSubmonoid.closure (Set.range a) = ⊤) : (MvPolynomial ι R ⧸ toricIdeal R a) ≃ₐ[R] AddMonoidAlgebra R M

The binomial presentation of a semigroup algebra. If the a i generate M, then X i ↦ single (a i) 1 identifies the quotient of MvPolynomial ι R by the toric ideal with the semigroup algebra R[M].

@[simp]

theorem TauCeti.quotientToricIdealAlgEquiv_mk {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommRing R] {a : ι → M} (ha : AddSubmonoid.closure (Set.range a) = ⊤) (p : MvPolynomial ι R) : (quotientToricIdealAlgEquiv R ha) ((Ideal.Quotient.mk (toricIdeal R a)) p) = (MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single (a i) 1) p

The presentation quotientToricIdealAlgEquiv sends the class of p to its image under X i ↦ single (a i) 1.

noncomputable def TauCeti.quotientToricIdealAlgEquivClosure {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommRing R] (a : ι → M) : (MvPolynomial ι R ⧸ toricIdeal R a) ≃ₐ[R] AddMonoidAlgebra R ↥(AddSubmonoid.closure (Set.range a))

The binomial presentation of the semigroup algebra of S = ⟨a i⟩. The map X i ↦ single (a i) 1 identifies the quotient of MvPolynomial ι R by the toric ideal with the semigroup algebra R[S] of the submonoid S generated by the a i.

@[simp]

theorem TauCeti.quotientToricIdealAlgEquivClosure_mk {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (R : Type u_4) [CommRing R] (a : ι → M) (p : MvPolynomial ι R) : (quotientToricIdealAlgEquivClosure R a) ((Ideal.Quotient.mk (toricIdeal R a)) p) = (MvPolynomial.aeval fun (i : ι) => AddMonoidAlgebra.single ⟨a i, ⋯⟩ 1) p

The presentation quotientToricIdealAlgEquivClosure sends the class of p to its image under X i ↦ single (a i) 1, computed in the semigroup algebra of the submonoid generated by the a i.

theorem TauCeti.exists_finset_toricIdeal_eq_span {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] [Finite ι] (a : ι → M) : ∃ (P : Finset ((ι →₀ ℕ) × (ι →₀ ℕ))), (∀ p ∈ P, (Finsupp.linearCombination ℕ a) p.1 = (Finsupp.linearCombination ℕ a) p.2) ∧ ∀ (R : Type u) [inst : CommRing R], toricIdeal R a = Ideal.span ((fun (p : (ι →₀ ℕ) × (ι →₀ ℕ)) => (MvPolynomial.monomial p.1) 1 - (MvPolynomial.monomial p.2) 1) '' ↑P)

Finite binomial generation. For finitely many exponents a i, there are finitely many pairs (u, v) with ∑ i, u i • a i = ∑ i, v i • a i whose binomials X^u - X^v generate the toric ideal over every commutative ring. The pairs are chosen over ℤ, where the polynomial ring is noetherian, and the generators are transported by change of coefficients.