A converse to Schur's lemma when subobjects split

In a preadditive category with kernels in which every object is injective, an object is simple exactly when its endomorphism ring is nontrivial and every nonzero endomorphism is a unit. This criterion retains division endomorphism rings larger than the coefficient field, as occur for representations over nonsplitting fields.

The sufficiency (CategoryTheory.simple_of_nontrivial_end_of_isUnit) needs no kernels, nor do its consequences below. The nontriviality condition excludes zero objects. Splitting is essential for the converse: an arbitrary object with a division endomorphism ring need not be simple. CategoryTheory.simple_of_ringEquiv_end transports this criterion along a ring isomorphism from a division ring. In a k-linear category in which every object is injective, a one-dimensional endomorphism space suffices for simplicity over any field k (CategoryTheory.simple_of_finrank_end_eq_one); algebraic closure is not needed.

Finite-dimensional representations

After importing Mathlib.RepresentationTheory.FinGroupCharZero, apply CategoryTheory.simple_iff_nontrivial_end_and_isUnit V directly to V : FDRep k G, where k is a field, G is a finite group, and [NeZero (Nat.card G : k)]. Mathlib's Maschke instance supplies injectivity of every such representation. In particular, taking V := TauCeti.indFDRep A gives the endomorphism-division criterion for induction over arbitrary fields whose characteristic does not divide the group order; neither characteristic zero nor algebraic closure is needed.

References

• J.-P. Serre, Linear Representations of Finite Groups, §2.2, Schur's lemma.
• Mathlib's CategoryTheory.isIso_of_hom_simple supplies the forward implication. The converse uses the retraction argument of FDRep.simple_iff_end_is_rank_one, replacing its scalar-endomorphism hypothesis by invertibility of nonzero endomorphisms.
• Module.nonempty_algEquiv_iff_finrank_eq_one identifies a one-dimensional endomorphism algebra with the coefficient field.

theorem CategoryTheory.simple_of_nontrivial_end_of_isUnit {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [∀ (Y : C), Injective Y] (X : C) [Nontrivial (End X)] (hunit : ∀ (f : End X), f ≠ 0 → IsUnit f) : Simple X

If every object is injective, an object whose endomorphism ring is nontrivial and in which every nonzero element is a unit is simple.

theorem CategoryTheory.simple_iff_nontrivial_end_and_isUnit {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasKernels C] [∀ (Y : C), Injective Y] (X : C) : Simple X ↔ Nontrivial (End X) ∧ ∀ (f : End X), f ≠ 0 → IsUnit f

If every object is injective, simplicity is equivalent to having a nontrivial endomorphism ring in which every nonzero element is a unit.

theorem CategoryTheory.simple_of_ringEquiv_end {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [∀ (Y : C), Injective Y] (X : C) {D : Type u_2} [DivisionRing D] (e : D ≃+* End X) : Simple X

If every object is injective, an object whose endomorphism ring is isomorphic to a division ring is simple.

theorem CategoryTheory.simple_of_finrank_end_eq_one {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (k : Type u_2) [Field k] [Linear k C] [∀ (Y : C), Injective Y] (X : C) (h : Module.finrank k (X ⟶ X) = 1) : Simple X

If every object is injective, a one-dimensional endomorphism space forces simplicity over any field. The converse requires a scalar-Schur hypothesis.