The Lindemann–Weierstrass theorem over a Galois number field

Let K be a number field, Galois over ℚ, together with an embedding of K into ℂ (an Algebra K ℂ structure). A formal exponential sum x = ∑ δ_γ [γ] ∈ K[K] evaluates to the complex number expEval K x = ∑ δ_γ exp γ. This file proves that this evaluation is injective: distinct elements of K have K-linearly independent exponentials.

• expEval_ne_zero_of_forall_galConj_eq: the weak Lindemann–Weierstrass theorem. A nonzero formal sum fixed by the conjugations galConj τ, τ ∈ Gal(K/ℚ), does not evaluate to 0.
• expEval_injective: the evaluation expEval K : K[K] →ₐ[K] ℂ is injective. The product of the conjugates of a formal sum x is Galois-invariant, it is nonzero when x is since K[K] is a domain, and its evaluation vanishes when that of x does.
• linearIndependent_exp_algebraMap: the same statement as linear independence of the family γ ↦ exp γ of exponentials of the elements of K.

The weak theorem follows Hermite's argument. After clearing denominators, the coefficients δ_γ are algebraic integers and l γ is an algebraic integer for a positive integer l and every γ in the support S of x. Fix γ₀ ∈ S. For large primes p the auxiliary value a = auxValue x l p γ₀ is a nonzero algebraic integer (auxValue_ne_zero, isIntegral_auxValue), so some complex conjugate of a has absolute value at least 1 (NumberField.exists_conjugate_one_le_norm). Since K / ℚ is normal and x is Galois-invariant, the conjugates of a are the auxiliary values at the conjugates of γ₀ (auxValue_galConj), and if expEval K x = 0 these all have absolute value less than 1 for large p (eventually_norm_auxValue_lt_one).

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 4, §4.2, Theorem 4.11 and its proof, and the deduction of Theorem 4.8 from it.
• Y. Zhao, formalization of the Lindemann–Weierstrass theorem in Lean, Basic.lean, which reduces to Galois-invariant exponential sums by taking the product of all conjugates.

theorem TauCeti.LindemannWeierstrass.expEval_ne_zero_of_forall_galConj_eq {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] [Algebra K ℂ] {x : AddMonoidAlgebra K K} (hx : x ≠ 0) (hfix : ∀ (τ : Gal(K/ℚ)), (galConj τ) x = x) : (expEval K) x ≠ 0

The weak Lindemann–Weierstrass theorem. Let K be a number field, Galois over ℚ and embedded in ℂ. If a nonzero formal exponential sum x = ∑ δ_γ [γ] ∈ K[K] is fixed by the conjugation galConj τ for every τ ∈ Gal(K/ℚ), then ∑ δ_γ exp γ ≠ 0.

theorem TauCeti.LindemannWeierstrass.expEval_injective {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] [Algebra K ℂ] : Function.Injective ⇑(expEval K)

The Lindemann–Weierstrass theorem over a Galois number field. Let K be a number field, Galois over ℚ and embedded in ℂ. Then the exponential evaluation ∑ δ_γ [γ] ↦ ∑ δ_γ exp γ of formal sums in K[K] is injective: the exponentials of distinct elements of K are linearly independent over K.

theorem TauCeti.LindemannWeierstrass.linearIndependent_exp_algebraMap {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] [Algebra K ℂ] : LinearIndependent K fun (γ : K) => Complex.exp ((algebraMap K ℂ) γ)

The Lindemann–Weierstrass theorem over a Galois number field, linear independence form. Let K be a number field, Galois over ℚ and embedded in ℂ. Then the exponentials of the elements of K are linearly independent over K.