Mixed coordinates on the complex points of a split affine semigroup

An affine semigroup that splits as a product (ι →₀ ℕ) × (κ →₀ ℤ) of a free commutative monoid and a free abelian group has a completely explicit space of complex points: a ℂ-algebra homomorphism out of its monoid algebra is the same data as a family of complex numbers indexed by ι together with a family of units of ℂ indexed by κ. The exponents of the free monoid factor are nonnegative, so the corresponding coordinates are unconstrained, while the free abelian factor contains the inverse of each of its generators and therefore forces the remaining coordinates to be invertible.

This is the mixed chart ℂ ^ k × (ℂ ^ *) ^ l of toric geometry. The dual semigroup of a smooth k-dimensional cone in a lattice of rank k + l splits in exactly this way, with ι indexing the rays of the cone and κ the remaining vectors of an integral basis extending their primitive generators. The coordinates indexed by ι may vanish: the boundary is the union of their coordinate hyperplanes, while the coordinates indexed by κ remain units.

The identification is assembled from the universal properties of the two free factors, so it is a bijection of the functor-of-points carrier and mentions no generating family. The main result is that it is a homeomorphism for the monomial-embedding topology attached to an arbitrary finite generating family of the semigroup: the topology of the complex points, defined with no reference to a splitting, is the product topology of the mixed coordinates. Both directions are computed by named lemmas, so no consumer has to unfold the equivalence: a coordinate of a point is its value on the monomial of the corresponding standard generator, and conversely the value of a point on an arbitrary monomial is the expected mixed monomial in the coordinates.

Main declarations

• TauCeti.Toric.regularAffinePointEquiv: the mixed coordinates of the complex points of a split affine semigroup, with TauCeti.Toric.regularAffinePointEquiv_fst_apply, TauCeti.Toric.val_regularAffinePointEquiv_snd_apply and TauCeti.Toric.regularAffinePointEquiv_symm_apply_single computing the two directions, and TauCeti.Toric.apply_single_ne_zero_iff_regularAffinePointEquiv_fst_ne_zero characterizing monomial nonvanishing.
• TauCeti.Toric.continuous_regularAffinePointEquiv and TauCeti.Toric.continuous_regularAffinePointEquiv_symm: both directions are continuous for the monomial-embedding topology of any finite generating family.
• TauCeti.Toric.regularAffinePointHomeomorph: the resulting homeomorphism.

References

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

noncomputable def TauCeti.Toric.regularAffinePointEquiv {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : AffineSemigroupComplexPoint S ≃ (ι → ℂ) × (κ → ℂˣ)

The mixed coordinates of the complex points of an affine semigroup S split as (ι →₀ ℕ) × (κ →₀ ℤ): a complex point is the same data as a family of complex numbers indexed by ι, the values on the generators of the free commutative monoid factor, and a family of units indexed by κ, the values on the generators of the free abelian factor.

@[simp]

theorem TauCeti.Toric.regularAffinePointEquiv_symm_apply_single {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) (z : (ι → ℂ) × (κ → ℂˣ)) (s : S) : ((regularAffinePointEquiv e).symm z) (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = ((e s).1.prod fun (i : ι) (n : ℕ) => z.1 i ^ n) * ↑((e s).2.prod fun (j : κ) (n : ℤ) => z.2 j ^ n)

The complex point attached to a family of mixed coordinates takes, on the monomial of s : S, the mixed monomial value prescribed by the exponents of s: a product of natural powers of the unconstrained coordinates times a product of integral powers of the invertible ones.

theorem TauCeti.Toric.apply_single_ne_zero_iff_regularAffinePointEquiv_fst_ne_zero {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) (x : AffineSemigroupComplexPoint S) (s : S) : x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) ≠ 0 ↔ ∀ i ∈ (e s).1.support, ((regularAffinePointEquiv e) x).1 i ≠ 0

A monomial is nonzero at a complex point exactly when every free-commutative-monoid coordinate occurring in its support is nonzero. The free-abelian-coordinate factor is always a unit.

@[simp]

theorem TauCeti.Toric.regularAffinePointEquiv_fst_apply {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) (x : AffineSemigroupComplexPoint S) (i : ι) : ((regularAffinePointEquiv e) x).1 i = x (MonoidAlgebra.single (Multiplicative.ofAdd (e.symm (Finsupp.single i 1, 0))) 1)

The coordinate of a complex point indexed by i : ι is its value on the monomial of the i-th generator of the free commutative monoid factor.

@[simp]

theorem TauCeti.Toric.val_regularAffinePointEquiv_snd_apply {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) (x : AffineSemigroupComplexPoint S) (j : κ) : ↑(((regularAffinePointEquiv e) x).2 j) = x (MonoidAlgebra.single (Multiplicative.ofAdd (e.symm (0, Finsupp.single j 1))) 1)

The coordinate of a complex point indexed by j : κ is, as a complex number, its value on the monomial of the j-th generator of the free abelian factor.

theorem TauCeti.Toric.inv_val_regularAffinePointEquiv_snd_apply {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) (x : AffineSemigroupComplexPoint S) (j : κ) : (↑(((regularAffinePointEquiv e) x).2 j))⁻¹ = x (MonoidAlgebra.single (Multiplicative.ofAdd (e.symm (0, -Finsupp.single j 1))) 1)

The inverse of the coordinate indexed by j : κ is the value of the point on the monomial of the opposite generator; this is what makes that coordinate a unit.

theorem TauCeti.Toric.continuous_regularAffinePointEquiv {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} {r : ℕ} (g : AddGeneratingFamily S r) (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : Continuous ⇑(regularAffinePointEquiv e)

Reading off the mixed coordinates is continuous for the monomial-embedding topology of any finite generating family: each coordinate is evaluation at a fixed monomial, and so is the inverse of each invertible coordinate.

theorem TauCeti.Toric.continuous_regularAffinePointEquiv_symm {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} {r : ℕ} (g : AddGeneratingFamily S r) (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : Continuous ⇑(regularAffinePointEquiv e).symm

Building a complex point from mixed coordinates is continuous for the monomial-embedding topology of any finite generating family: the monomial-embedding topology is the coarsest one making evaluation at every monomial continuous, and evaluation at the monomial of s is a mixed monomial in the coordinates.

noncomputable def TauCeti.Toric.regularAffinePointHomeomorph {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} {r : ℕ} (g : AddGeneratingFamily S r) (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : AffineSemigroupComplexPoint S ≃ₜ (ι → ℂ) × (κ → ℂˣ)

A splitting of an affine semigroup as (ι →₀ ℕ) × (κ →₀ ℤ) identifies its complex points, with the monomial-embedding topology of any finite generating family, with the mixed chart (ι → ℂ) × (κ → ℂˣ).

@[simp]

theorem TauCeti.Toric.coe_regularAffinePointHomeomorph {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} {r : ℕ} (g : AddGeneratingFamily S r) (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : ⇑(regularAffinePointHomeomorph g e) = ⇑(regularAffinePointEquiv e)

@[simp]

theorem TauCeti.Toric.coe_regularAffinePointHomeomorph_symm {S : Type u_1} [AddCommMonoid S] {ι : Type u_2} {κ : Type u_3} {r : ℕ} (g : AddGeneratingFamily S r) (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : ⇑(regularAffinePointHomeomorph g e).symm = ⇑(regularAffinePointEquiv e).symm