The topology of the coordinate-free complex torus

For an additive commutative group N, the complex torus ComplexTorus N is the group of ℂˣ-valued additive characters of N →+ ℤ. This file equips it with the topology of pointwise convergence: the coarsest topology for which the evaluation of every integral character is continuous. Any free presentation e : (N →+ ℤ) ≃+ (ι →₀ ℤ) identifies the torus with (ℂˣ)^ι as a topological group, for an arbitrary index type ι. Its ambient coordinates in ℂ^ι are continuous and have range the locus where every coordinate is nonzero. When ι is finite, these ambient coordinates form an open embedding.

The torus is a Hausdorff topological group for every N, and every additive homomorphism of such groups induces a continuous homomorphism of tori. When N is a finitely generated free ℤ-module, the torus is also second countable and locally compact.

Character evaluations are continuous by the topology of pointwise convergence. For a chosen presentation, the Laurent-monomial formula expresses each evaluation of the inverse coordinate map as a finite product of powers, proving continuous_complexTorusCoordinates_symm.

Main declarations

• TauCeti.Toric.complexTorusTopology: the topology of pointwise convergence.
• TauCeti.Toric.continuous_complexTorus_iff: a map into the torus is continuous exactly when each character evaluation of it is.
• TauCeti.Toric.complexTorusCoordinatesContinuousMulEquiv: a free presentation of the character lattice identifies the torus with (ℂˣ)^ι as a topological group.
• TauCeti.Toric.complexTorusAmbient and TauCeti.Toric.continuous_complexTorusAmbient: continuous ambient coordinates in ℂ^ι, with range the locus where every coordinate is nonzero.
• TauCeti.Toric.isOpenEmbedding_complexTorusAmbient: for finite ι, the ambient coordinates embed the torus openly into ℂ^ι.
• TauCeti.Toric.continuous_complexTorusMap: lattice maps induce continuous torus maps.

References

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

@[instance_reducible]

noncomputable instance TauCeti.Toric.complexTorusTopology {N : Type u_1} [AddCommGroup N] : TopologicalSpace (ComplexTorus N)

The topology of pointwise convergence on the complex torus: the coarsest topology for which evaluation of every integral character is continuous.

theorem TauCeti.Toric.isInducing_coe_complexTorus {N : Type u_1} [AddCommGroup N] : Topology.IsInducing fun (x : ComplexTorus N) => ⇑x

The torus topology is induced by the coercion to functions on the character lattice.

theorem TauCeti.Toric.isEmbedding_coe_complexTorus {N : Type u_1} [AddCommGroup N] : Topology.IsEmbedding fun (x : ComplexTorus N) => ⇑x

The coercion of torus points to functions on the character lattice is an embedding.

theorem TauCeti.Toric.continuous_complexTorus_apply {N : Type u_1} [AddCommGroup N] (m : IntegralCharacter N) : Continuous fun (x : ComplexTorus N) => x m

Evaluation at a fixed integral character is continuous on the torus.

theorem TauCeti.Toric.continuous_characterEvaluation {N : Type u_1} [AddCommGroup N] (m : IntegralCharacter N) : Continuous ⇑(characterEvaluation m)

Character evaluation is a continuous homomorphism on the torus.

theorem TauCeti.Toric.continuous_complexTorus_iff {N : Type u_1} [AddCommGroup N] {X : Type u_4} [TopologicalSpace X] {f : X → ComplexTorus N} : Continuous f ↔ ∀ (m : IntegralCharacter N), Continuous fun (a : X) => (f a) m

A map into the torus is continuous exactly when its composite with every character evaluation is continuous.

instance TauCeti.Toric.instIsTopologicalGroupComplexTorus {N : Type u_1} [AddCommGroup N] : IsTopologicalGroup (ComplexTorus N)

The complex torus is a topological group for the pointwise-convergence topology.

instance TauCeti.Toric.instT2SpaceComplexTorus {N : Type u_1} [AddCommGroup N] : T2Space (ComplexTorus N)

The complex torus is Hausdorff.

theorem TauCeti.Toric.continuous_complexTorusMap {N : Type u_1} {N' : Type u_2} [AddCommGroup N] [AddCommGroup N'] (f : N →+ N') : Continuous ⇑(complexTorusMap f)

The map of tori induced by a lattice map is continuous.

Coordinates supplied by a free presentation of the character lattice

theorem TauCeti.Toric.continuous_complexTorusCoordinates {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : Continuous ⇑(complexTorusCoordinates e)

The coordinates of a free presentation are continuous on the torus.

theorem TauCeti.Toric.continuous_complexTorusCoordinates_symm {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : Continuous ⇑(complexTorusCoordinates e).symm

The inverse of the coordinates of a free presentation is continuous: every character evaluation is a Laurent monomial in the coordinates.

noncomputable def TauCeti.Toric.complexTorusCoordinatesContinuousMulEquiv {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : ComplexTorus N ≃ₜ* (ι → ℂˣ)

A free presentation of the character lattice identifies the coordinate-free complex torus with a product of copies of ℂˣ as a topological group.

@[simp]

theorem TauCeti.Toric.coe_complexTorusCoordinatesContinuousMulEquiv {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : ⇑(complexTorusCoordinatesContinuousMulEquiv e) = ⇑(complexTorusCoordinates e)

@[simp]

theorem TauCeti.Toric.coe_complexTorusCoordinatesContinuousMulEquiv_symm {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : ⇑(complexTorusCoordinatesContinuousMulEquiv e).symm = ⇑(complexTorusCoordinates e).symm

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

The ambient coordinates of the torus supplied by a free presentation e: the coordinates of e, read as complex numbers. For finite ι, they embed the torus openly into ℂ^ι.

theorem TauCeti.Toric.continuous_complexTorusAmbient {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : Continuous (complexTorusAmbient e)

The ambient coordinates are continuous for any index type.

@[simp]

theorem TauCeti.Toric.complexTorusAmbient_apply {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (x : ComplexTorus N) (i : ι) : complexTorusAmbient e x i = ↑(x (e.symm (Finsupp.single i 1)))

An ambient coordinate is the complex value of the corresponding coordinate character.

@[simp]

theorem TauCeti.Toric.complexTorusAmbient_ne_zero {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (x : ComplexTorus N) (i : ι) : complexTorusAmbient e x i ≠ 0

The ambient coordinates of a torus point are nonzero.

@[simp]

theorem TauCeti.Toric.complexTorusAmbient_mul {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (x y : ComplexTorus N) : complexTorusAmbient e (x * y) = complexTorusAmbient e x * complexTorusAmbient e y

The ambient coordinates of a product are the pointwise product of the ambient coordinates.

@[simp]

theorem TauCeti.Toric.complexTorusAmbient_one {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : complexTorusAmbient e 1 = 1

The ambient coordinates of the identity are all equal to one.

@[simp]

theorem TauCeti.Toric.complexTorusAmbient_inv {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (x : ComplexTorus N) : complexTorusAmbient e x⁻¹ = (complexTorusAmbient e x)⁻¹

The ambient coordinates of an inverse are the pointwise inverse of the ambient coordinates.

theorem TauCeti.Toric.isOpenEmbedding_complexTorusAmbient {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) [Finite ι] : Topology.IsOpenEmbedding (complexTorusAmbient e)

For finite ι, the ambient coordinates are an open embedding of the torus into ℂ^ι.

theorem TauCeti.Toric.range_complexTorusAmbient {N : Type u_1} {ι : Type u_3} [AddCommGroup N] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) : Set.range (complexTorusAmbient e) = {z : ι → ℂ | ∀ (i : ι), z i ≠ 0}

The range of the ambient coordinates is the locus where every coordinate is nonzero.

instance TauCeti.Toric.instSecondCountableTopologyComplexTorusOfFreeOfFiniteInt {N : Type u_1} [AddCommGroup N] [Module.Free ℤ N] [Module.Finite ℤ N] : SecondCountableTopology (ComplexTorus N)

The complex torus is second countable: an integral basis of N embeds it openly into a finite-dimensional complex space.

instance TauCeti.Toric.instLocallyCompactSpaceComplexTorusOfFreeOfFiniteInt {N : Type u_1} [AddCommGroup N] [Module.Free ℤ N] [Module.Finite ℤ N] : LocallyCompactSpace (ComplexTorus N)

The complex torus is locally compact: an integral basis of N embeds it openly into a finite-dimensional complex space.