Toric maps of analytic realizations are holomorphic

A morphism of regular fans f : FanHom Φ Ψ induces the continuous map TauCeti.Toric.FanHom.analyticMap between their analytic realizations. This file proves that it is holomorphic for the complex manifold structures of the two realizations.

Holomorphy is local. On the chart of a cone σ of Φ, the glued map is the pullback of complex points along the map of dual semigroups into the chart of the least target cone υ, followed by the inclusion of that chart. For extending bases of σ and υ, the inclusion of the chart of σ is a biholomorphism onto its open image, the pullback is holomorphic because it carries monomials to monomials, and the inclusion of the chart of υ is holomorphic.

Main declarations

• TauCeti.Toric.FanHom.contMDiff_analyticMap: the map of analytic realizations induced by a morphism of regular fans is holomorphic.

References

• W. Fulton, Introduction to Toric Varieties, §§1.4 and 2.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §3.3.

theorem TauCeti.Toric.FanHom.contMDiff_analyticMap {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N') → ℂ)) n ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ))

The map between the analytic realizations of two regular fans induced by a fan morphism is holomorphic, for their complex manifold structures modelled on ℂ ^ n and ℂ ^ n', where n and n' are the ranks of the two lattices.