The character action on the complex points of an affine semigroup

The complex points of an affine semigroup S are the algebra homomorphisms ℂ[S] →ₐ[ℂ] ℂ, that is, the multiplicative characters S → ℂ. The invertible characters AddChar S ℂˣ form a commutative monoid under pointwise multiplication, and they act on the complex points by multiplying values: the point t • x takes the value t s * x (χ ^ s) on the monomial of s.

For the dual semigroup S = σ^∨ ∩ M of a toric cone in the character lattice M = N →+ ℤ, the coordinate-free complex torus AddChar M ℂˣ acts through restriction of characters to S. This file records that restricted action for an arbitrary submonoid S of an additive monoid M, so that the torus of the lattice acts on every affine chart and the face-localization maps between charts are equivariant.

The distinguished complex point, which takes the value 1 on every monomial, has trivial stabilizer, and its orbit under the invertible characters of S is exactly the locus where no monomial vanishes. For a split semigroup S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ), this locus is the set of points whose unconstrained coordinates are all nonzero; it is open and dense in the complex points of S, and the action is coordinatewise multiplication. These are the affine pieces of the dense torus of a toric variety.

Translation by a fixed character is a homeomorphism for the monomial-embedding topology of any finite generating family, packaged as a ContinuousConstSMul fact so that Mathlib's Homeomorph.smul applies. The coordinate-free complex torus also acts jointly continuously.

Main declarations

• TauCeti.Toric.AffineSemigroupComplexPoint.instMulActionAddCharUnitsComplex: the action of the invertible characters of S on its complex points, with TauCeti.Toric.AffineSemigroupComplexPoint.smul_apply_single computing it on monomials.
• TauCeti.Toric.AffineSemigroupComplexPoint.instMulActionAddCharUnitsComplexSubtypeMem: the action of the invertible characters of an ambient monoid on the complex points of a submonoid, through restriction, with TauCeti.Toric.AffineSemigroupComplexPoint.ambient_smul_apply_single.
• TauCeti.Toric.AffineSemigroupComplexPoint.comap_smul and TauCeti.Toric.AffineSemigroupComplexPoint.comap_inclusion_smul: the maps on complex points induced by semigroup homomorphisms are equivariant.
• TauCeti.Toric.AffineSemigroupComplexPoint.mem_orbit_default_iff: the orbit of the distinguished point is the locus where no monomial vanishes, and TauCeti.Toric.AffineSemigroupComplexPoint.smul_default_injective: the characters act freely on it.
• TauCeti.Toric.AffineSemigroupComplexPoint.continuousConstSMul_affinePointTopology: translation by a character is continuous for the monomial-embedding topology, and TauCeti.Toric.AffineSemigroupComplexPoint.isOpen_orbit_default: the orbit of the distinguished point is open.
• TauCeti.Toric.AffineSemigroupComplexPoint.continuousSMul_complexTorus_affinePointTopology: joint continuity of the coordinate-free torus action on affine complex points.
• TauCeti.Toric.regularAffinePointEquiv_smul_fst and TauCeti.Toric.regularAffinePointEquiv_smul_snd: in the mixed coordinates of a split semigroup the action is coordinatewise multiplication; TauCeti.Toric.mem_orbit_default_iff_regularAffinePointEquiv and TauCeti.Toric.dense_orbit_default: the orbit of the distinguished point is the locus where the unconstrained coordinates are nonzero, which is dense.

References

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

The action of the invertible characters of the semigroup

@[instance_reducible]

noncomputable instance TauCeti.Toric.AffineSemigroupComplexPoint.instSMulAddCharUnitsComplex {S : Type u_1} [AddCommMonoid S] : SMul (AddChar S ℂˣ) (AffineSemigroupComplexPoint S)

An invertible character t : AddChar S ℂˣ acts on a complex point x of S by multiplying its values: t • x sends the monomial of s to t s * x (χ ^ s).

theorem TauCeti.Toric.AffineSemigroupComplexPoint.smul_def {S : Type u_1} [AddCommMonoid S] (t : AddChar S ℂˣ) (x : AffineSemigroupComplexPoint S) : t • x = (MonoidAlgebra.lift ℂ ℂ (Multiplicative S)) ((Units.coeHom ℂ).comp t.toMonoidHom * (MonoidAlgebra.lift ℂ ℂ (Multiplicative S)).symm x)

The twisted point, as the algebra homomorphism induced by the pointwise product of the character and the multiplicative character underlying the point.

@[simp]

theorem TauCeti.Toric.AffineSemigroupComplexPoint.smul_apply_single {S : Type u_1} [AddCommMonoid S] (t : AddChar S ℂˣ) (x : AffineSemigroupComplexPoint S) (s : S) : (t • x) (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = ↑(t s) * x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)

The twisted point takes the product of the character value and the original value on every monomial.

@[instance_reducible]

noncomputable instance TauCeti.Toric.AffineSemigroupComplexPoint.instMulActionAddCharUnitsComplex {S : Type u_1} [AddCommMonoid S] : MulAction (AddChar S ℂˣ) (AffineSemigroupComplexPoint S)

The invertible characters of S act on the complex points of S.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_smul {S : Type u_1} {T : Type u_2} [AddCommMonoid S] [AddCommMonoid T] (f : S →+ T) (t : AddChar T ℂˣ) (x : AffineSemigroupComplexPoint T) : comap f (t • x) = t.compAddMonoidHom f • comap f x

Pulling back along a semigroup homomorphism is equivariant, the character being restricted along the homomorphism.

The orbit of the distinguished point

theorem TauCeti.Toric.AffineSemigroupComplexPoint.smul_default_injective {S : Type u_1} [AddCommMonoid S] : Function.Injective fun (t : AddChar S ℂˣ) => t • default

The invertible characters act freely on the distinguished point: it has trivial stabilizer.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.mem_orbit_default_iff {S : Type u_1} [AddCommMonoid S] {x : AffineSemigroupComplexPoint S} : x ∈ MulAction.orbit (AddChar S ℂˣ) default ↔ ∀ (s : S), x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) ≠ 0

The orbit of the distinguished point under the invertible characters is the locus of complex points at which no monomial vanishes: such a point is itself an invertible character.

Continuity

theorem TauCeti.Toric.AffineSemigroupComplexPoint.continuous_const_smul_affinePointTopology {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) (t : AddChar S ℂˣ) : Continuous fun (x : AffineSemigroupComplexPoint S) => t • x

Translation by a fixed character is continuous for the monomial-embedding topology of any finite generating family: it multiplies every monomial value by a constant.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.continuousConstSMul_affinePointTopology {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) : ContinuousConstSMul (AddChar S ℂˣ) (AffineSemigroupComplexPoint S)

The invertible characters act by homeomorphisms for the monomial-embedding topology of any finite generating family.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.isOpen_orbit_default {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) : IsOpen (MulAction.orbit (AddChar S ℂˣ) default)

The orbit of the distinguished point is open for the monomial-embedding topology of any finite generating family: it is the locus where the finitely many coordinates of the embedding are all nonzero.

The action of the characters of an ambient monoid

@[instance_reducible]

noncomputable instance TauCeti.Toric.AffineSemigroupComplexPoint.instSMulAddCharUnitsComplexSubtypeMemAddSubmonoid {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} : SMul (AddChar M ℂˣ) (AffineSemigroupComplexPoint ↥S)

The invertible characters of an ambient monoid M act on the complex points of a submonoid S ≤ M through restriction of characters to S. For the dual semigroup of a toric cone in the character lattice N →+ ℤ, this is the action of the coordinate-free complex torus on the affine chart of the cone.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.ambient_smul_def {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} (t : AddChar M ℂˣ) (x : AffineSemigroupComplexPoint ↥S) : t • x = t.compAddMonoidHom S.subtype • x

The ambient characters act through their restriction to the submonoid.

@[simp]

theorem TauCeti.Toric.AffineSemigroupComplexPoint.ambient_smul_apply_single {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} (t : AddChar M ℂˣ) (x : AffineSemigroupComplexPoint ↥S) (s : ↥S) : (t • x) (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = ↑(t ↑s) * x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)

The ambient characters act through their values on the elements of the submonoid.

@[instance_reducible]

noncomputable instance TauCeti.Toric.AffineSemigroupComplexPoint.instMulActionAddCharUnitsComplexSubtypeMemAddSubmonoid {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} : MulAction (AddChar M ℂˣ) (AffineSemigroupComplexPoint ↥S)

The invertible characters of an ambient monoid act on the complex points of a submonoid.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_inclusion_smul {M : Type u_3} [AddCommMonoid M] {S S' : AddSubmonoid M} (h : S ≤ S') (t : AddChar M ℂˣ) (x : AffineSemigroupComplexPoint ↥S') : comap (AddSubmonoid.inclusion h) (t • x) = t • comap (AddSubmonoid.inclusion h) x

The map on complex points induced by an inclusion of submonoids is equivariant for the ambient characters.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.orbit_default_subset {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) : MulAction.orbit (AddChar M ℂˣ) default ⊆ MulAction.orbit (AddChar ↥S ℂˣ) default

The orbit of the distinguished point under the ambient characters is contained in its orbit under the invertible characters of the submonoid. The two orbits agree when every invertible character of the submonoid is the restriction of an ambient one, as for the dual semigroup of a toric cone with an extending basis.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.continuousConstSMul_affinePointTopology_ambient {r : ℕ} {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} (g : AddGeneratingFamily (↥S) r) : ContinuousConstSMul (AddChar M ℂˣ) (AffineSemigroupComplexPoint ↥S)

Translation by a fixed ambient character is continuous for the monomial-embedding topology of any finite generating family.

theorem TauCeti.Toric.AffineSemigroupComplexPoint.continuousSMul_complexTorus_affinePointTopology {r : ℕ} {N : Type u_4} [AddCommGroup N] {S : AddSubmonoid (IntegralCharacter N)} (g : AddGeneratingFamily (↥S) r) : ContinuousSMul (ComplexTorus N) (AffineSemigroupComplexPoint ↥S)

The coordinate-free complex torus acts jointly continuously on affine complex points with the monomial-embedding topology.

The action in mixed coordinates

theorem TauCeti.Toric.regularAffinePointEquiv_smul_fst {S : Type u_1} [AddCommMonoid S] {ι : Type u_3} {κ : Type u_4} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) (t : AddChar S ℂˣ) (x : AffineSemigroupComplexPoint S) (i : ι) : ((regularAffinePointEquiv e) (t • x)).1 i = ↑(t (e.symm (Finsupp.single i 1, 0))) * ((regularAffinePointEquiv e) x).1 i

In the mixed coordinates of a split semigroup, a character multiplies each unconstrained coordinate by its value on the corresponding standard generator.

theorem TauCeti.Toric.regularAffinePointEquiv_smul_snd {S : Type u_1} [AddCommMonoid S] {ι : Type u_3} {κ : Type u_4} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) (t : AddChar S ℂˣ) (x : AffineSemigroupComplexPoint S) (j : κ) : ((regularAffinePointEquiv e) (t • x)).2 j = t (e.symm (0, Finsupp.single j 1)) * ((regularAffinePointEquiv e) x).2 j

In the mixed coordinates of a split semigroup, a character multiplies each invertible coordinate by its value on the corresponding standard generator.

@[simp]

theorem TauCeti.Toric.regularAffinePointEquiv_default {S : Type u_1} [AddCommMonoid S] {ι : Type u_3} {κ : Type u_4} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : (regularAffinePointEquiv e) default = 1

The distinguished point has all mixed coordinates equal to 1.

theorem TauCeti.Toric.mem_orbit_default_iff_regularAffinePointEquiv {S : Type u_1} [AddCommMonoid S] {ι : Type u_3} {κ : Type u_4} (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) {x : AffineSemigroupComplexPoint S} : x ∈ MulAction.orbit (AddChar S ℂˣ) default ↔ ∀ (i : ι), ((regularAffinePointEquiv e) x).1 i ≠ 0

In mixed coordinates, the orbit of the distinguished point is the locus where every unconstrained coordinate is nonzero.

theorem TauCeti.Toric.dense_orbit_default {S : Type u_1} [AddCommMonoid S] {r : ℕ} {ι : Type u_3} {κ : Type u_4} (g : AddGeneratingFamily S r) (e : S ≃+ (ι →₀ ℕ) × (κ →₀ ℤ)) : Dense (MulAction.orbit (AddChar S ℂˣ) default)

The orbit of the distinguished point is dense in the complex points of a split semigroup, for the monomial-embedding topology of any finite generating family: in mixed coordinates it is the locus where the unconstrained coordinates are nonzero.