Dual semigroups of product cones

An integral character on a product lattice is nonnegative on a product cone precisely when its restrictions to the two factors are nonnegative. Consequently the dual semigroup of a product cone is canonically the product of the two dual semigroups. This identification uses restriction of characters and their coproduct, with no bases or regularity hypotheses, and supplies the character identification for products of affine toric schemes.

References

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

@[simp]

theorem TauCeti.Toric.mem_dualSemigroup_prod {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (σ : PointedCone ℝ V) (τ : PointedCone ℝ V') (m : N × N' →+ ℤ) : m ∈ dualSemigroup ⋯ (Submodule.prod σ τ) ↔ m.comp (AddMonoidHom.inl N N') ∈ dualSemigroup hi σ ∧ m.comp (AddMonoidHom.inr N N') ∈ dualSemigroup hi' τ

A character is nonnegative on a product cone exactly when its restrictions to both factors are nonnegative.

noncomputable def TauCeti.Toric.dualSemigroupProdEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (σ : PointedCone ℝ V) (τ : PointedCone ℝ V') : ↥(dualSemigroup ⋯ (Submodule.prod σ τ)) ≃+ ↥(dualSemigroup hi σ) × ↥(dualSemigroup hi' τ)

Restriction to the two factors identifies the dual semigroup of a product cone with the product of the factor dual semigroups. The inverse takes the coproduct of characters.

@[simp]

theorem TauCeti.Toric.dualSemigroupProdEquiv_fst_apply {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (σ : PointedCone ℝ V) (τ : PointedCone ℝ V') (m : ↥(dualSemigroup ⋯ (Submodule.prod σ τ))) (n : N) : ↑((dualSemigroupProdEquiv hi hi' σ τ) m).1 n = ↑m (n, 0)

The first component of the product equivalence evaluates a character on the first factor.

@[simp]

theorem TauCeti.Toric.dualSemigroupProdEquiv_snd_apply {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (σ : PointedCone ℝ V) (τ : PointedCone ℝ V') (m : ↥(dualSemigroup ⋯ (Submodule.prod σ τ))) (n : N') : ↑((dualSemigroupProdEquiv hi hi' σ τ) m).2 n = ↑m (0, n)

The second component of the product equivalence evaluates a character on the second factor.

@[simp]

theorem TauCeti.Toric.dualSemigroupProdEquiv_symm_apply {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') (σ : PointedCone ℝ V) (τ : PointedCone ℝ V') (m : ↥(dualSemigroup hi σ) × ↥(dualSemigroup hi' τ)) (n : N × N') : ↑((dualSemigroupProdEquiv hi hi' σ τ).symm m) n = ↑m.1 n.1 + ↑m.2 n.2

The inverse product equivalence sums the values of the two factor characters.