Criteria for irreducibility

This file collects three ways of recognising an irreducible representation from outside, without inspecting its subrepresentations one by one, and the finite-dimensional existence statement that makes the second of them usable.

A representation on a one-dimensional vector space is irreducible, whatever the group and however it acts: a subrepresentation is in particular a subspace, and a line has only the two trivial subspaces. Nontriviality, the other half of irreducibility, is the same dimension count. This is how the smallest representations of a group are recognised as irreducible without knowing anything about the group -- the trivial representation, a character, a sign.

The second criterion turns a lattice-theoretic statement about a fixed ambient representation into a statement about a subrepresentation on its own: a subrepresentation that is an atom of the lattice of subrepresentations carries an irreducible representation. Irreducibility of a subrepresentation σ of ρ is a statement about the subrepresentations of σ.toRepresentation, one level down from ρ, whereas minimality is a statement inside the lattice attached to ρ; the translation between them is the correspondence sending a subrepresentation of σ.toRepresentation to its image in ρ under the inclusion of σ.toSubmodule. In practice the atom form is the one that gets proved -- one exhibits an invariant subspace of the ambient representation and shows it has no proper nonzero invariant subspace -- and the irreducibility form is the one that gets used.

At the other extreme, a representation whose algebra map exhausts End k V is irreducible, because a vector space is a simple module over its own endomorphism ring, so a nonzero vector can be carried to any other. This is the criterion a matrix block of a semisimple group algebra is recognised as irreducible by.

Main results

• Representation.IsIrreducible.nontrivial: an irreducible representation has a nonzero carrier.
• Representation.IsIrreducible.finrank_pos: a finite-dimensional irreducible representation has positive dimension.
• Representation.IsIrreducible.natCast_finrank_ne_zero: in characteristic zero that dimension is nonzero, hence invertible, in the base field.
• Representation.IsIrreducible.finiteDimensional: an irreducible representation of a finite monoid is finite-dimensional.
• Representation.isIrreducible_of_finrank_eq_one: a line is irreducible.
• Representation.isIrreducible_of_linearEquiv: irreducibility transports along an equivariant linear equivalence.
• Representation.isIrreducible_toRepresentation_of_isAtom: an atom of the lattice of subrepresentations carries an irreducible representation.
• Representation.isIrreducible_of_asAlgebraHom_surjective: a representation whose algebra map exhausts the endomorphisms is irreducible.
• Representation.isIrreducible_of_finrank_intertwiningMap_self_eq_one: a semisimple representation whose equivariant endomorphisms are the scalars is irreducible.
• Representation.asAlgebraHom_surjective_of_isIrreducible: over an algebraically closed field, every finite-dimensional irreducible representation exhausts the endomorphisms.
• Representation.exists_ne_zero_forall_exists_rTensor_asAlgebraHom_eq_tmul: consequently the monoid algebra, acting on the left factor of a nonzero tensor in V ⊗ M, reaches every v ⊗ m for one fixed nonzero m.
• Representation.exists_isAtom_le: every nonzero finite-dimensional subrepresentation contains an atom, so the atom criterion always has something to apply to.
• Representation.exists_isAtom: in particular a nonzero finite-dimensional representation has an atom.
• Representation.exists_isIrreducible_subrepresentation: consequently every nonzero finite-dimensional representation contains an irreducible subrepresentation.
• Representation.IsIrreducible.exists_forall_apply_eq_smul: Schur's lemma over an algebraically closed field, for an unbundled equivariant endomorphism.
• Representation.IsIrreducible.exists_unit_smul_of_intertwines: two equivariant isomorphisms out of an irreducible representation differ by a unit scalar.

theorem Representation.IsIrreducible.nontrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) : Nontrivial V

An irreducible representation has a nonzero carrier. This is IsSimpleModule.nontrivial for ρ.asModule, read back on V along ρ.asModuleEquiv; the Mathlib statement is not an instance, so nothing supplies Nontrivial V without naming it.

theorem Representation.IsIrreducible.finrank_pos {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) : 0 < Module.finrank k V

A finite-dimensional irreducible representation has positive dimension. This is what makes the degree of an irreducible character positive, and, cast into the base field by Representation.IsIrreducible.natCast_finrank_ne_zero, what lets the orthogonality relations and the integrated operator divide by that degree.

theorem Representation.IsIrreducible.natCast_finrank_ne_zero {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [CharZero k] [FiniteDimensional k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) : ↑(Module.finrank k V) ≠ 0

The dimension of an irreducible representation is nonzero in the base field. In characteristic zero it is therefore invertible there: this is the scalar the orthogonality relations and the integrated operator of an irreducible representation are normalised by.

theorem Representation.IsIrreducible.finiteDimensional {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [Finite G] {ρ : Representation k G V} (h : ρ.IsIrreducible) : FiniteDimensional k V

An irreducible representation of a finite monoid is finite-dimensional. A simple module is cyclic -- it is generated by any one of its nonzero elements -- so ρ.asModule is a quotient of k[G], which is finite-dimensional over k when G is finite. No finiteness has to be assumed of V, which is what makes the hypothesis [FiniteDimensional k V] redundant on statements that already assume irreducibility over a finite monoid.

theorem Representation.isIrreducible_of_finrank_eq_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (h : Module.finrank k V = 1) : ρ.IsIrreducible

A representation on a one-dimensional vector space is irreducible.

instance Representation.isIrreducible_trivial_self {k : Type u_1} {G : Type u_2} [Field k] [Monoid G] : (trivial k G k).IsIrreducible

The trivial representation of a monoid on the base field is irreducible, being a line.

theorem Representation.isIrreducible_of_linearEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] {W : Type u_4} [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (e : V ≃ₗ[k] W) (he : ∀ (g : G) (v : V), e ((ρ g) v) = (σ g) (e v)) (h : ρ.IsIrreducible) : σ.IsIrreducible

Irreducibility transports along an equivariant linear equivalence. A linear equivalence intertwining two representations matches their lattices of subrepresentations, by taking preimages of invariant subspaces, so one is irreducible exactly when the other is.

Only one direction is stated; the reverse is this one applied to e.symm.

theorem Representation.isIrreducible_toRepresentation_of_isAtom {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {σ : Subrepresentation ρ} (h : IsAtom σ) : σ.toRepresentation.IsIrreducible

A subrepresentation that is an atom of the lattice of subrepresentations -- nonzero, with no subrepresentation strictly between it and zero -- carries an irreducible representation. The translation is the correspondence between the subrepresentations of σ.toRepresentation and the subrepresentations of ρ contained in σ, given by pushing forward along the inclusion.

theorem Representation.isIrreducible_of_asAlgebraHom_surjective {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [Nontrivial V] (ρ : Representation k G V) (h : Function.Surjective ⇑ρ.asAlgebraHom) : ρ.IsIrreducible

A representation whose algebra map exhausts the endomorphisms is irreducible. Every nonzero vector then generates, because a vector space is a simple module over its endomorphism ring.

theorem Representation.isIrreducible_of_finrank_intertwiningMap_self_eq_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} [ρ.IsSemisimpleRepresentation] (h : Module.finrank k (ρ.IntertwiningMap ρ) = 1) : ρ.IsIrreducible

A semisimple representation whose intertwiners are the scalars is irreducible. If every subrepresentation has an invariant complement and the equivariant endomorphisms of ρ form a line, then ρ is irreducible: an idempotent equivariant endomorphism is a scalar c with c * c = c, hence 0 or 1, so ρ is indecomposable (isIndecomposableModule_of_forall_isIdempotentElem), and an indecomposable semisimple module is simple (IsIndecomposableModule.isSimpleModule).

Over a field in which the order of a finite group is invertible every representation is semisimple (Maschke), so there this is the converse of Schur's lemma for an absolutely irreducible representation.

theorem Representation.asAlgebraHom_surjective_of_isIrreducible {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [IsAlgClosed k] [FiniteDimensional k V] (ρ : Representation k G V) (hρ : ρ.IsIrreducible) : Function.Surjective ⇑ρ.asAlgebraHom

Burnside density theorem. The monoid algebra of a finite-dimensional irreducible representation over an algebraically closed field exhausts the full endomorphism algebra.

Jacobson density gives all endomorphisms linear over the representation's commuting endomorphism ring. Schur's lemma identifies that ring with the base field, so these are exactly the k-linear endomorphisms.

theorem Representation.exists_ne_zero_forall_exists_rTensor_asAlgebraHom_eq_tmul {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [IsAlgClosed k] [FiniteDimensional k V] (ρ : Representation k G V) (hρ : ρ.IsIrreducible) {M : Type u_4} [AddCommGroup M] [Module k M] {z : TensorProduct k V M} (hz : z ≠ 0) : ∃ (m : M), m ≠ 0 ∧ ∀ (v : V), ∃ (r : MonoidAlgebra k G), (LinearMap.rTensor M (ρ.asAlgebraHom r)) z = v ⊗ₜ[k] m

Burnside density on a tensor product. Let ρ be a finite-dimensional irreducible representation over an algebraically closed field and M any vector space. Acting on the left factor of a nonzero z ∈ V ⊗ M by the monoid algebra reaches every pure tensor v ⊗ m with one fixed nonzero m: there is m ≠ 0 such that for each v some r ∈ k[G] has (ρ r ⊗ 1) z = v ⊗ m.

Atoms exist in finite dimensions

theorem Representation.exists_isAtom_le {k : Type u_4} {G : Type u_5} {V : Type u_6} [DivisionRing k] [Monoid G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {σ : Subrepresentation ρ} [FiniteDimensional k ↥σ.toSubmodule] (hσ : σ ≠ ⊥) : ∃ τ ≤ σ, IsAtom τ

Atoms exist. Every nonzero finite-dimensional subrepresentation contains an atom of the lattice of subrepresentations.

Finite-dimensionality is what makes a minimal nonzero subrepresentation exist, and only the subrepresentation being minimised inside has to be finite-dimensional: the ambient representation may be infinite-dimensional, the scalars need only be a division ring, and the acting monoid stays arbitrary. Over a field it combines with Representation.isIrreducible_toRepresentation_of_isAtom to exhibit an irreducible subrepresentation inside any nonzero one; that companion needs the field, because Representation.IsIrreducible is defined only there.

theorem Representation.exists_isAtom {k : Type u_4} {G : Type u_5} {V : Type u_6} [DivisionRing k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Nontrivial V] (ρ : Representation k G V) : ∃ (σ : Subrepresentation ρ), IsAtom σ

A nonzero finite-dimensional representation has a minimal nonzero subrepresentation. This is Representation.exists_isAtom_le applied to the whole space, which is nonzero exactly because V is; the scalars need only be a division ring and the acting monoid stays arbitrary.

theorem Representation.IsIrreducible.exists_forall_apply_eq_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [IsAlgClosed k] [FiniteDimensional k V] {ρ : Representation k G V} [ρ.IsIrreducible] (f : V →ₗ[k] V) (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (ρ g) (f v)) : ∃ (c : k), ∀ (v : V), f v = c • v

Schur's lemma, scalar form. Over an algebraically closed field, a linear endomorphism of a finite-dimensional irreducible representation commuting with the action is multiplication by a scalar. This is Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed read pointwise on an unbundled endomorphism.

theorem Representation.IsIrreducible.exists_unit_smul_of_intertwines {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [IsAlgClosed k] [FiniteDimensional k V] {W : Type u_4} [AddCommGroup W] [Module k W] {ρ : Representation k G V} [hρ : ρ.IsIrreducible] {σ : Representation k G W} (a b : V ≃ₗ[k] W) (ha : ∀ (g : G) (v : V), a ((ρ g) v) = (σ g) (a v)) (hb : ∀ (g : G) (v : V), b ((ρ g) v) = (σ g) (b v)) : ∃ (c : kˣ), ∀ (v : V), a v = ↑c • b v

Two equivariant isomorphisms out of an irreducible representation differ by a unit scalar. If a b : V ≃ₗ[k] W both carry the action ρ to the same σ, then b⁻¹ ∘ a is an equivariant automorphism of V, hence a nonzero scalar by Schur's lemma (Representation.IsIrreducible.exists_forall_apply_eq_smul).

theorem Representation.exists_isIrreducible_subrepresentation {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Nontrivial V] (ρ : Representation k G V) : ∃ (σ : Subrepresentation ρ), σ ≠ ⊥ ∧ σ.toRepresentation.IsIrreducible

Every nonzero finite-dimensional representation contains an irreducible subrepresentation. Finite-dimensionality alone suffices; no semisimplicity is assumed. This produces a single irreducible subrepresentation, not a decomposition: a representation that is not semisimple need not be the sum of its irreducible subrepresentations.