Joint eigenvectors of commuting semisimple families

The eigenvalue function of a joint eigenvector of a monoid-hom representation ρ : G →* Module.End K V is a character: it maps 1 to 1, is multiplicative, and, for a group, valued in units, assembling into MonoidHom.unitHomOfJointEigenvector : G →* Kˣ. For an algebra representation it is moreover additive and R-linear, assembling into AlgHom.eigenvalueHomOfJointEigenvector : A →ₐ[R] K. This much needs no division — a nonzero vector cancels over a commutative ring without zero divisors acting torsion-freely, and on a group multiplicativity exhibits the inverse of χ g as χ g⁻¹. This yields the simultaneous-diagonalization toolkit for a commuting family of semisimple endomorphisms: the joint eigenspaces are supremum-independent, they span (over an algebraically closed field, in finite dimension), and every invariant submodule is the supremum of its intersections with them.

When G is a finite commutative group there is a second, unconditional route to the same spanning statements. Averaging against the characters of G produces Fourier projectors onto the joint eigenspaces, so they exhaust the whole space — and cut out every invariant submodule — with no algebraic-closedness, finite-dimensionality or semisimplicity hypothesis; all that is needed is enough roots of unity in K and Nat.card G invertible there.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/CharacterDecomp.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), extracted as representation-theoretic infrastructure with no modular-forms dependence: there G is the group (ZMod N)ˣ of diamond operators, and the character eigenspaces are the nebentypus components of M_k(Γ₁(N)).

Main results

• MonoidHom.unitHomOfJointEigenvector: the eigenvalue function of a nonzero joint eigenvector of a group representation, as a monoid homomorphism G →* Kˣ.
• AlgHom.eigenvalueHomOfJointEigenvector: the eigenvalue function of a nonzero joint eigenvector of an algebra representation, as an algebra homomorphism A →ₐ[R] K.
• iSupIndep_iInf_eigenspace, iSup_iInf_eigenspace_eq_top_of_isSemisimple, iSup_inf_iInf_eigenspace_of_invariant: joint eigenspaces of a commuting family are independent (with no further hypotheses), exhaust the space when semisimple, and decompose every invariant submodule — with the character-indexed forms (…_unitHom…) for group representations.
• MonoidHom.finite_nonzeroJointWeights, MonoidHom.natCard_nonzeroJointWeights_le_finrank: a representation on a finite module over a domain has finitely many nonzero joint weights, with their number bounded by its rank.
• iSup_iInf_eigenspace_unitHom_eq_top_of_commGroup, iSup_inf_iInf_eigenspace_unitHom_of_invariant_of_commGroup: for a finite commutative G with [HasEnoughRootsOfUnity K (Monoid.exponent G)] and IsUnit (Nat.card G : K), the character eigenspaces span the whole space, and every invariant submodule is the supremum of its intersections with them — proved by finite-group Fourier projectors, so neither semisimplicity nor finite dimension is assumed.

The restriction bridge

theorem Submodule.inf_iInf_eigenspace_of_forall_mapsTo {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [Module K V] {ι : Type u_4} {f : ι → Module.End K V} (p : Submodule K V) (hp : ∀ (i : ι), Set.MapsTo ⇑(f i) ↑p ↑p) (χ : ι → K) : p ⊓ ⨅ (i : ι), (f i).eigenspace (χ i) = map p.subtype (⨅ (i : ι), Module.End.eigenspace (LinearMap.restrict (f i) ⋯) (χ i))

The restriction bridge for joint eigenspaces: for a family of endomorphisms mapping a submodule p into itself, the part of a joint eigenspace lying in p is the image of the joint eigenspace of the restricted family. This is the eigenspace analogue of Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo.

Eigenvalues of a joint eigenvector

Over a commutative ring with cancellation acting torsion-freely, so that a nonzero vector cancels.

theorem MonoidHom.eigenvalue_one_of_jointEigenvector {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] [MulOne G] (ρ : G →* Module.End K V) (χ : G → K) (v : V) (hv : v ≠ 0) (hv_mem : ∀ (g : G), v ∈ (ρ g).eigenspace (χ g)) : χ 1 = 1

If v ≠ 0 is a joint eigenvector of a monoid-hom representation ρ : G →* Module.End K V with eigenvalues χ g, then the eigenvalue at the identity is 1.

theorem MonoidHom.eigenvalue_mul_of_jointEigenvector {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] [MulOne G] (ρ : G →* Module.End K V) (χ : G → K) (v : V) (hv : v ≠ 0) (hv_mem : ∀ (g : G), v ∈ (ρ g).eigenspace (χ g)) (g₁ g₂ : G) : χ (g₁ * g₂) = χ g₁ * χ g₂

If v ≠ 0 is a joint eigenvector of a monoid-hom representation ρ : G →* Module.End K V with eigenvalues χ g, then the eigenvalues are multiplicative: χ (g₁ * g₂) = χ g₁ * χ g₂.

def AlgHom.eigenvalueHomOfJointEigenvector {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] {R : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Algebra R K] [Module R V] [IsScalarTower R K V] (ρ : A →ₐ[R] Module.End K V) (χ : A → K) (v : V) (hv : v ≠ 0) (hv_mem : ∀ (a : A), v ∈ (ρ a).eigenspace (χ a)) : A →ₐ[R] K

Given a joint eigenvector v ≠ 0 for an algebra representation ρ : A →ₐ[R] Module.End K V, the eigenvalue function χ : A → K is an R-algebra homomorphism.

Equations

• ρ.eigenvalueHomOfJointEigenvector χ v hv hv_mem = { toFun := χ, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgHom.eigenvalueHomOfJointEigenvector_apply {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] {R : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Algebra R K] [Module R V] [IsScalarTower R K V] (ρ : A →ₐ[R] Module.End K V) (χ : A → K) (v : V) (hv : v ≠ 0) (hv_mem : ∀ (a : A), v ∈ (ρ a).eigenspace (χ a)) (a : A) : (ρ.eigenvalueHomOfJointEigenvector χ v hv hv_mem) a = χ a

def MonoidHom.unitHomOfJointEigenvector {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] [Group G] (ρ : G →* Module.End K V) (χ : G → K) (v : V) (hv : v ≠ 0) (hv_mem : ∀ (g : G), v ∈ (ρ g).eigenspace (χ g)) : G →* Kˣ

Given a joint eigenvector v ≠ 0 for a monoid-hom representation ρ : G →* Module.End K V of a group G, the eigenvalue function χ : G → K factors through a monoid homomorphism G →* Kˣ.

Equations

• ρ.unitHomOfJointEigenvector χ v hv hv_mem = { toFun := χ, map_one' := ⋯, map_mul' := ⋯ }.toHomUnits

@[simp]

theorem MonoidHom.unitHomOfJointEigenvector_apply {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] [Group G] (ρ : G →* Module.End K V) (χ : G → K) (v : V) (hv : v ≠ 0) (hv_mem : ∀ (g : G), v ∈ (ρ g).eigenspace (χ g)) (g : G) : ↑((ρ.unitHomOfJointEigenvector χ v hv hv_mem) g) = χ g

theorem MonoidHom.eigenvalue_ne_zero_of_jointEigenvector {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] [Group G] (ρ : G →* Module.End K V) (χ : G → K) (v : V) (hv : v ≠ 0) (hv_mem : ∀ (g : G), v ∈ (ρ g).eigenspace (χ g)) (g : G) : χ g ≠ 0

The eigenvalues of a nonzero joint eigenvector of a group representation are nonzero.

theorem TauCeti.exists_unitHom_of_iInf_eigenspace_ne_bot {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsCancelMulZero K] [Module K V] [Module.IsTorsionFree K V] [Group G] {ρ : G →* Module.End K V} {χ : G → K} (hχ : ⨅ (g : G), (ρ g).eigenspace (χ g) ≠ ⊥) : ∃ (χ₀ : G →* Kˣ), (fun (g : G) => ↑(χ₀ g)) = χ

If the joint eigenspace of an eigenvalue function χ of a group representation is nonzero, then χ is (the underlying function of) a character G →* Kˣ.

Independence of joint eigenspaces

Over a commutative domain acting torsion-freely.

theorem TauCeti.iSupIndep_iInf_eigenspace {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsDomain K] [Module K V] [Module.IsTorsionFree K V] {ι : Type u_4} (f : ι → Module.End K V) : iSupIndep fun (χ : ι → K) => ⨅ (i : ι), (f i).eigenspace (χ i)

The joint eigenspaces of any family of endomorphisms, indexed by their eigenvalue functions, are supremum-independent — no commutation and no semisimplicity.

theorem TauCeti.iSupIndep_iInf_eigenspace_unitHom {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsDomain K] [Module K V] [Module.IsTorsionFree K V] [MulOne G] {ρ : G →* Module.End K V} : iSupIndep fun (χ₀ : G →* Kˣ) => ⨅ (g : G), (ρ g).eigenspace ↑(χ₀ g)

Character-indexed independence of the joint eigenspaces, for any representation.

instance MonoidHom.finite_nonzeroJointWeights {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsDomain K] [Module K V] [Module.IsTorsionFree K V] [MulOne G] [Module.Finite K V] (ρ : G →* Module.End K V) : Finite { χ : G →* Kˣ // ⨅ (g : G), (ρ g).eigenspace ↑(χ g) ≠ ⊥ }

A representation on a finite module has only finitely many characters with nonzero joint weight space.

theorem MonoidHom.natCard_nonzeroJointWeights_le_finrank {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsDomain K] [Module K V] [Module.IsTorsionFree K V] [MulOne G] [Module.Finite K V] (ρ : G →* Module.End K V) : Nat.card { χ : G →* Kˣ // ⨅ (g : G), (ρ g).eigenspace ↑(χ g) ≠ ⊥ } ≤ Module.finrank K V

The number of characters with nonzero joint weight space in a representation on a finite module is bounded by the rank of the module.

Simultaneous diagonalization

The spanning statements for semisimple families, over an algebraically closed field.

theorem TauCeti.iSup_iInf_eigenspace_eq_top_of_isSemisimple {K : Type u_2} {V : Type u_3} [AddCommGroup V] [Field K] [IsAlgClosed K] [Module K V] [FiniteDimensional K V] {ι : Type u_4} (f : ι → Module.End K V) (hcomm : Pairwise fun (i j : ι) => Commute (f i) (f j)) (hss : ∀ (i : ι), (f i).IsSemisimple) : ⨆ (χ : ι → K), ⨅ (i : ι), (f i).eigenspace (χ i) = ⊤

Over an algebraically closed field and in finite dimension, the joint eigenspaces of a pairwise-commuting family of semisimple endomorphisms exhaust the space.

theorem TauCeti.iSup_inf_iInf_eigenspace_of_invariant {K : Type u_2} {V : Type u_3} [AddCommGroup V] [Field K] [IsAlgClosed K] [Module K V] {ι : Type u_4} (f : ι → Module.End K V) (p : Submodule K V) [FiniteDimensional K ↥p] (hp : ∀ (i : ι), ∀ x ∈ p, (f i) x ∈ p) (hcomm : Pairwise fun (i j : ι) => Commute (LinearMap.restrict (f i) ⋯) (LinearMap.restrict (f j) ⋯)) (hss : ∀ (i : ι), Module.End.IsSemisimple (LinearMap.restrict (f i) ⋯)) : ⨆ (χ : ι → K), p ⊓ ⨅ (i : ι), (f i).eigenspace (χ i) = p

A finite-dimensional submodule invariant under a pairwise-commuting family of endomorphisms whose restrictions to it are semisimple is the supremum of its intersections with the joint eigenspaces: the restricted family diagonalizes, with no assumption on the ambient operators.

theorem TauCeti.iSup_iInf_eigenspace_unitHom_eq_top {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [Field K] [IsAlgClosed K] [Module K V] [Group G] {ρ : G →* Module.End K V} [FiniteDimensional K V] (hcomm : Pairwise fun (g₁ g₂ : G) => Commute (ρ g₁) (ρ g₂)) (hss : ∀ (g : G), (ρ g).IsSemisimple) : ⨆ (χ₀ : G →* Kˣ), ⨅ (g : G), (ρ g).eigenspace ↑(χ₀ g) = ⊤

Character-indexed spanning: for a commuting semisimple representation of a group over an algebraically closed field, in finite dimension, the joint eigenspaces indexed by characters G →* Kˣ exhaust the space.

theorem TauCeti.iSup_inf_iInf_eigenspace_unitHom_of_invariant {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [Field K] [IsAlgClosed K] [Module K V] [Group G] {ρ : G →* Module.End K V} (p : Submodule K V) [FiniteDimensional K ↥p] (hp : ∀ (g : G), ∀ x ∈ p, (ρ g) x ∈ p) (hcomm : Pairwise fun (g₁ g₂ : G) => Commute (LinearMap.restrict (ρ g₁) ⋯) (LinearMap.restrict (ρ g₂) ⋯)) (hss : ∀ (g : G), Module.End.IsSemisimple (LinearMap.restrict (ρ g) ⋯)) : ⨆ (χ₀ : G →* Kˣ), p ⊓ ⨅ (g : G), (ρ g).eigenspace ↑(χ₀ g) = p

Character-indexed decomposition of a finite-dimensional invariant submodule, assuming only that the restricted representation is semisimple.

Unconditional decomposition for finite commutative groups

For a finite commutative group G acting through ρ : G →* Module.End K V on any module over a commutative domain with enough roots of unity in which Nat.card G is invertible — with no finite-dimensionality assumption — the classical character projectors |G|⁻¹ • ∑ d, χ(d)⁻¹ • ρ d decompose every vector into joint eigenvectors, so the joint eigenspaces indexed by G →* Kˣ span.

theorem TauCeti.iSup_inf_iInf_eigenspace_unitHom_of_invariant_of_commGroup {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsDomain K] [Module K V] [CommGroup G] [Finite G] {ρ : G →* Module.End K V} [HasEnoughRootsOfUnity K (Monoid.exponent G)] (hcard : IsUnit ↑(Nat.card G)) (p : Submodule K V) (hp : ∀ (g : G), ∀ x ∈ p, (ρ g) x ∈ p) : ⨆ (χ₀ : G →* Kˣ), p ⊓ ⨅ (g : G), (ρ g).eigenspace ↑(χ₀ g) = p

Unconditional decomposition of an invariant submodule: the character projectors preserve every ρ-invariant submodule, so it is the supremum of its intersections with the joint eigenspaces — again with no finite-dimensionality hypothesis.

theorem TauCeti.iSup_iInf_eigenspace_unitHom_eq_top_of_commGroup {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [CommRing K] [IsDomain K] [Module K V] [CommGroup G] [Finite G] {ρ : G →* Module.End K V} [HasEnoughRootsOfUnity K (Monoid.exponent G)] (hcard : IsUnit ↑(Nat.card G)) : ⨆ (χ₀ : G →* Kˣ), ⨅ (g : G), (ρ g).eigenspace ↑(χ₀ g) = ⊤

Unconditional character-indexed spanning for a finite commutative group acting on an arbitrary module over a commutative domain with enough roots of unity: the classical character projectors decompose every vector, with no finite-dimensionality or semisimplicity hypotheses.