Continuous characters of ℝˣ and ℂˣ

This file classifies the continuous homomorphisms ℝˣ → ℂˣ and ℂˣ → ℂˣ, the quasi-characters of the two archimedean local fields. Every continuous character of ℝˣ is x ↦ |x| ^ s * sgn(x) ^ ε with s : ℂ and ε : ZMod 2, and every continuous character of ℂˣ is z ↦ |z| ^ s * (z / |z|) ^ k with s : ℂ and k : ℤ. In both cases the parameters are unique, and multiplying characters adds them. The exponents s are complex: the unitary characters x ↦ |x| ^ (i t) form a continuous family that no integer or sign data can record. These are the archimedean components of Hecke characters, and their parameters are the data of an infinity type at the real and complex places.

The analytic input is TauCeti.existsUnique_eq_expUnitHom_complex: every continuous homomorphism from the additive real line to ℂˣ is t ↦ exp (t * s), with no differentiability hypothesis. It reads off the exponent s of a character from its restriction to the positive reals, and the angular frequency k of a character of ℂˣ from its restriction to the unit circle.

Main definitions

• TauCeti.realSignCharacter: the sign character of ℝˣ.
• TauCeti.complexAngularCharacter: the character z ↦ z / |z| of ℂˣ.
• TauCeti.realUnitsCharacter s ε: the character x ↦ |x| ^ s * sgn(x) ^ ε of ℝˣ.
• TauCeti.complexUnitsCharacter s k: the character z ↦ |z| ^ s * (z / |z|) ^ k of ℂˣ.
• TauCeti.realUnitsCharacterEquiv: Multiplicative (ℂ × ZMod 2) ≃* (ℝˣ →ₜ* ℂˣ).
• TauCeti.complexUnitsCharacterEquiv: Multiplicative (ℂ × ℤ) ≃* (ℂˣ →ₜ* ℂˣ).

Main results

• TauCeti.existsUnique_eq_expUnitHom_complex: continuous homomorphisms ℝ → ℂˣ are exponentials.
• TauCeti.realUnitsCharacter_comp_expUnitHom, TauCeti.realUnits_ext: restriction to the positive reals and extensionality for characters of ℝˣ.
• TauCeti.exists_eq_realUnitsCharacter, TauCeti.realUnitsCharacter_injective2: the classification of the continuous characters of ℝˣ.
• TauCeti.complexUnitsCharacter_comp_expUnitHom_one, TauCeti.complexUnitsCharacter_comp_expUnitHom_I, TauCeti.complexUnits_ext: restriction to the positive reals and unit circle and extensionality for characters of ℂˣ.
• TauCeti.exists_eq_complexUnitsCharacter, TauCeti.complexUnitsCharacter_injective2: the classification of the continuous characters of ℂˣ.
• TauCeti.realUnitsCharacter_map_normSq, TauCeti.complexUnitsCharacter_map_conj: the pullbacks of these characters along the norm ℂˣ → ℝˣ and along complex conjugation.

References

• J. Tate, Fourier analysis in number fields and Hecke's zeta-functions, in J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, §2.3.

The basic characters

noncomputable def TauCeti.realSignCharacter : ℝˣ →ₜ* ℂˣ

The sign character x ↦ sgn x of ℝˣ, with values ±1 in ℂˣ.

Equations

• TauCeti.realSignCharacter = { toMonoidHom := Units.map ((↑SignType.castHom).comp ↑signHom), continuous_toFun := TauCeti.realSignCharacter._proof_1✝ }

@[simp]

theorem TauCeti.coe_realSignCharacter_apply (x : ℝˣ) : ↑(realSignCharacter x) = ↑(SignType.sign ↑x)

Evaluating the sign character at x gives the sign of x.

noncomputable def TauCeti.complexAngularCharacter : ℂˣ →ₜ* ℂˣ

The angular character z ↦ z / |z| of ℂˣ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_complexAngularCharacter_apply (z : ℂˣ) : ↑(complexAngularCharacter z) = ↑z / ↑‖↑z‖

Evaluating the angular character at z gives z / |z|.

Characters of ℝˣ

noncomputable def TauCeti.realUnitsCharacter (s : ℂ) (ε : ZMod 2) : ℝˣ →ₜ* ℂˣ

The character x ↦ |x| ^ s * sgn(x) ^ ε of ℝˣ, for a complex exponent s and a parity ε : ZMod 2.

Equations

• TauCeti.realUnitsCharacter s ε = TauCeti.normCpowCharacter ℝ s * TauCeti.realSignCharacter ^ ε.val

@[simp]

theorem TauCeti.coe_realUnitsCharacter_apply (s : ℂ) (ε : ZMod 2) (x : ℝˣ) : ↑((realUnitsCharacter s ε) x) = ↑|↑x| ^ s * ↑(SignType.sign ↑x) ^ ε.val

Evaluating realUnitsCharacter s ε at x gives |x| ^ s * sgn(x) ^ ε.

theorem TauCeti.norm_coe_realUnitsCharacter_apply (s : ℂ) (ε : ZMod 2) (x : ℝˣ) : ‖↑((realUnitsCharacter s ε) x)‖ = |↑x| ^ s.re

The absolute value of realUnitsCharacter s ε at x is |x| ^ re s; the sign character contributes absolute value 1.

@[simp]

theorem TauCeti.realUnitsCharacter_zero_right (s : ℂ) : realUnitsCharacter s 0 = normCpowCharacter ℝ s

With parity 0, realUnitsCharacter s 0 is the norm-power character x ↦ |x| ^ s.

@[simp]

theorem TauCeti.realUnitsCharacter_zero_left (ε : ZMod 2) : realUnitsCharacter 0 ε = realSignCharacter ^ ε.val

With exponent 0, realUnitsCharacter 0 ε is the power sgn ^ ε of the sign character.

@[simp]

theorem TauCeti.realSignCharacter_sq : realSignCharacter ^ 2 = 1

The sign character has order two.

@[simp]

theorem TauCeti.realUnitsCharacter_add (s t : ℂ) (ε η : ZMod 2) : realUnitsCharacter (s + t) (ε + η) = realUnitsCharacter s ε * realUnitsCharacter t η

Adding parameters multiplies the characters of ℝˣ.

theorem TauCeti.realUnitsCharacter_comp_expUnitHom (s : ℂ) (ε : ZMod 2) : (realUnitsCharacter s ε).comp (expUnitHom 1) = expUnitHom s

Restricting realUnitsCharacter s ε to the positive reals gives expUnitHom s; the sign parameter is invisible on the identity component.

theorem TauCeti.realUnitsCharacter_neg_one (s : ℂ) (ε : ZMod 2) : ↑((realUnitsCharacter s ε) (-1)) = (-1) ^ ε.val

Evaluating realUnitsCharacter s ε at -1 gives (-1) ^ ε; the exponent s is invisible there.

theorem TauCeti.realUnits_ext {χ ψ : ℝˣ →ₜ* ℂˣ} (hneg : χ (-1) = ψ (-1)) (hexp : χ.comp (expUnitHom 1) = ψ.comp (expUnitHom 1)) : χ = ψ

Continuous characters of ℝˣ agree once they agree at -1 and on the positive reals.

theorem TauCeti.exists_eq_realUnitsCharacter (χ : ℝˣ →ₜ* ℂˣ) : ∃ (s : ℂ) (ε : ZMod 2), χ = realUnitsCharacter s ε

Every continuous character of ℝˣ is x ↦ |x| ^ s * sgn(x) ^ ε.

theorem TauCeti.realUnitsCharacter_injective2 : Function.Injective2 realUnitsCharacter

The exponent and the parity of x ↦ |x| ^ s * sgn(x) ^ ε are jointly determined by the character.

@[simp]

theorem TauCeti.realUnitsCharacter_inj {s t : ℂ} {ε η : ZMod 2} : realUnitsCharacter s ε = realUnitsCharacter t η ↔ s = t ∧ ε = η

Two characters x ↦ |x| ^ s * sgn(x) ^ ε agree exactly when their parameters do.

noncomputable def TauCeti.realUnitsCharacterEquiv : Multiplicative (ℂ × ZMod 2) ≃* (ℝˣ →ₜ* ℂˣ)

Classification of the continuous characters of ℝˣ. The continuous characters of ℝˣ are exactly the characters x ↦ |x| ^ s * sgn(x) ^ ε, for unique s : ℂ and ε : ZMod 2, and multiplying characters adds their parameters.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.realUnitsCharacterEquiv_apply (s : ℂ) (ε : ZMod 2) : realUnitsCharacterEquiv (Multiplicative.ofAdd (s, ε)) = realUnitsCharacter s ε

The classification equivalence sends (s, ε) to x ↦ |x| ^ s * sgn(x) ^ ε.

@[simp]

theorem TauCeti.realUnitsCharacterEquiv_symm_apply (s : ℂ) (ε : ZMod 2) : realUnitsCharacterEquiv.symm (realUnitsCharacter s ε) = Multiplicative.ofAdd (s, ε)

The inverse classification equivalence recovers the parameters of a real-units character.

Characters of ℂˣ

noncomputable def TauCeti.complexUnitsCharacter (s : ℂ) (k : ℤ) : ℂˣ →ₜ* ℂˣ

The character z ↦ |z| ^ s * (z / |z|) ^ k of ℂˣ, for a complex exponent s and an angular frequency k : ℤ.

Equations

• TauCeti.complexUnitsCharacter s k = TauCeti.normCpowCharacter ℂ s * TauCeti.complexAngularCharacter ^ k

@[simp]

theorem TauCeti.coe_complexUnitsCharacter_apply (s : ℂ) (k : ℤ) (z : ℂˣ) : ↑((complexUnitsCharacter s k) z) = ↑‖↑z‖ ^ s * (↑z / ↑‖↑z‖) ^ k

Evaluating complexUnitsCharacter s k at z gives |z| ^ s * (z / |z|) ^ k.

theorem TauCeti.norm_coe_complexUnitsCharacter_apply (s : ℂ) (k : ℤ) (z : ℂˣ) : ‖↑((complexUnitsCharacter s k) z)‖ = ‖↑z‖ ^ s.re

The absolute value of complexUnitsCharacter s k at z is |z| ^ re s; the angular character contributes absolute value 1.

theorem TauCeti.coe_complexUnitsCharacter_intCast (a b : ℤ) (z : ℂˣ) : ↑((complexUnitsCharacter (↑(a + b)) (a - b)) z) = ↑z ^ a * (starRingEnd ℂ) ↑z ^ b

Integer embedding exponents a and b give the algebraic character z ↦ z^a conj(z)^b. Their sum is the modulus exponent and their difference is the angular frequency.

@[simp]

theorem TauCeti.complexUnitsCharacter_zero_right (s : ℂ) : complexUnitsCharacter s 0 = normCpowCharacter ℂ s

With angular frequency 0, complexUnitsCharacter s 0 is the norm-power character z ↦ |z| ^ s.

@[simp]

theorem TauCeti.complexUnitsCharacter_zero_left (k : ℤ) : complexUnitsCharacter 0 k = complexAngularCharacter ^ k

With exponent 0, complexUnitsCharacter 0 k is the power (z / |z|) ^ k of the angular character.

@[simp]

theorem TauCeti.complexUnitsCharacter_add (s t : ℂ) (k l : ℤ) : complexUnitsCharacter (s + t) (k + l) = complexUnitsCharacter s k * complexUnitsCharacter t l

Adding parameters multiplies the characters of ℂˣ.

theorem TauCeti.realUnitsCharacter_map_normSq (s : ℂ) (ε : ZMod 2) (z : ℂˣ) : (realUnitsCharacter s ε) ((Units.map ↑Complex.normSq) z) = (complexUnitsCharacter (2 * s) 0) z

Pulling back x ↦ |x| ^ s * sgn(x) ^ ε along the norm z ↦ |z|² of ℂ / ℝ gives z ↦ |z| ^ (2 * s): the sign character is trivial on the positive values of the norm.

theorem TauCeti.complexUnitsCharacter_map_conj (s : ℂ) (k : ℤ) (z : ℂˣ) : (complexUnitsCharacter s k) ((Units.map ↑(starRingEnd ℂ)) z) = (complexUnitsCharacter s (-k)) z

Precomposing z ↦ |z| ^ s * (z / |z|) ^ k with complex conjugation negates the angular frequency.

theorem TauCeti.complexUnitsCharacter_comp_expUnitHom_one (s : ℂ) (k : ℤ) : (complexUnitsCharacter s k).comp (expUnitHom 1) = expUnitHom s

Restricting complexUnitsCharacter s k to the positive reals gives expUnitHom s; the angular frequency is invisible there.

theorem TauCeti.complexUnitsCharacter_comp_expUnitHom_I (s : ℂ) (k : ℤ) : (complexUnitsCharacter s k).comp (expUnitHom Complex.I) = expUnitHom (↑k * Complex.I)

Restricting complexUnitsCharacter s k to the standard parametrization of the unit circle gives expUnitHom (k * I); the modulus exponent is invisible there.

theorem TauCeti.complexUnits_ext {χ ψ : ℂˣ →ₜ* ℂˣ} (hpos : χ.comp (expUnitHom 1) = ψ.comp (expUnitHom 1)) (hcirc : χ.comp (expUnitHom Complex.I) = ψ.comp (expUnitHom Complex.I)) : χ = ψ

Continuous characters of ℂˣ agree once they agree on the positive reals and on the unit circle.

theorem TauCeti.exists_eq_complexUnitsCharacter (χ : ℂˣ →ₜ* ℂˣ) : ∃ (s : ℂ) (k : ℤ), χ = complexUnitsCharacter s k

Every continuous character of ℂˣ is z ↦ |z| ^ s * (z / |z|) ^ k.

theorem TauCeti.complexUnitsCharacter_injective2 : Function.Injective2 complexUnitsCharacter

The exponent and the angular frequency of z ↦ |z| ^ s * (z / |z|) ^ k are jointly determined by the character.

@[simp]

theorem TauCeti.complexUnitsCharacter_inj {s t : ℂ} {k l : ℤ} : complexUnitsCharacter s k = complexUnitsCharacter t l ↔ s = t ∧ k = l

Two characters z ↦ |z| ^ s * (z / |z|) ^ k agree exactly when their parameters do.

noncomputable def TauCeti.complexUnitsCharacterEquiv : Multiplicative (ℂ × ℤ) ≃* (ℂˣ →ₜ* ℂˣ)

Classification of the continuous characters of ℂˣ. The continuous characters of ℂˣ are exactly the characters z ↦ |z| ^ s * (z / |z|) ^ k, for unique s : ℂ and k : ℤ, and multiplying characters adds their parameters.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.complexUnitsCharacterEquiv_apply (s : ℂ) (k : ℤ) : complexUnitsCharacterEquiv (Multiplicative.ofAdd (s, k)) = complexUnitsCharacter s k

The classification equivalence sends (s, k) to z ↦ |z| ^ s * (z / |z|) ^ k.

@[simp]

theorem TauCeti.complexUnitsCharacterEquiv_symm_apply (s : ℂ) (k : ℤ) : complexUnitsCharacterEquiv.symm (complexUnitsCharacter s k) = Multiplicative.ofAdd (s, k)

The inverse classification equivalence recovers the parameters of a complex-units character.