The complex manifold of algebraic toric complex points

The complex points of the scheme of a regular fan carry the affine-chart topology, not the Zariski topology. Pulling the atlas of the analytic realization back along the chartwise comparison makes this carrier a complex manifold. The pulled-back structure agrees locally with the independently defined regular affine-chart structures for any extending basis and finite generating family: every algebraic affine chart inclusion is a local biholomorphism.

The comparison is a biholomorphism, and the scheme-theoretic map on complex points induced by a fan morphism is holomorphic. The comparison intertwines this map with the analytic toric map.

References

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

@[instance_reducible]

noncomputable def TauCeti.Toric.Fan.algebraicComplexPointChartedSpace {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) : ChartedSpace (Fin (Module.finrank ℤ N) → ℂ) Φ.AlgebraicComplexPoint

The complex atlas on algebraic complex points of a regular fan, pulled back from its analytic realization. Its affine charts have the regular-coordinate complex structures.

theorem TauCeti.Toric.Fan.isManifold_algebraicComplexPoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (n : WithTop ℕ∞) : IsManifold (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) n Φ.AlgebraicComplexPoint

The algebraic complex points of a regular fan form a complex manifold.

noncomputable def TauCeti.Toric.Fan.algebraicAnalyticDiffeomorph {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (n : WithTop ℕ∞) : Diffeomorph (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) Φ.AlgebraicComplexPoint (↑(Φ.analyticRealization hΦ)) n

The algebraic–analytic comparison is a biholomorphism for the affine-chart complex structures, at every smoothness order.

@[simp]

theorem TauCeti.Toric.Fan.coe_algebraicAnalyticDiffeomorph {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (n : WithTop ℕ∞) : ⇑(algebraicAnalyticDiffeomorph hΦ n) = ⇑(algebraicAnalyticEquiv hΦ)

The biholomorphism is the existing chartwise algebraic–analytic comparison.

@[simp]

theorem TauCeti.Toric.Fan.coe_algebraicAnalyticDiffeomorph_symm {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (n : WithTop ℕ∞) : ⇑(algebraicAnalyticDiffeomorph hΦ n).symm = ⇑(algebraicAnalyticEquiv hΦ).symm

The inverse biholomorphism is the inverse chartwise comparison.

theorem TauCeti.Toric.Fan.isLocalDiffeomorph_ofAffinePoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {k l s : ℕ} {B : Module.Basis (ToricRay ↑σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay ↑σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) s) (n : WithTop ℕ∞) : IsLocalDiffeomorph (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) n (AlgebraicComplexPoint.ofAffinePoint σ)

Every algebraic affine chart inclusion is a local biholomorphism for the independently defined regular-cone structure of any extending basis and finite generating family. In particular, its local inverse is holomorphic, so these chart inclusions, which cover all algebraic complex points, characterize the pulled-back complex structure in both directions.

theorem TauCeti.Toric.FanHom.contMDiff_algebraicComplexPointMap {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) {N' V' : Type} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΨ : Ψ.IsRegular) (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N') → ℂ)) n f.algebraicComplexPointMap

A morphism of regular fans acts holomorphically on the complex points of their schemes.