Simple objects of Rep k G and FDRep k G, and their isomorphism classes

Two notions of "irreducible representation" coexist. Representation.IsIrreducible ρ says that the lattice of subrepresentations of ρ has exactly two elements, and it is the notion in which the representation-theoretic arguments of this repository are phrased. CategoryTheory.Simple X says that X is nonzero and every monomorphism f into X satisfies IsIso f ↔ f ≠ 0; it is the notion in which the categorical machinery is phrased -- Schur's lemma FDRep.finrank_hom_simple_simple, the characters of simple objects, semisimple categories. This file supplies the dictionary between them.

Over Rep k G the dictionary is bookkeeping. Rep k G is equivalent to the category of k[G]-modules (Rep.equivalenceModuleMonoidAlgebra), an equivalence transports simplicity in both directions, and a module is a simple object exactly when it is a simple module (simple_iff_isSimpleModule).

Mathlib does not identify FDRep k G with a module category, so it needs an argument in each direction. One is formal: the forgetful functor to Rep k G is faithful, preserves zero morphisms and monomorphisms, and reflects isomorphisms, and such a functor reflects simplicity (CategoryTheory.Functor.simple_of_simple_obj). The other uses finite-dimensionality, and is where the restriction to FDRep earns its keep: a subrepresentation of a finite-dimensional representation is again finite-dimensional, so it is again an object of FDRep k G, and its inclusion is a monomorphism which is nonzero exactly when the subrepresentation is nonzero and an isomorphism exactly when the subrepresentation is everything. Simplicity of the object therefore says precisely that the lattice of subrepresentations is {⊥, ⊤} with ⊥ ≠ ⊤.

The irreducible-to-simple directions are registered as instances. The converse directions are the theorems Rep.isIrreducible_of_simple and FDRep.isIrreducible_of_simple; they are deliberately not instances, since with the forward directions they would close a cycle in the instance graph. One consequence of the converse directions not being instances is that inference cannot get from Simple X to the simplicity of the k[G]-module X.ρ.asModule, even though Mathlib registers that module as simple whenever X.ρ is irreducible. The single composite FDRep.isSimpleModule_asModule_of_simple is therefore registered as an instance as well, so that Simple X alone suffices for the module-level API.

A classification statement is valued in a type of isomorphism classes, and for simple objects of FDRep k G that type needs no device: unlike abstract simple modules, which range over every universe, the objects of FDRep k G already form a type, and Mathlib already quotients the objects of a category by isomorphism. TauCeti.SimpleFDRepClasses is that quotient, namely CategoryTheory.Skeleton of the full subcategory of simple objects, together with the constructor, eliminator and lift a consumer needs. It lives here rather than beside its comparison with the module-level quotient (TauCeti.SimpleFDRepClasses.toSimpleSubmoduleClasses, in TauCeti.RepresentationTheory.Simple.FDRepClasses) so that naming the isomorphism classes does not drag in the semisimple isotypic-component theory that only the comparison needs.

Main results

• Rep.simple_iff_isIrreducible: an object of Rep k G is simple exactly when the representation it carries is irreducible.
• Rep.simple_of_isIrreducible and Rep.isIrreducible_of_simple: the two directions as an instance and a theorem, respectively.
• FDRep.simple_iff_isIrreducible: the same for FDRep k G.
• FDRep.simple_of_isIrreducible and FDRep.isIrreducible_of_simple: the corresponding instance and theorem for FDRep.
• FDRep.isSimpleModule_asModule_of_simple: the instance making Mathlib's simple-module API on X.ρ.asModule available from Simple X alone.
• TauCeti.SimpleFDRepClasses: the isomorphism classes of simple objects of FDRep k G.
• TauCeti.SimpleFDRepClasses.mk_eq_mk_iff: two simple objects have the same class exactly when they are isomorphic in FDRep k G.
• TauCeti.SimpleFDRepClasses.ind and TauCeti.SimpleFDRepClasses.lift: the eliminator and the lift of an isomorphism-invariant function.

theorem Rep.simple_iff_isIrreducible {k : Type u} {G : Type v} [Field k] [Monoid G] (A : Rep k G) : CategoryTheory.Simple A ↔ A.ρ.IsIrreducible

An object of Rep k G is simple exactly when the representation it carries is irreducible.

instance Rep.simple_of_isIrreducible {k : Type u} {G : Type v} [Field k] [Monoid G] (A : Rep k G) [A.ρ.IsIrreducible] : CategoryTheory.Simple A

An irreducible representation is a simple object of Rep k G.

theorem Rep.isIrreducible_of_simple {k : Type u} {G : Type v} [Field k] [Monoid G] (A : Rep k G) [CategoryTheory.Simple A] : A.ρ.IsIrreducible

A simple object of Rep k G carries an irreducible representation.

theorem FDRep.simple_iff_isIrreducible {k : Type u} {G : Type v} [Field k] [Monoid G] (X : FDRep k G) : CategoryTheory.Simple X ↔ Representation.IsIrreducible X.ρ

An object of FDRep k G is simple exactly when the representation it carries is irreducible.

instance FDRep.simple_of_isIrreducible {k : Type u} {G : Type v} [Field k] [Monoid G] (X : FDRep k G) [Representation.IsIrreducible X.ρ] : CategoryTheory.Simple X

An irreducible finite-dimensional representation is a simple object of FDRep k G.

theorem FDRep.isIrreducible_of_simple {k : Type u} {G : Type v} [Field k] [Monoid G] (X : FDRep k G) [CategoryTheory.Simple X] : Representation.IsIrreducible X.ρ

A simple object of FDRep k G carries an irreducible representation.

instance FDRep.isSimpleModule_asModule_of_simple {k : Type u} {G : Type v} [Field k] [Monoid G] (X : FDRep k G) [CategoryTheory.Simple X] : IsSimpleModule (MonoidAlgebra k G) (Representation.asModule X.ρ)

The module carried by a simple object of FDRep k G is a simple module over the group algebra. Registered so that Mathlib's simple-module API on X.ρ.asModule is available from Simple X alone, since FDRep.isIrreducible_of_simple is deliberately not an instance.

def TauCeti.SimpleFDRepClasses (k : Type u) (G : Type v) [Ring k] [Monoid G] : Type (max (u + 1) v)

The isomorphism classes of simple objects of FDRep k G: the skeleton of the full subcategory they span.

Equations

• TauCeti.SimpleFDRepClasses k G = CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Simple)

def TauCeti.SimpleFDRepClasses.mk {k : Type u} {G : Type v} [Ring k] [Monoid G] (X : FDRep k G) [CategoryTheory.Simple X] : SimpleFDRepClasses k G

The isomorphism class of a simple object of FDRep k G.

Equations

• TauCeti.SimpleFDRepClasses.mk X = CategoryTheory.toSkeleton { obj := X, property := ⋯ }

@[simp]

theorem TauCeti.SimpleFDRepClasses.mk_eq_mk_iff {k : Type u} {G : Type v} [Ring k] [Monoid G] (X Y : FDRep k G) [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : mk X = mk Y ↔ Nonempty (X ≅ Y)

Two simple objects have the same class exactly when they are isomorphic.

theorem TauCeti.SimpleFDRepClasses.ind {k : Type u} {G : Type v} [Ring k] [Monoid G] {motive : SimpleFDRepClasses k G → Prop} (h : ∀ (X : FDRep k G) (hX : CategoryTheory.Simple X), motive (mk X)) (c : SimpleFDRepClasses k G) : motive c

To prove a property of every simple-object class, it suffices to prove it on the class of each simple object.

noncomputable def TauCeti.SimpleFDRepClasses.lift {k : Type u} {G : Type v} [Ring k] [Monoid G] {α : Sort u_1} (f : (X : FDRep k G) → [CategoryTheory.Simple X] → α) (h : ∀ (X Y : FDRep k G) [inst : CategoryTheory.Simple X] [inst_1 : CategoryTheory.Simple Y], Nonempty (X ≅ Y) → f X = f Y) : SimpleFDRepClasses k G → α

Define a function on simple-object classes from an isomorphism-invariant function on simple objects.

Equations

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

@[simp]

theorem TauCeti.SimpleFDRepClasses.lift_mk {k : Type u} {G : Type v} [Ring k] [Monoid G] {α : Sort u_1} {f : (X : FDRep k G) → [CategoryTheory.Simple X] → α} {h : ∀ (X Y : FDRep k G) [inst : CategoryTheory.Simple X] [inst_1 : CategoryTheory.Simple Y], Nonempty (X ≅ Y) → f X = f Y} (X : FDRep k G) [CategoryTheory.Simple X] : lift f h (mk X) = f X

The lift of an isomorphism-invariant function, evaluated at the class of a simple object.