Documentation

TauCeti.Geometry.Toric.Analytic.Cone.TorusAction.Basic

The torus action on the affine chart of a toric cone #

The coordinate-free complex torus ComplexTorus N of an integral lattice N consists of the invertible characters of the character lattice N →+ ℤ. The dual semigroup of a toric cone σ is a submonoid of that lattice, so the torus acts on the complex points of the affine toric scheme of σ by restricting characters to the dual semigroup and multiplying values on monomials.

In the affine analytic chart attached to an integral basis extending the primitive ray generators of σ, the action is coordinatewise multiplication: a torus point multiplies the coordinate indexed by a basis vector by its value on the coordinate functional of that vector. The orbit of the distinguished point, at which every monomial takes the value 1, is exactly the locus where all ray coordinates are nonzero; the torus acts freely on it, so it is a copy of the torus, and it is open and dense in the chart. This is the dense torus of the affine toric variety of σ.

Main declarations #

References #

The action in the chart of an extending basis #

source
theorem TauCeti.Toric.coneChartEquiv_smul_fst {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (T : ComplexTorus N) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (ρ : ToricRay σ) :
((coneChartEquiv hi hσ hb) (T • x)).1 ρ = ↑(T (b.coord (Sum.inl ρ)).toAddMonoidHom) * ((coneChartEquiv hi hσ hb) x).1 ρ

A torus point multiplies the coordinate of the chart indexed by a ray by its value on the coordinate functional of the primitive generator of that ray.

source
theorem TauCeti.Toric.coneChartEquiv_smul_snd {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (T : ComplexTorus N) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (j : ι) :
((coneChartEquiv hi hσ hb) (T • x)).2 j = T (b.coord (Sum.inr j)).toAddMonoidHom * ((coneChartEquiv hi hσ hb) x).2 j

A torus point multiplies the coordinate of the chart indexed by a complementary basis vector by its value on the coordinate functional of that vector.

source
@[simp]
theorem TauCeti.Toric.coneChartEquiv_default {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) :
(coneChartEquiv hi hσ hb) default = 1

The distinguished point has all chart coordinates equal to 1.

The dense torus of the chart #

source
theorem TauCeti.Toric.complexTorus_smul_default_injective {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) :
Function.Injective fun (T : ComplexTorus N) => T • default

The torus acts freely on the distinguished point of the affine chart: the coordinate functionals of an extending basis lie in the dual semigroup and determine a torus point.

source
theorem TauCeti.Toric.mem_orbit_complexTorus_default_iff {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} :
x ∈ MulAction.orbit (ComplexTorus N) default ↔ ∀ (ρ : ToricRay σ), ((coneChartEquiv hi hσ hb) x).1 ρ ≠ 0

The torus orbit of the distinguished point is the locus of the affine chart where every ray coordinate is nonzero: a point with nonzero ray coordinates is the translate of the distinguished point by the torus point with those basis coordinates.

source
theorem TauCeti.Toric.orbit_complexTorus_default_eq_orbit {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) :
MulAction.orbit (ComplexTorus N) default = MulAction.orbit (AddChar ↥(dualSemigroup hi σ) ℂˣ) default

Every invertible character of the dual semigroup of a cone with an extending basis is the restriction of a torus point: the torus orbit of the distinguished point is its orbit under all invertible characters of the dual semigroup.

source
theorem TauCeti.Toric.isOpen_orbit_complexTorus_default {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) :
IsOpen (MulAction.orbit (ComplexTorus N) default)

The dense torus of the affine chart is open for the monomial-embedding topology of any finite generating family of the dual semigroup.

source
theorem TauCeti.Toric.dense_orbit_complexTorus_default {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) :
Dense (MulAction.orbit (ComplexTorus N) default)

The dense torus of the affine chart is dense for the monomial-embedding topology of any finite generating family of the dual semigroup.

The affine chart of the zero cone #

source
noncomputable def TauCeti.Toric.zeroConeChartHomeomorphOfBasis {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {l s : ℕ} {B : Module.Basis (ToricRay ⊥ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ⊥), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (g : AddGeneratingFamily (↥(dualSemigroup hi ⊥)) s) :
ComplexTorus N ≃ₜ AffineSemigroupComplexPoint ↥(dualSemigroup hi ⊥)

An extending basis identifies the coordinate-free complex torus with the affine chart of the zero cone, for the monomial-embedding topology of any finite generating family. The identification sends a torus point to its translate of the distinguished point, independently of these choices.

Instances For
    source
    @[simp]
    theorem TauCeti.Toric.zeroConeChartHomeomorphOfBasis_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {l s : ℕ} {B : Module.Basis (ToricRay ⊥ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ⊥), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (g : AddGeneratingFamily (↥(dualSemigroup hi ⊥)) s) (t : ComplexTorus N) :
    (zeroConeChartHomeomorphOfBasis hi hB g) t = t • default

    The zero-cone chart identification is the orbit map of the distinguished point.