Toric maps on the dense complex torus

The analytic map of a fan morphism is equivariant for the complex-torus homomorphism induced by its lattice map. On the canonical dense torus inclusion it agrees with that homomorphism. Since analytic fan realizations are Hausdorff, this restriction determines the analytic map uniquely among continuous maps. Thus the lattice map determines its extension to the fan realization without reference to choices of affine coordinates.

References

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

theorem TauCeti.Toric.FanHom.analyticChartMap_smul {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 Φ Ψ) {σ : ↑Φ.cones} {τ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑τ) (t : ComplexTorus N) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : (CategoryTheory.ConcreteCategory.hom (f.analyticChartMap h)) (t • x) = (complexTorusMap f.latticeMap) t • (CategoryTheory.ConcreteCategory.hom (f.analyticChartMap h)) x

The map between affine charts is equivariant for the torus homomorphism induced by the lattice map of the fan morphism.

@[simp]

theorem TauCeti.Toric.FanHom.analyticMap_smul {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) (t : ComplexTorus N) (x : ↑(Φ.analyticRealization hΦ)) : (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) (t • x) = (complexTorusMap f.latticeMap) t • (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) x

Analytic toric maps are equivariant for the lattice-induced homomorphism of complex tori.

@[simp]

theorem TauCeti.Toric.FanHom.analyticMap_analyticTorusι {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) (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) : (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) (Φ.analyticTorusι hΦ hΦ0 t) = Ψ.analyticTorusι hΨ ⋯ ((complexTorusMap f.latticeMap) t)

On the canonical dense torus inclusion, the analytic toric map is the homomorphism of tori induced by the underlying lattice map. The fan morphism supplies target nonemptiness from source nonemptiness; any other target witness gives a definitionally equal inclusion.

theorem TauCeti.Toric.FanHom.eq_analyticMap_iff {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) (hΦ0 : Nonempty ↑Φ.cones) {g : Φ.analyticRealization hΦ ⟶ Ψ.analyticRealization hΨ} : g = f.analyticMap hΦ hΨ ↔ ∀ (t : ComplexTorus N), (CategoryTheory.ConcreteCategory.hom g) (Φ.analyticTorusι hΦ hΦ0 t) = Ψ.analyticTorusι hΨ ⋯ ((complexTorusMap f.latticeMap) t)

A continuous map is the analytic toric map exactly when it extends the lattice-induced map of dense tori. Source nonemptiness is needed to define the canonical torus inclusions; the fan morphism supplies target nonemptiness. Any other target witness gives the same statement by definitional equality.