The normal-crossings form of the toric boundary

The boundary of the analytic realization of a regular fan is the union of the ray-indexed components TauCeti.Toric.Fan.analyticBoundaryComponent. In the affine chart of a cone σ, read in the regular coordinates of an integral basis extending the primitive ray generators of σ, these components are coordinate hyperplanes: a point of the chart lies in the component of a ray ρ exactly when ρ is a ray of σ and the coordinate indexed by ρ vanishes. Components of rays outside σ miss the chart.

Taking for σ the cone whose torus orbit contains a given point, and identifying the regular coordinates linearly with ℂ ^ n, this gives the simple-normal-crossings normal form of the boundary: near every point there is a holomorphic chart of the realization, defined on the whole affine chart of σ and biholomorphic onto its image, together with an injection from the components through the point to the coordinate indices, such that a point of the chart lies in a component exactly when that component passes through the given point and the corresponding coordinate vanishes. In particular every boundary component is a closed complex hypersurface, locally a coordinate hyperplane.

Main declarations

• TauCeti.Toric.Fan.analyticAffineChartι_mem_analyticBoundaryComponent_iff: in the regular coordinates of an affine chart, a boundary component is the vanishing locus of the coordinate of its ray.
• TauCeti.Toric.Fan.exists_partialDiffeomorph_analyticBoundaryComponent_normalForm: the toric boundary has the holomorphic coordinate-hyperplane normal form near every point.

References

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

theorem TauCeti.Toric.Fan.analyticAffineChartι_mem_analyticBoundaryComponent_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {ι : Type u_1} {b : Module.Basis (ToricRay ↑σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (ρ : Φ.Ray) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x ∈ Φ.analyticBoundaryComponent hΦ ρ ↔ ∃ (h : Ray.toCone Φ ρ ≤ σ), ((coneChartEquiv ⋯ ⋯ hb) x).1 (Ray.toToricRay Φ ρ σ h) = 0

In the regular coordinates of the affine chart of a cone σ, a point lies in the boundary component of a ray ρ exactly when ρ is a ray of σ and the coordinate indexed by ρ vanishes.

theorem TauCeti.Toric.Fan.exists_partialDiffeomorph_analyticBoundaryComponent_normalForm {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (x : ↑(Φ.analyticRealization hΦ)) (n : WithTop ℕ∞) : ∃ (s : Set Φ.Ray) (j : ↑s ↪ Fin (Module.finrank ℤ N)) (e : PartialDiffeomorph (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (↑(Φ.analyticRealization hΦ)) (Fin (Module.finrank ℤ N) → ℂ) n), x ∈ e.source ∧ (∀ (ρ : Φ.Ray), x ∈ Φ.analyticBoundaryComponent hΦ ρ ↔ ρ ∈ s) ∧ ∀ y ∈ e.source, ∀ (ρ : Φ.Ray), y ∈ Φ.analyticBoundaryComponent hΦ ρ ↔ ∃ (hρ : ρ ∈ s), ↑e.toPartialEquiv y (j ⟨ρ, hρ⟩) = 0

The toric boundary has the holomorphic coordinate-hyperplane normal form near every point x of the realization. There are a biholomorphism e from an open neighbourhood of x onto an open subset of ℂ ^ n, for n the rank of the lattice, and an injection j from the set s of boundary components through x to the coordinate indices, such that a point of the neighbourhood lies in a boundary component exactly when that component passes through x and the coordinate it is assigned vanishes.