Theorem. the single orbit in Clifford restriction [fgap-001P]
✍️source
isSemisimpleRepresentation_comp_subtype exists_isAtom_forall_nonempty_linearEquiv_conjSubrep
L∃∀N

Let \(N\trianglelefteq G\) be finite, and work over a field for which the relevant finite-group modules are semisimple. If \(V\) is an irreducible \(G\)-representation, then the irreducible constituents of \(V|_N\) lie in 1 \(G\)-orbit under conjugation. Equivalently, after choosing 1 constituent \(W\), every other constituent is isomorphic to some \(,{}^gW\).

This is the orbit assertion in Clifford theory. It does not by itself say that all constituents occur with the same multiplicity, nor does it construct extensions across the inertia subgroup. Compare [lux2010representations, thm. 3.6.2(a), pp. 223--225].

Theorem. the single orbit in Clifford restriction [fgap-001P]
✍️source
isSemisimpleRepresentation_comp_subtype exists_isAtom_forall_nonempty_linearEquiv_conjSubrep
L∃∀N

Reference. Representations of groups: A computational approach [lux2010representations]

The human-curated Group-Algebra route [fgap-001G]
📄PDF

Definition. the Group Algebra and its universal extension [fgap-001H]

MonoidAlgebra.lift MonoidAlgebra.lift_single
L∃∀N

Theorem. representations are Group-Algebra modules [fgap-001I]

Representation.asModule Representation.ofModule Rep.equivalenceModuleMonoidAlgebra
L∃∀N

Proof.

Example. the regular representation reads the basis [fgap-001J]

Theorem. Maschke averaging [fgap-001K]

MonoidAlgebra.Submodule.exists_isCompl
L∃∀N

Proof.

Theorem. Wedderburn blocks over an algebraically closed field [fgap-001L]

exists_algEquiv_pi_matrix_conjClasses
L∃∀N

Definition. characters, class functions, and the character table [fgap-001M]

basisOfIrreducibleCharacters characterTable card_inv_mul_sum_characterTable_mul_characterTable_inv card_conjClass_mul_sum_characterTable_mul_characterTable_inv
L∃∀N

Theorem. primitive central idempotents as block projectors [fgap-001N]

primitiveCentralIdempotent asAlgebraHom_primitiveCentralIdempotent primitiveCentralIdempotent_mul_primitiveCentralIdempotent
L∃∀N

Theorem. the Frobenius--Schur trichotomy [fgap-0021]

frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one frobeniusSchurIndicator_eq_one_iff frobeniusSchurIndicator_eq_neg_one_iff frobeniusSchurIndicator_eq_zero_iff
L∃∀N

Remark. real types are not Schur indices [fgap-001Y]

Definition. conjugate constituents and the inertia subgroup [fgap-001O]

Theorem. the single orbit in Clifford restriction [fgap-001P]
✍️source
isSemisimpleRepresentation_comp_subtype exists_isAtom_forall_nonempty_linearEquiv_conjSubrep
L∃∀N

Theorem. Clifford homogeneity and the semidirect route [fgap-001Q]

Example. semidirect products make Clifford theory concrete [fgap-0020]

Remark. from a presentation to checked representation data [fgap-001R]

Definition. factor sets and twisted Group Algebras [fgap-001S]

of_mul_of lift isProjectiveRepEquivAlgHom
L∃∀N

Remark. the qualified Clifford bridge [fgap-001Z]

Remark. the inertia obstruction is projective [fgap-001T]

proposition. the canonical grading of a Group Algebra [fgap-001U]

AddMonoidAlgebra.grade.isInternal AddMonoidAlgebra.grade.gradedAlgebra AddMonoidAlgebra.single_mem_grade
L∃∀N

proposition. the standard Hopf structure on a Group Algebra [fgap-001V]

MonoidAlgebra.instHopfAlgebra MonoidAlgebra.counit_single MonoidAlgebra.comul_single MonoidAlgebra.antipode_single
L∃∀N

Proof.

Remark. what the real quaternion example settles [fgap-001W]

Remark. the Hessian-group outlook [fgap-001X]

Theorem. Clifford homogeneity and the semidirect route [fgap-001Q]

Example. semidirect products make Clifford theory concrete [fgap-0020]

Remark. the qualified Clifford bridge [fgap-001Z]