Naturality of the algebraic–analytic toric comparison

A fan morphism acts on algebraic complex points by composition with its morphism of fan schemes. On an affine chart this is pullback along the map of dual semigroups, exactly as for the analytic toric map. Consequently the algebraic–analytic comparison commutes with toric maps. This identifies the actual scheme-theoretic map on complex points, rather than defining it by conjugating an analytic map.

The map on algebraic complex points is continuous for the topology glued from affine charts, even for nonregular fans. Identity and composition agree with those of scheme morphisms.

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.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicComplexPointMap_ofAffinePoint {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 Φ Ψ) (σ : ↑Φ.cones) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) : f.algebraicComplexPointMap (Fan.AlgebraicComplexPoint.ofAffinePoint σ x) = Fan.AlgebraicComplexPoint.ofAffinePoint ⟨f.leastCone ⋯, ⋯⟩ ((CategoryTheory.ConcreteCategory.hom (f.analyticChartMap ⋯)) x)

On an affine chart, the algebraic map on complex points pulls back along the map of dual semigroups into the least target cone. This holds without regularity of either fan.

theorem TauCeti.Toric.FanHom.continuous_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 Φ Ψ) : Continuous f.algebraicComplexPointMap

The scheme-theoretic map on complex points is continuous for the glued monomial topologies, including for nonregular fans.

theorem TauCeti.Toric.FanHom.algebraicAnalyticEquiv_naturality {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 Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (p : Φ.AlgebraicComplexPoint) : (Fan.algebraicAnalyticEquiv hΨ) (f.algebraicComplexPointMap p) = (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ((Fan.algebraicAnalyticEquiv hΦ) p)

The algebraic–analytic comparison commutes with a toric map of regular fans.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicAnalyticEquiv_symm_naturality {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 Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (p : ↑(Φ.analyticRealization hΦ)) : (Fan.algebraicAnalyticEquiv hΨ).symm ((CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) p) = f.algebraicComplexPointMap ((Fan.algebraicAnalyticEquiv hΦ).symm p)

The inverse algebraic–analytic comparison also commutes with toric maps.