Reseña: Representations of finite groups

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra titulado Representations of finite groups.

Su autor es Jeremy Sylvestre (de la Univ. de Alberta en Canadá).

Su resumen es

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.

El trabajo se ha publicado el 12 de agosto en AFP (The Archive of Formal Proofs).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.