Linear representations

AbbreviationIrreducible representation#

A representation ρ is irreducible if it is non-trivial and has no proper non-trivial subrepresentations.

Representation.IsIrreducible.{u_1, u_2, u_3} {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G]
  [Field k] [AddCommGroup V] [_root_.Module k V] (ρ : Representation k G V) : Prop

Sources

• Mathlib documentation: Representation.IsIrreducible
• Source of Representation.IsIrreducible in Mathlib/RepresentationTheory/Irreducible.lean
• Mathlib undergraduate list: Linear algebra › Linear representations

MathlibRepresentation.IsIrreducible

Uses 2 · Used by 1

Statement usesRational number · Representation

Used byOrthogonality of characters

TheoremSchur's lemma (Linear representations)#

Schur's Lemma: the dimension of the Hom-space between two irreducible representation is 0 if they are not isomorphic, and 1 if they are.

FDRep.finrank_hom_simple_simple.{u, v} {k : Type u} {G : Type v} [Field k] [Monoid G]
  [IsAlgClosed k] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W] :
  Module.finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0

Sources

• Mathlib documentation: FDRep.finrank_hom_simple_simple
• Source of FDRep.finrank_hom_simple_simple in Mathlib/RepresentationTheory/FDRep.lean
• Mathlib undergraduate list: Linear algebra › Linear representations

MathlibFDRep.finrank_hom_simple_simple

Uses 10 · Used by 1

Statement usesAlgebraically closed field · Cardinal · Category of finite-dimensional representations · Isomorphism · Linear independence · The category of modules over a ring

Proof usesNoetherian module · Noetherian ring · Schur's lemma (1000+ theorems) · Sum of subspaces

Used byOrthogonality of characters

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.