(Joint Center)Library MathComp.mxrepresentation

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime ssralg poly polydiv finset.
Require Import fingroup morphism perm automorphism quotient finalg action zmodp.
Require Import commutator cyclic center pgroup matrix mxalgebra 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. 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.

Set Implicit Arguments.

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).

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 Gcancel ((@mulmx _ m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).

Lemma repr_mxKV m x :
  x \in Gcancel ((@mulmx _ m n n)^~ (rG x^-1)) (mulmx^~ (rG x)).

Lemma repr_mx_unit x : x \in GrG 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 Gf ×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%NG^`(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.

Implicit 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 GrG 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 rGmx_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 Gquo_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 GrGH (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 Gkquo_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}).
Local Notation nG := #|pred_of_set (gval G)|.

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).
Canonical gring_row_linear := [linear of gring_row].

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.
Canonical gring_proj_linear x := [linear of gring_proj x].

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).
Canonical gring_mx_linear := [linear of gring_mx].

Lemma gring_mxJ a x :
  x \in Ggring_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.
Canonical gring_op_linear := [linear of gring_op].

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

Lemma gring_opG x : x \in Ggring_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.

Implicit Arguments centgmxP [R gT G n rG f].
Implicit Arguments rkerP [R gT G n rG x].

Section ChangeOfRing.

Variables (aR rR : comUnitRingType) (f : {rmorphism aRrR}).
Local Notation "A ^f" := (map_mx (GRing.RMorphism.apply 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 : aRrR) 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).

Local Notation E_G := (enveloping_algebra_mx rG).

Lemma repr_mx_free x : x \in Grow_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)%MSW ×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.
Implicit Arguments mxmoduleP [m U].

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

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

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

Lemma eqmx_module m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
  (U :=: V)%MSmxmodule 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 Ux \in G → (W UW ×m rG x U)%MS.

Lemma mxmodule_eigenvector m (U : 'M_(m, n)) :
    mxmodule U\rank U = 1%N
  {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 Vmxmodule (U + V)%MS.

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

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

Lemma bigcapmx_module I r (P : pred I) U :
  ( i, P imxmodule (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)).
Canonical val_submod_linear m := [linear of @val_submod m].
Canonical in_submod_linear m := [linear of @in_submod m].

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)%MSval_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)).
Canonical val_factmod_linear m := [linear of @val_factmod m].
Canonical in_factmod_linear m := [linear of @in_factmod m].

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)%MSval_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)%MSin_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 Gval_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 Gin_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_GB \in E_GA ×m B \in E_G)%MS.

Lemma mxmodule_envelop m1 m2 (U : 'M_(m1, n)) (W : 'M_(m2, n)) A :
  (mxmodule Umxvec A E_GW UW ×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 GW ×m rG x ×m f = W ×m f ×m rG x)
          (W dom_hom_mx f)%MS.
Implicit Arguments hom_mxP [m f W].

Lemma hom_envelop_mxC m f (W : 'M_(m, n)) A :
  (W dom_hom_mx fA \in E_GW ×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)%MSmxmodule Umxmodule (U ×m f).

Lemma kermx_hom_module m (U : 'M_(m, n)) f :
  (U dom_hom_mx f)%MSmxmodule Umxmodule (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)%MSmxmodule Umxmodule 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.

Definition rfix_mx (H : {set gT}) :=
  let commrH := \matrix_(i < #|H|) mxvec (rG (enum_val i) - 1%:M) in
  kermx (lin1_mx (mxvec \o mulmx commrH \o lin_mul_row)).

Lemma rfix_mxP m (W : 'M_(m, n)) (H : {set gT}) :
  reflect ( x, x \in HW ×m rG x = W) (W rfix_mx H)%MS.
Implicit Arguments rfix_mxP [m W].

Lemma rfix_mx_id (H : {set gT}) x : x \in Hrfix_mx H ×m rG x = rfix_mx H.

Lemma rfix_mxS (H K : {set gT}) : H \subset K → (rfix_mx K rfix_mx H)%MS.

Lemma rfix_mx_conjsg (H : {set gT}) x :
  x \in GH \subset G → (rfix_mx (H :^ x) :=: rfix_mx H ×m rG x)%MS.

Lemma norm_sub_rstabs_rfix_mx (H : {set gT}) :
  H \subset G'N_G(H) \subset rstabs (rfix_mx H).

Lemma normal_rfix_mx_module H : H <| Gmxmodule (rfix_mx H).

Lemma rfix_mx_module : mxmodule (rfix_mx G).

Lemma rfix_mx_rstabC (H : {set gT}) m (U : 'M[F]_(m, n)) :
  H \subset G(H \subset rstab rG U) = (U rfix_mx H)%MS.

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.
Implicit 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.

CoInductive 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)%MSmx_iso U V.

Lemma mx_iso_refl U : mx_iso U U.

Lemma mx_iso_sym U V : mx_iso U Vmx_iso V U.

Lemma mx_iso_trans U V W : mx_iso U Vmx_iso V Wmx_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 Vmxmodule Umxmodule 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)%MSU != 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 Umxmodule U.

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

Lemma mx_iso_simple U V : mx_iso U Vmxsimple Umxsimple V.

Lemma mxsimple_cyclic u U :
  mxsimple Uu != 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 Umxsimple V → (U dom_hom_mx f)%MS
  (U ×m f V)%MSU ×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)%MSU ×m f != 0 → (U :&: kermx f)%MS = 0.

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

The isomorphism part of Schur's lemma.
Lemma mx_Schur_iso U V f :
    mxsimple Umxsimple V → (U dom_hom_mx f)%MS
  (U ×m f V)%MSU ×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.

Lemma nz_row_mxsimple U : mxsimple Unz_row U != 0.

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

Lemma mxsimple_isoP U V :
  mxsimple Ureflect (mx_iso U V) (mxsimple_iso U V).

Lemma mxsimple_iso_simple U V :
  mxsimple_iso U Vmxsimple Umxsimple V.

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.

CoInductive 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 iW i != 0 → mxsimple (W i)) →
  mxsemisimple V.

Lemma mxsimple_semisimple U : mxsimple Umxsemisimple U.

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

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

Lemma eqmx_semisimple U V : (U :=: V)%MSmxsemisimple Umxsemisimple V.

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

Lemma mxsemisimple_module U : mxsemisimple Umxmodule U.

Completely reducible modules, and Maeschke's Theorem.

CoInductive mxsplits (V U : 'M_n) :=
  MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W).

Definition mx_completely_reducible V :=
   U, mxmodule U → (U V)%MSmxsplits V U.

Lemma mx_reducibleS U V :
    mxmodule U → (U V)%MS
  mx_completely_reducible Vmx_completely_reducible U.

Lemma mx_Maschke : [char F]^'.-group Gmx_completely_reducible 1%:M.

Lemma mxsemisimple_reducible V : mxsemisimple Vmx_completely_reducible V.

Lemma mx_reducible_semisimple V :
  mxmodule Vmx_completely_reducible Vclassically (mxsemisimple V).

Lemma mxsemisimpleS U V :
  mxmodule U → (U V)%MSmxsemisimple Vmxsemisimple U.

Lemma hom_mxsemisimple_iso I P U W f :
  let V := (\sum_(i : I | P i) W i)%MS in
  mxsimple U → ( i, P iW i != 0 → mxsimple (W i)) →
  (V dom_hom_mx f)%MS → (U V ×m f)%MS
  {i | P i & mx_iso (W i) U}.

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)%MSmx_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 Umxsimple V
  reflect (mx_iso U V) (component_mx U == component_mx V).

Lemma component_mx_disjoint U V :
    mxsimple Umxsimple Vcomponent_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_enummxsimple M;
  _ : M, mxsimple Mhas (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 Mcomponent_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.

Canonical socle_subType := SubType _ _ _ socle_sort_rect PackSocleK.
Definition socle_eqMixin := Eval hnf in [eqMixin of sG by <:].
Canonical socle_eqType := Eval hnf in EqType sG socle_eqMixin.
Definition socle_choiceMixin := Eval hnf in [choiceMixin of sG by <:].
Canonical socle_choiceType := ChoiceType sG socle_choiceMixin.

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

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

Definition socle_countMixin := CanCountMixin socle_finType_subproof.
Canonical socle_countType := CountType sG socle_countMixin.
Canonical socle_subCountType := [subCountType of sG].
Definition socle_finMixin := CanFinMixin socle_finType_subproof.
Canonical socle_finType := FinType sG socle_finMixin.
Canonical socle_subFinType := [subFinType of sG].

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 Umx_completely_reducible U → (U Socle)%MS.

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

Lemma reducible_Socle1 : mx_completely_reducible 1%:MSocle = 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.
Section CentHom.

Variable f : 'M[F]_n.

Lemma row_full_dom_hom : row_full (dom_hom_mx f) = centgmx rG f.

Lemma memmx_cent_envelop : (f \in 'C(E_G))%MS = centgmx rG f.

Lemma kermx_centg_module : centgmx rG fmxmodule (kermx f).

Lemma centgmx_hom m (U : 'M_(m, n)) : centgmx rG f → (U dom_hom_mx f)%MS.

End CentHom.

(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 UU != 0 → row_full U).

Schur's lemma for endomorphisms.
Lemma mx_Schur :
  mx_irreducible f, centgmx rG ff != 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 Ais_scalar_mx A.

Lemma mx_abs_irrW : mx_absolutely_irreduciblemx_irreducible.

Lemma linear_mx_abs_irr : n = 1%Nmx_absolutely_irreducible.

Lemma abelian_abs_irr : abelian Gmx_absolutely_irreducible = (n == 1%N).

End OneRepresentation.

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

Implicit Arguments val_submod_inj [n U m].
Implicit Arguments val_factmod_inj [n U m].

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 Umxmodule rH U.

End Stabilisers.

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

Lemma subg_mx_irr : mx_irreducible rHmx_irreducible rG.

Lemma subg_mx_abs_irr :
   mx_absolutely_irreducible rHmx_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 @* Dmxmodule 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)%MSmxmodule 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 rUmx_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 rGmx_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 Ggroup_splitting_field (G / H).

Lemma coset_splitting_field gT (H : {set gT}) :
  group_closure_field gTgroup_closure_field (coset_groupType 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 rGmx_irreducible rGcyclic 'Z(G).

Lemma mx_faithful_irr_abelian_cyclic n (rG : mx_representation F G n) :
  mx_faithful rGmx_irreducible rGabelian Gcyclic G.

Hypothesis splitG : group_splitting_field G.

Lemma mx_irr_abelian_linear n (rG : mx_representation F G n) :
  mx_irreducible rGabelian Gn = 1%N.

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

Lemma linear_mxsimple n (rG : mx_representation F G n) (M : 'M_n) :
  mxmodule rG M\rank M = 1%Nmxsimple 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 rGcyclic 'Z(G / rker rG)%g.

Lemma der1_sub_rker :
    group_splitting_field Gmx_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).

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

Lemma mxrank_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2n1 = 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 rG2mx_rsim rG2 rG1.

Lemma mx_rsim_trans n1 n2 n3
                    (rG1 : reprG n1) (rG2 : reprG n2) (rG3 : reprG n3) :
  mx_rsim rG1 rG2mx_rsim rG2 rG3mx_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 GrG1 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 rG2mx_irreducible rG1mx_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 rG2rker rG1 = rker rG2.

Lemma mx_rsim_faithful n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
  mx_rsim rG1 rG2mx_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)%MSmxdirect (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 Gmx_rsim rG1 rG2rG1 x = c%:MrG2 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)%MSmx_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)%MSmxdirect (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)%MSmxdirect 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 Mx \in Gmxsimple 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 Vx \in Gmx_iso rH (U ×m rG x) (V ×m rG x).

Lemma Clifford_componentJ M x :
    mxsimple rH Mx \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_tgT |
     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)%MSmax_submod U1 V1max_submod U2 V2.

Definition mx_subseries := all modG.

Definition mx_composition_series V :=
  mx_subseries V ( i, i < size Vmax_submod (0 :: V)`_i V`_i).
Local Notation mx_series := mx_composition_series.

Fact mx_subseries_module V i : mx_subseries Vmxmodule rG V`_i.

Fact mx_subseries_module' V i : mx_subseries Vmxmodule rG (0 :: V)`_i.

Definition subseries_repr V i (modV : all modG V) :=
  section_repr (mx_subseries_module' i modV) (mx_subseries_module i modV).

Definition series_repr V i (compV : mx_composition_series V) :=
  subseries_repr i (proj1 compV).

Lemma mx_series_lt V : mx_composition_series Vpath ltmx 0 V.

Lemma max_size_mx_series (V : seq 'M[F]_n) :
   path ltmx 0 Vsize V \rank (last 0 V).

Lemma mx_series_repr_irr V i (compV : mx_composition_series V) :
  i < size Vmx_irreducible (series_repr i compV).

Lemma mx_series_rcons U V :
  mx_series (rcons U V) [/\ mx_series U, modG V & max_submod (last 0 U) V].

Theorem mx_Schreier U :
    mx_subseries Upath ltmx 0 U
  classically ( V, [/\ mx_series V, last 0 V :=: 1%:M & subseq U V])%MS.

Lemma mx_second_rsim U V (modU : modG U) (modV : modG V) :
  let modI := capmx_module modU modV in let modA := addsmx_module modU modV in
  mx_rsim (section_repr modI modU) (section_repr modV modA).

Lemma section_eqmx_add U1 U2 V1 V2 modU1 modU2 modV1 modV2 :
    (U1 :=: U2)%MS → (U1 + V1 :=: U2 + V2)%MS
  mx_rsim (@section_repr U1 V1 modU1 modV1) (@section_repr U2 V2 modU2 modV2).

Lemma section_eqmx U1 U2 V1 V2 modU1 modU2 modV1 modV2
                   (eqU : (U1 :=: U2)%MS) (eqV : (V1 :=: V2)%MS) :
  mx_rsim (@section_repr U1 V1 modU1 modV1) (@section_repr U2 V2 modU2 modV2).

Lemma mx_butterfly U V W modU modV modW :
    ~~ (U == V)%MSmax_submod U Wmax_submod V W
  let modUV := capmx_module modU modV in
     max_submod (U :&: V)%MS U
   mx_rsim (@section_repr V W modV modW) (@section_repr _ U modUV modU).

Lemma mx_JordanHolder_exists U V :
    mx_composition_series UmodG Vmax_submod V (last 0 U) →
  {W : seq 'M_n | mx_composition_series W & last 0 W = V}.

Let rsim_rcons U V compU compUV i : i < size U
  mx_rsim (@series_repr U i compU) (@series_repr (rcons U V) i compUV).

Let last_mod U (compU : mx_series U) : modG (last 0 U).

Let rsim_last U V modUm modV compUV :
  mx_rsim (@section_repr (last 0 U) V modUm modV)
          (@series_repr (rcons U V) (size U) compUV).
Local Notation rsimT := mx_rsim_trans.
Local Notation rsimC := mx_rsim_sym.

Lemma mx_JordanHolder U V compU compV :
  let m := size U in (last 0 U :=: last 0 V)%MS
  m = size V ( p : 'S_m, i : 'I_m,
     mx_rsim (@series_repr U i compU) (@series_repr V (p i) compV)).

Lemma mx_JordanHolder_max U (m := size U) V compU modV :
    (last 0 U :=: 1%:M)%MSmx_irreducible (@factmod_repr _ G n rG V modV) →
   i : 'I_m, mx_rsim (factmod_repr modV) (@series_repr U i compU).

End JordanHolder.

Section Regular.

Variables (gT : finGroupType) (G : {group gT}).
Local Notation nG := #|pred_of_set (gval G)|.

Local Notation rF := (GRing.Field.comUnitRingType F) (only parsing).
Local Notation aG := (regular_repr rF G).
Local Notation R_G := (group_ring rF G).

Lemma gring_free : row_free R_G.

Lemma gring_op_id A : (A \in R_G)%MSgring_op aG A = A.

Lemma gring_rowK A : (A \in R_G)%MSgring_mx aG (gring_row A) = A.

Lemma mem_gring_mx m a (M : 'M_(m, nG)) :
  (gring_mx aG a \in M ×m R_G)%MS = (a M)%MS.

Lemma mem_sub_gring m A (M : 'M_(m, nG)) :
  (A \in M ×m R_G)%MS = (A \in R_G)%MS && (gring_row A M)%MS.

Section GringMx.

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

Lemma gring_mxP a : (gring_mx rG a \in enveloping_algebra_mx rG)%MS.

Lemma gring_opM A B :
  (B \in R_G)%MSgring_op rG (A ×m B) = gring_op rG A ×m gring_op rG B.

Hypothesis irrG : mx_irreducible rG.

Lemma rsim_regular_factmod :
  {U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (factmod_repr modU)}}.

Lemma rsim_regular_series U (compU : mx_composition_series aG U) :
    (last 0 U :=: 1%:M)%MS
   i : 'I_(size U), mx_rsim rG (series_repr i compU).

Hypothesis F'G : [char F]^'.-group G.

Lemma rsim_regular_submod :
  {U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (submod_repr modU)}}.

End GringMx.

Definition gset_mx (A : {set gT}) := \sum_(x in A) aG x.

Local Notation tG := #|pred_of_set (classes (gval G))|.

Definition classg_base := \matrix_(k < tG) mxvec (gset_mx (enum_val k)).

Let groupCl : {in G, x, {subset x ^: G G}}.

Lemma classg_base_free : row_free classg_base.

Lemma classg_base_center : (classg_base :=: 'Z(R_G))%MS.

Lemma regular_module_ideal m (M : 'M_(m, nG)) :
  mxmodule aG M = right_mx_ideal R_G (M ×m R_G).

Definition irrType := socleType aG.
Identity Coercion type_of_irrType : irrType >-> socleType.

Variable sG : irrType.

Definition irr_degree (i : sG) := \rank (socle_base i).
Local Notation "'n_ i" := (irr_degree i) : group_ring_scope.
Local Open Scope group_ring_scope.

Lemma irr_degreeE i : 'n_i = \rank (socle_base i).
Lemma irr_degree_gt0 i : 'n_i > 0.

Definition irr_repr i : mx_representation F G 'n_i := socle_repr i.
Lemma irr_reprE i x : irr_repr i x = submod_mx (socle_module i) x.

Lemma rfix_regular : (rfix_mx aG G :=: gring_row (gset_mx G))%MS.

Lemma principal_comp_subproof : mxsimple aG (rfix_mx aG G).

Fact principal_comp_key : unit.
Definition principal_comp_def :=
  PackSocle (component_socle sG principal_comp_subproof).
Definition principal_comp := locked_with principal_comp_key principal_comp_def.
Local Notation "1" := principal_comp : irrType_scope.

Lemma irr1_rfix : (1%irr :=: rfix_mx aG G)%MS.

Lemma rank_irr1 : \rank 1%irr = 1%N.

Lemma degree_irr1 : 'n_1 = 1%N.

Definition Wedderburn_subring (i : sG) := <<i ×m R_G>>%MS.

Local Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope.

Let sums_R : (\sum_i 'R_i :=: Socle sG ×m R_G)%MS.

Lemma Wedderburn_ideal i : mx_ideal R_G 'R_i.

Lemma Wedderburn_direct : mxdirect (\sum_i 'R_i)%MS.

Lemma Wedderburn_disjoint i j : i != j → ('R_i :&: 'R_j)%MS = 0.

Lemma Wedderburn_annihilate i j : i != j → ('R_i × 'R_j)%MS = 0.

Lemma Wedderburn_mulmx0 i j A B :
  i != j → (A \in 'R_i)%MS → (B \in 'R_j)%MSA ×m B = 0.

Hypothesis F'G : [char F]^'.-group G.

Lemma irr_mx_sum : (\sum_(i : sG) i = 1%:M)%MS.

Lemma Wedderburn_sum : (\sum_i 'R_i :=: R_G)%MS.

Definition Wedderburn_id i :=
  vec_mx (mxvec 1%:M ×m proj_mx 'R_i (\sum_(j | j != i) 'R_j)%MS).

Local Notation "''e_' i" := (Wedderburn_id i) : group_ring_scope.

Lemma Wedderburn_sum_id : \sum_i 'e_i = 1%:M.

Lemma Wedderburn_id_mem i : ('e_i \in 'R_i)%MS.

Lemma Wedderburn_is_id i : mxring_id 'R_i 'e_i.

Lemma Wedderburn_closed i : ('R_i × 'R_i = 'R_i)%MS.

Lemma Wedderburn_is_ring i : mxring 'R_i.

Lemma Wedderburn_min_ideal m i (E : 'A_(m, nG)) :
  E != 0 → (E 'R_i)%MSmx_ideal R_G E → (E :=: 'R_i)%MS.

Section IrrComponent.

The component of the socle of the regular module that is associated to an irreducible representation.

Variables (n : nat) (rG : mx_representation F G n).
Local Notation E_G := (enveloping_algebra_mx rG).

Let not_rsim_op0 (iG j : sG) A :
    mx_rsim rG (socle_repr iG) → iG != j → (A \in 'R_j)%MS
  gring_op rG A = 0.

Definition irr_comp := odflt 1%irr [pick i | gring_op rG 'e_i != 0].
Local Notation iG := irr_comp.

Hypothesis irrG : mx_irreducible rG.

Lemma rsim_irr_comp : mx_rsim rG (irr_repr iG).

Lemma irr_comp'_op0 j A : j != iG → (A \in 'R_j)%MSgring_op rG A = 0.

Lemma irr_comp_envelop : ('R_iG ×m lin_mx (gring_op rG) :=: E_G)%MS.

Lemma ker_irr_comp_op : ('R_iG :&: kermx (lin_mx (gring_op rG)))%MS = 0.

Lemma regular_op_inj :
  {in [pred A | (A \in 'R_iG)%MS] &, injective (gring_op rG)}.

Lemma rank_irr_comp : \rank 'R_iG = \rank E_G.

End IrrComponent.

Lemma irr_comp_rsim n1 n2 rG1 rG2 :
  @mx_rsim _ G n1 rG1 n2 rG2irr_comp rG1 = irr_comp rG2.

Lemma irr_reprK i : irr_comp (irr_repr i) = i.

Lemma irr_repr'_op0 i j A :
  j != i → (A \in 'R_j)%MSgring_op (irr_repr i) A = 0.

Lemma op_Wedderburn_id i : gring_op (irr_repr i) 'e_i = 1%:M.

Lemma irr_comp_id (M : 'M_nG) (modM : mxmodule aG M) (iM : sG) :
  mxsimple aG M → (M iM)%MSirr_comp (submod_repr modM) = iM.

Lemma irr1_repr x : x \in Girr_repr 1 x = 1%:M.

Hypothesis splitG : group_splitting_field G.

Lemma rank_Wedderburn_subring i : \rank 'R_i = ('n_i ^ 2)%N.

Lemma sum_irr_degree : (\sum_i 'n_i ^ 2 = nG)%N.

Lemma irr_mx_mult i : socle_mult i = 'n_i.

Lemma mxtrace_regular :
  {in G, x, \tr (aG x) = \sum_i \tr (socle_repr i x) *+ 'n_i}.

Definition linear_irr := [set i | 'n_i == 1%N].

Lemma irr_degree_abelian : abelian G i, 'n_i = 1%N.

Lemma linear_irr_comp i : 'n_i = 1%N → (i :=: socle_base i)%MS.

Lemma Wedderburn_subring_center i : ('Z('R_i) :=: mxvec 'e_i)%MS.

Lemma Wedderburn_center :
  ('Z(R_G) :=: \matrix_(i < #|sG|) mxvec 'e_(enum_val i))%MS.

Lemma card_irr : #|sG| = tG.

Section CenterMode.

Variable i : sG.

Let i0 := Ordinal (irr_degree_gt0 i).

Definition irr_mode x := irr_repr i x i0 i0.

Lemma irr_mode1 : irr_mode 1 = 1.

Lemma irr_center_scalar : {in 'Z(G), x, irr_repr i x = (irr_mode x)%:M}.

Lemma irr_modeM : {in 'Z(G) &, {morph irr_mode : x y / (x × y)%g >-> x × y}}.

Lemma irr_modeX n : {in 'Z(G), {