Complex points of the toric scheme of a fan

A complex point of the toric scheme X_Φ of a finite fan Φ is a morphism Spec ℂ ⟶ X_Φ over Spec ℂ, for the structure morphism TauCeti.Toric.Fan.algebraicRealizationOver. It is neither a point of the underlying topological space of X_Φ nor a bare scheme morphism from Spec ℂ: on an affine chart a bare morphism is a ring homomorphism from the coordinate ring to ℂ, which need not be ℂ-linear.

On the affine chart of a cone σ, complex points are exactly the ℂ-algebra homomorphisms from its coordinate ring to ℂ, the carrier AffineSemigroupComplexPoint of the analytic chart of σ, by TauCeti.AlgebraicGeometry.specOverHomEquivAlgHom. This file shows that the complex points of X_Φ are glued from these affine complex points exactly as the analytic realization is glued from its charts: every complex point of X_Φ lies in some affine chart, and points of the charts of σ and τ give the same complex point exactly when they come from a common point of the chart of σ ⊓ τ under the two face maps faceAffinePointMap. The complex points of X_Φ carry the topology glued from the monomial-embedding topologies of the affine charts, which do not depend on the generating families used to define them. For a regular fan, the algebraic and the analytic gluings agree, so the complex points of X_Φ are homeomorphic to the analytic realization, by a homeomorphism that is the identity of complex points on every affine chart.

Main declarations

• TauCeti.Toric.Fan.AlgebraicComplexPoint: the complex points of the toric scheme of a fan.
• TauCeti.Toric.FanHom.algebraicComplexPointMap: the action of fan morphisms on complex points, with identity and composition rules.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.ofAffinePoint: the complex point given by a point of the affine chart of a cone.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.exists_ofAffinePoint_eq: every complex point lies in an affine chart.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.ofAffinePoint_eq_ofAffinePoint_iff: two chart points give the same complex point exactly when they come from the chart of the intersection cone.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.isOpen_iff_forall_isOpen_preimage_ofAffinePoint: the topology on complex points glued from the monomial-embedding topologies of the affine charts.
• TauCeti.Toric.Fan.algebraicAnalyticEquiv: for a regular fan, the bijection between complex points of the toric scheme and points of the analytic realization, computed on affine charts by TauCeti.Toric.Fan.algebraicAnalyticEquiv_ofAffinePoint.
• TauCeti.Toric.Fan.algebraicAnalyticHomeomorph: the same bijection is a homeomorphism.

References

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

theorem TauCeti.Toric.spec_map_faceAffinePointMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {τ σ : PointedCone ℝ V} (h : τ.IsFaceOf σ) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)) : AlgebraicGeometry.Spec.map (CommRingCat.ofHom (faceAffinePointMap hi h x).toRingHom) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom x.toRingHom)) (faceAffineToricSchemeMap hi h)

On complex points, the face map of a face τ of σ is the face morphism of affine toric schemes: applying Spec to the restricted point is composing with faceAffineToricSchemeMap.

@[reducible, inline]

abbrev TauCeti.Toric.Fan.AlgebraicComplexPoint {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Type

The complex points of the toric scheme X_Φ of a finite fan: the morphisms Spec ℂ ⟶ X_Φ over Spec ℂ.

noncomputable def TauCeti.Toric.Fan.AlgebraicComplexPoint.ofAffinePoint {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) : Φ.AlgebraicComplexPoint

The complex point of the toric scheme given by a complex point of the affine chart of a cone, a ℂ-algebra homomorphism from its coordinate ring to ℂ.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.coe_ofAffinePoint {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) : ↑(ofAffinePoint σ x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom x.toRingHom)) (Φ.affineToricChartι σ)

The complex point of a chart point is Spec of the point followed by the chart inclusion.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.ofAffinePoint_faceAffinePointMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {τ σ : ↑Φ.cones} (h : (↑τ).IsFaceOf ↑σ) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑τ)) : ofAffinePoint σ (faceAffinePointMap ⋯ h x) = ofAffinePoint τ x

A point of the chart of a face τ of σ and its image under the face map give the same complex point of the toric scheme.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.exists_ofAffinePoint_eq {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (p : Φ.AlgebraicComplexPoint) : ∃ (σ : ↑Φ.cones) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)), ofAffinePoint σ x = p

Every complex point of the toric scheme of a finite fan lies in one of its affine charts.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.ofAffinePoint_injective {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) : Function.Injective (ofAffinePoint σ)

A complex point of the affine chart of a cone is determined by its complex point of the toric scheme.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.ofAffinePoint_eq_ofAffinePoint_iff {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {σ τ : ↑Φ.cones} (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) (y : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑τ)) : ofAffinePoint σ x = ofAffinePoint τ y ↔ ∃ (z : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ (↑σ ⊓ ↑τ))), faceAffinePointMap ⋯ ⋯ z = x ∧ faceAffinePointMap ⋯ ⋯ z = y

Points of the affine charts of two cones σ and τ give the same complex point of the toric scheme exactly when they come from a common point of the chart of σ ⊓ τ under the two face maps.

The topology glued from the affine charts

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.AlgebraicComplexPoint.instTopologicalSpace {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} : TopologicalSpace Φ.AlgebraicComplexPoint

The topology on the complex points of the toric scheme glued from the affine charts: a set is open exactly when its preimage in the complex points of every affine chart is open for the monomial-embedding topology of the analytic chart, which by TauCeti.Toric.Fan.analyticAffineChart_str_eq is the topology induced by any finite generating family of the dual semigroup.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.isOpen_iff_forall_isOpen_preimage_ofAffinePoint {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (s : Set Φ.AlgebraicComplexPoint) : IsOpen s ↔ ∀ (σ : ↑Φ.cones), IsOpen ((fun (x : ↑(Φ.analyticAffineChart σ)) => ofAffinePoint σ x) ⁻¹' s)

A set of complex points of the toric scheme is open exactly when its preimage in the complex points of every affine chart is open.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.continuous_ofAffinePoint {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) : Continuous fun (x : ↑(Φ.analyticAffineChart σ)) => ofAffinePoint σ x

The complex point of the toric scheme depends continuously on a point of an affine chart.

noncomputable def TauCeti.Toric.FanHom.algebraicComplexPointMap {N N' V V' : Type} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (p : Φ.AlgebraicComplexPoint) : Ψ.AlgebraicComplexPoint

The map on algebraic complex points induced by a fan morphism: compose the morphism Spec ℂ ⟶ X_Φ over Spec ℂ with the toric morphism X_Φ ⟶ X_Ψ.

@[simp]

theorem TauCeti.Toric.FanHom.coe_algebraicComplexPointMap {N N' V V' : Type} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (p : Φ.AlgebraicComplexPoint) : ↑(f.algebraicComplexPointMap p) = CategoryTheory.CategoryStruct.comp (↑p) f.algebraicMap

On scheme morphisms, the map of complex points is postcomposition by the algebraic map.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicComplexPointMap_id {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (p : Φ.AlgebraicComplexPoint) : (FanHom.id Φ).algebraicComplexPointMap p = p

The identity fan morphism acts identically on algebraic complex points.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicComplexPointMap_comp {N N' N'' V V' V'' : Type} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (f : FanHom Φ Ψ) (g : FanHom Ψ Ω) (p : Φ.AlgebraicComplexPoint) : (g.comp f).algebraicComplexPointMap p = g.algebraicComplexPointMap (f.algebraicComplexPointMap p)

Composition of fan morphisms acts by composition on algebraic complex points.

The comparison with the analytic realization of a regular fan

theorem TauCeti.Toric.Fan.analyticAffineChartι_eq_analyticAffineChartι_iff_ofAffinePoint_eq {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) {σ τ : ↑Φ.cones} (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) (y : ↑(Φ.analyticAffineChartDiagram.obj τ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) y ↔ AlgebraicComplexPoint.ofAffinePoint σ x = AlgebraicComplexPoint.ofAffinePoint τ y

The analytic realization and the complex points of the toric scheme of a regular fan are glued from the same affine charts along the same identifications: two chart points have the same image in the analytic realization exactly when they give the same complex point of the toric scheme.

noncomputable def TauCeti.Toric.Fan.algebraicAnalyticEquiv {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) : Φ.AlgebraicComplexPoint ≃ ↑(Φ.analyticRealization hΦ)

The point of the analytic realization of a regular fan corresponding to a complex point of its toric scheme, read off in any affine chart containing it.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_ofAffinePoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : (algebraicAnalyticEquiv hΦ) (AlgebraicComplexPoint.ofAffinePoint σ x) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x

On every affine chart the comparison is the identity of complex points: the complex point of the toric scheme given by a point x of the chart of σ corresponds to the point x of the analytic chart of σ.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_symm_analyticAffineChartι {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : (algebraicAnalyticEquiv hΦ).symm ((CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x) = AlgebraicComplexPoint.ofAffinePoint σ x

The inverse comparison sends the point x of the analytic chart of σ to the complex point of the toric scheme given by x.

noncomputable def TauCeti.Toric.Fan.algebraicAnalyticHomeomorph {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) : Φ.AlgebraicComplexPoint ≃ₜ ↑(Φ.analyticRealization hΦ)

For a regular fan, the complex points of the toric scheme, with the topology glued from the affine charts, are homeomorphic to the analytic realization, by a homeomorphism that is the identity of complex points on every affine chart.

@[simp]

theorem TauCeti.Toric.Fan.coe_algebraicAnalyticHomeomorph {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) : ⇑(algebraicAnalyticHomeomorph hΦ) = ⇑(algebraicAnalyticEquiv hΦ)

The homeomorphism is the bijection algebraicAnalyticEquiv.

@[simp]

theorem TauCeti.Toric.Fan.coe_algebraicAnalyticHomeomorph_symm {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) : ⇑(algebraicAnalyticHomeomorph hΦ).symm = ⇑(algebraicAnalyticEquiv hΦ).symm

The inverse homeomorphism is the inverse of the bijection algebraicAnalyticEquiv.