Topology of the analytic realization of a regular fan

The analytic realization of a regular fan is Hausdorff, second countable and locally compact.

Second countability and local compactness hold because the realization is covered by finitely many open affine analytic charts, each of which has these properties. Hausdorffness is where the fan axioms enter. A space glued from open charts is Hausdorff exactly when the gluing relation between any two charts is closed in their product. For the charts of two cones σ and τ, a point of the first and a point of the second are identified exactly when they are restrictions of a point of the chart of σ ⊓ τ. By the separation lemma the dual semigroup of σ ⊓ τ is generated by those of σ and τ, so this happens exactly when the two points satisfy the binomial equations x(χˢ) y(χᵗ) = x(χˢ') y(χᵗ') for s + t = s' + t'. These equations are closed conditions.

Main declarations

• TauCeti.Toric.Fan.isClosed_setOf_analyticAffineChartι_eq: the gluing relation between two affine analytic charts is closed.
• TauCeti.Toric.Fan.t2Space_analyticRealization: the analytic realization is Hausdorff.
• TauCeti.Toric.Fan.secondCountableTopology_analyticRealization and TauCeti.Toric.Fan.locallyCompactSpace_analyticRealization: it is second countable and locally compact.

References

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

theorem TauCeti.Toric.Fan.isClosed_setOf_analyticAffineChartι_eq {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : IsClosed {p : ↑(Φ.analyticAffineChartDiagram.obj σ) × ↑(Φ.analyticAffineChartDiagram.obj τ) | (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) p.1 = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) p.2}

The points of the affine analytic charts of two cones σ and τ that are identified in the analytic realization form a closed subset of the product of the two charts.

instance TauCeti.Toric.Fan.t2Space_analyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : T2Space ↑(Φ.analyticRealization hΦ)

The analytic realization of a regular fan is Hausdorff.

instance TauCeti.Toric.Fan.secondCountableTopology_analyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : SecondCountableTopology ↑(Φ.analyticRealization hΦ)

The analytic realization of a regular fan is second countable: it is covered by finitely many second countable affine analytic charts.

instance TauCeti.Toric.Fan.locallyCompactSpace_analyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : LocallyCompactSpace ↑(Φ.analyticRealization hΦ)

The analytic realization of a regular fan is locally compact.