The orbit–cone correspondence on the analytic realization of a fan

Every cone σ of a regular fan has a distinguished point in the analytic realization: the image of the distinguished point of the top face of σ in the affine chart of σ. Its torus orbit is the image of the stratum of the top face of σ in that chart. This file proves that these orbits are all the torus orbits of the realization, that distinct cones give distinct orbits, and that the closure order on orbits is the reverse of the face order on cones.

The key point is that the stratum of a point does not depend on the chart used to see it. A point of the chart of σ that lies in the stratum of a face F of σ comes from the chart of σ ⊓ τ whenever it also lies in the chart of τ; restriction along a face inclusion preserves strata, so the strata seen in the charts of σ and τ are both the stratum of the same cone. Consequently a point of the chart of σ lies in the orbit of a cone τ exactly when its affine stratum is indexed by τ, and the orbit of τ meets the chart of σ precisely when τ is a face of σ, in the affine stratum of τ. Since every chart is an open subspace of the realization, the closure order is computed in a single chart, where it is the affine closure order.

Main declarations

• TauCeti.Toric.Fan.analyticDistinguishedPoint: the distinguished point of a cone.
• TauCeti.Toric.Fan.analyticConeOrbit: the torus orbit of a cone, with TauCeti.Toric.Fan.analyticConeOrbit_eq_orbit identifying it with the orbit of the distinguished point.
• TauCeti.Toric.Fan.analyticAffineChartι_mem_analyticConeOrbit_iff: a point of a chart lies in the orbit of τ exactly when its affine stratum is indexed by τ.
• TauCeti.Toric.Fan.existsUnique_mem_analyticConeOrbit: the orbits of the cones partition the realization.
• TauCeti.Toric.Fan.coneEquivOrbitRelQuotient: the orbit–cone correspondence between the cones of the fan and the torus orbits of its analytic realization.
• TauCeti.Toric.Fan.analyticConeOrbit_subset_closure_iff and TauCeti.Toric.Fan.closure_analyticConeOrbit: the correspondence reverses the closure order.
• TauCeti.Toric.Fan.mem_stabilizer_analyticDistinguishedPoint_iff: the stabilizer of the distinguished point of σ is the subtorus trivial on the characters vanishing on σ.

References

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

Strata do not depend on the chart

def TauCeti.Toric.Fan.orbitFace {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (h : τ ≤ σ) : (↑σ).Face

A cone τ of a fan, viewed as a face of a cone σ containing it. This is the affine stratum in the chart of σ that represents the global orbit of τ.

@[simp]

theorem TauCeti.Toric.Fan.coe_orbitFace {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (h : τ ≤ σ) : ↑(Φ.orbitFace h) = ↑τ

The cone underlying orbitFace is the smaller cone.

@[simp]

theorem TauCeti.Toric.Fan.orbitFace_refl {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : Φ.orbitFace ⋯ = ⊤

A cone viewed as a face of itself is the top face.

theorem TauCeti.Toric.Fan.coe_eq_coe_of_analyticAffineChartι_eq {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ τ : ↑Φ.cones} {x : ↑(Φ.analyticAffineChartDiagram.obj σ)} {y : ↑(Φ.analyticAffineChartDiagram.obj τ)} (hxy : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) y) {F : (↑σ).Face} {G : (↑τ).Face} (hx : x ∈ affineConeOrbit ⋯ F) (hy : y ∈ affineConeOrbit ⋯ G) : ↑F = ↑G

The stratum of a point of the analytic realization does not depend on the chart: if points of the charts of σ and τ have the same image, and lie in the strata of a face F of σ and a face G of τ, then F and G are the same cone.

Distinguished points and orbits of cones

noncomputable def TauCeti.Toric.Fan.analyticDistinguishedPoint {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : ↑(Φ.analyticRealization hΦ)

The distinguished point of a cone σ of a regular fan: the distinguished point of the top face of σ in the affine chart of σ, viewed in the analytic realization.

theorem TauCeti.Toric.Fan.analyticDistinguishedPoint_def {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticDistinguishedPoint hΦ σ = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) (distinguishedPoint ⋯ ⊤)

The distinguished point of a cone is the image of the distinguished point of its top face.

theorem TauCeti.Toric.Fan.analyticAffineChartι_distinguishedPoint {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (h : τ ≤ σ) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) (distinguishedPoint ⋯ (Φ.orbitFace h)) = Φ.analyticDistinguishedPoint hΦ τ

The distinguished point of a face τ of σ, seen in the chart of σ, is the distinguished point of τ as a face of σ.

noncomputable def TauCeti.Toric.Fan.analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Set ↑(Φ.analyticRealization hΦ)

The torus orbit of a cone σ of a regular fan: the image in the analytic realization of the stratum of the top face of σ in the affine chart of σ. By analyticConeOrbit_eq_orbit, it is the torus orbit of the distinguished point of σ.

theorem TauCeti.Toric.Fan.analyticConeOrbit_def {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticConeOrbit hΦ σ = ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) '' affineConeOrbit ⋯ ⊤

The orbit of a cone is the image of the stratum of its top face.

theorem TauCeti.Toric.Fan.analyticConeOrbit_eq_orbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticConeOrbit hΦ σ = MulAction.orbit (ComplexTorus N) (Φ.analyticDistinguishedPoint hΦ σ)

The orbit of a cone σ is the torus orbit of the distinguished point of σ.

theorem TauCeti.Toric.Fan.smul_mem_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : ↑Φ.cones} (T : ComplexTorus N) {x : ↑(Φ.analyticRealization hΦ)} (hx : x ∈ Φ.analyticConeOrbit hΦ σ) : T • x ∈ Φ.analyticConeOrbit hΦ σ

The torus preserves the orbit of every cone.

theorem TauCeti.Toric.Fan.analyticDistinguishedPoint_mem_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticDistinguishedPoint hΦ σ ∈ Φ.analyticConeOrbit hΦ σ

The distinguished point of a cone lies in its orbit.

theorem TauCeti.Toric.Fan.analyticAffineChartι_mem_analyticConeOrbit_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ τ : ↑Φ.cones} {x : ↑(Φ.analyticAffineChartDiagram.obj σ)} {F : (↑σ).Face} (hx : x ∈ affineConeOrbit ⋯ F) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x ∈ Φ.analyticConeOrbit hΦ τ ↔ ↑F = ↑τ

A point of the chart of σ in the stratum of a face F lies in the orbit of a cone τ exactly when F is the cone τ.

theorem TauCeti.Toric.Fan.preimage_analyticAffineChartι_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (h : τ ≤ σ) : ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) ⁻¹' Φ.analyticConeOrbit hΦ τ = affineConeOrbit ⋯ (Φ.orbitFace h)

The orbit of a face τ of σ meets the chart of σ in the stratum of τ.

theorem TauCeti.Toric.Fan.preimage_analyticAffineChartι_analyticConeOrbit_of_not_le {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (h : ¬τ ≤ σ) : ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) ⁻¹' Φ.analyticConeOrbit hΦ τ = ∅

The orbit of a cone τ does not meet the chart of a cone σ that does not contain τ.

theorem TauCeti.Toric.Fan.mem_range_analyticAffineChartι_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ τ : ↑Φ.cones} {x : ↑(Φ.analyticRealization hΦ)} (hx : x ∈ Φ.analyticConeOrbit hΦ σ) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) ↔ σ ≤ τ

A point in the orbit of σ belongs to the affine chart of τ exactly when σ ≤ τ.

noncomputable def TauCeti.Toric.Fan.analyticConeOrbitChartEquiv {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {υ : ↑Φ.cones} (h : σ ≤ υ) : ↑(affineConeOrbit ⋯ (Φ.orbitFace h)) ≃ ↑(Φ.analyticConeOrbit hΦ σ)

The affine orbit of σ in any containing chart parametrizes the entire global orbit. The parametrization is the affine chart inclusion, independent of coordinate choices.

@[simp]

theorem TauCeti.Toric.Fan.coe_analyticConeOrbitChartEquiv_apply {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {υ : ↑Φ.cones} (h : σ ≤ υ) (x : ↑(affineConeOrbit ⋯ (Φ.orbitFace h))) : ↑((Φ.analyticConeOrbitChartEquiv hΦ σ h) x) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ υ)) ↑x

The affine parametrization of a global orbit is given by the affine chart inclusion.

@[simp]

theorem TauCeti.Toric.Fan.analyticAffineChartι_analyticConeOrbitChartEquiv_symm_apply {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {υ : ↑Φ.cones} (h : σ ≤ υ) (x : ↑(Φ.analyticConeOrbit hΦ σ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ υ)) ↑((Φ.analyticConeOrbitChartEquiv hΦ σ h).symm x) = ↑x

Applying the affine chart inclusion to the inverse orbit parametrization recovers the point.

The orbit–cone correspondence

theorem TauCeti.Toric.Fan.existsUnique_mem_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (x : ↑(Φ.analyticRealization hΦ)) : ∃! σ : ↑Φ.cones, x ∈ Φ.analyticConeOrbit hΦ σ

The orbits of the cones partition the analytic realization: every point lies in the orbit of a unique cone.

theorem TauCeti.Toric.Fan.exists_mem_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (x : ↑(Φ.analyticRealization hΦ)) : ∃ (σ : ↑Φ.cones), x ∈ Φ.analyticConeOrbit hΦ σ

Every point of the analytic realization lies in the orbit of some cone.

theorem TauCeti.Toric.Fan.eq_of_mem_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ τ : ↑Φ.cones} {x : ↑(Φ.analyticRealization hΦ)} (hσ : x ∈ Φ.analyticConeOrbit hΦ σ) (hτ : x ∈ Φ.analyticConeOrbit hΦ τ) : σ = τ

The orbits of two cones meet only when the cones are equal.

noncomputable def TauCeti.Toric.Fan.coneEquivOrbitRelQuotient {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : ↑Φ.cones ≃ MulAction.orbitRel.Quotient (ComplexTorus N) ↑(Φ.analyticRealization hΦ)

The orbit–cone correspondence for a regular fan: the cones of the fan correspond bijectively to the torus orbits of its analytic realization, a cone corresponding to the orbit of its distinguished point. By analyticConeOrbit_subset_closure_iff, the correspondence reverses the closure order.

@[simp]

theorem TauCeti.Toric.Fan.coneEquivOrbitRelQuotient_apply {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : (Φ.coneEquivOrbitRelQuotient hΦ) σ = Quotient.mk'' (Φ.analyticDistinguishedPoint hΦ σ)

The orbit–cone correspondence sends a cone to the orbit of its distinguished point.

theorem TauCeti.Toric.Fan.orbit_coneEquivOrbitRelQuotient {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : ((Φ.coneEquivOrbitRelQuotient hΦ) σ).orbit = Φ.analyticConeOrbit hΦ σ

The torus orbit corresponding to a cone is its orbit analyticConeOrbit.

theorem TauCeti.Toric.Fan.coneEquivOrbitRelQuotient_symm_mk {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : ↑Φ.cones} {x : ↑(Φ.analyticRealization hΦ)} (hx : x ∈ Φ.analyticConeOrbit hΦ σ) : (Φ.coneEquivOrbitRelQuotient hΦ).symm (Quotient.mk'' x) = σ

The cone corresponding to the torus orbit of a point is the cone whose orbit contains it.

The closure order

theorem TauCeti.Toric.Fan.mem_closure_analyticConeOrbit_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ τ : ↑Φ.cones} {x : ↑(Φ.analyticRealization hΦ)} (hx : x ∈ Φ.analyticConeOrbit hΦ σ) : x ∈ closure (Φ.analyticConeOrbit hΦ τ) ↔ τ ≤ σ

A point of the orbit of σ lies in the closure of the orbit of τ exactly when τ is a face of σ.

theorem TauCeti.Toric.Fan.closure_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (τ : ↑Φ.cones) : closure (Φ.analyticConeOrbit hΦ τ) = ⋃ σ ∈ Set.Ici τ, Φ.analyticConeOrbit hΦ σ

The closure of the orbit of a cone τ is the union of the orbits of the cones containing τ.

theorem TauCeti.Toric.Fan.isLocallyClosed_analyticConeOrbit {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : IsLocallyClosed (Φ.analyticConeOrbit hΦ σ)

Every global cone orbit is locally closed in the analytic realization.

theorem TauCeti.Toric.Fan.analyticConeOrbit_subset_closure_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : Φ.analyticConeOrbit hΦ σ ⊆ closure (Φ.analyticConeOrbit hΦ τ) ↔ τ ≤ σ

Under the orbit–cone correspondence, inclusion of cones is the reverse of the closure order on orbits.

Stabilizers

theorem TauCeti.Toric.Fan.mem_stabilizer_analyticDistinguishedPoint_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) (T : ComplexTorus N) : T ∈ MulAction.stabilizer (ComplexTorus N) (Φ.analyticDistinguishedPoint hΦ σ) ↔ ∀ (m : N →+ ℤ), (∀ y ∈ ↑σ, (⋯.realCharacter m) y = 0) → T m = 1

The stabilizer of the distinguished point of a cone σ is the subtorus of torus points that are trivial on the characters vanishing on σ.