Library mathcomp.character.mxrepresentation

This file provides linkage between classic Group Theory and commutative algebra -- representation theory. Since general abstract linear algebra is still being sorted out, we develop the required theory here on the assumption that all vector spaces are matrix spaces, indeed that most are row matrix spaces; our representation theory is specialized to the latter case. We provide many definitions and results of representation theory: enveloping algebras, reducible, irreducible and absolutely irreducible representations, representation centralisers, submodules and kernels, simple and semisimple modules, the Schur lemmas, Maschke's theorem, components, socles, homomorphisms and isomorphisms, the Jacobson density theorem, similar representations, the Jordan-Holder theorem, Clifford's theorem and Wedderburn components, regular representations and the Wedderburn structure theorem for semisimple group rings, and the construction of a splitting field of an irreducible representation, and of reduced, tensored, and factored representations. mx_representation F G n == the Structure type for representations of G with n x n matrices with coefficients in F. Note that rG : mx_representation F G n coerces to a function from the element type of G to 'M_n, and conversely all such functions have a Canonical mx_representation. mx_repr G r <-> r : gT -> 'M_n defines a (matrix) group representation on G : {set gT} (Prop predicate). enveloping_algebra_mx rG == a #|G| x (n ^ 2) matrix whose rows are the mxvec encodings of the image of G under rG, and whose row space therefore encodes the enveloping algebra of the representation of G. rker rG == the kernel of the representation of r on G, i.e., the subgroup of elements of G mapped to the identity by rG. mx_faithful rG == the representation rG of G is faithful (its kernel is trivial). rfix_mx rG H == an n x n matrix whose row space is the set of vectors fixed (centralised) by the representation of H by rG. rcent rG A == the subgroup of G whose representation via rG commutes with the square matrix A. rcenter rG == the subgroup of G whose representation via rG consists of scalar matrices. mxcentg rG f <=> f commutes with every matrix in the representation of G (i.e., f is a total rG-homomorphism). rstab rG U == the subgroup of G whose representation via r fixes all vectors in U, pointwise. rstabs rG U == the subgroup of G whose representation via r fixes the row space of U globally. mxmodule rG U <=> the row-space of the matrix U is a module (globally invariant) under the representation rG of G. max_submod rG U V <-> U < V is not a proper is a proper subset of any proper rG-submodule of V (if both U and V are modules, then U is a maximal proper submodule of V). mx_subseries rG Us <=> Us : seq 'M_n is a list of rG-modules mx_composition_series rG Us <-> Us is an increasing composition series for an rG-module (namely, last 0 Us). mxsimple rG M <-> M is a simple rG-module (i.e., minimal and nontrivial) This is a Prop predicate on square matrices. mxnonsimple rG U <-> U is constructively not a submodule, that is, U contains a proper nontrivial submodule. mxnonsimple_sat rG U == U is not a simple as an rG-module. This is a bool predicate, which requires a decField structure on the scalar field. mxsemisimple rG W <-> W is constructively a direct sum of simple modules. mxsplits rG V U <-> V splits over U in rG, i.e., U has an rG-invariant complement in V. mx_completely_reducible rG V <-> V splits over all its submodules; note that this is only classically equivalent to stating that V is semisimple. mx_irreducible rG <-> the representation rG is irreducible, i.e., the full module 1%:M of rG is simple. mx_absolutely_irreducible rG == the representation rG of G is absolutely irreducible: its enveloping algebra is the full matrix ring. This is only classically equivalent to the more standard ``rG does not reduce in any field extension''. group_splitting_field F G <-> F is a splitting field for the group G: every irreducible representation of G is absolutely irreducible. Any field can be embedded classically into a splitting field. group_closure_field F gT <-> F is a splitting field for every group G : {group gT}, and indeed for any section of such a group. This is a convenient constructive substitute for algebraic closures, that can be constructed classically. dom_hom_mx rG f == a square matrix encoding the set of vectors for which multiplication by the n x n matrix f commutes with the representation of G, i.e., the largest domain on which f is an rG homomorphism. mx_iso rG U V <-> U and V are (constructively) rG-isomorphic; this is a Prop predicate. mx_simple_iso rG U V == U and V are rG-isomorphic if one of them is simple; this is a bool predicate. cyclic_mx rG u == the cyclic rG-module generated by the row vector u annihilator_mx rG u == the annihilator of the row vector u in the enveloping algebra the representation rG. row_hom_mx rG u == the image of u by the set of all rG-homomorphisms on its cyclic module, or, equivalently, the null-space of the annihilator of u. component_mx rG M == when M is a simple rG-module, the component of M in the representation rG, i.e. the module generated by all the (simple) modules rG-isomorphic to M. socleType rG == a Structure that represents the type of all components of rG (more precisely, it coerces to such a type via socle_sort). For sG : socleType, values of type sG (to be exact, socle_sort sG) coerce to square matrices. For any representation rG we can construct sG : socleType rG classically; the socleType structure encapsulates this use of classical logic. DecSocleType rG == a socleType rG structure, for a representation over a decidable field type. socle_base W == for W : (sG : socleType), a simple module whose component is W; socle_simple W and socle_module W are proofs that socle_base W is a simple module. socle_mult W == the multiplicity of socle_base W in W : sG. := \rank W %/ \rank (socle_base W) Socle sG == the Socle of rG, given sG : socleType rG, i.e., the (direct) sum of all the components of rG. mx_rsim rG rG' <-> rG and rG' are similar representations of the same group G. Note that rG and rG' must then have equal, but not necessarily convertible, degree. submod_repr modU == a representation of G on 'rV(\rank U) equivalent to the restriction of rG to U (here modU : mxmodule rG U). socle_repr W := submod_repr (socle_module W) val/in_submod rG U == the projections resp. from/onto 'rV(\rank U), that correspond to submod_repr r G U (these work both on vectors and row spaces). factmod_repr modV == a representation of G on 'rV(\rank (cokermx V)) that is equivalent to the factor module 'rV_n / V induced by V and rG (here modV : mxmodule rG V). val/in_factmod rG U == the projections for factmod_repr r G U. section_repr modU modV == the restriction to in_factmod V U of the factor representation factmod_repr modV (for modU : mxmodule rG U and modV : mxmodule rG V); section_repr modU modV is irreducible iff max_submod rG U V. subseries_repr modUs i == the representation for the section module in_factmod (0 :: Us)`i Us`i, where modUs : mx_subseries rG Us. series_repr compUs i == the representation for the section module in_factmod (0 :: Us)`i Us`i, where compUs : mx_composition_series rG Us. The Jordan-Holder theorem asserts the uniqueness of the set of such representations, up to similarity and permutation. regular_repr F G == the regular F-representation of the group G. group_ring F G == a #|G| x #|G|^2 matrix that encodes the free group ring of G -- that is, the enveloping algebra of the regular F-representation of G. gring_index x == the index corresponding to x \in G in the matrix encoding of regular_repr and group_ring. gring_row A == the row vector corresponding to A \in group_ring F G in the regular FG-module. gring_proj x A == the 1 x 1 matrix holding the coefficient of x \in G in (A \in group_ring F G)%MS. gring_mx rG u == the image of a row vector u of the regular FG-module, in the enveloping algebra of another representation rG. gring_op rG A == the image of a matrix of the free group ring of G, in the enveloping algebra of rG. gset_mx F G C == the group sum of C in the free group ring of G -- the sum of the images of all the x \in C in group_ring F G. classg_base F G == a #|classes G| x #|G|^2 matrix whose rows encode the group sums of the conjugacy classes of G -- this is a basis of 'Z(group_ring F G)%MS. irrType F G == a type indexing irreducible representations of G over a field F, provided its characteristic does not divide the order of G; it also indexes Wedderburn subrings. := socleType (regular_repr F G) irr_repr i == the irreducible representation corresponding to the index i : irrType sG := socle_repr i as i coerces to a component matrix. 'n_i, irr_degree i == the degree of irr_repr i; the notation is only active after Open Scope group_ring_scope. linear_irr sG == the set of sG-indices of linear irreducible representations of G. irr_comp sG rG == the sG-index of the unique irreducible representation similar to rG, at least when rG is irreducible and the characteristic is coprime. irr_mode i z == the unique eigenvalue of irr_repr i z, at least when irr_repr i z is scalar (e.g., when z \in 'Z(G)). [1 sG]%irr == the index of the principal representation of G, in sG : irrType F G. The i argument ot irr_repr, irr_degree and irr_mode is in the %irr scope. This notation may be replaced locally by an interpretation of 1%irr as [1 sG] for some specific irrType sG. 'R_i, Wedderburn_subring i == the subring (indeed, the component) of the free group ring of G corresponding to the component i : sG of the regular FG-module, where sG : irrType F g. In coprime characteristic the Wedderburn structure theorem asserts that the free group ring is the direct sum of these subrings; as with 'n_i above, the notation is only active in group_ring_scope. 'e_i, Wedderburn_id i == the projection of the identity matrix 1%:M on the Wedderburn subring of i : sG (with sG a socleType). In coprime characteristic this is the identity element of the subring, and the basis of its center if the field F is a splitting field. As 'R_i, 'e_i is in group_ring_scope. subg_repr rG sHG == the restriction to H of the representation rG of G; here sHG : H \subset G. eqg_repr rG eqHG == the representation rG of G viewed a a representation of H; here eqHG : G == H. morphpre_repr f rG == the representation of f @*^-1 G obtained by composing the group morphism f with rG. morphim_repr rGf sGD == the representation of G induced by a representation rGf of f @* G; here sGD : G \subset D where D is the domain of the group morphism f. rconj_repr rG uB == the conjugate representation x |-> B * rG x * B^-1; here uB : B \in unitmx. quo_repr sHK nHG == the representation of G / H induced by rG, given sHK : H \subset rker rG, and nHG : G \subset 'N(H). kquo_repr rG == the representation induced on G / rker rG by rG. map_repr f rG == the representation f \o rG, whose module is the tensor product of the module of rG with the extension field into which f : {rmorphism F -> Fstar} embeds F. 'Cl%act == the transitive action of G on the Wedderburn components of H, with nsGH : H <| G, given by Clifford's theorem. More precisely this is a total action of G on socle_sort sH, where sH : socleType (subg_repr rG (normal_sub sGH)). More involved constructions are encapsulated in two Coq submodules: MatrixGenField == a module that encapsulates the lengthy details of the construction of appropriate extension fields. We assume we have an irreducible representation r of a group G, and a non-scalar matrix A that centralises an r(G), as this data is readily extracted from the Jacobson density theorem. It then follows from Schur's lemma that the ring generated by A is a field on which the extension of the representation r of G is reducible. Note that this is equivalent to the more traditional quotient of the polynomial ring by an irreducible polynomial (the minimal polynomial of A), but much better suited to our needs. Here are the main definitions of MatrixGenField; they all have three proofs as arguments: rG : mx_repr r G, irrG : mx_irreducible rG, and cGA : mxcentg rG A, which ensure the validity of the construction and allow us to define Canonical instances (the ~~ is_scalar_mx A assumption is only needed to prove reducibility). + gen_of irrG cGA == the carrier type of the field generated by A. It is at least equipped with a fieldType structure; we also propagate any decFieldType/finFieldType structures on the original field. + gen irrG cGA == the morphism injecting into gen_of rG irrG cGA. + groot irrG cGA == the root of mxminpoly A in the gen_of field. + gen_repr irrG cGA == an alternative to the field extension representation, which consists in reconsidering the original module as a module over the new gen_of field, thereby DIVIDING the original dimension n by the degree of the minimal polynomial of A. This can be simpler than the extension method, and is actually required by the proof that odd groups are p-stable (B & G 6.1-2, and Appendix A) but is only applicable if G is the LARGEST group represented by rG (e.g., NOT for B & G 2.6). + val_gen/in_gen rG irrG cGA : the bijections from/to the module corresponding to gen_repr. + rowval_gen rG irrG cGA : the projection of row spaces in the module corresponding to gen_repr to row spaces in 'rV_n. We build on the MatrixFormula toolkit to define decision procedures for the reducibility property: + mxmodule_form rG U == a formula asserting that the interpretation of U is a module of the representation rG of G via r. + mxnonsimple_form rG U == a formula asserting that the interpretation of U contains a proper nontrivial rG-module.