The cone-by-cone properness criterion for analytic toric maps

Let f : Φ → Ψ be a morphism of regular fans with real-linear map f_ℝ, and let τ be a cone of Ψ. The source cones σ with f_ℝ σ ⊆ τ are exactly those whose charts the analytic map sends into the chart of τ, and their union always lies in the inverse image f_ℝ⁻¹ τ. The support condition for τ asks that the two sets be equal. This file proves that, for a nonempty source fan, the analytic map is proper exactly when the support condition holds for every target cone.

For the necessity of the support condition, the proof follows the one for compact realizations (TauCeti.Toric.Fan.isComplete_of_compactSpace_analyticRealization). Given w with f_ℝ w ∈ τ, the torus points t k at which each character m has absolute value exp (-k ⟨m, w⟩) are sent by the analytic map to torus points at which every character of the dual semigroup of τ has absolute value at most 1. These lie in a compact part of the chart of τ, so properness gives a cluster point p of the t k. The image of p lies in the chart of τ, so p lies in the orbit of a source cone σ with f_ℝ σ ⊆ τ, hence in the chart of σ, and then w ∈ σ.

For the sufficiency, every compact subset of the target realization is covered by finitely many parts of charts, of cones τ, where the generators of the dual semigroup of τ have absolute value less than some R. The torus points t mapped into such a part are those for which the point w of V with ⟨m, w⟩ = -log ‖t m‖ satisfies -log R ≤ ⟨m, f_ℝ w⟩ for the generators m. By Hoffman's error bound (TauCeti.exists_forall_abs_apply_sub_le_of_forall_neg_le) such a w is within bounded distance of a point of f_ℝ⁻¹ τ, which by the support condition lies in a source cone σ mapped into τ. So t lies in a part of the chart of σ where the generators of the dual semigroup of σ are bounded by a constant depending only on R. These finitely many compact sets contain the torus points of the open preimage, hence its closure.

The nonemptiness hypothesis is necessary for the criterion: the empty subfan of a nonempty fan has a proper inclusion, but 0 lies in the inverse image of every ambient cone and in no cone of the empty subfan. Sufficiency holds without it.

Main declarations

• TauCeti.Toric.FanHom.preimage_realMap_eq_iUnion_of_isProperMap: if the analytic map of a morphism of regular fans with nonempty source is proper, then for every target cone τ the inverse image of τ is the union of the source cones mapped into τ.
• TauCeti.Toric.FanHom.isProperMap_analyticMap_of_preimage_realMap_subset: conversely, if for every target cone τ the inverse image of τ is covered by the source cones mapped into τ, then the analytic map is proper.
• TauCeti.Toric.FanHom.isProperMap_analyticMap_iff: the cone-by-cone properness criterion for a nonempty source fan.
• TauCeti.Toric.FanHom.isProperMap_analyticMap_of_isEmpty and TauCeti.Toric.FanHom.not_forall_preimage_realMap_eq_iUnion_of_isEmpty: a map out of a fan with no cones is proper but, for a nonempty target, fails the support condition.
• TauCeti.Toric.FanHom.isProperMap_analyticMap_iff_isEmpty_or: the criterion for an arbitrary source fan.

References

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

theorem TauCeti.Toric.FanHom.preimage_realMap_eq_iUnion_of_isProperMap {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) (hf : IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ))) (τ : ↑Ψ.cones) : ⇑f.realMap ⁻¹' ↑↑τ = ⋃ (σ : ↑Φ.cones), ⋃ (_ : PointedCone.map f.realMap ↑σ ≤ ↑τ), ↑↑σ

If the analytic map of a morphism of regular fans with nonempty source is proper, then for every target cone τ the inverse image of τ under the real-linear map is the union of the source cones mapped into τ. The nonemptiness hypothesis is necessary: the inclusion of the empty subfan is proper, but 0 lies in the inverse image of every cone and in no cone of the empty fan.

theorem TauCeti.Toric.FanHom.isProperMap_analyticMap_of_preimage_realMap_subset {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 : ∀ (τ : ↑Ψ.cones), ⇑f.realMap ⁻¹' ↑↑τ ⊆ ⋃ (σ : ↑Φ.cones), ⋃ (_ : PointedCone.map f.realMap ↑σ ≤ ↑τ), ↑↑σ) : IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ))

If, for every target cone τ, the inverse image of τ under the real-linear map is covered by the source cones mapped into τ, then the analytic map of a morphism of regular fans is proper. The inverse inclusion always holds.

theorem TauCeti.Toric.FanHom.isProperMap_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) : IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ↔ ∀ (τ : ↑Ψ.cones), ⇑f.realMap ⁻¹' ↑↑τ = ⋃ (σ : ↑Φ.cones), ⋃ (_ : PointedCone.map f.realMap ↑σ ≤ ↑τ), ↑↑σ

The cone-by-cone properness criterion. The analytic map of a morphism of regular fans with nonempty source is proper exactly when, for every target cone τ, the inverse image of τ under the real-linear map is the union of the source cones mapped into τ. The nonemptiness hypothesis is necessary: the inclusion of the empty subfan is proper, but 0 lies in the inverse image of every cone and in no cone of the empty fan. See TauCeti.Toric.FanHom.isProperMap_analyticMap_iff_isEmpty_or for the form without it.

theorem TauCeti.Toric.FanHom.isProperMap_analyticMap_of_isEmpty {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) [IsEmpty ↑Φ.cones] : IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ))

The analytic map out of the realization of a fan with no cones is proper, since that realization is empty.

theorem TauCeti.Toric.FanHom.not_forall_preimage_realMap_eq_iUnion_of_isEmpty {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 Φ Ψ) [IsEmpty ↑Φ.cones] (hΨ0 : Nonempty ↑Ψ.cones) : ¬∀ (τ : ↑Ψ.cones), ⇑f.realMap ⁻¹' ↑↑τ = ⋃ (σ : ↑Φ.cones), ⋃ (_ : PointedCone.map f.realMap ↑σ ≤ ↑τ), ↑↑σ

A morphism from a fan with no cones to a nonempty fan fails the cone-by-cone support condition: 0 lies in the inverse image of every target cone, and in no source cone. Together with TauCeti.Toric.FanHom.isProperMap_analyticMap_of_isEmpty, this shows that the nonemptiness hypothesis of TauCeti.Toric.FanHom.isProperMap_analyticMap_iff cannot be dropped; the inclusion of the empty subfan of a nonempty fan is such a morphism.

theorem TauCeti.Toric.FanHom.isProperMap_analyticMap_iff_isEmpty_or {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) : IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ↔ IsEmpty ↑Φ.cones ∨ ∀ (τ : ↑Ψ.cones), ⇑f.realMap ⁻¹' ↑↑τ = ⋃ (σ : ↑Φ.cones), ⋃ (_ : PointedCone.map f.realMap ↑σ ≤ ↑τ), ↑↑σ

The cone-by-cone properness criterion, for an arbitrary source fan. The analytic map of a morphism of regular fans is proper exactly when the source fan has no cones or, for every target cone τ, the inverse image of τ under the real-linear map is the union of the source cones mapped into τ. By TauCeti.Toric.FanHom.not_forall_preimage_realMap_eq_iUnion_of_isEmpty, the first case cannot be absorbed into the second when the target fan is nonempty.

theorem TauCeti.Toric.FanHom.isProperMap_analyticMap_of_isComplete {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) (hc : Φ.IsComplete) : IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ))

A continuous analytic map from the realization of a complete regular fan is proper.