Documentation

TauCeti.Geometry.Toric.Analytic.Fan.Compact

Compactness of the analytic realization of a regular fan #

A nonempty regular fan has compact analytic realization exactly when it is complete, that is, when its cones cover the ambient real vector space V.

Both directions read the absolute values of characters on the dense torus. For a torus point t, the numbers -log ‖t m‖ are additive in the character m, so they are the values at a single point w of V of the real extensions of the characters (TauCeti.Toric.IsIntegralLattice.exists_realCharacter_apply_eq). When w lies in a cone σ, every character of the dual semigroup of σ has absolute value at most 1 at t, so t lies in the image of the compact part of the chart of σ where all monomials are bounded by 1 (TauCeti.Toric.isCompact_setOf_forall_norm_apply_single_le_one). For a complete fan these finitely many compact sets cover the dense torus, and hence its closure, the whole realization.

Conversely, given w in V, the torus points t k with ‖t k m‖ = exp (-k ⟨m, w⟩) have a cluster point in a compact realization, which lies in the chart of some cone σ. Near that point every character of the dual semigroup of σ is bounded, which forces 0 ≤ ⟨m, w⟩ for each of them, and a regular cone is cut out by its dual semigroup (TauCeti.Toric.IsRegularCone.mem_iff_forall_realCharacter_nonneg), so w ∈ σ.

The converse needs the fan to be nonempty: the realization of the empty fan is empty, hence compact, but the empty fan is not complete.

Main declarations #

References #

source
theorem TauCeti.Toric.IsIntegralLattice.exists_complexTorus_norm_eq {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) (v : V) :
∃ (t : ComplexTorus N), ∀ (m : IntegralCharacter N), ‖↑(t m)‖ = Real.exp (-(h.realCharacter m) v)

For every point v of V there is a torus point at which every integral character m has absolute value exp (-⟨m, v⟩).

source
theorem TauCeti.Toric.IsIntegralLattice.exists_realCharacter_apply_eq_neg_log_norm {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (h : IsIntegralLattice i) (t : ComplexTorus N) :
∃ (w : V), ∀ (m : N →+ ℤ), (h.realCharacter m) w = -Real.log ‖↑(t m)‖

Conversely, every torus point t has a point w of V at which every integral character m takes the value -log ‖t m‖.

source
theorem TauCeti.Toric.Fan.isCompact_image_analyticAffineChartι_setOf_forall_norm_apply_single_le_one {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) :
IsCompact (⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) '' {x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ) | ∀ (s : ↥(dualSemigroup ⋯ ↑σ)), ‖x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)‖ ≤ 1})

The part of the chart of a cone σ where every monomial has absolute value at most 1 is a compact subset of the realization.

source
theorem TauCeti.Toric.Fan.isCompact_image_analyticAffineChartι_setOf_forall_norm_apply_single_toFun_le {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {r : ℕ} (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) r) (R : ℝ) :
IsCompact (⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) '' {x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ) | ∀ (j : Fin r), ‖x (MonoidAlgebra.single (Multiplicative.ofAdd (g.toFun j)) 1)‖ ≤ R})

For a finite generating family g of the dual semigroup of a cone σ, the part of the chart of σ where the monomials of g have absolute value at most R is a compact subset of the realization.

source
theorem TauCeti.Toric.Fan.isOpen_image_analyticAffineChartι_setOf_forall_norm_apply_single_toFun_lt {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {r : ℕ} (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) r) (R : ℝ) :
IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) '' {x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ) | ∀ (j : Fin r), ‖x (MonoidAlgebra.single (Multiplicative.ofAdd (g.toFun j)) 1)‖ < R})

For a finite generating family g of the dual semigroup of a cone σ, the part of the chart of σ where the monomials of g have absolute value less than R is open in the realization.

source
theorem TauCeti.Toric.Fan.analyticTorusι_mem_image_setOf_forall_norm_apply_single_le_one {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) {σ : ↑Φ.cones} {t : ComplexTorus N} (ht : ∀ (m : ↥(dualSemigroup ⋯ ↑σ)), ‖↑(t ↑m)‖ ≤ 1) :
Φ.analyticTorusι hΦ hΦ0 t ∈ ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) '' {x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ) | ∀ (s : ↥(dualSemigroup ⋯ ↑σ)), ‖x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)‖ ≤ 1}

A torus point at which every character of the dual semigroup of a cone σ has absolute value at most 1 lies in the part of the chart of σ where every monomial has absolute value at most 1.

source
theorem TauCeti.Toric.Fan.compactSpace_analyticRealization_of_isComplete {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (hc : Φ.IsComplete) :
CompactSpace ↑(Φ.analyticRealization hΦ)

The analytic realization of a complete regular fan is compact.

source
theorem TauCeti.Toric.Fan.mem_of_mapClusterPt_analyticTorusι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) {w : V} {t : ℕ → ComplexTorus N} (ht : ∀ (k : ℕ) (m : IntegralCharacter N), ‖↑((t k) m)‖ = Real.exp (-(⋯.realCharacter m) (↑k • w))) {σ : ↑Φ.cones} {y : ↑(Φ.analyticAffineChartDiagram.obj σ)} (h : MapClusterPt ((CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) y) Filter.atTop fun (k : ℕ) => Φ.analyticTorusι hΦ hΦ0 (t k)) :
w ∈ ↑σ

Let t k be torus points at which every integral character m has absolute value exp (-k ⟨m, w⟩). If they cluster at a point of the chart of a cone σ, then w ∈ σ.

source
theorem TauCeti.Toric.Fan.isComplete_of_compactSpace_analyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) [CompactSpace ↑(Φ.analyticRealization hΦ)] :
Φ.IsComplete

A nonempty regular fan with compact analytic realization is complete.

source
theorem TauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isComplete {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) :
CompactSpace ↑(Φ.analyticRealization hΦ) ↔ Φ.IsComplete

A nonempty regular fan has compact analytic realization exactly when it is complete. The nonemptiness hypothesis is necessary: the realization of the empty fan is empty, hence compact, while the empty fan is not complete. See TauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isEmpty_or_isComplete for the form without it.

source
theorem TauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isEmpty_or_isComplete {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) :
CompactSpace ↑(Φ.analyticRealization hΦ) ↔ IsEmpty ↑Φ.cones ∨ Φ.IsComplete

A regular fan has compact analytic realization exactly when it has no cones or is complete. The two cases are exclusive, since a complete fan is nonempty (TauCeti.Toric.Fan.IsComplete.nonempty_cones): fans with no cones, such as the empty subfan of any fan, are exactly the fans with compact realization that are not complete.