Dual semigroups of toric cones

An integral character of a lattice extends uniquely to a real-linear functional on the ambient real vector space (TauCeti.Toric.IsIntegralLattice.realCharacter). The dual semigroup of a cone consists of the integral characters whose real extensions are nonnegative on the cone. When the cone is rational polyhedral, this is the additive monoid whose semigroup algebra is the coordinate ring of the corresponding affine toric variety; the definition itself imposes no finiteness hypothesis on the cone.

The construction is expressed as the inverse image of Mathlib's PointedCone.dual, so its order reversal and its behavior on cone hulls come directly from the convex-geometric duality API. Maps of lattices carrying one cone into another induce contravariant maps of dual semigroups.

Main declarations

• TauCeti.Toric.dualSemigroup: integral characters nonnegative on a cone.
• TauCeti.Toric.dualSemigroupMap: the contravariant map induced by a compatible map of lattices and cones.

References

The construction follows §1.2 of W. Fulton, Introduction to Toric Varieties, and §1.2 of D. Cox, J. Little and H. Schenck, Toric Varieties.

The dual semigroup

noncomputable def TauCeti.Toric.dualSemigroup {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : AddSubmonoid (N →+ ℤ)

The dual semigroup of a cone consists of the integral characters whose real-linear extensions are nonnegative on the cone.

theorem TauCeti.Toric.dualSemigroup_def {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : dualSemigroup hi σ = (PointedCone.dual (Module.Dual.eval ℝ V) ↑σ).latticePoints hi.realCharacter

The dual semigroup is the lattice-point monoid of Mathlib's dual cone under real extension of integral characters.

@[simp]

theorem TauCeti.Toric.mem_dualSemigroup {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (m : N →+ ℤ) : m ∈ dualSemigroup hi σ ↔ ∀ ⦃x : V⦄, x ∈ σ → 0 ≤ (hi.realCharacter m) x

An integral character belongs to the dual semigroup exactly when its real extension is nonnegative at every point of the cone.

theorem TauCeti.Toric.dualSemigroup_anti {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {σ τ : PointedCone ℝ V} (h : σ ≤ τ) : dualSemigroup hi τ ≤ dualSemigroup hi σ

Enlarging a cone shrinks its dual semigroup.

theorem TauCeti.Toric.dualSemigroup_antitone {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) : Antitone (dualSemigroup hi)

Taking the dual semigroup reverses the order on pointed cones.

@[simp]

theorem TauCeti.Toric.dualSemigroup_bot {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) : dualSemigroup hi ⊥ = ⊤

The dual semigroup of the zero cone is the full character group.

@[simp]

theorem TauCeti.Toric.dualSemigroup_top {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) : dualSemigroup hi ⊤ = ⊥

The dual semigroup of the whole space is trivial: the dual cone of the whole space is zero (PointedCone.dual_univ), and real extension of integral characters is injective.

instance TauCeti.Toric.subsingleton_dualSemigroup_top {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) : Subsingleton ↥(dualSemigroup hi ⊤)

The dual semigroup of the whole space has a single element, so the complex monoid algebra of the corresponding affine toric chart is ℂ (MonoidAlgebra.uniqueAlgEquiv), and the chart is a point.

@[simp]

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

The dual semigroup of a join is the intersection of the two dual semigroups.

theorem TauCeti.Toric.mem_dualSemigroup_hull_image {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (s : Set N) (m : N →+ ℤ) : m ∈ dualSemigroup hi (PointedCone.hull ℝ (⇑i '' s)) ↔ ∀ n ∈ s, 0 ≤ m n

On a cone generated by a set of lattice vectors, membership in the dual semigroup is equivalent to the corresponding family of integral inequalities.

Functoriality

noncomputable def TauCeti.Toric.dualSemigroupMap {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : ↥(dualSemigroup hi' τ) →+ ↥(dualSemigroup hi σ)

A compatible map of lattices carrying a source cone into a target cone induces the contravariant map on dual semigroups by precomposition of characters.

theorem TauCeti.Toric.dualSemigroupMap_apply {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) (m : ↥(dualSemigroup hi' τ)) (n : N) : ↑((dualSemigroupMap hi hi' f g hfg hστ) m) n = ↑m (f n)

The map on dual semigroups is precomposition by the underlying map of lattices.

@[simp]

theorem TauCeti.Toric.coe_dualSemigroupMap {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) (m : ↥(dualSemigroup hi' τ)) : ↑((dualSemigroupMap hi hi' f g hfg hστ) m) = (↑m).comp f

The underlying character of the image of a character under the map on dual semigroups is its precomposition with the underlying map of lattices.

theorem TauCeti.Toric.coe_dualSemigroupMap_id {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) {σ' : PointedCone ℝ V} (hσσ' : Set.MapsTo ⇑LinearMap.id ↑σ ↑σ') (m : ↥(dualSemigroup hi σ')) : ↑((dualSemigroupMap hi hi (AddMonoidHom.id N) LinearMap.id ⋯ hσσ') m) = ↑m

Along the identity of a lattice, a cone inclusion σ ≤ σ' induces the inclusion of dual semigroups: the image of a character is the same character.

@[simp]

theorem TauCeti.Toric.dualSemigroupMap_id {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : dualSemigroupMap hi hi (AddMonoidHom.id N) LinearMap.id ⋯ ⋯ = AddMonoidHom.id ↥(dualSemigroup hi σ)

The identity map of a lattice induces the identity map of its dual semigroup.

theorem TauCeti.Toric.dualSemigroupMap_comp {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} {υ : PointedCone ℝ V''} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (hi'' : IsIntegralLattice i'') (f : N →+ N') (f' : N' →+ N'') (g : V →ₗ[ℝ] V') (g' : V' →ₗ[ℝ] V'') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hf'g' : ∀ (n : N'), g' (i' n) = i'' (f' n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) (hτυ : Set.MapsTo ⇑g' ↑τ ↑υ) : dualSemigroupMap hi hi'' (f'.comp f) (g' ∘ₗ g) ⋯ ⋯ = (dualSemigroupMap hi hi' f g hfg hστ).comp (dualSemigroupMap hi' hi'' f' g' hf'g' hτυ)

Contravariant dual-semigroup maps turn a composite of compatible cone maps into the composite of the induced maps.

noncomputable def TauCeti.Toric.dualSemigroupEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N ≃+ N') (e : V ≃ₗ[ℝ] V') (hfe : ∀ (n : N), e (i n) = i' (f n)) (hστ : PointedCone.map (↑e) σ = τ) : ↥(dualSemigroup hi' τ) ≃+ ↥(dualSemigroup hi σ)

A lattice equivalence carrying one cone onto another identifies their dual semigroups contravariantly, by precomposition of characters.

@[simp]

theorem TauCeti.Toric.dualSemigroupEquiv_apply {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N ≃+ N') (e : V ≃ₗ[ℝ] V') (hfe : ∀ (n : N), e (i n) = i' (f n)) (hστ : PointedCone.map (↑e) σ = τ) (m : ↥(dualSemigroup hi' τ)) (n : N) : ↑((dualSemigroupEquiv hi hi' f e hfe hστ) m) n = ↑m (f n)

The dual-semigroup equivalence precomposes with the integral lattice equivalence.

@[simp]

theorem TauCeti.Toric.dualSemigroupEquiv_symm_apply {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (f : N ≃+ N') (e : V ≃ₗ[ℝ] V') (hfe : ∀ (n : N), e (i n) = i' (f n)) (hστ : PointedCone.map (↑e) σ = τ) (m : ↥(dualSemigroup hi σ)) (n : N') : ↑((dualSemigroupEquiv hi hi' f e hfe hστ).symm m) n = ↑m (f.symm n)

The inverse dual-semigroup equivalence precomposes with the inverse lattice equivalence.