The complex manifold structure of the coordinate-free complex torus

A free presentation e : (N →+ ℤ) ≃+ (ι →₀ ℤ) of the character lattice, with ι finite, embeds the complex torus ComplexTorus N openly into ℂ^ι, as the locus where every coordinate is nonzero. Mathlib's singleton-chart construction therefore makes the torus a complex manifold modelled on ℂ^ι.

Although the chart names coordinates, the complex structure does not depend on the presentation: in the coordinates of two presentations, every torus map induced by a lattice map, and in particular the identity, is a Laurent monomial map, which is holomorphic where all coordinates are invertible. Character evaluations are holomorphic for the same reason.

Main declarations

• TauCeti.Toric.complexTorusChartedSpace: the complex charted-space structure induced by a free presentation of the character lattice.
• TauCeti.Toric.isManifold_complexTorusChartedSpace: this charted space is a complex manifold.
• TauCeti.Toric.complexTorusAmbient_complexTorusMap: in coordinates, a torus map induced by a lattice map is a Laurent monomial map.
• TauCeti.Toric.contMDiff_complexTorusMap: torus maps induced by lattice maps are holomorphic.
• TauCeti.Toric.contMDiff_id_complexTorusChartedSpace: changing the presentation preserves the complex structure.
• TauCeti.Toric.contMDiff_characterEvaluation: character evaluations are holomorphic.

References

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

@[instance_reducible]

noncomputable def TauCeti.Toric.complexTorusChartedSpace {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : ChartedSpace (ι → ℂ) (ComplexTorus N)

The complex charted-space structure on the torus induced by a free presentation of the character lattice. Its sole chart is the open embedding by the ambient coordinates.

theorem TauCeti.Toric.complexTorusChartedSpace_chartAt {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (x : ComplexTorus N) : ↑(chartAt (ι → ℂ) x) = complexTorusAmbient e

Every chart of the torus charted-space structure is the ambient coordinate map.

theorem TauCeti.Toric.complexTorusChartedSpace_chartAt_target {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (x : ComplexTorus N) : (chartAt (ι → ℂ) x).target = {z : ι → ℂ | ∀ (i : ι), z i ≠ 0}

The target of every chart of the torus charted-space structure is the locus where every coordinate is nonzero.

theorem TauCeti.Toric.isManifold_complexTorusChartedSpace {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (n : WithTop ℕ∞) : have x := complexTorusChartedSpace e; IsManifold (modelWithCornersSelf ℂ (ι → ℂ)) n (ComplexTorus N)

The complex torus, with the chart induced by a free presentation of its character lattice, is a complex manifold to every differentiability order.

theorem TauCeti.Toric.contMDiff_complexTorusAmbient {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (n : WithTop ℕ∞) : have x := complexTorusChartedSpace e; ContMDiff (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ (ι → ℂ)) n (complexTorusAmbient e)

The ambient coordinates are holomorphic for the charted-space structure they induce.

theorem TauCeti.Toric.contMDiff_complexTorusAmbient_comp_iff {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) {E : Type u_5} {H : Type u_6} {M : Type u_7} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ComplexTorus N} {n : WithTop ℕ∞} : have x := complexTorusChartedSpace e; ContMDiff I (modelWithCornersSelf ℂ (ι → ℂ)) n (complexTorusAmbient e ∘ f) ↔ ContMDiff I (modelWithCornersSelf ℂ (ι → ℂ)) n f

A map to the coordinate-free complex torus is holomorphic exactly when its ambient coordinates are holomorphic. This criterion works for any charted-space source.

theorem TauCeti.Toric.contMDiff_prod_zpow_complexTorusAmbient {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (a : ι → ℤ) (n : WithTop ℕ∞) : have x := complexTorusChartedSpace e; ContMDiff (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ ℂ) n fun (x : ComplexTorus N) => ∏ i : ι, complexTorusAmbient e x i ^ a i

A Laurent monomial in the ambient coordinates is a holomorphic function on the torus.

theorem TauCeti.Toric.contMDiff_characterEvaluation {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (m : IntegralCharacter N) (n : WithTop ℕ∞) : have x := complexTorusChartedSpace e; ContMDiff (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ ℂ) n ⇑(characterEvaluation m)

Evaluation of an integral character is a holomorphic map from the torus to ℂˣ.

theorem TauCeti.Toric.complexTorusAmbient_complexTorusMap {N : Type u_1} {N' : Type u_2} {ι : Type u_3} {ι' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (e' : IntegralCharacter N' ≃+ (ι' →₀ ℤ)) (f : N →+ N') (x : ComplexTorus N) (j : ι') : complexTorusAmbient e' ((complexTorusMap f) x) j = ∏ i : ι, complexTorusAmbient e x i ^ (e (f.compHom' (e'.symm (Finsupp.single j 1)))) i

In the coordinates of two free presentations, the torus map induced by a lattice map f is the Laurent monomial map whose exponents are the coordinates of the pulled-back coordinate characters.

theorem TauCeti.Toric.contMDiff_complexTorusMap {N : Type u_1} {N' : Type u_2} {ι : Type u_3} {ι' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (e' : IntegralCharacter N' ≃+ (ι' →₀ ℤ)) [Fintype ι'] (f : N →+ N') (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ (ι' → ℂ)) n ⇑(complexTorusMap f)

The torus map induced by a lattice map is holomorphic for the charted-space structures induced by any free presentations of the two character lattices.

theorem TauCeti.Toric.contMDiff_id_complexTorusChartedSpace {N : Type u_1} {ι : Type u_3} {ι' : Type u_4} [AddCommGroup N] [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) [Fintype ι'] (e₂ : IntegralCharacter N ≃+ (ι' →₀ ℤ)) (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ (ι' → ℂ)) n id

The identity map between the torus equipped with the charted-space structures of two free presentations of its character lattice is holomorphic: the complex structure does not depend on the presentation.