Library mathcomp.character.mxrepresentation

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg poly polydiv finset fingroup morphism.
From mathcomp Require Import perm automorphism quotient finalg action zmodp.
From mathcomp Require Import commutator cyclic center pgroup matrix mxalgebra.
From mathcomp Require Import mxpoly.

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. centgmx 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 and U is not a proper 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. DecSocleType rG is opaque. 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 of 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)). 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. mxnonsimple_form rG U == a formula asserting that the interpretation of U contains a proper nontrivial rG-module. mxnonsimple_sat rG U <=> mxnonsimple_form rG U is satisfied. 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 rG of a group G, and a non-scalar matrix A that centralises rG(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 rG 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: (implicit) rG : mx_repr n G, irrG : mx_irreducible rG and cGA : centgmx rG A. These ensure the validity of the construction and allow us to define Canonical instances; we assume degree_mxminpoly A > 1 (which is equivalent to ~~ is_scalar_mx A) only 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 irrG cGA. + groot irrG cGA == the root of mxminpoly A in the gen_of irrG cGA field. + pval x, rVval x, mxval x == the interpretation of x : gen_of irrG cGA as a polynomial, a row vector, and a matrix, respectively. Both irrG and cGA are implicit arguments here. + 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, 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). + gen_dim A == the dimension of gen_repr irrG cGA (only depends on A). + in_gen irrG cGA W == the ROWWISE image of a matrix W : 'M[F]_(m, n), i.e., interpreting W as a sequence of m tow vectors, under the bijection from rG to gen_repr irrG cGA. The sequence length m is a maximal implicit argument passed between the explicit argument cGA and W. + val_gen W == the ROWWISE image of an 'M[gen_of irrG cGA]_(m, gen_dim A) matrix W under the bijection from gen_repr irrG cGA to rG. + rowval_gen W == the ROWSPACE image of W under the bijection from gen_repr irrG cGA to rG, i.e., a 'M[F]_n matrix whose row space is the image of the row space of W. This is the A-ideal generated by val_gen W. + gen_sat e f <=> f : GRing.formula (gen_of irrG cGA) is satisfied in environment e : seq (gen_of irrG cGA), provided F has a decFieldType structure. + gen_env e, gen_term t, gen_form f == interpretations of environments, terms, and RING formulas over gen_of irrG cGA as row vector formulae, used to construct gen_sat.

Set Implicit Arguments.

Declare Scope irrType_scope.
Declare Scope group_ring_scope.

Import GroupScope GRing.Theory.
Local Open Scope ring_scope.

Reserved Notation "''n_' i" (at level 8, i at level 2, format "''n_' i").
Reserved Notation "''R_' i" (at level 8, i at level 2, format "''R_' i").
Reserved Notation "''e_' i" (at level 8, i at level 2, format "''e_' i").

Delimit Scope irrType_scope with irr.

Section RingRepr.

Variable R : comUnitRingType.

Section OneRepresentation.

Variable gT : finGroupType.

Definition mx_repr (G : {set gT}) n (r : gT 'M[R]_n) :=
  r 1%g = 1%:M {in G &, {morph r : x y / (x × y)%g >-> x ×m y}}.

Structure mx_representation G n :=
  MxRepresentation { repr_mx :> gT 'M_n; _ : mx_repr G repr_mx }.

Variables (G : {group gT}) (n : nat) (rG : mx_representation G n).
Arguments rG _%group_scope : extra scopes.

Lemma repr_mx1 : rG 1 = 1%:M.

Lemma repr_mxM : {in G &, {morph rG : x y / (x × y)%g >-> x ×m y}}.

Lemma repr_mxK m x :
  x \in G cancel ((@mulmx R m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).

Lemma repr_mxKV m x :
  x \in G cancel ((@mulmx R m n n)^~ (rG x^-1)) (mulmx^~ (rG x)).

Lemma repr_mx_unit x : x \in G rG x \in unitmx.

Lemma repr_mxV : {in G, {morph rG : x / x^-1%g >-> invmx x}}.

This is only used in the group ring construction below, as we only have developped the theory of matrix subalgebras for F-algebras.
Definition enveloping_algebra_mx := \matrix_(i < #|G|) mxvec (rG (enum_val i)).

Section Stabiliser.

Variables (m : nat) (U : 'M[R]_(m, n)).

Definition rstab := [set x in G | U ×m rG x == U].

Lemma rstab_sub : rstab \subset G.

Lemma rstab_group_set : group_set rstab.

Canonical rstab_group := Group rstab_group_set.

End Stabiliser.

Centralizer subgroup and central homomorphisms.
Section CentHom.

Variable f : 'M[R]_n.

Definition rcent := [set x in G | f ×m rG x == rG x ×m f].

Lemma rcent_sub : rcent \subset G.

Lemma rcent_group_set : group_set rcent.
Canonical rcent_group := Group rcent_group_set.

Definition centgmx := G \subset rcent.

Lemma centgmxP : reflect ( x, x \in G f ×m rG x = rG x ×m f) centgmx.

End CentHom.

Representation kernel, and faithful representations.

Definition rker := rstab 1%:M.
Canonical rker_group := Eval hnf in [group of rker].

Lemma rkerP x : reflect (x \in G rG x = 1%:M) (x \in rker).

Lemma rker_norm : G \subset 'N(rker).

Lemma rker_normal : rker <| G.

Definition mx_faithful := rker \subset [1].

Lemma mx_faithful_inj : mx_faithful {in G &, injective rG}.

Lemma rker_linear : n = 1 G^`(1)%g \subset rker.

Representation center.

Definition rcenter := [set g in G | is_scalar_mx (rG g)].

Fact rcenter_group_set : group_set rcenter.
Canonical rcenter_group := Group rcenter_group_set.

Lemma rcenter_normal : rcenter <| G.

End OneRepresentation.

Arguments rkerP {gT G n rG x}.

Section Proper.

Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variable rG : mx_representation G n.

Lemma repr_mxMr : {in G &, {morph rG : x y / (x × y)%g >-> x × y}}.

Lemma repr_mxVr : {in G, {morph rG : x / (x^-1)%g >-> x^-1}}.

Lemma repr_mx_unitr x : x \in G rG x \is a GRing.unit.

Lemma repr_mxX m : {in G, {morph rG : x / (x ^+ m)%g >-> x ^+ m}}.

End Proper.

Section ChangeGroup.

Variables (gT : finGroupType) (G H : {group gT}) (n : nat).
Variables (rG : mx_representation G n).

Section SubGroup.

Hypothesis sHG : H \subset G.

Lemma subg_mx_repr : mx_repr H rG.
Definition subg_repr := MxRepresentation subg_mx_repr.
Local Notation rH := subg_repr.

Lemma rcent_subg U : rcent rH U = H :&: rcent rG U.

Section Stabiliser.

Variables (m : nat) (U : 'M[R]_(m, n)).

Lemma rstab_subg : rstab rH U = H :&: rstab rG U.

End Stabiliser.

Lemma rker_subg : rker rH = H :&: rker rG.

Lemma subg_mx_faithful : mx_faithful rG mx_faithful rH.

End SubGroup.

Section SameGroup.

Hypothesis eqGH : G :==: H.

Lemma eqg_repr_proof : H \subset G.

Definition eqg_repr := subg_repr eqg_repr_proof.
Local Notation rH := eqg_repr.

Lemma rcent_eqg U : rcent rH U = rcent rG U.

Section Stabiliser.

Variables (m : nat) (U : 'M[R]_(m, n)).

Lemma rstab_eqg : rstab rH U = rstab rG U.

End Stabiliser.

Lemma rker_eqg : rker rH = rker rG.

Lemma eqg_mx_faithful : mx_faithful rH = mx_faithful rG.

End SameGroup.

End ChangeGroup.

Section Morphpre.

Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Variables (G : {group rT}) (n : nat) (rG : mx_representation G n).

Lemma morphpre_mx_repr : mx_repr (f @*^-1 G) (rG \o f).
Canonical morphpre_repr := MxRepresentation morphpre_mx_repr.
Local Notation rGf := morphpre_repr.

Section Stabiliser.

Variables (m : nat) (U : 'M[R]_(m, n)).

Lemma rstab_morphpre : rstab rGf U = f @*^-1 (rstab rG U).

End Stabiliser.

Lemma rker_morphpre : rker rGf = f @*^-1 (rker rG).

End Morphpre.

Section Morphim.

Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
Variables (n : nat) (rGf : mx_representation (f @* G) n).

Definition morphim_mx of G \subset D := fun xrGf (f x).

Hypothesis sGD : G \subset D.

Lemma morphim_mxE x : morphim_mx sGD x = rGf (f x).

Let sG_f'fG : G \subset f @*^-1 (f @* G).

Lemma morphim_mx_repr : mx_repr G (morphim_mx sGD).
Canonical morphim_repr := MxRepresentation morphim_mx_repr.
Local Notation rG := morphim_repr.

Section Stabiliser.
Variables (m : nat) (U : 'M[R]_(m, n)).

Lemma rstab_morphim : rstab rG U = G :&: f @*^-1 rstab rGf U.

End Stabiliser.

Lemma rker_morphim : rker rG = G :&: f @*^-1 (rker rGf).

End Morphim.

Section Conjugate.

Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation G n) (B : 'M[R]_n).

Definition rconj_mx of B \in unitmx := fun xB ×m rG x ×m invmx B.

Hypothesis uB : B \in unitmx.

Lemma rconj_mx_repr : mx_repr G (rconj_mx uB).
Canonical rconj_repr := MxRepresentation rconj_mx_repr.
Local Notation rGB := rconj_repr.

Lemma rconj_mxE x : rGB x = B ×m rG x ×m invmx B.

Lemma rconj_mxJ m (W : 'M_(m, n)) x : W ×m rGB x ×m B = W ×m B ×m rG x.

Lemma rcent_conj A : rcent rGB A = rcent rG (invmx B ×m A ×m B).

Lemma rstab_conj m (U : 'M_(m, n)) : rstab rGB U = rstab rG (U ×m B).

Lemma rker_conj : rker rGB = rker rG.

Lemma conj_mx_faithful : mx_faithful rGB = mx_faithful rG.

End Conjugate.

Section Quotient.

Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variable rG : mx_representation G n.

Definition quo_mx (H : {set gT}) of H \subset rker rG & G \subset 'N(H) :=
  fun Hx : coset_of HrG (repr Hx).

Section SubQuotient.

Variable H : {group gT}.
Hypotheses (krH : H \subset rker rG) (nHG : G \subset 'N(H)).
Let nHGs := subsetP nHG.

Lemma quo_mx_coset x : x \in G quo_mx krH nHG (coset H x) = rG x.

Lemma quo_mx_repr : mx_repr (G / H)%g (quo_mx krH nHG).
Canonical quo_repr := MxRepresentation quo_mx_repr.
Local Notation rGH := quo_repr.

Lemma quo_repr_coset x : x \in G rGH (coset H x) = rG x.

Lemma rcent_quo A : rcent rGH A = (rcent rG A / H)%g.

Lemma rstab_quo m (U : 'M_(m, n)) : rstab rGH U = (rstab rG U / H)%g.

Lemma rker_quo : rker rGH = (rker rG / H)%g.

End SubQuotient.

Definition kquo_mx := quo_mx (subxx (rker rG)) (rker_norm rG).
Lemma kquo_mxE : kquo_mx = quo_mx (subxx (rker rG)) (rker_norm rG).

Canonical kquo_repr := @MxRepresentation _ _ _ kquo_mx (quo_mx_repr _ _).

Lemma kquo_repr_coset x :
  x \in G kquo_repr (coset (rker rG) x) = rG x.

Lemma kquo_mx_faithful : mx_faithful kquo_repr.

End Quotient.

Section Regular.

Variables (gT : finGroupType) (G : {group gT}).
Definition gcard := #|G|. (* hides the projections to set *)
Local Notation nG := gcard.

Definition gring_index (x : gT) := enum_rank_in (group1 G) x.

Lemma gring_valK : cancel enum_val gring_index.

Lemma gring_indexK : {in G, cancel gring_index enum_val}.

Definition regular_mx x : 'M[R]_nG :=
  \matrix_i delta_mx 0 (gring_index (enum_val i × x)).

Lemma regular_mx_repr : mx_repr G regular_mx.
Canonical regular_repr := MxRepresentation regular_mx_repr.
Local Notation aG := regular_repr.

Definition group_ring := enveloping_algebra_mx aG.
Local Notation R_G := group_ring.

Definition gring_row : 'M[R]_nG 'rV_nG := row (gring_index 1).

Lemma gring_row_mul A B : gring_row (A ×m B) = gring_row A ×m B.

Definition gring_proj x := row (gring_index x) \o trmx \o gring_row.

Lemma gring_projE : {in G &, x y, gring_proj x (aG y) = (x == y)%:R}.

Lemma regular_mx_faithful : mx_faithful aG.

Section GringMx.

Variables (n : nat) (rG : mx_representation G n).

Definition gring_mx := vec_mx \o mulmxr (enveloping_algebra_mx rG).

Lemma gring_mxJ a x :
  x \in G gring_mx (a ×m aG x) = gring_mx a ×m rG x.

End GringMx.

Lemma gring_mxK : cancel (gring_mx aG) gring_row.

Section GringOp.

Variables (n : nat) (rG : mx_representation G n).

Definition gring_op := gring_mx rG \o gring_row.

Lemma gring_opE a : gring_op a = gring_mx rG (gring_row a).

Lemma gring_opG x : x \in G gring_op (aG x) = rG x.

Lemma gring_op1 : gring_op 1%:M = 1%:M.

Lemma gring_opJ A b :
  gring_op (A ×m gring_mx aG b) = gring_op A ×m gring_mx rG b.

Lemma gring_op_mx b : gring_op (gring_mx aG b) = gring_mx rG b.

Lemma gring_mxA a b :
  gring_mx rG (a ×m gring_mx aG b) = gring_mx rG a ×m gring_mx rG b.

End GringOp.

End Regular.

End RingRepr.

Arguments mx_representation R {gT} G%g n%N.
Arguments mx_repr {R gT} G%g {n%N} r.
Arguments group_ring R {gT} G%g.
Arguments regular_repr R {gT} G%g.

Arguments centgmxP {R gT G n rG f}.
Arguments rkerP {R gT G n rG x}.
Arguments repr_mxK {R gT G%G n%N} rG {m%N} [x%g] Gx.
Arguments repr_mxKV {R gT G%G n%N} rG {m%N} [x%g] Gx.
Arguments gring_valK {gT G%G} i%R : rename.
Arguments gring_indexK {gT G%G} x%g.
Arguments gring_mxK {R gT G%G} v%R : rename.

Section ChangeOfRing.

Variables (aR rR : comUnitRingType) (f : {rmorphism aR rR}).
Local Notation "A ^f" := (map_mx (GRing.RMorphism.sort f) A) : ring_scope.
Variables (gT : finGroupType) (G : {group gT}).

Lemma map_regular_mx x : (regular_mx aR G x)^f = regular_mx rR G x.

Lemma map_gring_row (A : 'M_#|G|) : (gring_row A)^f = gring_row A^f.

Lemma map_gring_proj x (A : 'M_#|G|) : (gring_proj x A)^f = gring_proj x A^f.

Section OneRepresentation.

Variables (n : nat) (rG : mx_representation aR G n).

Definition map_repr_mx (f0 : aR rR) rG0 (g : gT) : 'M_n := map_mx f0 (rG0 g).

Lemma map_mx_repr : mx_repr G (map_repr_mx f rG).
Canonical map_repr := MxRepresentation map_mx_repr.
Local Notation rGf := map_repr.

Lemma map_reprE x : rGf x = (rG x)^f.

Lemma map_reprJ m (A : 'M_(m, n)) x : (A ×m rG x)^f = A^f ×m rGf x.

Lemma map_enveloping_algebra_mx :
  (enveloping_algebra_mx rG)^f = enveloping_algebra_mx rGf.

Lemma map_gring_mx a : (gring_mx rG a)^f = gring_mx rGf a^f.

Lemma map_gring_op A : (gring_op rG A)^f = gring_op rGf A^f.

End OneRepresentation.

Lemma map_regular_repr : map_repr (regular_repr aR G) =1 regular_repr rR G.

Lemma map_group_ring : (group_ring aR G)^f = group_ring rR G.

Stabilisers, etc, are only mapped properly for fields.

End ChangeOfRing.

Section FieldRepr.

Variable F : fieldType.

Section OneRepresentation.

Variable gT : finGroupType.

Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n).
Arguments rG _%group_scope : extra scopes.

Local Notation E_G := (enveloping_algebra_mx rG).

Lemma repr_mx_free x : x \in G row_free (rG x).

Section Stabilisers.

Variables (m : nat) (U : 'M[F]_(m, n)).

Definition rstabs := [set x in G | U ×m rG x U]%MS.

Lemma rstabs_sub : rstabs \subset G.

Lemma rstabs_group_set : group_set rstabs.
Canonical rstabs_group := Group rstabs_group_set.

Lemma rstab_act x m1 (W : 'M_(m1, n)) :
  x \in rstab rG U (W U)%MS W ×m rG x = W.

Lemma rstabs_act x m1 (W : 'M_(m1, n)) :
  x \in rstabs (W U)%MS (W ×m rG x U)%MS.

Definition mxmodule := G \subset rstabs.

Lemma mxmoduleP : reflect {in G, x, U ×m rG x U}%MS mxmodule.

End Stabilisers.
Arguments mxmoduleP {m U}.

Lemma rstabS m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
  (U V)%MS rstab rG V \subset rstab rG U.

Lemma eqmx_rstab m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
  (U :=: V)%MS rstab rG U = rstab rG V.

Lemma eqmx_rstabs m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
  (U :=: V)%MS rstabs U = rstabs V.

Lemma eqmx_module m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
  (U :=: V)%MS mxmodule U = mxmodule V.

Lemma mxmodule0 m : mxmodule (0 : 'M_(m, n)).

Lemma mxmodule1 : mxmodule 1%:M.

Lemma mxmodule_trans m1 m2 (U : 'M_(m1, n)) (W : 'M_(m2, n)) x :
  mxmodule U x \in G (W U W ×m rG x U)%MS.

Lemma mxmodule_eigenvector m (U : 'M_(m, n)) :
    mxmodule U \rank U = 1
  {u : 'rV_n & {a | (U :=: u)%MS & {in G, x, u ×m rG x = a x *: u}}}.

Lemma addsmx_module m1 m2 U V :
  @mxmodule m1 U @mxmodule m2 V mxmodule (U + V)%MS.

Lemma sumsmx_module I r (P : pred I) U :
  ( i, P i mxmodule (U i)) mxmodule (\sum_(i <- r | P i) U i)%MS.

Lemma capmx_module m1 m2 U V :
  @mxmodule m1 U @mxmodule m2 V mxmodule (U :&: V)%MS.

Lemma bigcapmx_module I r (P : pred I) U :
  ( i, P i mxmodule (U i)) mxmodule (\bigcap_(i <- r | P i) U i)%MS.

Sub- and factor representations induced by a (sub)module.
Section Submodule.

Variable U : 'M[F]_n.

Definition val_submod m : 'M_(m, \rank U) 'M_(m, n) := mulmxr (row_base U).
Definition in_submod m : 'M_(m, n) 'M_(m, \rank U) :=
   mulmxr (invmx (row_ebase U) ×m pid_mx (\rank U)).

Lemma val_submodE m W : @val_submod m W = W ×m val_submod 1%:M.

Lemma in_submodE m W : @in_submod m W = W ×m in_submod 1%:M.

Lemma val_submod1 : (val_submod 1%:M :=: U)%MS.

Lemma val_submodP m W : (@val_submod m W U)%MS.

Lemma val_submodK m : cancel (@val_submod m) (@in_submod m).

Lemma val_submod_inj m : injective (@val_submod m).

Lemma val_submodS m1 m2 (V : 'M_(m1, \rank U)) (W : 'M_(m2, \rank U)) :
  (val_submod V val_submod W)%MS = (V W)%MS.

Lemma in_submodK m W : (W U)%MS val_submod (@in_submod m W) = W.

Lemma val_submod_eq0 m W : (@val_submod m W == 0) = (W == 0).

Lemma in_submod_eq0 m W : (@in_submod m W == 0) = (W U^C)%MS.

Lemma mxrank_in_submod m (W : 'M_(m, n)) :
  (W U)%MS \rank (in_submod W) = \rank W.

Definition val_factmod m : _ 'M_(m, n) :=
  mulmxr (row_base (cokermx U) ×m row_ebase U).
Definition in_factmod m : 'M_(m, n) _ := mulmxr (col_base (cokermx U)).

Lemma val_factmodE m W : @val_factmod m W = W ×m val_factmod 1%:M.

Lemma in_factmodE m W : @in_factmod m W = W ×m in_factmod 1%:M.

Lemma val_factmodP m W : (@val_factmod m W U^C)%MS.

Lemma val_factmodK m : cancel (@val_factmod m) (@in_factmod m).

Lemma val_factmod_inj m : injective (@val_factmod m).

Lemma val_factmodS m1 m2 (V : 'M_(m1, _)) (W : 'M_(m2, _)) :
  (val_factmod V val_factmod W)%MS = (V W)%MS.

Lemma val_factmod_eq0 m W : (@val_factmod m W == 0) = (W == 0).

Lemma in_factmod_eq0 m (W : 'M_(m, n)) : (in_factmod W == 0) = (W U)%MS.

Lemma in_factmodK m (W : 'M_(m, n)) :
  (W U^C)%MS val_factmod (in_factmod W) = W.

Lemma in_factmod_addsK m (W : 'M_(m, n)) :
  (in_factmod (U + W)%MS :=: in_factmod W)%MS.

Lemma add_sub_fact_mod m (W : 'M_(m, n)) :
  val_submod (in_submod W) + val_factmod (in_factmod W) = W.

Lemma proj_factmodS m (W : 'M_(m, n)) :
  (val_factmod (in_factmod W) U + W)%MS.

Lemma in_factmodsK m (W : 'M_(m, n)) :
  (U W)%MS (U + val_factmod (in_factmod W) :=: W)%MS.

Lemma mxrank_in_factmod m (W : 'M_(m, n)) :
  (\rank (in_factmod W) + \rank U)%N = \rank (U + W).

Definition submod_mx of mxmodule U :=
  fun xin_submod (val_submod 1%:M ×m rG x).

Definition factmod_mx of mxmodule U :=
  fun xin_factmod (val_factmod 1%:M ×m rG x).

Hypothesis Umod : mxmodule U.

Lemma in_submodJ m (W : 'M_(m, n)) x :
  (W U)%MS in_submod (W ×m rG x) = in_submod W ×m submod_mx Umod x.

Lemma val_submodJ m (W : 'M_(m, \rank U)) x :
  x \in G val_submod (W ×m submod_mx Umod x) = val_submod W ×m rG x.

Lemma submod_mx_repr : mx_repr G (submod_mx Umod).

Canonical submod_repr := MxRepresentation submod_mx_repr.

Lemma in_factmodJ m (W : 'M_(m, n)) x :
  x \in G in_factmod (W ×m rG x) = in_factmod W ×m factmod_mx Umod x.

Lemma val_factmodJ m (W : 'M_(m, \rank (cokermx U))) x :
  x \in G
  val_factmod (W ×m factmod_mx Umod x) =
     val_factmod (in_factmod (val_factmod W ×m rG x)).

Lemma factmod_mx_repr : mx_repr G (factmod_mx Umod).
Canonical factmod_repr := MxRepresentation factmod_mx_repr.

For character theory.
Properties of enveloping algebra as a subspace of 'rV_(n ^ 2).

Lemma envelop_mx_id x : x \in G (rG x \in E_G)%MS.

Lemma envelop_mx1 : (1%:M \in E_G)%MS.

Lemma envelop_mxP A :
  reflect ( a, A = \sum_(x in G) a x *: rG x) (A \in E_G)%MS.

Lemma envelop_mxM A B : (A \in E_G B \in E_G A ×m B \in E_G)%MS.

Lemma mxmodule_envelop m1 m2 (U : 'M_(m1, n)) (W : 'M_(m2, n)) A :
  (mxmodule U mxvec A E_G W U W ×m A U)%MS.

Module homomorphisms; any square matrix f defines a module homomorphism over some domain, namely, dom_hom_mx f.

Definition dom_hom_mx f : 'M_n :=
  kermx (lin1_mx (mxvec \o mulmx (cent_mx_fun E_G f) \o lin_mul_row)).

Lemma hom_mxP m f (W : 'M_(m, n)) :
  reflect ( x, x \in G W ×m rG x ×m f = W ×m f ×m rG x)
          (W dom_hom_mx f)%MS.
Arguments hom_mxP {m f W}.

Lemma hom_envelop_mxC m f (W : 'M_(m, n)) A :
  (W dom_hom_mx f A \in E_G W ×m A ×m f = W ×m f ×m A)%MS.

Lemma dom_hom_invmx f :
  f \in unitmx (dom_hom_mx (invmx f) :=: dom_hom_mx f ×m f)%MS.

Lemma dom_hom_mx_module f : mxmodule (dom_hom_mx f).

Lemma hom_mxmodule m (U : 'M_(m, n)) f :
  (U dom_hom_mx f)%MS mxmodule U mxmodule (U ×m f).

Lemma kermx_hom_module m (U : 'M_(m, n)) f :
  (U dom_hom_mx f)%MS mxmodule U mxmodule (U :&: kermx f)%MS.

Lemma scalar_mx_hom a m (U : 'M_(m, n)) : (U dom_hom_mx a%:M)%MS.

Lemma proj_mx_hom (U V : 'M_n) :
    (U :&: V = 0)%MS mxmodule U mxmodule V
  (U + V dom_hom_mx (proj_mx U V))%MS.

The subspace fixed by a subgroup H of G; it is a module if H <| G. The definition below is extensionally equivalent to the straightforward \bigcap_(x in H) kermx (rG x - 1%:M) but it avoids the dependency on the choice function; this allows it to commute with ring morphisms.
The cyclic module generated by a single vector.
Definition cyclic_mx u := <<E_G ×m lin_mul_row u>>%MS.

Lemma cyclic_mxP u v :
  reflect (exists2 A, A \in E_G & v = u ×m A)%MS (v cyclic_mx u)%MS.
Arguments cyclic_mxP {u v}.

Lemma cyclic_mx_id u : (u cyclic_mx u)%MS.

Lemma cyclic_mx_eq0 u : (cyclic_mx u == 0) = (u == 0).

Lemma cyclic_mx_module u : mxmodule (cyclic_mx u).

Lemma cyclic_mx_sub m u (W : 'M_(m, n)) :
  mxmodule W (u W)%MS (cyclic_mx u W)%MS.

Lemma hom_cyclic_mx u f :
  (u dom_hom_mx f)%MS (cyclic_mx u ×m f :=: cyclic_mx (u ×m f))%MS.

The annihilator of a single vector.

Definition annihilator_mx u := (E_G :&: kermx (lin_mul_row u))%MS.

Lemma annihilator_mxP u A :
  reflect (A \in E_G u ×m A = 0)%MS (A \in annihilator_mx u)%MS.

The subspace of homomorphic images of a row vector.

Definition row_hom_mx u :=
  (\bigcap_j kermx (vec_mx (row j (annihilator_mx u))))%MS.

Lemma row_hom_mxP u v :
  reflect (exists2 f, u dom_hom_mx f & u ×m f = v)%MS (v row_hom_mx u)%MS.

Sub-, isomorphic, simple, semisimple and completely reducible modules. All these predicates are intuitionistic (since, e.g., testing simplicity requires a splitting algorithm fo r the mas field). They are all specialized to square matrices, to avoid spurrious height parameters. Module isomorphism is an intentional property in general, but it can be decided when one of the two modules is known to be simple.

Variant mx_iso (U V : 'M_n) : Prop :=
  MxIso f of f \in unitmx & (U dom_hom_mx f)%MS & (U ×m f :=: V)%MS.

Lemma eqmx_iso U V : (U :=: V)%MS mx_iso U V.

Lemma mx_iso_refl U : mx_iso U U.

Lemma mx_iso_sym U V : mx_iso U V mx_iso V U.

Lemma mx_iso_trans U V W : mx_iso U V mx_iso V W mx_iso U W.

Lemma mxrank_iso U V : mx_iso U V \rank U = \rank V.

Lemma mx_iso_module U V : mx_iso U V mxmodule U mxmodule V.

Simple modules (we reserve the term "irreducible" for representations).

Definition mxsimple (V : 'M_n) :=
  [/\ mxmodule V, V != 0 &
       U : 'M_n, mxmodule U (U V)%MS U != 0 (V U)%MS].

Definition mxnonsimple (U : 'M_n) :=
   V : 'M_n, [&& mxmodule V, (V U)%MS, V != 0 & \rank V < \rank U].

Lemma mxsimpleP U :
  [/\ mxmodule U, U != 0 & ¬ mxnonsimple U] mxsimple U.

Lemma mxsimple_module U : mxsimple U mxmodule U.

Lemma mxsimple_exists m (U : 'M_(m, n)) :
  mxmodule U U != 0 classically (exists2 V, mxsimple V & V U)%MS.

Lemma mx_iso_simple U V : mx_iso U V mxsimple U mxsimple V.

Lemma mxsimple_cyclic u U :
  mxsimple U u != 0 (u U)%MS (U :=: cyclic_mx u)%MS.

The surjective part of Schur's lemma.
Lemma mx_Schur_onto m (U : 'M_(m, n)) V f :
    mxmodule U mxsimple V (U dom_hom_mx f)%MS
  (U ×m f V)%MS U ×m f != 0 (U ×m f :=: V)%MS.

The injective part of Schur's lemma.
Lemma mx_Schur_inj U f :
  mxsimple U (U dom_hom_mx f)%MS U ×m f != 0 (U :&: kermx f)%MS = 0.

The injectve part of Schur's lemma, stated as isomorphism with the image.
The isomorphism part of Schur's lemma.
Lemma mx_Schur_iso U V f :
    mxsimple U mxsimple V (U dom_hom_mx f)%MS
  (U ×m f V)%MS U ×m f != 0 mx_iso U V.

A boolean test for module isomorphism that is only valid for simple modules; this is the only case that matters in practice.
For us, "semisimple" means "sum of simple modules"; this is classically, but not intuitionistically, equivalent to the "completely reducible" alternate characterization.

Implicit Type I : finType.

Variant mxsemisimple (V : 'M_n) :=
  MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
     i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.

This is a slight generalization of Aschbacher 12.5 for finite sets.
Lemma sum_mxsimple_direct_compl m I W (U : 'M_(m, n)) :
    let V := (\sum_(i : I) W i)%MS in
    ( i : I, mxsimple (W i)) mxmodule U (U V)%MS
  {J : {set I} | let S := U + \sum_(i in J) W i in S :=: V mxdirect S}%MS.

Lemma sum_mxsimple_direct_sub I W (V : 'M_n) :
    ( i : I, mxsimple (W i)) (\sum_i W i :=: V)%MS
  {J : {set I} | let S := \sum_(i in J) W i in S :=: V mxdirect S}%MS.

Lemma mxsemisimple0 : mxsemisimple 0.

Lemma intro_mxsemisimple (I : Type) r (P : pred I) W V :
    (\sum_(i <- r | P i) W i :=: V)%MS
    ( i, P i W i != 0 mxsimple (W i))
  mxsemisimple V.

Lemma mxsimple_semisimple U : mxsimple U mxsemisimple U.

Lemma addsmx_semisimple U V :
  mxsemisimple U mxsemisimple V mxsemisimple (U + V)%MS.

Lemma sumsmx_semisimple (I : finType) (P : pred I) V :
  ( i, P i mxsemisimple (V i)) mxsemisimple (\sum_(i | P i) V i)%MS.

Lemma eqmx_semisimple U V : (U :=: V)%MS mxsemisimple U mxsemisimple V.

Lemma hom_mxsemisimple (V f : 'M_n) :
  mxsemisimple V (V dom_hom_mx f)%MS mxsemisimple (V ×m f).

Lemma mxsemisimple_module U : mxsemisimple U mxmodule U.

Completely reducible modules, and Maeschke's Theorem.
The component associated to a given irreducible module.

Section Components.

Fact component_mx_key : unit.
Definition component_mx_expr (U : 'M[F]_n) :=
  (\sum_i cyclic_mx (row i (row_hom_mx (nz_row U))))%MS.
Definition component_mx := locked_with component_mx_key component_mx_expr.
Canonical component_mx_unfoldable := [unlockable fun component_mx].

Variable U : 'M[F]_n.
Hypothesis simU : mxsimple U.

Let u := nz_row U.
Let iso_u := row_hom_mx u.
Let nz_u : u != 0 := nz_row_mxsimple simU.
Let Uu : (u U)%MS := nz_row_sub U.
Let defU : (U :=: cyclic_mx u)%MS := mxsimple_cyclic simU nz_u Uu.
Local Notation compU := (component_mx U).

Lemma component_mx_module : mxmodule compU.

Lemma genmx_component : <<compU>>%MS = compU.

Lemma component_mx_def : {I : finType & {W : I 'M_n |
   i, mx_iso U (W i) & compU = \sum_i W i}}%MS.

Lemma component_mx_semisimple : mxsemisimple compU.

Lemma mx_iso_component V : mx_iso U V (V compU)%MS.

Lemma component_mx_id : (U compU)%MS.

Lemma hom_component_mx_iso f V :
    mxsimple V (compU dom_hom_mx f)%MS (V compU ×m f)%MS
  mx_iso U V.

Lemma component_mx_iso V : mxsimple V (V compU)%MS mx_iso U V.

Lemma hom_component_mx f :
  (compU dom_hom_mx f)%MS (compU ×m f compU)%MS.

End Components.

Lemma component_mx_isoP U V :
    mxsimple U mxsimple V
  reflect (mx_iso U V) (component_mx U == component_mx V).

Lemma component_mx_disjoint U V :
    mxsimple U mxsimple V component_mx U != component_mx V
  (component_mx U :&: component_mx V = 0)%MS.

Section Socle.

Record socleType := EnumSocle {
  socle_base_enum : seq 'M[F]_n;
  _ : M, M \in socle_base_enum mxsimple M;
  _ : M, mxsimple M has (mxsimple_iso M) socle_base_enum

Lemma socle_exists : classically socleType.

Section SocleDef.

Variable sG0 : socleType.

Definition socle_enum := map component_mx (socle_base_enum sG0).

Lemma component_socle M : mxsimple M component_mx M \in socle_enum.

Inductive socle_sort : predArgType := PackSocle W of W \in socle_enum.

Local Notation sG := socle_sort.
Local Notation e0 := (socle_base_enum sG0).

Definition socle_base W := let: PackSocle W _ := W in e0`_(index W socle_enum).

Coercion socle_val W : 'M[F]_n := component_mx (socle_base W).

Definition socle_mult (W : sG) := (\rank W %/ \rank (socle_base W))%N.

Lemma socle_simple W : mxsimple (socle_base W).

Definition socle_module (W : sG) := mxsimple_module (socle_simple W).

Definition socle_repr W := submod_repr (socle_module W).

Lemma nz_socle (W : sG) : W != 0 :> 'M_n.

Lemma socle_mem (W : sG) : (W : 'M_n) \in socle_enum.

Lemma PackSocleK W e0W : @PackSocle W e0W = W :> 'M_n.

Lemma socleP (W W' : sG) : reflect (W = W') (W == W')%MS.

Fact socle_can_subproof :
  cancel (fun WSeqSub (socle_mem W)) (fun sPackSocle (valP s)).

End SocleDef.

Coercion socle_sort : socleType >-> predArgType.

Variable sG : socleType.

Section SubSocle.

Variable P : pred sG.
Notation S := (\sum_(W : sG | P W) socle_val W)%MS.

Lemma subSocle_module : mxmodule S.

Lemma subSocle_semisimple : mxsemisimple S.
Local Notation ssimS := subSocle_semisimple.

Lemma subSocle_iso M :
  mxsimple M (M S)%MS {W : sG | P W & mx_iso (socle_base W) M}.

Lemma capmx_subSocle m (M : 'M_(m, n)) :
  mxmodule M (M :&: S :=: \sum_(W : sG | P W) (M :&: W))%MS.

End SubSocle.

Lemma subSocle_direct P : mxdirect (\sum_(W : sG | P W) W).

Definition Socle := (\sum_(W : sG) W)%MS.

Lemma simple_Socle M : mxsimple M (M Socle)%MS.

Lemma semisimple_Socle U : mxsemisimple U (U Socle)%MS.

Lemma reducible_Socle U :
  mxmodule U mx_completely_reducible U (U Socle)%MS.

Lemma genmx_Socle : <<Socle>>%MS = Socle.

Lemma reducible_Socle1 : mx_completely_reducible 1%:M Socle = 1%:M.

Lemma Socle_module : mxmodule Socle.

Lemma Socle_semisimple : mxsemisimple Socle.

Lemma Socle_direct : mxdirect Socle.

Lemma Socle_iso M : mxsimple M {W : sG | mx_iso (socle_base W) M}.

End Socle.

Centralizer subgroup and central homomorphisms.
(Globally) irreducible, and absolutely irreducible representations. Note that unlike "reducible", "absolutely irreducible" can easily be decided.

Definition mx_irreducible := mxsimple 1%:M.

Lemma mx_irrP :
  mx_irreducible n > 0 ( U, @mxmodule n U U != 0 row_full U).

Schur's lemma for endomorphisms.
Lemma mx_Schur :
  mx_irreducible f, centgmx rG f f != 0 f \in unitmx.

Definition mx_absolutely_irreducible := (n > 0) && row_full E_G.

Lemma mx_abs_irrP :
  reflect (n > 0 a_, A, A = \sum_(x in G) a_ x A *: rG x)

Lemma mx_abs_irr_cent_scalar :
  mx_absolutely_irreducible A, centgmx rG A is_scalar_mx A.

Lemma mx_abs_irrW : mx_absolutely_irreducible mx_irreducible.

Lemma linear_mx_abs_irr : n = 1 mx_absolutely_irreducible.

Lemma abelian_abs_irr : abelian G mx_absolutely_irreducible = (n == 1).

End OneRepresentation.

Arguments mxmoduleP {gT G n rG m U}.
Arguments envelop_mxP {gT G n rG A}.
Arguments hom_mxP {gT G n rG m f W}.
Arguments rfix_mxP {gT G n rG m W}.
Arguments cyclic_mxP {gT G n rG u v}.
Arguments annihilator_mxP {gT G n rG u A}.
Arguments row_hom_mxP {gT G n rG u v}.
Arguments mxsimple_isoP {gT G n rG U V}.
Arguments socleP {gT G n rG sG0 W W'}.
Arguments mx_abs_irrP {gT G n rG}.

Arguments val_submod {n U m} W.
Arguments in_submod {n} U {m} W.
Arguments val_submodK {n U m} W : rename.
Arguments in_submodK {n U m} [W] sWU.
Arguments val_submod_inj {n U m} [W1 W2] : rename.

Arguments val_factmod {n U m} W.
Arguments in_factmod {n} U {m} W.
Arguments val_factmodK {n U m} W : rename.
Arguments in_factmodK {n} U {m} [W] sWU.
Arguments val_factmod_inj {n U m} [W1 W2] : rename.

Section Proper.

Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variable rG : mx_representation F G n.

Lemma envelop_mx_ring : mxring (enveloping_algebra_mx rG).

End Proper.

Section JacobsonDensity.

Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variable rG : mx_representation F G n.
Hypothesis irrG : mx_irreducible rG.

Local Notation E_G := (enveloping_algebra_mx rG).
Local Notation Hom_G := 'C(E_G)%MS.

Lemma mx_Jacobson_density : ('C(Hom_G) E_G)%MS.

Lemma cent_mx_scalar_abs_irr : \rank Hom_G 1 mx_absolutely_irreducible rG.

End JacobsonDensity.

Section ChangeGroup.

Variables (gT : finGroupType) (G H : {group gT}) (n : nat).
Variables (rG : mx_representation F G n).

Section SubGroup.

Hypothesis sHG : H \subset G.

Local Notation rH := (subg_repr rG sHG).

Lemma rfix_subg : rfix_mx rH = rfix_mx rG.

Section Stabilisers.

Variables (m : nat) (U : 'M[F]_(m, n)).

Lemma rstabs_subg : rstabs rH U = H :&: rstabs rG U.

Lemma mxmodule_subg : mxmodule rG U mxmodule rH U.

End Stabilisers.

Lemma mxsimple_subg M : mxmodule rG M mxsimple rH M mxsimple rG M.

Lemma subg_mx_irr : mx_irreducible rH mx_irreducible rG.

Lemma subg_mx_abs_irr :
   mx_absolutely_irreducible rH mx_absolutely_irreducible rG.

End SubGroup.

Section SameGroup.

Hypothesis eqGH : G :==: H.

Local Notation rH := (eqg_repr rG eqGH).

Lemma rfix_eqg : rfix_mx rH = rfix_mx rG.

Section Stabilisers.

Variables (m : nat) (U : 'M[F]_(m, n)).

Lemma rstabs_eqg : rstabs rH U = rstabs rG U.

Lemma mxmodule_eqg : mxmodule rH U = mxmodule rG U.

End Stabilisers.

Lemma mxsimple_eqg M : mxsimple rH M mxsimple rG M.

Lemma eqg_mx_irr : mx_irreducible rH mx_irreducible rG.

Lemma eqg_mx_abs_irr :
  mx_absolutely_irreducible rH = mx_absolutely_irreducible rG.

End SameGroup.

End ChangeGroup.

Section Morphpre.

Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Variables (G : {group rT}) (n : nat) (rG : mx_representation F G n).

Local Notation rGf := (morphpre_repr f rG).

Section Stabilisers.
Variables (m : nat) (U : 'M[F]_(m, n)).

Lemma rstabs_morphpre : rstabs rGf U = f @*^-1 (rstabs rG U).

Lemma mxmodule_morphpre : G \subset f @* D mxmodule rGf U = mxmodule rG U.

End Stabilisers.

Lemma rfix_morphpre (H : {set aT}) :
  H \subset D (rfix_mx rGf H :=: rfix_mx rG (f @* H))%MS.

Lemma morphpre_mx_irr :
  G \subset f @* D (mx_irreducible rGf mx_irreducible rG).

Lemma morphpre_mx_abs_irr :
    G \subset f @* D
  mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.

End Morphpre.

Section Morphim.

Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
Variables (n : nat) (rGf : mx_representation F (f @* G) n).

Hypothesis sGD : G \subset D.

Let sG_f'fG : G \subset f @*^-1 (f @* G).

Local Notation rG := (morphim_repr rGf sGD).

Section Stabilisers.
Variables (m : nat) (U : 'M[F]_(m, n)).

Lemma rstabs_morphim : rstabs rG U = G :&: f @*^-1 rstabs rGf U.

Lemma mxmodule_morphim : mxmodule rG U = mxmodule rGf U.

End Stabilisers.

Lemma rfix_morphim (H : {set aT}) :
  H \subset D (rfix_mx rG H :=: rfix_mx rGf (f @* H))%MS.

Lemma mxsimple_morphim M : mxsimple rG M mxsimple rGf M.

Lemma morphim_mx_irr : (mx_irreducible rG mx_irreducible rGf).

Lemma morphim_mx_abs_irr :
  mx_absolutely_irreducible rG = mx_absolutely_irreducible rGf.

End Morphim.

Section Submodule.

Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation F G n) (U : 'M[F]_n) (Umod : mxmodule rG U).
Local Notation rU := (submod_repr Umod).
Local Notation rU' := (factmod_repr Umod).

Lemma rfix_submod (H : {set gT}) :
  H \subset G (rfix_mx rU H :=: in_submod U (U :&: rfix_mx rG H))%MS.

Lemma rfix_factmod (H : {set gT}) :
  H \subset G (in_factmod U (rfix_mx rG H) rfix_mx rU' H)%MS.

Lemma rstab_submod m (W : 'M_(m, \rank U)) :
  rstab rU W = rstab rG (val_submod W).

Lemma rstabs_submod m (W : 'M_(m, \rank U)) :
  rstabs rU W = rstabs rG (val_submod W).

Lemma val_submod_module m (W : 'M_(m, \rank U)) :
   mxmodule rG (val_submod W) = mxmodule rU W.

Lemma in_submod_module m (V : 'M_(m, n)) :
  (V U)%MS mxmodule rU (in_submod U V) = mxmodule rG V.

Lemma rstab_factmod m (W : 'M_(m, n)) :
  rstab rG W \subset rstab rU' (in_factmod U W).

Lemma rstabs_factmod m (W : 'M_(m, \rank (cokermx U))) :
  rstabs rU' W = rstabs rG (U + val_factmod W)%MS.

Lemma val_factmod_module m (W : 'M_(m, \rank (cokermx U))) :
  mxmodule rG (U + val_factmod W)%MS = mxmodule rU' W.

Lemma in_factmod_module m (V : 'M_(m, n)) :
  mxmodule rU' (in_factmod U V) = mxmodule rG (U + V)%MS.

Lemma rker_submod : rker rU = rstab rG U.

Lemma rstab_norm : G \subset 'N(rstab rG U).

Lemma rstab_normal : rstab rG U <| G.

Lemma submod_mx_faithful : mx_faithful rU mx_faithful rG.

Lemma rker_factmod : rker rG \subset rker rU'.

Lemma factmod_mx_faithful : mx_faithful rU' mx_faithful rG.

Lemma submod_mx_irr : mx_irreducible rU mxsimple rG U.

End Submodule.

Section Conjugate.

Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation F G n) (B : 'M[F]_n).

Hypothesis uB : B \in unitmx.

Local Notation rGB := (rconj_repr rG uB).

Lemma rfix_conj (H : {set gT}) :
   (rfix_mx rGB H :=: B ×m rfix_mx rG H ×m invmx B)%MS.

Lemma rstabs_conj m (U : 'M_(m, n)) : rstabs rGB U = rstabs rG (U ×m B).

Lemma mxmodule_conj m (U : 'M_(m, n)) : mxmodule rGB U = mxmodule rG (U ×m B).

Lemma conj_mx_irr : mx_irreducible rGB mx_irreducible rG.

End Conjugate.

Section Quotient.

Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation F G n) (H : {group gT}).
Hypotheses (krH : H \subset rker rG) (nHG : G \subset 'N(H)).
Let nHGs := subsetP nHG.

Local Notation rGH := (quo_repr krH nHG).

Local Notation E_ r := (enveloping_algebra_mx r).
Lemma quo_mx_quotient : (E_ rGH :=: E_ rG)%MS.

Lemma rfix_quo (K : {group gT}) :
  K \subset G (rfix_mx rGH (K / H)%g :=: rfix_mx rG K)%MS.

Lemma rstabs_quo m (U : 'M_(m, n)) : rstabs rGH U = (rstabs rG U / H)%g.

Lemma mxmodule_quo m (U : 'M_(m, n)) : mxmodule rGH U = mxmodule rG U.

Lemma quo_mx_irr : mx_irreducible rGH mx_irreducible rG.

End Quotient.

Section SplittingField.

Implicit Type gT : finGroupType.

Definition group_splitting_field gT (G : {group gT}) :=
   n (rG : mx_representation F G n),
     mx_irreducible rG mx_absolutely_irreducible rG.

Definition group_closure_field gT :=
   G : {group gT}, group_splitting_field G.

Lemma quotient_splitting_field gT (G : {group gT}) (H : {set gT}) :
  G \subset 'N(H) group_splitting_field G group_splitting_field (G / H).

Lemma coset_splitting_field gT (H : {set gT}) :
  group_closure_field gT group_closure_field (coset_of H).

End SplittingField.

Section Abelian.

Variables (gT : finGroupType) (G : {group gT}).

Lemma mx_faithful_irr_center_cyclic n (rG : mx_representation F G n) :
  mx_faithful rG mx_irreducible rG cyclic 'Z(G).

Lemma mx_faithful_irr_abelian_cyclic n (rG : mx_representation F G n) :
  mx_faithful rG mx_irreducible rG abelian G cyclic G.

Hypothesis splitG : group_splitting_field G.

Lemma mx_irr_abelian_linear n (rG : mx_representation F G n) :
  mx_irreducible rG abelian G n = 1.

Lemma mxsimple_abelian_linear n (rG : mx_representation F G n) M :
  abelian G mxsimple rG M \rank M = 1.

Lemma linear_mxsimple n (rG : mx_representation F G n) (M : 'M_n) :
  mxmodule rG M \rank M = 1 mxsimple rG M.

End Abelian.

Section AbelianQuotient.

Variables (gT : finGroupType) (G : {group gT}).
Variables (n : nat) (rG : mx_representation F G n).

Lemma center_kquo_cyclic : mx_irreducible rG cyclic 'Z(G / rker rG)%g.

Lemma der1_sub_rker :
    group_splitting_field G mx_irreducible rG
  (G^`(1) \subset rker rG)%g = (n == 1)%N.

End AbelianQuotient.

Section Similarity.

Variables (gT : finGroupType) (G : {group gT}).
Local Notation reprG := (mx_representation F G).

Variant mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop :=
  MxReprSim B of n1 = n2 & row_free B
              & x, x \in G rG1 x ×m B = B ×m rG2 x.

Lemma mxrank_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2 n1 = n2.

Lemma mx_rsim_refl n (rG : reprG n) : mx_rsim rG rG.

Lemma mx_rsim_sym n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2 mx_rsim rG2 rG1.

Lemma mx_rsim_trans n1 n2 n3
                    (rG1 : reprG n1) (rG2 : reprG n2) (rG3 : reprG n3) :
  mx_rsim rG1 rG2 mx_rsim rG2 rG3 mx_rsim rG1 rG3.

Lemma mx_rsim_def n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
    mx_rsim rG1 rG2
   B, exists2 B', B' ×m B = 1%:M &
     x, x \in G rG1 x = B ×m rG2 x ×m B'.

Lemma mx_rsim_iso n (rG : reprG n) (U V : 'M_n)
                  (modU : mxmodule rG U) (modV : mxmodule rG V) :
  mx_rsim (submod_repr modU) (submod_repr modV) mx_iso rG U V.

Lemma mx_rsim_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2 mx_irreducible rG1 mx_irreducible rG2.

Lemma mx_rsim_abs_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
    mx_rsim rG1 rG2
  mx_absolutely_irreducible rG1 = mx_absolutely_irreducible rG2.

Lemma rker_mx_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2 rker rG1 = rker rG2.

Lemma mx_rsim_faithful n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2 mx_faithful rG1 = mx_faithful rG2.

Lemma mx_rsim_factmod n (rG : reprG n) U V
                     (modU : mxmodule rG U) (modV : mxmodule rG V) :
    (U + V :=: 1%:M)%MS mxdirect (U + V)
  mx_rsim (factmod_repr modV) (submod_repr modU).

Lemma mxtrace_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2 {in G, x, \tr (rG1 x) = \tr (rG2 x)}.

Lemma mx_rsim_scalar n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) x c :
   x \in G mx_rsim rG1 rG2 rG1 x = c%:M rG2 x = c%:M.

End Similarity.

Section Socle.

Variables (gT : finGroupType) (G : {group gT}).
Variables (n : nat) (rG : mx_representation F G n) (sG : socleType rG).

Lemma socle_irr (W : sG) : mx_irreducible (socle_repr W).

Lemma socle_rsimP (W1 W2 : sG) :
  reflect (mx_rsim (socle_repr W1) (socle_repr W2)) (W1 == W2).

Local Notation mG U := (mxmodule rG U).
Local Notation sr modV := (submod_repr modV).

Lemma mx_rsim_in_submod U V (modU : mG U) (modV : mG V) :
  let U' := <<in_submod V U>>%MS in
    (U V)%MS
   modU' : mxmodule (sr modV) U', mx_rsim (sr modU) (sr modU').

Lemma rsim_submod1 U (modU : mG U) : (U :=: 1%:M)%MS mx_rsim (sr modU) rG.

Lemma mxtrace_submod1 U (modU : mG U) :
  (U :=: 1%:M)%MS {in G, x, \tr (sr modU x) = \tr (rG x)}.

Lemma mxtrace_dadd_mod U V W (modU : mG U) (modV : mG V) (modW : mG W) :
    (U + V :=: W)%MS mxdirect (U + V)
  {in G, x, \tr (sr modU x) + \tr (sr modV x) = \tr (sr modW x)}.

Lemma mxtrace_dsum_mod (I : finType) (P : pred I) U W
                       (modU : i, mG (U i)) (modW : mG W) :
    let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS mxdirect S
  {in G, x, \sum_(i | P i) \tr (sr (modU i) x) = \tr (sr modW x)}.

Lemma mxtrace_component U (simU : mxsimple rG U) :
   let V := component_mx rG U in
   let modV := component_mx_module rG U in let modU := mxsimple_module simU in
  {in G, x, \tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.

Lemma mxtrace_Socle : let modS := Socle_module sG in
  {in G, x,
    \tr (sr modS x) = \sum_(W : sG) \tr (socle_repr W x) *+ socle_mult W}.

End Socle.

Section Clifford.

Variables (gT : finGroupType) (G H : {group gT}).
Hypothesis nsHG : H <| G.
Variables (n : nat) (rG : mx_representation F G n).
Let sHG := normal_sub nsHG.
Let nHG := normal_norm nsHG.
Let rH := subg_repr rG sHG.

Lemma Clifford_simple M x : mxsimple rH M x \in G mxsimple rH (M ×m rG x).

Lemma Clifford_hom x m (U : 'M_(m, n)) :
  x \in 'C_G(H) (U dom_hom_mx rH (rG x))%MS.

Lemma Clifford_iso x U : x \in 'C_G(H) mx_iso rH U (U ×m rG x).

Lemma Clifford_iso2 x U V :
  mx_iso rH U V x \in G mx_iso rH (U ×m rG x) (V ×m rG x).

Lemma Clifford_componentJ M x :
    mxsimple rH M x \in G
  (component_mx rH (M ×m rG x) :=: component_mx rH M ×m rG x)%MS.

Hypothesis irrG : mx_irreducible rG.

Lemma Clifford_basis M : mxsimple rH M
  {X : {set gT} | X \subset G &
    let S := \sum_(x in X) M ×m rG x in S :=: 1%:M mxdirect S}%MS.

Variable sH : socleType rH.

Definition Clifford_act (W : sH) x :=
  let Gx := subgP (subg G x) in
  PackSocle (component_socle sH (Clifford_simple (socle_simple W) Gx)).

Let valWact W x : (Clifford_act W x :=: W ×m rG (sgval (subg G x)))%MS.

Fact Clifford_is_action : is_action G Clifford_act.

Definition Clifford_action := Action Clifford_is_action.

Local Notation "'Cl" := Clifford_action (at level 8) : action_scope.

Lemma val_Clifford_act W x : x \in G ('Cl%act W x :=: W ×m rG x)%MS.

Lemma Clifford_atrans : [transitive G, on [set: sH] | 'Cl].

Lemma Clifford_Socle1 : Socle sH = 1%:M.

Lemma Clifford_rank_components (W : sH) : (#|sH| × \rank W)%N = n.

Theorem Clifford_component_basis M : mxsimple rH M
  {t : nat & {x_ : sH 'I_t gT |
     W, let sW := (\sum_j M ×m rG (x_ W j))%MS in
      [/\ j, x_ W j \in G, (sW :=: W)%MS & mxdirect sW]}}.

Lemma Clifford_astab : H <*> 'C_G(H) \subset 'C([set: sH] | 'Cl).

Lemma Clifford_astab1 (W : sH) : 'C[W | 'Cl] = rstabs rG W.

Lemma Clifford_rstabs_simple (W : sH) :
  mxsimple (subg_repr rG (rstabs_sub rG W)) W.

End Clifford.

Section JordanHolder.

Variables (gT : finGroupType) (G : {group gT}).
Variables (n : nat) (rG : mx_representation F G n).
Local Notation modG := ((mxmodule rG) n).

Lemma section_module (U V : 'M_n) (modU : modG U) (modV : modG V) :
  mxmodule (factmod_repr modU) <<in_factmod U V>>%MS.

Definition section_repr U V (modU : modG U) (modV : modG V) :=
  submod_repr (section_module modU modV).

Lemma mx_factmod_sub U modU :
  mx_rsim (@section_repr U _ modU (mxmodule1 rG)) (factmod_repr modU).

Definition max_submod (U V : 'M_n) :=
  (U < V)%MS ( W, ¬ [/\ modG W, U < W & W < V])%MS.

Lemma max_submodP U V (modU : modG U) (modV : modG V) :
  (U V)%MS (max_submod U V mx_irreducible (section_repr modU modV)).

Lemma max_submod_eqmx U1 U2 V1 V2 :
  (U1 :=: U2)%MS (V1 :=: V2)%MS max_submod