The dense torus of an analytic toric fan realization

For a nonempty regular fan, the orbit indexed by the zero cone is the analytic dense torus. This module records that this set is independent of the witness of nonemptiness and is dense and open in the analytic realization. Its canonical parametrization by the coordinate-free complex torus is an open embedding, and determines continuous maps into Hausdorff spaces uniquely.

Main declarations

• TauCeti.Toric.Fan.analyticDenseTorus: the orbit of the zero cone in a nonempty fan.
• TauCeti.Toric.Fan.dense_analyticDenseTorus: the analytic dense torus is dense.
• TauCeti.Toric.Fan.isOpen_analyticDenseTorus: the analytic dense torus is open.
• TauCeti.Toric.Fan.analyticTorusι: the canonical parametrization by the complex torus.
• TauCeti.Toric.Fan.isOpenEmbedding_analyticTorusι: the parametrization is an open embedding.
• TauCeti.Toric.Fan.analyticRealization_hom_ext_torus: continuous maps to a Hausdorff space are determined by their values on the complex torus.

References

• W. Fulton, Introduction to Toric Varieties, §3.1.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §§3.2--3.3.

noncomputable def TauCeti.Toric.Fan.analyticDenseTorus {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : Set ↑(Phi.analyticRealization hPhi)

The analytic dense torus of a nonempty regular fan is the orbit indexed by its zero cone.

theorem TauCeti.Toric.Fan.analyticDenseTorus_def {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : Phi.analyticDenseTorus hPhi hPhi0 = Phi.analyticConeOrbit hPhi ⟨⊥, ⋯⟩

The analytic dense torus is the orbit indexed by the selected zero cone.

theorem TauCeti.Toric.Fan.analyticDenseTorus_eq {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 hPhi1 : Nonempty ↑Phi.cones) : Phi.analyticDenseTorus hPhi hPhi0 = Phi.analyticDenseTorus hPhi hPhi1

The analytic dense torus does not depend on the witness that the fan is nonempty.

theorem TauCeti.Toric.Fan.analyticDenseTorus_eq_analyticConeOrbit_bot {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (sigma : ↑Phi.cones) : Phi.analyticDenseTorus hPhi ⋯ = Phi.analyticConeOrbit hPhi ⟨⊥, ⋯⟩

Using a cone as the nonemptiness witness identifies the dense torus with the orbit of the zero cone obtained as a face of that cone.

theorem TauCeti.Toric.Fan.dense_analyticDenseTorus {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : Dense (Phi.analyticDenseTorus hPhi hPhi0)

The orbit of the zero cone is dense in the analytic fan realization.

theorem TauCeti.Toric.Fan.isOpen_analyticDenseTorus {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : IsOpen (Phi.analyticDenseTorus hPhi hPhi0)

The analytic dense torus is open in the fan realization.

noncomputable def TauCeti.Toric.Fan.analyticTorusι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) (t : ComplexTorus N) : ↑(Phi.analyticRealization hPhi)

The canonical inclusion of the coordinate-free complex torus into the realization of a nonempty regular fan, obtained by translating the distinguished point of the zero cone. By proof irrelevance, different nonemptiness witnesses give definitionally equal inclusions.

theorem TauCeti.Toric.Fan.analyticTorusι_def {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) (t : ComplexTorus N) : Phi.analyticTorusι hPhi hPhi0 t = t • Phi.analyticDistinguishedPoint hPhi ⟨⊥, ⋯⟩

The torus inclusion is translation of the distinguished point of the zero cone.

theorem TauCeti.Toric.Fan.analyticTorusι_eq_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) (sigma : ↑Phi.cones) (t : ComplexTorus N) : Phi.analyticTorusι hPhi hPhi0 t = (CategoryTheory.ConcreteCategory.hom (Phi.analyticAffineChartι hPhi sigma)) (t • default)

In every affine chart the torus inclusion is translation of the point whose monomial values are all one. In particular this formula does not choose coordinates on the lattice.

@[simp]

theorem TauCeti.Toric.Fan.analyticTorusι_mul {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) (s t : ComplexTorus N) : Phi.analyticTorusι hPhi hPhi0 (s * t) = s • Phi.analyticTorusι hPhi hPhi0 t

The torus inclusion respects translation.

theorem TauCeti.Toric.Fan.analyticTorusι_injective {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : Function.Injective (Phi.analyticTorusι hPhi hPhi0)

The canonical torus parametrization is injective.

@[simp]

theorem TauCeti.Toric.Fan.range_analyticTorusι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : Set.range (Phi.analyticTorusι hPhi hPhi0) = Phi.analyticDenseTorus hPhi hPhi0

The range of the canonical torus inclusion is exactly the analytic dense torus.

theorem TauCeti.Toric.Fan.continuous_analyticTorusι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : Continuous (Phi.analyticTorusι hPhi hPhi0)

The canonical torus inclusion is continuous for the coordinate-free torus topology.

theorem TauCeti.Toric.Fan.isOpenEmbedding_analyticTorusι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) : Topology.IsOpenEmbedding (Phi.analyticTorusι hPhi hPhi0)

The canonical torus inclusion is an open embedding.

theorem TauCeti.Toric.Fan.analyticRealization_hom_ext_torus {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) {Z : TopCat} [T2Space ↑Z] {g g' : Phi.analyticRealization hPhi ⟶ Z} (h : ∀ (t : ComplexTorus N), (CategoryTheory.ConcreteCategory.hom g) (Phi.analyticTorusι hPhi hPhi0 t) = (CategoryTheory.ConcreteCategory.hom g') (Phi.analyticTorusι hPhi hPhi0 t)) : g = g'

Maps from a nonempty regular fan realization to a Hausdorff space agree if they agree at every point of the canonical complex torus.