Dual semigroups of faces of toric cones

A character m in the dual semigroup of a cone σ cuts out the face σ ⊓ ker m of σ. When σ is finitely generated, the dual semigroup of that face is generated by the dual semigroup of σ together with -m: every character nonnegative on the face becomes nonnegative on σ after adding a multiple of m. This is the semigroup form of the statement that the affine chart of the face is the localization of the chart of σ away from the monomial of m.

Main declarations

• TauCeti.Toric.exists_add_nsmul_mem_dualSemigroup and TauCeti.Toric.dualSemigroup_inf_ker_eq_sup: the dual semigroup of the face cut out by a character m of a finitely generated cone σ is the dual semigroup of σ with -m adjoined.
• TauCeti.Toric.IsRegularCone.realCharacter_eq_zero_on_face_iff: vanishing of a dual-semigroup character on a face in terms of its regular ray coordinates.

References

The description of the dual semigroup of a face follows §§1.2–1.3 of W. Fulton, Introduction to Toric Varieties, and §1.3 of D. Cox, J. Little and H. Schenck, Toric Varieties.

theorem TauCeti.Toric.neg_mem_dualSemigroup_inf_ker {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) (m : N →+ ℤ) : -m ∈ dualSemigroup hi (σ ⊓ ↑(LinearMap.ker (hi.realCharacter m)))

The negative of a character lies in the dual semigroup of the part of a cone on which the character vanishes.

theorem TauCeti.Toric.exists_add_nsmul_mem_dualSemigroup {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) {m : N →+ ℤ} (hm : m ∈ dualSemigroup hi σ) {u : N →+ ℤ} (hu : u ∈ dualSemigroup hi (σ ⊓ ↑(LinearMap.ker (hi.realCharacter m)))) : ∃ (n : ℕ), u + n • m ∈ dualSemigroup hi σ

Let m lie in the dual semigroup of a finitely generated cone σ. A character in the dual semigroup of the face σ ⊓ ker m lies in the dual semigroup of σ after adding a multiple of m.

theorem TauCeti.Toric.dualSemigroup_inf_ker_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σ : Submodule.FG σ) {m : N →+ ℤ} (hm : m ∈ dualSemigroup hi σ) : dualSemigroup hi (σ ⊓ ↑(LinearMap.ker (hi.realCharacter m))) = dualSemigroup hi σ ⊔ AddSubmonoid.closure {-m}

The dual semigroup of the face σ ⊓ ker m cut out by a character m in the dual semigroup of a finitely generated cone σ is generated by the dual semigroup of σ together with -m.

theorem TauCeti.Toric.IsRegularCone.realCharacter_eq_zero_on_face_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {I : Type u_3} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ I) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (m : ↥(dualSemigroup hi σ)) : (∀ y ∈ F, (hi.realCharacter ↑m) y = 0) ↔ ∀ ρ ∈ (faceOrderIso hi hσ) F, ((regularDualSemigroupEquiv hi ⋯ hb) m).1 ρ = 0

A character in the dual semigroup vanishes on a face of a regular cone exactly when all of its regular ray coordinates indexed by rays of that face vanish.