The complex manifold of a regular affine toric cone

The complex points of the affine toric scheme of a regular cone form a complex manifold. After choosing an integral basis extending the primitive ray generators and numbering the rays, the ambient cone chart embeds them as the open mixed-coordinate locus ℂ^k × (ℂˣ)^l ⊆ ℂ^k × ℂ^l. Mathlib's singleton-chart construction therefore supplies a charted space and a complex-manifold structure.

Although this construction names coordinates, its complex structure does not depend on the extending basis or the generating family. The transition between two extending bases is the mixed monomial biholomorphism computed in TauCeti.Geometry.Toric.Analytic.Cone.Chart; consequently the identity map between the two singleton-chart structures is holomorphic in both directions. The topology is likewise independent of the finite semigroup generating family used to present the affine complex points.

The monomials, that is, the character functions of the dual semigroup, are holomorphic on this manifold: in the ambient coordinates a monomial is a product of natural powers of the ray coordinates and integral powers of the torus coordinates, which do not vanish on the chart. Conversely, the ambient coordinates are themselves monomials, so a map into the complex points is holomorphic exactly when all of its monomials are; this criterion refers to no coordinates. In particular, pulling complex points back along a homomorphism of dual semigroups is holomorphic.

Main declarations

• TauCeti.Toric.isOpenEmbedding_coneChartAmbient: the ambient cone chart is an open embedding.
• TauCeti.Toric.coneChartedSpace: the complex charted-space structure induced by one system of regular cone coordinates.
• TauCeti.Toric.isManifold_coneChartedSpace: this charted space is a complex manifold.
• TauCeti.Toric.contMDiff_coneChartAmbient_comp_iff: a map into the complex points is holomorphic exactly when its ambient chart coordinates are.
• TauCeti.Toric.contMDiff_apply_single: every monomial is a holomorphic function.
• TauCeti.Toric.contMDiffOn_iff_forall_contMDiffOn_apply_single and TauCeti.Toric.contMDiff_iff_forall_contMDiff_apply_single: a map into the complex points is holomorphic exactly when its value on every monomial is.
• TauCeti.Toric.contMDiff_id_coneChartedSpace: changing the extending basis or the generating family preserves the complex structure.
• TauCeti.Toric.AffineSemigroupComplexPoint.contMDiff_comap: pulling complex points back along a homomorphism of dual semigroups is holomorphic.

References

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

theorem TauCeti.Toric.isOpenEmbedding_coneChartAmbient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : Topology.IsOpenEmbedding (coneChartAmbient hi hσ hB κ)

The ambient mixed-coordinate chart of a regular cone is an open embedding. Its range is the open locus on which every torus coordinate is nonzero.

@[instance_reducible]

noncomputable def TauCeti.Toric.coneChartedSpace {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : ChartedSpace ((Fin k → ℂ) × (Fin l → ℂ)) (AffineSemigroupComplexPoint ↥(dualSemigroup hi σ))

The complex charted-space structure on the affine complex points of a regular cone, induced by an extending integral basis and a numbering of the rays. Its sole chart is the open embedding into the ambient mixed-coordinate space.

theorem TauCeti.Toric.coe_coneChartedSpace_chartAt {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : ↑(chartAt ((Fin k → ℂ) × (Fin l → ℂ)) x) = coneChartAmbient hi hσ hB κ

Every chart in the cone charted-space structure is the ambient mixed-coordinate chart.

theorem TauCeti.Toric.coneChartedSpace_chartAt_target {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : (chartAt ((Fin k → ℂ) × (Fin l → ℂ)) x).target = mixedChartDomain k l

The target of every chart in the cone charted-space structure is the mixed-coordinate locus.

theorem TauCeti.Toric.isManifold_coneChartedSpace {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := coneChartedSpace hi hσ hB κ g; IsManifold (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n (AffineSemigroupComplexPoint ↥(dualSemigroup hi σ))

The affine complex points of a regular cone, with the singleton chart induced by an extending basis, form a complex manifold to every differentiability order.

theorem TauCeti.Toric.contMDiff_coneChartAmbient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := coneChartedSpace hi hσ hB κ g; ContMDiff (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n (coneChartAmbient hi hσ hB κ)

The ambient cone chart is holomorphic for the charted-space structure it induces.

theorem TauCeti.Toric.contMDiff_coneChartAmbient_comp_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) {E : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [TopologicalSpace M] [ChartedSpace H M] (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) {f : M → AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} {n : WithTop ℕ∞} : let x := affinePointTopology g; have x_1 := coneChartedSpace hi hσ hB κ g; ContMDiff I (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n (coneChartAmbient hi hσ hB κ ∘ f) ↔ ContMDiff I (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n f

A map into the affine complex points of a regular cone is holomorphic exactly when its ambient chart coordinates are.

theorem TauCeti.Toric.contMDiff_apply_single {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (m : ↥(dualSemigroup hi σ)) (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := coneChartedSpace hi hσ hB κ g; ContMDiff (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ ℂ) n fun (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) => x (MonoidAlgebra.single (Multiplicative.ofAdd m) 1)

Every monomial is a holomorphic function on the affine complex points of a regular cone: in the ambient mixed coordinates it is a product of natural powers of the ray coordinates and integral powers of the torus coordinates, and the latter do not vanish on the image of the chart.

theorem TauCeti.Toric.contMDiffOn_iff_forall_contMDiffOn_apply_single {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) {E : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [TopologicalSpace M] [ChartedSpace H M] (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) {f : M → AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} {t : Set M} {n : WithTop ℕ∞} : let x := affinePointTopology g; have x_1 := coneChartedSpace hi hσ hB κ g; ContMDiffOn I (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n f t ↔ ∀ (m : ↥(dualSemigroup hi σ)), ContMDiffOn I (modelWithCornersSelf ℂ ℂ) n (fun (x : M) => (f x) (MonoidAlgebra.single (Multiplicative.ofAdd m) 1)) t

A map into the affine complex points of a regular cone is holomorphic on a set exactly when its value on every monomial is. This is the holomorphic counterpart of TauCeti.Toric.continuous_iff_forall_continuous_apply_single.

theorem TauCeti.Toric.contMDiff_iff_forall_contMDiff_apply_single {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) {E : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [TopologicalSpace M] [ChartedSpace H M] (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) {f : M → AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)} {n : WithTop ℕ∞} : let x := affinePointTopology g; have x_1 := coneChartedSpace hi hσ hB κ g; ContMDiff I (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n f ↔ ∀ (m : ↥(dualSemigroup hi σ)), ContMDiff I (modelWithCornersSelf ℂ ℂ) n fun (x : M) => (f x) (MonoidAlgebra.single (Multiplicative.ofAdd m) 1)

A map into the affine complex points of a regular cone is holomorphic exactly when its value on every monomial is.

theorem TauCeti.Toric.contMDiff_id_coneChartedSpace {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s s' k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B B' : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (hB' : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (g' : AddGeneratingFamily (↥(dualSemigroup hi σ)) s') (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n id

The identity map between the affine complex-point spaces equipped with two regular coordinate systems is holomorphic. Both the extending basis and the finite generating family used to define the topology may change.

Maps of dual semigroups

theorem TauCeti.Toric.AffineSemigroupComplexPoint.contMDiff_comap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s s' k l : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) {N' : Type u_3} {V' : Type u_4} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {τ : PointedCone ℝ V'} {k' l' : ℕ} (hi' : IsIntegralLattice i') (hτ : IsToricCone i' τ) {C : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N'} (hC : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i' ρ (C (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (g' : AddGeneratingFamily (↥(dualSemigroup hi' τ)) s') (φ : ↥(dualSemigroup hi' τ) →+ ↥(dualSemigroup hi σ)) (n : WithTop ℕ∞) : let x := affinePointTopology g; have x_1 := coneChartedSpace hi hσ hB κ g; let x_2 := affinePointTopology g'; have x_3 := coneChartedSpace hi' hτ hC κ' g'; ContMDiff (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ ((Fin k' → ℂ) × (Fin l' → ℂ))) n (comap φ)

Pulling complex points back along a homomorphism of dual semigroups of regular cones is holomorphic, for the complex structures of any extending bases of the two cones: the value of a pulled-back point on a monomial is the value of the original point on the image monomial.