Orbit strata of a regular affine toric cone

The face F of a regular toric cone determines a stratum of its affine complex points. A point belongs to this stratum precisely when a monomial is nonzero at the point exactly when its character vanishes on F. This description is intrinsic: it uses neither an extending basis nor a numbering of the rays.

In regular coordinates, the stratum has the familiar form: the coordinate indexed by a ray is zero exactly when that ray belongs to F; every complementary coordinate is already invertible. This identifies the strata with the coordinate pieces of the mixed chart. In particular, every stratum is nonempty and locally closed, the strata are pairwise disjoint and cover the affine chart, and their closure order is the reverse of the face order.

The strata are exactly the orbits of the coordinate-free complex torus. Each stratum contains a distinguished point, taking the value 1 on the monomials of the characters vanishing on F and 0 on all others; the torus preserves every stratum, and in regular coordinates it moves the distinguished point to any other point of its stratum by rescaling the nonzero coordinates. This is the orbit–cone correspondence for the affine chart: faces of the cone correspond bijectively to torus orbits, reversing the closure order. The stabilizer of the distinguished point of F is the subtorus of torus points trivial on the characters vanishing on F: those characters are differences of characters of the dual semigroup vanishing on F, because F is cut out by a single character of the dual semigroup.

Main declarations

• TauCeti.Toric.affineConeOrbit: the intrinsic stratum associated to a face.
• TauCeti.Toric.mem_affineConeOrbit_iff_coneChartEquiv: its coordinate zero-pattern.
• TauCeti.Toric.closure_affineConeOrbit_eq_setOf_coneChartEquiv_fst_eq_zero: the coordinate form of its closure.
• TauCeti.Toric.closure_affineConeOrbit_toricRay_eq_setOf_coneChartEquiv_fst_eq_zero: the closure of the orbit of a ray is a coordinate hyperplane.
• TauCeti.Toric.isLocallyClosed_affineConeOrbit: every affine-cone orbit is locally closed.
• TauCeti.Toric.closure_affineConeOrbit: the intrinsic union formula for its closure.
• TauCeti.Toric.affineConeOrbit_subset_closure_iff: face inclusion is the reverse closure order.
• TauCeti.Toric.distinguishedPoint: the distinguished point of the stratum of a face, with TauCeti.Toric.distinguishedPoint_apply_single computing it on monomials and TauCeti.Toric.coneChartEquiv_distinguishedPoint_fst and TauCeti.Toric.coneChartEquiv_distinguishedPoint_snd computing its regular coordinates.
• TauCeti.Toric.smul_mem_affineConeOrbit_iff: the torus preserves every stratum.
• TauCeti.Toric.affineConeOrbit_eq_orbit and TauCeti.Toric.orbit_eq_affineConeOrbit: every stratum is a single torus orbit.
• TauCeti.Toric.faceEquivOrbitRelQuotient: the orbit–cone correspondence between the faces of a regular cone and the torus orbits in its affine chart.
• TauCeti.Toric.mem_stabilizer_distinguishedPoint_iff: the stabilizer of the distinguished point of a face is the subtorus of torus points trivial on the characters vanishing on that face.
• TauCeti.Toric.affineConeOrbitHomeomorph: complementary nonzero ray coordinates and torus coordinates parametrize an affine orbit with its subspace topology.
• TauCeti.Toric.isManifold_affineConeOrbitChartedSpace: these coordinates give the orbit a complex-manifold structure.
• TauCeti.Toric.contMDiff_affineConeOrbitAmbient: the defining orbit chart is holomorphic.
• TauCeti.Toric.contMDiff_subtypeVal_affineConeOrbit: the inclusion of an affine orbit in its cone chart is holomorphic.

References

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

def TauCeti.Toric.affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (F : σ.Face) : Set (AffineSemigroupComplexPoint ↥(dualSemigroup hi σ))

The stratum of the affine toric chart associated to a face F. Its points are those for which a monomial is nonzero exactly when the corresponding character vanishes identically on F. This is the coordinate-free description of the stratum attached to F; for a regular cone, affineConeOrbit_eq_orbit identifies it with the torus orbit of distinguishedPoint hi F.

@[simp]

theorem TauCeti.Toric.mem_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (F : σ.Face) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : x ∈ affineConeOrbit hi F ↔ ∀ (m : ↥(dualSemigroup hi σ)), x (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) ≠ 0 ↔ ∀ y ∈ F, (hi.realCharacter ↑m) y = 0

Membership in an affine-cone orbit is characterized by nonvanishing of precisely the monomials whose characters vanish on the associated face.

theorem TauCeti.Toric.mem_affineConeOrbit_iff_coneChartEquiv {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : x ∈ affineConeOrbit hi F ↔ ∀ (ρ : ToricRay σ), ((coneChartEquiv hi ⋯ hb) x).1 ρ = 0 ↔ ρ ∈ (IsRegularCone.faceOrderIso hi hσ) F

In regular coordinates, a point belongs to the orbit of F exactly when its ray coordinate is zero precisely at the rays contained in F.

theorem TauCeti.Toric.preimage_zeroPatternSet_eq_affineConeOrbit {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) : ⇑(coneChartEquiv hi ⋯ hb) ⁻¹' zeroPatternSet (ToricRay σ) (ι → ℂˣ) ℂ ((IsRegularCone.faceOrderIso hi hσ) F) = affineConeOrbit hi F

Under any extending-basis chart, the intrinsic orbit of F is the inverse image of the coordinate stratum attached to the rays of F.

Intrinsic consequences

theorem TauCeti.Toric.nonempty_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F : σ.Face) : (affineConeOrbit hi F).Nonempty

Every face-indexed affine-cone orbit is nonempty.

theorem TauCeti.Toric.existsUnique_face_mem_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : ∃! F : σ.Face, x ∈ affineConeOrbit hi F

The orbit strata form a partition: every affine complex point belongs to the orbit of a unique face.

theorem TauCeti.Toric.isLocallyClosed_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; IsLocallyClosed (affineConeOrbit hi F)

Every affine-cone orbit is locally closed in the monomial-embedding topology.

theorem TauCeti.Toric.closure_affineConeOrbit_eq_setOf_coneChartEquiv_fst_eq_zero {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; closure (affineConeOrbit hi F) = {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) | ∀ ρ ∈ (IsRegularCone.faceOrderIso hi hσ) F, ((coneChartEquiv hi ⋯ hb) x).1 ρ = 0}

The closure of the orbit of F consists of the points whose coordinates at all rays of F vanish; coordinates at other rays may vanish as well.

theorem TauCeti.Toric.closure_affineConeOrbit_toricRay_eq_setOf_coneChartEquiv_fst_eq_zero {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (ρ : ToricRay σ) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; closure (affineConeOrbit hi ↑ρ) = {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) | ((coneChartEquiv hi ⋯ hb) x).1 ρ = 0}

The closure of the orbit of a ray is the coordinate hyperplane on which the coordinate of that ray vanishes.

theorem TauCeti.Toric.mem_closure_affineConeOrbit_iff_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F G : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} (hx : x ∈ affineConeOrbit hi G) : have x_1 := affinePointTopology g; x ∈ closure (affineConeOrbit hi F) ↔ F ≤ G

A point of the orbit of G lies in the closure of the orbit of F exactly when F is a face of G.

theorem TauCeti.Toric.closure_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; closure (affineConeOrbit hi F) = ⋃ G ∈ Set.Ici F, affineConeOrbit hi G

The closure of the orbit stratum of F is the union of the strata indexed by faces containing F.

theorem TauCeti.Toric.affineConeOrbit_subset_closure_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F G : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; affineConeOrbit hi G ⊆ closure (affineConeOrbit hi F) ↔ F ≤ G

Face inclusion is the reverse closure order on affine-cone orbits.

noncomputable def TauCeti.Toric.affineConeOrbitHomeomorph {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; ↑(affineConeOrbit hi F) ≃ₜ ({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → { z : ℂ // z ≠ 0 }) × (ι → ℂˣ)

In an extending-basis chart, the orbit of a face is homeomorphic to the nonzero ray coordinates outside the face, together with all complementary torus coordinates. This gives the affine orbit its expected product topology without choosing a topology on a new carrier.

@[simp]

theorem TauCeti.Toric.val_affineConeOrbitHomeomorph_fst_apply {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (x : ↑(affineConeOrbit hi F)) (ρ : { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }) : ↑(((affineConeOrbitHomeomorph hi hσ hb F g) x).1 ρ) = ((coneChartEquiv hi ⋯ hb) ↑x).1 ↑ρ

The first orbit coordinates are exactly the nonzero ray coordinates of the affine chart.

@[simp]

theorem TauCeti.Toric.affineConeOrbitHomeomorph_snd_apply {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (x : ↑(affineConeOrbit hi F)) : ((affineConeOrbitHomeomorph hi hσ hb F g) x).2 = ((coneChartEquiv hi ⋯ hb) ↑x).2

The complementary torus coordinates are unchanged in the orbit chart.

@[simp]

theorem TauCeti.Toric.affineConeOrbitHomeomorph_symm_apply_coe {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (w : ({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → { z : ℂ // z ≠ 0 }) × (ι → ℂˣ)) : have x := affinePointTopology g; ↑((Homeomorph.symm (affineConeOrbitHomeomorph hi hσ hb F g)) w) = (coneChartEquiv hi ⋯ hb).symm ↑((zeroPatternSetHomeomorph (ToricRay σ) (ι → ℂˣ) ℂ ((IsRegularCone.faceOrderIso hi hσ) F)).symm w)

The inverse orbit chart reconstructs the underlying affine point from its coordinates.

noncomputable def TauCeti.Toric.affineConeOrbitAmbient {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (x : ↑(affineConeOrbit hi F)) : ({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ)

Ambient coordinates on an affine orbit: retain exactly the nonzero ray coordinates outside the face, and view all torus coordinates as complex numbers.

@[simp]

theorem TauCeti.Toric.affineConeOrbitAmbient_fst_apply {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (x : ↑(affineConeOrbit hi F)) (ρ : { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }) : (affineConeOrbitAmbient hi hσ hb F x).1 ρ = ((coneChartEquiv hi ⋯ hb) ↑x).1 ↑ρ

The first ambient coordinates are the nonzero ray coordinates of the cone chart.

@[simp]

theorem TauCeti.Toric.affineConeOrbitAmbient_snd_apply {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (x : ↑(affineConeOrbit hi F)) (j : ι) : (affineConeOrbitAmbient hi hσ hb F x).2 j = ↑(((coneChartEquiv hi ⋯ hb) ↑x).2 j)

The second ambient coordinates are the complex values of the torus coordinates.

@[simp]

theorem TauCeti.Toric.range_affineConeOrbitAmbient {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) : Set.range (affineConeOrbitAmbient hi hσ hb F) = {w : ({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ) | (∀ (ρ : { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }), w.1 ρ ≠ 0) ∧ ∀ (j : ι), w.2 j ≠ 0}

The ambient orbit chart ranges over pairs whose coordinates are all nonzero.

theorem TauCeti.Toric.isOpenEmbedding_affineConeOrbitAmbient {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; Topology.IsOpenEmbedding (affineConeOrbitAmbient hi hσ hb F)

The retained coordinates realize the affine orbit as an open subset of a complex vector space. In particular, their topology is the subspace topology inherited from the affine chart.

@[instance_reducible]

noncomputable def TauCeti.Toric.affineConeOrbitChartedSpace {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; ChartedSpace (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ)) ↑(affineConeOrbit hi F)

The complex charted-space structure on an affine orbit, using its complementary nonzero ray coordinates and torus coordinates. The orbit retains the topology induced from the affine chart.

theorem TauCeti.Toric.affineConeOrbitChartedSpace_chartAt {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (x : ↑(affineConeOrbit hi F)) : have x_1 := affinePointTopology g; ↑(chartAt (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ)) x) = affineConeOrbitAmbient hi hσ hb F

Every chart of the orbit charted space is the ambient coordinate map.

theorem TauCeti.Toric.affineConeOrbitChartedSpace_chartAt_target {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (x : ↑(affineConeOrbit hi F)) : have x_1 := affinePointTopology g; (chartAt (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ)) x).target = {w : ({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ) | (∀ (ρ : { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }), w.1 ρ ≠ 0) ∧ ∀ (j : ι), w.2 j ≠ 0}

The target of each orbit chart is the locus of nonzero ambient coordinates.

theorem TauCeti.Toric.isManifold_affineConeOrbitChartedSpace {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) [Fintype { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }] [Fintype ι] (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := affineConeOrbitChartedSpace hi hσ hb F g; IsManifold (modelWithCornersSelf ℂ (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ))) n ↑(affineConeOrbit hi F)

Every affine-cone orbit is a complex manifold, modeled on the nonzero ray directions outside its face and the complementary torus directions.

theorem TauCeti.Toric.contMDiff_affineConeOrbitAmbient {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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) [Fintype { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }] [Fintype ι] (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := affineConeOrbitChartedSpace hi hσ hb F g; ContMDiff (modelWithCornersSelf ℂ (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ))) (modelWithCornersSelf ℂ (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (ι → ℂ))) n (affineConeOrbitAmbient hi hσ hb F)

The ambient orbit coordinates are holomorphic for the charted-space structure they induce.

theorem TauCeti.Toric.contMDiff_subtypeVal_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) {k l : ℕ} {b : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) [Fintype { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }] (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := affineConeOrbitChartedSpace hi hσ hb F g; have x_2 := coneChartedSpace hi ⋯ hb κ g; ContMDiff (modelWithCornersSelf ℂ (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n fun (x : ↑(affineConeOrbit hi F)) => ↑x

The inclusion of an affine-cone orbit into the affine analytic chart is holomorphic. In regular coordinates it inserts zero in precisely the ray coordinates belonging to the face and retains all other coordinates.

theorem TauCeti.Toric.contMDiff_of_contMDiff_subtypeVal_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) {k l : ℕ} {b : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (F : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) [Fintype { ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F }] {E : Type u_4} {H : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ↑(affineConeOrbit hi F)} {n : WithTop ℕ∞} (hf : let x := affinePointTopology g; have x_1 := coneChartedSpace hi ⋯ hb κ g; ContMDiff I (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n fun (x : M) => ↑(f x)) : let x := affinePointTopology g; have x_1 := affineConeOrbitChartedSpace hi hσ hb F g; ContMDiff I (modelWithCornersSelf ℂ (({ ρ : ToricRay σ // ρ ∉ (IsRegularCone.faceOrderIso hi hσ) F } → ℂ) × (Fin l → ℂ))) n f

A map into an affine-cone orbit is holomorphic when its composite with the inclusion into the affine analytic chart is holomorphic. This is the elimination principle for the orbit's regular coordinate chart.

The strata are the torus orbits

noncomputable def TauCeti.Toric.distinguishedPoint {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (F : σ.Face) : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)

The distinguished point of the stratum of a face F: the complex point taking the value 1 on the monomials of the characters that vanish on F, and 0 on all other monomials. It lies in affineConeOrbit hi F, and for the smallest face it is the distinguished point default of the dense torus.

@[simp]

theorem TauCeti.Toric.distinguishedPoint_apply_single {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (F : σ.Face) (m : ↥(dualSemigroup hi σ)) : (distinguishedPoint hi F) (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) = if ∀ y ∈ F, (hi.realCharacter ↑m) y = 0 then 1 else 0

The distinguished point of F takes the value 1 on the monomial of a character vanishing on F, and 0 on the monomial of any other character.

theorem TauCeti.Toric.distinguishedPoint_mem_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (F : σ.Face) : distinguishedPoint hi F ∈ affineConeOrbit hi F

The distinguished point of a face lies in the stratum of that face.

@[simp]

theorem TauCeti.Toric.distinguishedPoint_bot {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) : distinguishedPoint hi ⊥ = default

Every character of the dual semigroup vanishes on the smallest face of σ, its lineality space, so the distinguished point of that face is the distinguished point default of the dense torus.

theorem TauCeti.Toric.smul_mem_affineConeOrbit_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (F : σ.Face) (T : ComplexTorus N) {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} : T • x ∈ affineConeOrbit hi F ↔ x ∈ affineConeOrbit hi F

The torus preserves every stratum: translating a point by a torus point multiplies its value on each monomial by a unit, so it does not change which monomials vanish.

theorem TauCeti.Toric.coneChartEquiv_distinguishedPoint_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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) (ρ : ToricRay σ) : ((coneChartEquiv hi ⋯ hb) (distinguishedPoint hi F)).1 ρ = if ρ ∈ (IsRegularCone.faceOrderIso hi hσ) F then 0 else 1

In the chart of an extending basis, the ray coordinates of the distinguished point of F vanish at the rays of F and equal 1 at all other rays.

@[simp]

theorem TauCeti.Toric.coneChartEquiv_distinguishedPoint_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σ : IsRegularCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (F : σ.Face) : ((coneChartEquiv hi ⋯ hb) (distinguishedPoint hi F)).2 = 1

In the chart of an extending basis, the torus coordinates of the distinguished point of every face are equal to 1.

theorem TauCeti.Toric.affineConeOrbit_eq_orbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F : σ.Face) : affineConeOrbit hi F = MulAction.orbit (ComplexTorus N) (distinguishedPoint hi F)

The stratum of a face F of a regular cone is a single torus orbit, namely the orbit of the distinguished point of F.

theorem TauCeti.Toric.orbit_eq_affineConeOrbit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) {F : σ.Face} {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} (hx : x ∈ affineConeOrbit hi F) : MulAction.orbit (ComplexTorus N) x = affineConeOrbit hi F

The torus orbit of any point of the stratum of a face F of a regular cone is that whole stratum.

noncomputable def TauCeti.Toric.faceEquivOrbitRelQuotient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) : σ.Face ≃ MulAction.orbitRel.Quotient (ComplexTorus N) (AffineSemigroupComplexPoint ↥(dualSemigroup hi σ))

The orbit–cone correspondence for the affine chart of a regular cone: the faces of the cone correspond bijectively to the torus orbits in its complex points, a face F corresponding to the orbit of its distinguished point, which is the stratum affineConeOrbit hi F. By affineConeOrbit_subset_closure_iff, the correspondence reverses the closure order.

@[simp]

theorem TauCeti.Toric.faceEquivOrbitRelQuotient_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F : σ.Face) : (faceEquivOrbitRelQuotient hi hσ) F = Quotient.mk'' (distinguishedPoint hi F)

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

theorem TauCeti.Toric.orbit_faceEquivOrbitRelQuotient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F : σ.Face) : ((faceEquivOrbitRelQuotient hi hσ) F).orbit = affineConeOrbit hi F

The torus orbit corresponding to a face is its stratum.

theorem TauCeti.Toric.orbit_faceEquivOrbitRelQuotient_subset_closure_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F G : σ.Face) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : have x := affinePointTopology g; ((faceEquivOrbitRelQuotient hi hσ) G).orbit ⊆ closure ((faceEquivOrbitRelQuotient hi hσ) F).orbit ↔ F ≤ G

Under the orbit–cone correspondence, face inclusion is the reverse of orbit closure inclusion.

theorem TauCeti.Toric.faceEquivOrbitRelQuotient_symm_mk {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) {F : σ.Face} {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} (hx : x ∈ affineConeOrbit hi F) : (faceEquivOrbitRelQuotient hi hσ).symm (Quotient.mk'' x) = F

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

theorem TauCeti.Toric.mem_stabilizer_distinguishedPoint_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) (F : σ.Face) (T : ComplexTorus N) : T ∈ MulAction.stabilizer (ComplexTorus N) (distinguishedPoint hi F) ↔ ∀ (m : N →+ ℤ), (∀ y ∈ F, (hi.realCharacter m) y = 0) → T m = 1

The stabilizer of the distinguished point of a face F of a regular cone is the subtorus of torus points that are trivial on the sublattice of characters vanishing on F.