The circle group: Fourier monomials are its finite-dimensional irreducible representations

For a positive period — the standing hypothesis [Fact (0 < T)], which is what Mathlib's compactness instance and its Fourier analysis on AddCircle T both require — the circle AddCircle T is a compact abelian group. This file builds its continuous representations on ℂ from Mathlib's Fourier monomials, shows that they exhaust the finite-dimensional irreducible continuous representations up to equivalence and are pairwise inequivalent, and checks that the general compact-group theory, specialized to the circle, returns Mathlib's Fourier analysis on the nose.

Concretely, fourierRep T n is the continuous representation of the circle on ℂ in which the group element x acts by multiplication by fourier n x. It is one-dimensional, hence irreducible, and unitary because fourier n x has modulus one; its character is fourier n again. Under those identifications:

• the L² inner product of two of these characters, computed for the normalized Haar measure of TauCeti/RepresentationTheory/Compact/Haar.lean, is Mathlib's AddCircle.orthonormal_fourier;
• the general first orthogonality relation character_orthonormal_self and the general second orthogonality relation character_orthonormal_distinct return the diagonal and off-diagonal halves of that same statement.

The list n ↦ fourierRep T n is moreover complete among the finite-dimensional irreducibles. A representation carried by ℂ acts by the scalar π x 1, which is a continuous additive character of AddCircle T and therefore a Fourier monomial by AddChar.exists_fourierAddChar_eq, so it is a fourierRep. A finite-dimensional irreducible one on an arbitrary carrier is only equivalent to a fourierRep, its carrier being a line by the dimension count for an irreducible representation of a commutative group over an algebraically closed field. The index n is uniquely determined, so ℤ indexes the finite-dimensional irreducibles exactly once.

The last two are recorded as anonymous examples: they are consistency checks on the general theory's normalization, not new API, and naming them would duplicate TauCeti.inner_characterLp_fourierRep.

Main definitions

• TauCeti.fourierChar: the n-th Fourier monomial as a linear character Multiplicative (AddCircle T) →* ℂˣ of the circle group.
• TauCeti.fourierRep: the n-th Fourier monomial as a one-dimensional continuous representation of the circle group.

Main statements

• TauCeti.haarProb_eq_haarAddCircle: the normalized Haar measure of the circle group is Mathlib's AddCircle.haarAddCircle.
• TauCeti.measurePreserving_ofAdd_haarAddCircle: Multiplicative.ofAdd carries AddCircle.haarAddCircle to that normalized Haar measure.
• TauCeti.isUnitary_fourierRep, TauCeti.isIrreducible_fourierRep: each fourierRep T n is a unitary irreducible representation.
• TauCeti.character_fourierRep: the character of fourierRep T n is fourier n.
• TauCeti.contIntertwiningMap_fourierRep_eq_zero_of_ne: for m ≠ n there is no nonzero continuous intertwiner fourierRep T n → fourierRep T m, so the Fourier representations are pairwise inequivalent.
• MonoidHom.exists_fourierChar_eq, ContRepresentation.exists_fourierRep_eq: every continuous linear character of the circle group, and every continuous representation of it carried by ℂ, is a Fourier one.
• TauCeti.nonempty_equiv_fourierRep_iff: two Fourier representations are equivalent only if they are equal.
• ContRepresentation.exists_nonempty_equiv_fourierRep, ContRepresentation.existsUnique_nonempty_equiv_fourierRep: the classification. Every finite-dimensional irreducible continuous representation of the circle group is equivalent to fourierRep T n for a unique n : ℤ.
• TauCeti.orthonormal_characterLp_fourierRep: the characters of the fourierRep T n are an orthonormal family in L² of the circle group for normalized Haar measure; this is AddCircle.orthonormal_fourier read through the general compact-group packaging.

Implementation notes

fourierRep T n acts by the scalar fourierChar T n, so its underlying representation is Representation.ofLinearCharacter (fourierChar T n) (TauCeti.toRepresentation_fourierRep); irreducibility and the character are then the corresponding facts about a linear character, not fresh one-dimensional computations.

ContRepresentation is stated for a multiplicative monoid, while AddCircle T is additive, so the group here is Multiplicative (AddCircle T). The measure-theoretic instances that makes that type usable as a compact group with Haar measure are in TauCeti/MeasureTheory/Group/TypeTags.lean; they are definitional, so haarProb_eq_haarAddCircle is just the uniqueness of a Haar probability measure applied on the multiplicative side. Because Multiplicative (AddCircle T) and AddCircle T are the same type with the same topology and σ-algebra, an integral over one is literally an integral over the other, which is what lets inner_characterLp_fourierRep end in Mathlib's orthonormality statement.

The two exhaustion statements are deliberately different in kind. On the carrier ℂ the Fourier representation is recovered on the nose, as an equality of representations (ContRepresentation.exists_fourierRep_eq); on an arbitrary carrier no equality is available, and ContRepresentation.exists_nonempty_equiv_fourierRep produces a ContRepresentation.Equiv instead. The passage between them is ContinuousLinearEquiv.congr, the transport of a representation along a continuous linear equivalence of carriers. What is not done here is the full Peter-Weyl identification of peterWeylBasis with AddCircle.fourierBasis under the indexing equivalence Σ π, Fin 1 × Fin 1 ≃ ℤ.

The general compact-group character theory that is specialized here is in TauCeti/RepresentationTheory/Compact/Character/Basic.lean. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

Tags

circle group, Fourier series, character, Peter-Weyl

noncomputable def TauCeti.fourierChar (T : ℝ) (n : ℤ) : Multiplicative (AddCircle T) →* ℂˣ

The n-th Fourier monomial as a linear character of the circle group. It is Mathlib's AddCircle.toCircle_addChar precomposed with multiplication by n, read as a multiplicative character valued in ℂˣ; TauCeti.coe_fourierChar identifies its value with fourier n.

Equations

• TauCeti.fourierChar T n = Circle.toUnits.comp (AddCircle.toCircle_addChar.compAddMonoidHom (zsmulAddGroupHom n)).toMonoidHom

@[simp]

theorem TauCeti.coe_fourierChar (T : ℝ) (n : ℤ) (x : Multiplicative (AddCircle T)) : ↑((fourierChar T n) x) = (fourier n) (Multiplicative.toAdd x)

theorem TauCeti.continuous_coe_fourierChar (T : ℝ) (n : ℤ) : Continuous fun (x : Multiplicative (AddCircle T)) => ↑((fourierChar T n) x)

The Fourier character is continuous as a ℂ-valued function: that is the continuity of fourier n. This is the hypothesis of MonoidHom.exists_fourierChar_eq.

noncomputable def TauCeti.fourierRep (T : ℝ) (n : ℤ) : ContRepresentation ℂ (Multiplicative (AddCircle T)) ℂ

The n-th Fourier character of the circle group, as a one-dimensional continuous representation on ℂ: the group element x acts by multiplication by fourier n x.

Equations

• TauCeti.fourierRep T n = { toMonoidHom := { toFun := fun (x : Multiplicative (AddCircle T)) => ↑((TauCeti.fourierChar T n) x) • 1, map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem TauCeti.fourierRep_apply (T : ℝ) (n : ℤ) (x : Multiplicative (AddCircle T)) (z : ℂ) : ((fourierRep T n) x) z = (fourier n) (Multiplicative.toAdd x) * z

theorem TauCeti.toRepresentation_fourierRep (T : ℝ) (n : ℤ) : ContRepresentation.toRepresentation ℂ (Multiplicative (AddCircle T)) ℂ (fourierRep T n) = Representation.ofLinearCharacter (fourierChar T n)

The Fourier representation is the one-dimensional representation of its linear character. Everything about it that only depends on the scalar action -- irreducibility, the character -- is read off from Representation.ofLinearCharacter through this identification.

theorem TauCeti.continuous_fourierRep (T : ℝ) (n : ℤ) : Continuous ⇑(fourierRep T n)

The Fourier representation is continuous: its action operator depends on the group element through the continuous map fourier n.

theorem TauCeti.isUnitary_fourierRep (T : ℝ) (n : ℤ) : (fourierRep T n).IsUnitary

The Fourier representation is unitary: multiplication by a number of modulus one is an isometry of ℂ.

theorem TauCeti.isIrreducible_fourierRep (T : ℝ) (n : ℤ) : (ContRepresentation.toRepresentation ℂ (Multiplicative (AddCircle T)) ℂ (fourierRep T n)).IsIrreducible

The Fourier representation is irreducible, being the one-dimensional representation of a linear character.

@[simp]

theorem TauCeti.character_fourierRep (T : ℝ) (n : ℤ) : (fourierRep T n).character ⋯ = fourier n

The character of the n-th Fourier representation is fourier n. A one-dimensional representation is its own character; this is Representation.char_ofLinearCharacter read through TauCeti.toRepresentation_fourierRep. The equality is one of continuous maps, so it identifies the character of fourierRep T n with Mathlib's Fourier monomial as an element of C(AddCircle T, ℂ), and every fact Mathlib proves about fourier n there — its continuity, its values, its L² norm — transfers to the character.

theorem TauCeti.contIntertwiningMap_fourierRep_eq_zero_of_ne (T : ℝ) (hT : T ≠ 0) {m n : ℤ} (h : m ≠ n) (f : ContIntertwiningMap (fourierRep T n) (fourierRep T m)) : f.toContinuousLinearMap = 0

The Fourier representations are pairwise inequivalent. For m ≠ n every continuous intertwiner fourierRep T n → fourierRep T m vanishes: such a map is multiplication by its value c at 1, and intertwining forces fourier n x * c = fourier m x * c for every x, so c = 0 by TauCeti.fourier_injective.

This is the hypothesis of the general second orthogonality relation ContRepresentation.character_orthonormal_distinct.

@[simp]

theorem TauCeti.nonempty_equiv_fourierRep_iff (T : ℝ) (hT : T ≠ 0) {m n : ℤ} : Nonempty ((fourierRep T m).Equiv (fourierRep T n)) ↔ m = n

Two Fourier representations are equivalent only if they are equal. The Fourier representations of the circle group are therefore indexed by ℤ without repetition.

theorem TauCeti.haarProb_eq_haarAddCircle (T : ℝ) [hT : Fact (0 < T)] : haarProb (Multiplicative (AddCircle T)) = AddCircle.haarAddCircle

Normalized Haar measure on the circle group is Mathlib's AddCircle.haarAddCircle. Both are Haar probability measures on a compact group, and there is only one such.

theorem TauCeti.measurePreserving_ofAdd_haarAddCircle (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.MeasurePreserving (⇑Multiplicative.ofAdd) AddCircle.haarAddCircle (haarProb (Multiplicative (AddCircle T)))

Multiplicative.ofAdd carries Mathlib's Haar measure on AddCircle T to the normalized Haar measure of the circle group, so it transports L² of the circle group to L²(AddCircle T).

theorem TauCeti.inner_characterLp_fourierRep (T : ℝ) [hT : Fact (0 < T)] (m n : ℤ) : inner ℂ ((fourierRep T m).characterLp ⋯) ((fourierRep T n).characterLp ⋯) = if m = n then 1 else 0

The L² inner product of two Fourier characters is Mathlib's Fourier orthonormality. Both sides are the Haar integral of fourier n · conj (fourier m); the left is that integral written for the general compact-group packaging of TauCeti/RepresentationTheory/Compact/Character/Basic.lean, the right is AddCircle.orthonormal_fourier.

theorem TauCeti.orthonormal_characterLp_fourierRep (T : ℝ) [hT : Fact (0 < T)] : Orthonormal ℂ fun (n : ℤ) => (fourierRep T n).characterLp ⋯

The characters of the Fourier representations are orthonormal. They form an orthonormal family in L² of the circle group for normalized Haar measure: the general compact-group character theory, specialized to the circle, is Mathlib's AddCircle.orthonormal_fourier. The identification of peterWeylBasis with AddCircle.fourierBasis is not proved here.

theorem MonoidHom.exists_fourierChar_eq {T : ℝ} [hT : Fact (0 < T)] (χ : Multiplicative (AddCircle T) →* ℂˣ) (hχ : Continuous fun (x : Multiplicative (AddCircle T)) => ↑(χ x)) : ∃ (n : ℤ), TauCeti.fourierChar T n = χ

Every continuous linear character of the circle group is a Fourier character. This is AddChar.exists_fourierAddChar_eq, the classification of the continuous additive characters of AddCircle T, read for the ℂˣ-valued multiplicative characters that Representation.ofLinearCharacter consumes.

theorem ContRepresentation.exists_fourierRep_eq {T : ℝ} [hT : Fact (0 < T)] (π : ContRepresentation ℂ (Multiplicative (AddCircle T)) ℂ) (hπ : Continuous ⇑π) : ∃ (n : ℤ), TauCeti.fourierRep T n = π

Every continuous representation of the circle group carried by ℂ is a Fourier representation. With TauCeti.contIntertwiningMap_fourierRep_eq_zero_of_ne this says that n ↦ fourierRep T n lists the continuous representations of the circle group on ℂ exactly once. The quantifier is over representations whose carrier is literally ℂ, which is what makes the conclusion an equality; ContRepresentation.exists_nonempty_equiv_fourierRep is the corresponding statement for an arbitrary finite-dimensional carrier, where only an equivalence can be asked for.

theorem ContRepresentation.exists_nonempty_equiv_fourierRep {T : ℝ} [hT : Fact (0 < T)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ (Multiplicative (AddCircle T)) V) (hπ : Continuous ⇑π) (hirr : (toRepresentation ℂ (Multiplicative (AddCircle T)) V π).IsIrreducible) : ∃ (n : ℤ), Nonempty (π.Equiv (TauCeti.fourierRep T n))

Every finite-dimensional irreducible continuous representation of the circle group is equivalent to a Fourier representation. Together with TauCeti.nonempty_equiv_fourierRep_iff this says that ℤ indexes the finite-dimensional irreducibles of the circle group exactly once.

The carrier is an arbitrary finite-dimensional complex normed space, so the conclusion is an equivalence rather than the equality of ContRepresentation.exists_fourierRep_eq.

theorem ContRepresentation.existsUnique_nonempty_equiv_fourierRep {T : ℝ} [hT : Fact (0 < T)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ (Multiplicative (AddCircle T)) V) (hπ : Continuous ⇑π) (hirr : (toRepresentation ℂ (Multiplicative (AddCircle T)) V π).IsIrreducible) : ∃! n : ℤ, Nonempty (π.Equiv (TauCeti.fourierRep T n))

The Fourier index of a finite-dimensional irreducible continuous representation of the circle group is unique. Existence is ContRepresentation.exists_nonempty_equiv_fourierRep and uniqueness is TauCeti.nonempty_equiv_fourierRep_iff, so ℤ is a complete and irredundant index of the finite-dimensional irreducibles.