The separation lemma for toric cones

Let σ and τ be lattice-rational cones meeting in a common face σ ⊓ τ, as any two cones of a fan do. The separation lemma produces an integral character m that is nonnegative on σ, nonpositive on τ, and vanishes on either cone exactly along σ ⊓ τ. Its proof applies Tucker's theorem over the integers to the lattice generators of σ together with the negatives of those of τ. The theorem gives a character nonnegative on this family and a relation among its members with natural-number coefficients, where every generator on which the character vanishes has a positive coefficient in the relation. The relation exhibits a vector of σ ⊓ τ as a positive combination of all such generators of σ, so each of them lies in the face σ ⊓ τ, and likewise for τ.

Consequently the dual semigroup of σ ⊓ τ is generated by the dual semigroups of σ and τ: by TauCeti.Toric.dualSemigroup_inf_ker_eq_sup it is obtained from that of σ by adjoining -m, which lies in the dual semigroup of τ. In terms of affine toric charts, the chart of σ ⊓ τ is cut out of the product of the charts of σ and τ by the relations among monomials. This is the input for the separatedness of toric varieties and the Hausdorff property of their complex points.

Every face of a lattice-rational cone in an integral lattice is cut out by an integral character nonnegative on the cone, by applying the separation lemma to the cone and its face. Regularity and salience are not required. This identifies the affine toric chart of any face with a localization at a single monomial, and hence an open subscheme of the chart of the cone. These consequences are developed in TauCeti.Geometry.Toric.Algebraic.FaceLocalization.

Main declarations

• TauCeti.Toric.exists_mem_dualSemigroup_neg_mem_dualSemigroup_inf_ker_eq: the separation lemma.
• TauCeti.Toric.IsLatticeRational.exists_mem_dualSemigroup_inf_ker_eq: every face is cut out by an integral supporting character.
• TauCeti.Toric.dualSemigroup_inf_eq_sup: the dual semigroup of σ ⊓ τ is generated by those of σ and τ.
• TauCeti.Toric.Fan.dualSemigroup_inf_eq_sup: the same for two cones of a fan.
• TauCeti.Toric.Fan.mem_dualSemigroup_ofCone_bot: every integral character is nonnegative on the cones of the fan of the zero cone.

References

• W. Fulton, Introduction to Toric Varieties, §1.2 (the separation lemma), §1.3 and §1.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §1.2 (the separation lemma), §1.3 and §3.1.
• A. W. Tucker, Dual systems of homogeneous linear relations, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, 1956.

theorem TauCeti.Toric.exists_mem_dualSemigroup_neg_mem_dualSemigroup_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτ : IsLatticeRational i τ) (hστ : (σ ⊓ τ).IsFaceOf σ) (hτσ : (σ ⊓ τ).IsFaceOf τ) : ∃ m ∈ dualSemigroup hi σ, -m ∈ dualSemigroup hi τ ∧ σ ⊓ ↑(LinearMap.ker (hi.realCharacter m)) = σ ⊓ τ ∧ τ ⊓ ↑(LinearMap.ker (hi.realCharacter m)) = σ ⊓ τ

The separation lemma. Let σ and τ be lattice-rational cones whose intersection is a face of each. There is an integral character m, nonnegative on σ and nonpositive on τ, whose kernel cuts out the common face σ ⊓ τ from both cones.

theorem TauCeti.Toric.IsLatticeRational.exists_mem_dualSemigroup_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτ : τ.IsFaceOf σ) : ∃ m ∈ dualSemigroup hi σ, σ ⊓ ↑(LinearMap.ker (hi.realCharacter m)) = τ

Every face τ of a lattice-rational cone σ in an integral lattice is cut out by a character in the dual semigroup of σ: there is m with σ ⊓ ker m = τ.

theorem TauCeti.Toric.dualSemigroup_inf_eq_sup {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτ : IsLatticeRational i τ) (hστ : (σ ⊓ τ).IsFaceOf σ) (hτσ : (σ ⊓ τ).IsFaceOf τ) : dualSemigroup hi (σ ⊓ τ) = dualSemigroup hi σ ⊔ dualSemigroup hi τ

Let σ and τ be lattice-rational cones whose intersection is a face of each. The dual semigroup of σ ⊓ τ is generated by the dual semigroups of σ and τ: every character nonnegative on the common face is a sum of one nonnegative on σ and one nonnegative on τ.

theorem TauCeti.Toric.Fan.dualSemigroup_inf_eq_sup {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) (hτ : τ ∈ Φ.cones) : dualSemigroup ⋯ (σ ⊓ τ) = dualSemigroup ⋯ σ ⊔ dualSemigroup ⋯ τ

The dual semigroup of the intersection of two cones of a fan is generated by the dual semigroups of the two cones.

theorem TauCeti.Toric.Fan.mem_dualSemigroup_ofCone_bot {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (m : N →+ ℤ) (σ : ↑(ofCone hi ⋯).cones) : m ∈ dualSemigroup ⋯ ↑σ

Every integral character is nonnegative on every cone of the fan of the zero cone, since that fan has the zero cone as its only cone.