Integral characters on the complex torus

For an additive lattice N, its integral character lattice is N →+ ℤ. The corresponding complex torus is represented without coordinates as the additive characters of this lattice with values in ℂˣ. Evaluation is therefore the canonical pairing between an additive character and its argument.

This file records the multiplicative laws of that pairing, its contravariant naturality in the character lattice (and hence covariance in N), and the fact that integral characters separate torus points. Given an identification of the character lattice with a free abelian group, complexTorusCoordinates connects this coordinate-free carrier to Tau Ceti's existing freeAbelianCharEquiv.

Main declarations

• TauCeti.Toric.IntegralCharacter: the integral character lattice of N.
• TauCeti.Toric.ComplexTorus: its coordinate-free complex torus.
• TauCeti.Toric.characterEvaluation: evaluation of a character as a homomorphism on the torus.
• TauCeti.Toric.complexTorusMap: the torus map induced by an additive map of lattices.
• TauCeti.Toric.complexTorusMap_surjective: a surjection onto a projective lattice induces a surjection of tori.
• TauCeti.Toric.mem_ker_complexTorusMap_mk'_iff: the kernel of the torus map of a quotient lattice N ⧸ H is the subtorus trivial on the characters vanishing on H.
• TauCeti.Toric.exists_characterEvaluation_ne: integral characters separate torus points.
• Module.Basis.integralCharacterRepr: the free presentation of the character lattice dual to an integral basis of N.
• TauCeti.Toric.complexTorusCoordinates: coordinates supplied by a free presentation of the character lattice.
• TauCeti.Toric.complexTorus_apply_eq_prod_zpow: the Laurent-monomial formula for evaluation of a character in those coordinates.
• Module.Basis.complexTorusCoordinates: coordinates supplied by an integral basis of the lattice, through its dual basis.

References

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

@[reducible, inline]

abbrev TauCeti.Toric.IntegralCharacter (N : Type u_4) [AddCommGroup N] : Type u_4

The group of integral characters of an additive commutative group N.

@[reducible, inline]

abbrev TauCeti.Toric.ComplexTorus (N : Type u_4) [AddCommGroup N] : Type u_4

The group of complex unit-valued characters on N →+ ℤ.

For a finite free ℤ-module N, this is its coordinate-free complex torus. AddChar is the additive-domain form of the equivalent Mathlib carrier Multiplicative (N →+ ℤ) →* ℂˣ; using it makes evaluation and pullback of characters direct.

def TauCeti.Toric.characterEvaluation {N : Type u_1} [AddCommGroup N] (m : IntegralCharacter N) : ComplexTorus N →* ℂˣ

Evaluation of the integral character m as a homomorphism on complex-torus points.

The map is the homomorphism obtained by evaluating an additive character at m.

@[simp]

theorem TauCeti.Toric.characterEvaluation_apply {N : Type u_1} [AddCommGroup N] (m : IntegralCharacter N) (x : ComplexTorus N) : (characterEvaluation m) x = x m

Character evaluation is ordinary application of the underlying additive character.

@[simp]

theorem TauCeti.Toric.characterEvaluation_zero {N : Type u_1} [AddCommGroup N] : characterEvaluation 0 = 1

Evaluation of the zero integral character is the trivial monoid homomorphism.

@[simp]

theorem TauCeti.Toric.characterEvaluation_add {N : Type u_1} [AddCommGroup N] (m₁ m₂ : IntegralCharacter N) : characterEvaluation (m₁ + m₂) = characterEvaluation m₁ * characterEvaluation m₂

Evaluation sends addition of integral characters to multiplication of monoid homomorphisms.

@[simp]

theorem TauCeti.Toric.characterEvaluation_neg {N : Type u_1} [AddCommGroup N] (m : IntegralCharacter N) : characterEvaluation (-m) = (characterEvaluation m)⁻¹

Evaluation sends negation of an integral character to inversion of a monoid homomorphism.

def TauCeti.Toric.complexTorusMap {N : Type u_1} {N' : Type u_2} [AddCommGroup N] [AddCommGroup N'] (f : N →+ N') : ComplexTorus N →* ComplexTorus N'

The map of complex tori induced covariantly by an additive map of lattices.

@[simp]

theorem TauCeti.Toric.complexTorusMap_apply {N : Type u_1} {N' : Type u_2} [AddCommGroup N] [AddCommGroup N'] (f : N →+ N') (x : ComplexTorus N) (m : IntegralCharacter N') : ((complexTorusMap f) x) m = (characterEvaluation (f.compHom' m)) x

The torus map induced by f evaluates by pulling the character back along f.

@[simp]

theorem TauCeti.Toric.complexTorusMap_id {N : Type u_1} [AddCommGroup N] : complexTorusMap (AddMonoidHom.id N) = MonoidHom.id (ComplexTorus N)

The identity lattice map induces the identity map of complex tori.

@[simp]

theorem TauCeti.Toric.complexTorusMap_comp {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] (g : N' →+ N'') (f : N →+ N') : complexTorusMap (g.comp f) = (complexTorusMap g).comp (complexTorusMap f)

Composition of lattice maps induces composition of the corresponding complex-torus maps.

theorem TauCeti.Toric.exists_complexTorusMap_comp_complexTorusMap_eq_id {N : Type u_1} {N' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [Module.Projective ℤ N'] {f : N →+ N'} (hf : Function.Surjective ⇑f) : ∃ (g : N' →+ N), (complexTorusMap f).comp (complexTorusMap g) = MonoidHom.id (ComplexTorus N')

A surjective map onto a projective lattice induces a map of complex tori with a section, itself induced by a section of the lattice map.

theorem TauCeti.Toric.complexTorusMap_surjective {N : Type u_1} {N' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [Module.Projective ℤ N'] {f : N →+ N'} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(complexTorusMap f)

A surjective map onto a projective lattice induces a surjective map of complex tori.

theorem TauCeti.Toric.mem_ker_complexTorusMap_mk'_iff {N : Type u_1} [AddCommGroup N] (H : AddSubgroup N) (x : ComplexTorus N) : x ∈ (complexTorusMap (QuotientAddGroup.mk' H)).ker ↔ ∀ (m : IntegralCharacter N), H ≤ AddMonoidHom.ker m → x m = 1

A torus point lies in the kernel of the torus map induced by the quotient by a sublattice H exactly when it is trivial on every integral character vanishing on H.

theorem TauCeti.Toric.exists_characterEvaluation_ne {N : Type u_1} [AddCommGroup N] {x y : ComplexTorus N} (h : x ≠ y) : ∃ (m : IntegralCharacter N), (characterEvaluation m) x ≠ (characterEvaluation m) y

Integral characters separate distinct points of the coordinate-free complex torus.

noncomputable def Module.Basis.integralCharacterRepr {N : Type u_1} [AddCommGroup N] {ι : Type u_4} [Finite ι] (B : Basis ι ℤ N) : TauCeti.Toric.IntegralCharacter N ≃+ (ι →₀ ℤ)

The free presentation of the character lattice dual to an integral basis B of N: an integral character corresponds to the family of its values on the basis vectors.

@[simp]

theorem Module.Basis.integralCharacterRepr_apply {N : Type u_1} [AddCommGroup N] {ι : Type u_4} [Finite ι] (B : Basis ι ℤ N) (m : TauCeti.Toric.IntegralCharacter N) (i : ι) : (B.integralCharacterRepr m) i = m (B i)

The coordinate of an integral character at a basis index is its value on that basis vector.

noncomputable def TauCeti.Toric.complexTorusCoordinates {N : Type u_1} [AddCommGroup N] {σ : Type u_4} (e : IntegralCharacter N ≃+ (σ →₀ ℤ)) : ComplexTorus N ≃* (σ → ℂˣ)

A free presentation of the character lattice identifies the coordinate-free complex torus with a product of copies of ℂˣ. The last step is Tau Ceti's freeAbelianCharEquiv.

@[simp]

theorem TauCeti.Toric.complexTorusCoordinates_apply {N : Type u_1} [AddCommGroup N] {σ : Type u_4} (e : IntegralCharacter N ≃+ (σ →₀ ℤ)) (x : ComplexTorus N) (i : σ) : (complexTorusCoordinates e) x i = x (e.symm (Finsupp.single i 1))

A coordinate supplied by a free presentation is evaluation at the corresponding transported standard generator of the character lattice.

@[simp]

theorem TauCeti.Toric.complexTorusCoordinates_symm_apply {N : Type u_1} [AddCommGroup N] {σ : Type u_4} (e : IntegralCharacter N ≃+ (σ →₀ ℤ)) (c : σ → ℂˣ) (m : IntegralCharacter N) : ((complexTorusCoordinates e).symm c) m = (e m).prod fun (i : σ) (n : ℤ) => c i ^ n

The torus point with prescribed coordinates evaluates an integral character to the Laurent monomial in those coordinates whose exponents are the coordinates of the character.

theorem TauCeti.Toric.complexTorus_apply_eq_prod_zpow {N : Type u_1} [AddCommGroup N] {σ : Type u_4} (e : IntegralCharacter N ≃+ (σ →₀ ℤ)) (x : ComplexTorus N) (m : IntegralCharacter N) : x m = (e m).prod fun (i : σ) (n : ℤ) => (complexTorusCoordinates e) x i ^ n

The Laurent-monomial formula: a torus point evaluates an integral character m to the product of its coordinates, in the presentation e, raised to the coordinates of m.

theorem TauCeti.Toric.complexTorus_apply_eq_prod_zpow_of_fintype {N : Type u_1} [AddCommGroup N] {σ : Type u_4} [Fintype σ] (e : IntegralCharacter N ≃+ (σ →₀ ℤ)) (x : ComplexTorus N) (m : IntegralCharacter N) : x m = ∏ i : σ, (complexTorusCoordinates e) x i ^ (e m) i

The Laurent-monomial formula for a finite index type.

noncomputable def Module.Basis.complexTorusCoordinates {N : Type u_1} {κ : Type u_2} [AddCommGroup N] [Module.Finite ℤ N] (b : Basis κ ℤ N) : TauCeti.Toric.ComplexTorus N ≃* (κ → ℂˣ)

The coordinates on the coordinate-free complex torus supplied by an integral basis of N: a torus point corresponds to its values on the dual basis characters, the coordinate functionals of the basis.

@[simp]

theorem Module.Basis.complexTorusCoordinates_apply {N : Type u_1} {κ : Type u_2} [AddCommGroup N] [Module.Finite ℤ N] (b : Basis κ ℤ N) (x : TauCeti.Toric.ComplexTorus N) (c : κ) : b.complexTorusCoordinates x c = x (b.coord c).toAddMonoidHom

The coordinate of a torus point indexed by a basis vector is its value on the coordinate functional of that vector.

@[simp]

theorem Module.Basis.complexTorusCoordinates_symm_apply {N : Type u_1} {κ : Type u_2} [AddCommGroup N] [Module.Finite ℤ N] (b : Basis κ ℤ N) (z : κ → ℂˣ) (c : κ) : (b.complexTorusCoordinates.symm z) (b.coord c).toAddMonoidHom = z c

The torus point with prescribed basis coordinates takes the prescribed value on each coordinate functional.