Email Gateway (Aug 22 2022 at 11:08): Email Gateway (Aug 22 2022 at 11:08):From: Larry Paulson <lp15@cam.ac.uk>
Representations of Finite Groups
Jeremy Sylvestre
"We provide a formal framework for the theory of representations of finite groups, as modules over the group ring. Along the way, we develop the general theory of groups (relying on the group_add class for the basics), modules, and vector spaces, to the extent required for theory of group representations. We then provide formal proofs of several important introductory theorems in the subject, including Maschke's theorem, Schur's lemma, and Frobenius reciprocity. We also prove that every irreducible representation is isomorphic to a submodule of the group ring, leading to the fact that for a finite group there are only finitely many isomorphism classes of irreducible representations. In all of this, no restriction is made on the characteristic of the ring or field of scalars until the definition of a group representation, and then the only restriction made is that the characteristic must not divide the order of the group."
http://afp.sourceforge.net/entries/Rep_Fin_Groups.shtml
This would appear to be a new approach to formalise in group theory, using the additive group type class for syntax, while retaining a locale to express the closure of the carrier set. And some substantial results seem to be proved. It’s always a pleasure to see such contributions!
Larry Paulson
Last updated: Apr 20 2024 at 12:26 UTC