The torus action on a fan realization is holomorphic

The coordinate-free complex torus acts on the analytic realization of a regular fan by translating points of the affine charts. This file proves that the action map ComplexTorus N × X_Φ → X_Φ is holomorphic, for the complex structure of the realization and the complex structure of the torus given by any free presentation of its character lattice.

Holomorphy is local. Near a point of the image of the affine chart of a cone σ, the action is the affine torus action on that chart, conjugated by the inclusion of the chart, which is a biholomorphism onto its open image. The affine action is holomorphic for the complex structure of an integral basis extending the primitive ray generators of σ. Consequently the canonical inclusion of the complex torus into the realization of a nonempty regular fan, the orbit map of the distinguished point of the zero cone, is holomorphic.

Main declarations

• TauCeti.Toric.Fan.contMDiffSMul_complexTorus_analyticRealization: the complex torus acts holomorphically on the analytic realization of a regular fan.
• TauCeti.Toric.Fan.contMDiff_analyticTorusι: the canonical torus inclusion is holomorphic.

References

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

theorem TauCeti.Toric.Fan.contMDiffSMul_complexTorus_analyticRealization {N V : Type u} {ι : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (n : WithTop ℕ∞) : have x := complexTorusChartedSpace e; ContMDiffSMul (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) n (ComplexTorus N) ↑(Φ.analyticRealization hΦ)

The coordinate-free complex torus acts holomorphically on the analytic realization of a regular fan. The torus carries the complex structure of a free presentation of its character lattice, and the realization its complex manifold structure modelled on ℂ ^ n.

theorem TauCeti.Toric.Fan.contMDiff_analyticTorusι {N V : Type u} {ι : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (n : WithTop ℕ∞) : have x := complexTorusChartedSpace e; ContMDiff (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) n (Φ.analyticTorusι hΦ hΦ0)

The canonical torus inclusion into the realization of a nonempty regular fan is holomorphic, for any finite free presentation of the character lattice: it is the orbit map of the distinguished point of the zero cone under the holomorphic torus action.