Theorems · Theorem · group theory

FDRep.simple_iff_end_is_rank_one

∀ {k : Type u} [inst : Field k] {G : Type u} [Finite G] [inst_2 : Group G] [IsAlgClosed k] [NeZero ↑(Nat.card G)]
  (V : FDRep k G), CategoryTheory.Simple V ↔ Module.finrank k (V ⟶ V) = 1

If G is finite and its order is nonzero in an algebraically closed field k, then an object of FDRep k G is simple if and only if its space of endomorphisms is a k-vector space of dimension 1.

Defined in

Mathlib.RepresentationTheory.FinGroupCharZero

Cited by

1 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFiniteGroupIsAlgClosedNeZero