Library mxrepresentation

  This file provides linkage between classic Group Theory and commutative 
 algebra -- representation theory. Since general abstract linear algebra  
 is still being sorted out, we develop the required theory here on the    
 assumption that all vector spaces are matrix spaces, indeed that most    
 are row matrix spaces; our representation theory is specialized to the   
 latter case. We provide many definitions and results of representation   
 theory: matrix ring centralizer, minimal polynomial, representation,     
 enveloping algebra, reducible, irreducible and absolutely irreducible    
 representation, representation kernels, the Schur lemma, Maschke's       
 theorem, the Jacobson Density theorem, 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 r commutes    
                 with the square matrix A.                                
 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 subspace 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 (i.e., 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; here we have    
                 modU : mxmodule rG U and modV : mxmodule rG V.           
                 It 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        
                 representation, 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 A == the group sum of A in the free group ring of G -- the 
                 sum of the images of all the x \in A 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.      
    irr_degree i == the degree of irr_repr i                              
   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.                            
 Wedderburn_subring i == the subring (indeed, the component) of the free  
                 group ring of G that corresponds 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.                                          
 Wedderburn_id_mx 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.                                    
 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     
                 with D the domain of the group morphism f.               
 rconj_repr rG uB == the conjugate representation mapping x to            
                 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  
                 tensor product of the module of rG with the extension    
                 field into which f embeds the base field of rG; here     
                 f : {rmorphism F -> Fstar}.                              
      'Cl%act == the transitive action of G on the Wedderburn components  
                 of H, with nsGH : H <| G, whose existence follows from   
                 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))         
     In addition, more involved constructions are encapsulated in two     
 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 (namely the 
                 minimal polynomial of A), but much better suited for our 
                 needs.                                                   
   Here are the main definitions of MatrixGenField; they all take as      
 argument three proofs: 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 Structures (~~ is_scalar_mx A 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.             


Import GroupScope GRing.Theory.
Local Open Scope ring_scope.

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 : forall m x,
  x \in G -> cancel ((@mulmx _ m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).

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

Lemma repr_mx_unit : forall 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 Structure 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 Structure rcent_group := Group rcent_group_set.

Definition centgmx := G \subset rcent.

Lemma centgmxP : reflect (forall 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 Structure rker_group := Eval hnf in [group of rker].

Lemma rkerP : forall 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%N -> G^`(1)%g \subset rker.

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 : forall x, x \in G -> GRing.unit (rG x).

Lemma repr_mxX : forall 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 : forall 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 : forall 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 Structure 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 x => rGf (f x).

Hypothesis sGD : G \subset D.

Lemma morphim_mxE : forall 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 Structure 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 x => B *m rG x *m invmx B.

Hypothesis uB : B \in unitmx.

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

Lemma rconj_mxE : forall x, rGB x = B *m rG x *m invmx B.

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

Lemma rcent_conj : forall A, rcent rGB A = rcent rG (invmx B *m A *m B).

Lemma rstab_conj : forall 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 H => rG (repr Hx).

Section SubQuotient.

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

Lemma quo_mx_coset : forall 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 Structure quo_repr := MxRepresentation quo_mx_repr.
Local Notation rGH := quo_repr.

Lemma quo_repr_coset : forall x, x \in G -> rGH (coset H x) = rG x.

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

Lemma rstab_quo : forall 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 Structure kquo_repr :=
  @MxRepresentation _ _ _ kquo_mx (quo_mx_repr _ _).

Lemma kquo_repr_coset : forall 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}).
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 Structure 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 Structure gring_row_linear := [linear of gring_row].

Lemma gring_row_mul : forall 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 Structure gring_proj_linear x := [linear of gring_proj x].

Lemma gring_projE : {in G &, forall 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 Structure gring_mx_linear := [linear of gring_mx].

Lemma gring_mxJ : forall 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.
Canonical Structure gring_op_linear := [linear of gring_op].

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

Lemma gring_opG : forall x, x \in G -> gring_op (aG x) = rG x.

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

Lemma gring_opJ : forall A b,
  gring_op (A *m gring_mx aG b) = gring_op A *m gring_mx rG b.

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

Lemma gring_mxA : forall 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 aR -> rR}).
Local Notation "A ^f" := (map_mx (GRing.RMorphism.apply f) A) : ring_scope.
Variables (gT : finGroupType) (G : {group gT}).

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

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

Lemma map_gring_proj : forall 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 Structure map_repr := MxRepresentation map_mx_repr.
Local Notation rGf := map_repr.

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

Lemma map_reprJ : forall 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 : forall a, (gring_mx rG a)^f = gring_mx rGf a^f.

Lemma map_gring_op : forall 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 : forall 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 Structure rstabs_group := Group rstabs_group_set.

Lemma rstab_act : forall x m1 (W : 'M_(m1, n)),
  x \in rstab rG U -> (W <= U)%MS -> W *m rG x = W.

Lemma rstabs_act : forall 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, forall x, U *m rG x <= U}%MS mxmodule.

End Stabilisers.
Implicit Arguments mxmoduleP [m U].

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

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

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

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

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

Lemma mxmodule1 : mxmodule 1%:M.

Lemma mxmodule_trans : forall 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 : forall m (U : 'M_(m, n)),
    mxmodule U -> \rank U = 1%N ->
  {u : 'rV_n & {a | (U :=: u)%MS & {in G, forall x, u *m rG x = a x *: u}}}.

Lemma addsmx_module : forall m1 m2 U V,
  @mxmodule m1 U -> @mxmodule m2 V -> mxmodule (U + V)%MS.

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

Lemma capmx_module : forall m1 m2 U V,
  @mxmodule m1 U -> @mxmodule m2 V -> mxmodule (U :&: V)%MS.

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

Lemma val_submodE : forall m W, @val_submod m W = W *m val_submod 1%:M.

Lemma in_submodE : forall m W, @in_submod m W = W *m in_submod 1%:M.

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

Lemma val_submodP : forall m W, (@val_submod m W <= U)%MS.

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

Lemma val_submod_inj : forall m, injective (@val_submod m).

Lemma val_submodS : forall 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 : forall m W, (W <= U)%MS -> val_submod (@in_submod m W) = W.

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

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

Lemma mxrank_in_submod : forall 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 Structure val_factmod_linear m := [linear of @val_factmod m].
Canonical Structure in_factmod_linear m := [linear of @in_factmod m].

Lemma val_factmodE : forall m W, @val_factmod m W = W *m val_factmod 1%:M.

Lemma in_factmodE : forall m W, @in_factmod m W = W *m in_factmod 1%:M.

Lemma val_factmodP : forall m W, (@val_factmod m W <= U^C)%MS.

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

Lemma val_factmod_inj : forall m, injective (@val_factmod m).

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

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

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

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

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

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

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

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

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

Definition submod_mx of mxmodule U :=
  fun x => in_submod (val_submod 1%:M *m rG x).

Definition factmod_mx of mxmodule U :=
  fun x => in_factmod (val_factmod 1%:M *m rG x).

Hypothesis Umod : mxmodule U.

Lemma in_submodJ : forall 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 : forall 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 Structure submod_repr := MxRepresentation submod_mx_repr.

Lemma in_factmodJ : forall 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 : forall 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 Structure factmod_repr := MxRepresentation factmod_mx_repr.

 For character theory. 
Lemma mxtrace_sub_fact_mod : forall x,
  \tr (submod_repr x) + \tr (factmod_repr x) = \tr (rG x).

End Submodule.

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

Lemma envelop_mx_id : forall x, x \in G -> (rG x \in E_G)%MS.

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

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

Lemma envelop_mxM : forall A B, (A \in E_G -> B \in E_G -> A *m B \in E_G)%MS.

Lemma mxmodule_envelop : forall 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 : forall m f (W : 'M_(m, n)),
  reflect (forall x, x \in G -> W *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 : forall 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 : forall f,
  f \in unitmx -> (dom_hom_mx (invmx f) :=: dom_hom_mx f *m f)%MS.

Lemma dom_hom_mx_module : forall f, mxmodule (dom_hom_mx f).

Lemma hom_mxmodule : forall m (U : 'M_(m, n)) f,
  (U <= dom_hom_mx f)%MS -> mxmodule U -> mxmodule (U *m f).

Lemma kermx_hom_module : forall m (U : 'M_(m, n)) f,
  (U <= dom_hom_mx f)%MS -> mxmodule U -> mxmodule (U :&: kermx f)%MS.

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

Lemma proj_mx_hom : forall 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.                                               

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 : forall m (W : 'M_(m, n)) (H : {set gT}),
  reflect (forall x, x \in H -> W *m rG x = W) (W <= rfix_mx H)%MS.
Implicit Arguments rfix_mxP [m W].

Lemma rfix_mx_id : forall (H : {set gT}) x,
  x \in H -> rfix_mx H *m rG x = rfix_mx H.

Lemma rfix_mxS : forall H K : {set gT},
  H \subset K -> (rfix_mx K <= rfix_mx H)%MS.

Lemma rfix_mx_conjsg : forall (H : {set gT}) x,
  x \in G -> H \subset G -> (rfix_mx (H :^ x) :=: rfix_mx H *m rG x)%MS.

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

Lemma normal_rfix_mx_module : forall H, H <| G -> mxmodule (rfix_mx H).

Lemma rfix_mx_module : mxmodule (rfix_mx G).

Lemma rfix_mx_rstabC : forall (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 : forall 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 : forall u, (u <= cyclic_mx u)%MS.

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

Lemma cyclic_mx_module : forall u, mxmodule (cyclic_mx u).

Lemma cyclic_mx_sub : forall m u (W : 'M_(m, n)),
  mxmodule W -> (u <= W)%MS -> (cyclic_mx u <= W)%MS.

Lemma hom_cyclic_mx : forall 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 : forall 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 : forall 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 spurrrious 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 : forall U V, (U :=: V)%MS -> mx_iso U V.

Lemma mx_iso_refl : forall U, mx_iso U U.

Lemma mx_iso_sym : forall U V, mx_iso U V -> mx_iso V U.

Lemma mx_iso_trans : forall U V W, mx_iso U V -> mx_iso V W -> mx_iso U W.

Lemma mxrank_iso : forall U V, mx_iso U V -> \rank U = \rank V.

Lemma mx_iso_module : forall 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 &
      forall U : 'M_n, mxmodule U -> (U <= V)%MS -> U != 0 -> (V <= U)%MS].

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

Lemma mxsimpleP : forall U,
  [/\ mxmodule U, U != 0 & ~ mxnonsimple U] <-> mxsimple U.

Lemma mxsimple_module : forall U, mxsimple U -> mxmodule U.

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

Lemma mx_iso_simple : forall U V, mx_iso U V -> mxsimple U -> mxsimple V.

Lemma mxsimple_cyclic : forall 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 : forall 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 : forall 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. 
Lemma mx_Schur_inj_iso : forall U f,
  mxsimple U -> (U <= dom_hom_mx f)%MS -> U *m f != 0 -> mx_iso U (U *m f).

 The isomorphism part of Schur's lemma. 
Lemma mx_Schur_iso : forall 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.                   

Lemma nz_row_mxsimple : forall U, mxsimple U -> nz_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 : forall U V,
  mxsimple U -> reflect (mx_iso U V) (mxsimple_iso U V).

Lemma mxsimple_iso_simple : forall U V,
  mxsimple_iso U V -> mxsimple U -> mxsimple 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
    forall 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 : forall m I W (U : 'M_(m, n)),
    let V := (\sum_(i : I) W i)%MS in
    (forall 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 : forall I W (V : 'M_n),
    (forall 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 : forall (I : Type) r (P : pred I) W V,
    (\sum_(i <- r | P i) W i :=: V)%MS ->
    (forall i, P i -> W i != 0 -> mxsimple (W i)) ->
  mxsemisimple V.

Lemma mxsimple_semisimple : forall U, mxsimple U -> mxsemisimple U.

Lemma addsmx_semisimple : forall U V,
  mxsemisimple U -> mxsemisimple V -> mxsemisimple (U + V)%MS.

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

Lemma eqmx_semisimple : forall U V,
  (U :=: V)%MS -> mxsemisimple U -> mxsemisimple V.

Lemma hom_mxsemisimple : forall V f : 'M_n,
  mxsemisimple V -> (V <= dom_hom_mx f)%MS -> mxsemisimple (V *m f).

Lemma mxsemisimple_module : forall U, mxsemisimple U -> mxmodule 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 :=
  forall U, mxmodule U -> (U <= V)%MS -> mxsplits V U.

Lemma mx_reducibleS : forall U V,
    mxmodule U -> (U <= V)%MS ->
  mx_completely_reducible V -> mx_completely_reducible U.

Lemma mx_Maschke : [char F]^'.-group G -> mx_completely_reducible 1%:M.

Lemma mxsemisimple_reducible : forall V,
  mxsemisimple V -> mx_completely_reducible V.

Lemma mx_reducible_semisimple : forall V,
  mxmodule V -> mx_completely_reducible V -> classically (mxsemisimple V).

Lemma mxsemisimpleS : forall U V,
  mxmodule U -> (U <= V)%MS -> mxsemisimple V -> mxsemisimple U.

Lemma hom_mxsemisimple_iso : forall I P U W f,
  let V := (\sum_(i : I | P i) W i)%MS in
  mxsimple U -> (forall i, P i -> W 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.
Local Notation component_mx_expr U :=
  (\sum_i cyclic_mx (row i (row_hom_mx (nz_row U))))%MS.
Definition component_mx :=
  let: tt := component_mx_key in fun U : 'M[F]_n => component_mx_expr U.

Variable U : 'M[F]_n.
Hypothesis simU : mxsimple 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_mxE : compU = component_mx_expr U.

Lemma component_mx_module : mxmodule compU.

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

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

Lemma component_mx_semisimple : mxsemisimple compU.

Lemma mx_iso_component : forall V, mx_iso U V -> (V <= compU)%MS.

Lemma component_mx_id : (U <= compU)%MS.

Lemma hom_component_mx_iso : forall f V,
    mxsimple V -> (compU <= dom_hom_mx f)%MS -> (V <= compU *m f)%MS ->
  mx_iso U V.

Lemma component_mx_iso : forall V, mxsimple V -> (V <= compU)%MS -> mx_iso U V.

Lemma hom_component_mx : forall f,
  (compU <= dom_hom_mx f)%MS -> (compU *m f <= compU)%MS.

End Components.

Lemma component_mx_isoP : forall U V,
    mxsimple U -> mxsimple V ->
  reflect (mx_iso U V) (component_mx U == component_mx V).

Lemma component_mx_disjoint : forall 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;
  _ : forall M, M \in socle_base_enum -> mxsimple M;
  _ : forall 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 : forall 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 : forall 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 : forall W : sG, W != 0 :> 'M_n.

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

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

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

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

Fact socle_finType_subproof :
  cancel (fun W => SeqSub (socle_mem W)) (fun s => PackSocle (valP s)).

Definition socle_countMixin := CanCountMixin socle_finType_subproof.
Canonical Structure socle_countType := CountType sG socle_countMixin.
Canonical Structure socle_subCountType := [subCountType of sG].
Definition socle_finMixin := CanFinMixin socle_finType_subproof.
Canonical Structure socle_finType := FinType sG socle_finMixin.
Canonical Structure 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 : forall M,
  mxsimple M -> (M <= S)%MS -> {W : sG | P W & mx_iso (socle_base W) M}.

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

End SubSocle.

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

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

Lemma simple_Socle : forall M, mxsimple M -> (M <= Socle)%MS.

Lemma semisimple_Socle : forall U, mxsemisimple U -> (U <= Socle)%MS.

Lemma reducible_Socle : forall 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 : forall 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 f -> mxmodule (kermx f).

Lemma centgmx_hom : forall 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 /\ (forall U, @mxmodule n U -> U != 0 -> row_full U).

 Schur's lemma for endomorphisms. 
Lemma mx_Schur :
  mx_irreducible -> forall 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 /\ exists a_, forall A, A = \sum_(x \in G) a_ x A *: rG x)
          mx_absolutely_irreducible.

Lemma mx_abs_irr_cent_scalar :
  mx_absolutely_irreducible -> forall A, centgmx rG A -> is_scalar_mx A.

Lemma mx_abs_irrW : mx_absolutely_irreducible -> mx_irreducible.

Lemma linear_mx_abs_irr : n = 1%N -> mx_absolutely_irreducible.

Lemma abelian_abs_irr : abelian G -> mx_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 U -> mxmodule rH U.

End Stabilisers.

Lemma mxsimple_subg : forall 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 : forall 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 : forall 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 : forall H : {set aT},
  H \subset D -> (rfix_mx rG H :=: rfix_mx rGf (f @* H))%MS.

Lemma mxsimple_morphim : forall 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 : forall H : {set gT},
  H \subset G -> (rfix_mx rU H :=: in_submod U (U :&: rfix_mx rG H))%MS.

Lemma rfix_factmod : forall H : {set gT},
  H \subset G -> (in_factmod U (rfix_mx rG H) <= rfix_mx rU' H)%MS.

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

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

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

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

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

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

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

Lemma in_factmod_module : forall 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 : forall H : {set gT},
   (rfix_mx rGB H :=: B *m rfix_mx rG H *m invmx B)%MS.

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

Lemma mxmodule_conj : forall 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)).

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 : forall K : {group gT},
  K \subset G -> (rfix_mx rGH (K / H)%g :=: rfix_mx rG K)%MS.

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

Lemma mxmodule_quo : forall 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}) :=
  forall n (rG : mx_representation F G n),
     mx_irreducible rG -> mx_absolutely_irreducible rG.

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

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

Lemma coset_splitting_field : forall gT (H : {set gT}),
  group_closure_field gT -> group_closure_field (coset_groupType H).

End SplittingField.

Section Abelian.

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

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

Lemma mx_faithful_irr_abelian_cyclic : forall 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 : forall n (rG : mx_representation F G n),
  mx_irreducible rG -> abelian G -> n = 1%N.

Lemma mxsimple_abelian_linear : forall n (rG : mx_representation F G n) M,
  abelian G -> mxsimple rG M -> \rank M = 1%N.

Lemma linear_mxsimple : forall n (rG : mx_representation F G n) (M : 'M_n),
  mxmodule rG M -> \rank M = 1%N -> 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).

CoInductive mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop :=
  MxReprSim B of n1 = n2 & row_free B
              & forall x, x \in G -> rG1 x *m B = B *m rG2 x.

Lemma mxrank_rsim : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
  mx_rsim rG1 rG2 -> n1 = n2.

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

Lemma mx_rsim_sym : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
  mx_rsim rG1 rG2 -> mx_rsim rG2 rG1.

Lemma mx_rsim_trans :
  forall 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 : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
    mx_rsim rG1 rG2 ->
  exists B, exists2 B', B' *m B = 1%:M &
    forall x, x \in G -> rG1 x = B *m rG2 x *m B'.

Lemma mx_rsim_iso : forall n (rG : reprG n) (U V : 'M_n),
    forall (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 : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
  mx_rsim rG1 rG2 -> mx_irreducible rG1 -> mx_irreducible rG2.

Lemma mx_rsim_abs_irr : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
    mx_rsim rG1 rG2 ->
  mx_absolutely_irreducible rG1 = mx_absolutely_irreducible rG2.

Lemma rker_mx_rsim : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
  mx_rsim rG1 rG2 -> rker rG1 = rker rG2.

Lemma mx_rsim_faithful : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
  mx_rsim rG1 rG2 -> mx_faithful rG1 = mx_faithful rG2.

Lemma mx_rsim_factmod : forall n (rG : reprG n) U V,
  forall (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 : forall n1 n2 (rG1 : reprG n1) (rG2 : reprG n2),
  mx_rsim rG1 rG2 -> {in G, forall x, \tr (rG1 x) = \tr (rG2 x)}.

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 : forall W : sG, mx_irreducible (socle_repr W).

Lemma socle_rsimP : forall 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 : forall U V (modU : mG U) (modV : mG V),
  let U' := <<in_submod V U>>%MS in
    (U <= V)%MS ->
  exists modU' : mxmodule (sr modV) U', mx_rsim (sr modU) (sr modU').

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

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

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

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

Lemma mxtrace_component : forall 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, forall x, \tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.

Lemma mxtrace_Socle : let modS := Socle_module sG in
  {in G, forall 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).

Lemma Clifford_simple : forall M x,
  mxsimple rH M -> x \in G -> mxsimple rH (M *m rG x).

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

Lemma Clifford_iso : forall x U, x \in 'C_G(H) -> mx_iso rH U (U *m rG x).

Lemma Clifford_iso2 : forall 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 : forall 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 : forall 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 : forall 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 0) : action_scope.

Lemma val_Clifford_act : forall 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 : forall W : sH, (#|sH| * \rank W)%N = n.

Theorem Clifford_component_basis : forall M, mxsimple rH M ->
  {t : nat & {x_ : sH -> 'I_t -> gT |
    forall W, let sW := (\sum_j M *m rG (x_ W j))%MS in
      [/\ forall 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 : forall W : sH, 'C[W | 'Cl] = rstabs rG W.

Lemma Clifford_rstabs_simple : forall 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 : forall (U V : 'M_n) (modU : modG U),
  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 : forall U modU,
  mx_rsim (@section_repr U _ modU (mxmodule1 rG)) (factmod_repr modU).

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

Lemma max_submodP : forall 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 : forall U1 U2 V1 V2,
  (U1 :=: U2)%MS -> (V1 :=: V2)%MS -> max_submod U1 V1 -> max_submod U2 V2.

Definition mx_subseries := all modG.

Definition mx_composition_series V :=
  mx_subseries V /\ (forall i, i < size V -> max_submod (0 :: V)`_i V`_i).
Local Notation mx_series := mx_composition_series.

Fact mx_subseries_module : forall V i, mx_subseries V -> mxmodule rG V`_i.

Fact mx_subseries_module' : forall V i,
   mx_subseries V -> mxmodule 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 : forall V, mx_composition_series V -> path ltmx 0 V.

Lemma max_size_mx_series : forall V : seq 'M[F]_n,
   path ltmx 0 V -> size V <= \rank (last 0 V).

Lemma mx_series_repr_irr : forall V i (compV : mx_composition_series V),
  i < size V -> mx_irreducible (series_repr i compV).

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

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

Lemma mx_second_rsim : forall 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 : forall 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 : forall U1 U2 V1 V2 modU1 modU2 modV1 modV2,
    forall (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 : forall U V W modU modV modW,
    ~~ (U == V)%MS -> max_submod U W -> max_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 : forall U V,
    mx_composition_series U -> modG V -> max_submod V (last 0 U) ->
  {W : seq 'M_n | mx_composition_series W & last 0 W = V}.

Let rsim_rcons : forall 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 : forall U (compU : mx_series U), modG (last 0 U).

Let rsim_last : forall 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 : forall U V compU compV (m := size U),
    (last 0 U :=: last 0 V)%MS ->
  m = size V /\ (exists p : 'S_m, forall i : 'I_m,
     mx_rsim (@series_repr U i compU) (@series_repr V (p i) compV)).

Lemma mx_JordanHolder_max : forall U (m := size U) V compU modV,
    (last 0 U :=: 1%:M)%MS -> mx_irreducible (@factmod_repr _ G n rG V modV) ->
  exists 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 : forall A, (A \in R_G)%MS -> gring_op aG A = A.

Lemma gring_rowK : forall A, (A \in R_G)%MS -> gring_mx aG (gring_row A) = A.

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

Lemma mem_sub_gring : forall 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 : forall a, (gring_mx rG a \in enveloping_algebra_mx rG)%MS.

Lemma gring_opM : forall A B,
  (B \in R_G)%MS -> gring_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 : forall U (compU : mx_composition_series aG U),
    (last 0 U :=: 1%:M)%MS ->
  exists 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, forall 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 : forall 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).
Lemma irr_degreeE : forall i, irr_degree i = \rank (socle_base i).
Local Notation n_ := irr_degree.

Lemma irr_degree_gt0 : forall i, n_ i > 0.

Definition irr_repr i : mx_representation F G (n_ i) := socle_repr i.
Lemma irr_reprE : forall 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).

Definition principal_comp :=
  locked (PackSocle (component_socle sG principal_comp_subproof)).
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_ := Wedderburn_subring.

Let sums_R : (\sum_i R_ i :=: Socle sG *m R_G)%MS.

Lemma Wedderburn_ideal : forall i, mx_ideal R_G (R_ i).

Lemma Wedderburn_direct : mxdirect (\sum_i R_ i)%MS.

Lemma Wedderburn_disjoint : forall i j, i != j -> (R_ i :&: R_ j)%MS = 0.

Lemma Wedderburn_annihilate : forall i j, i != j -> (R_ i * R_ j)%MS = 0.

Lemma Wedderburn_mulmx0 : forall i j A B,
  i != j -> (A \in R_ i)%MS -> (B \in R_ j)%MS -> A *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_ := Wedderburn_id.

Lemma Wedderburn_sum_id : \sum_i e_ i = 1%:M.

Lemma Wedderburn_id_mem : forall i, (e_ i \in R_ i)%MS.

Lemma Wedderburn_is_id : forall i, mxring_id (R_ i) (e_ i).

Lemma Wedderburn_closed : forall i, (R_ i * R_ i = R_ i)%MS.

Lemma Wedderburn_is_ring : forall i, mxring (R_ i).

Lemma Wedderburn_min_ideal : forall m i (E : 'A_(m, nG)),
  E != 0 -> (E <= R_ i)%MS -> mx_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 : forall (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 : forall j A,
  j != iG -> (A \in R_ j)%MS -> gring_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 : forall n1 n2 rG1 rG2,
  @mx_rsim _ G n1 rG1 n2 rG2 -> irr_comp rG1 = irr_comp rG2.

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

Lemma irr_comp_id : forall (M : 'M_nG) (modM : mxmodule aG M) (iM : sG),
  mxsimple aG M -> (M <= iM)%MS -> irr_comp (submod_repr modM) = iM.

Lemma irr1_repr : forall x, x \in G -> irr_repr 1 x = 1%:M.

Hypothesis splitG : group_splitting_field G.

Lemma rank_Wedderburn_subring : forall i, \rank (R_ i) = (n_ i ^ 2)%N.

Lemma sum_irr_degree : (\sum_i n_ i ^ 2 = nG)%N.

Lemma irr_mx_mult : forall i, socle_mult i = n_ i.

Lemma mxtrace_regular :
  {in G, forall 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 -> forall i, n_ i = 1%N.

Lemma linear_irr_comp : forall i, n_ i = 1%N -> (i :=: socle_base i)%MS.

Lemma Wedderburn_subring_center : forall 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.


Definition irr_mode x := irr_repr i x i0 i0.

Lemma irr_mode1 : irr_mode 1 = 1.

Lemma irr_center_scalar : {in 'Z(G), forall 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 : forall n,
  {in 'Z(G), {morph irr_mode : x / (x ^+ n)%g >-> x ^+ n}}.

Lemma irr_mode_unit : {in 'Z(G), forall x, GRing.unit (irr_mode x)}.

Lemma irr_mode_neq0 : {in 'Z(G), forall x, irr_mode x != 0}.

Lemma irr_modeV : {in 'Z(G), {morph irr_mode : x / (x^-1)%g >-> x^-1}}.

End CenterMode.

Lemma irr1_mode : forall x, x \in G -> irr_mode 1 x = 1.

End Regular.

Local Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.

Section LinearIrr.

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

Lemma card_linear_irr : forall sG : irrType G,
    [char F]^'.-group G -> group_splitting_field G ->
  #|linear_irr sG| = #|G : G^`(1)|%g.

Lemma primitive_root_splitting_abelian : forall z : F,
  #|G|.-primitive_root z -> abelian G -> group_splitting_field G.

Lemma cycle_repr_structure : forall x (sG : irrType G),
    G :=: <[x]> -> [char F]^'.-group G -> group_splitting_field G ->
  exists2 w : F, #|G|.-primitive_root w &
  exists iphi : 'I_#|G| -> sG,
  [/\ bijective iphi,
      #|sG| = #|G|,
      forall i, irr_mode (iphi i) x = w ^+ i
    & forall i, irr_repr (iphi i) x = (w ^+ i)%:M].

Lemma splitting_cyclic_primitive_root :
    cyclic G -> [char F]^'.-group G -> group_splitting_field G ->
  classically {z : F | #|G|.-primitive_root z}.

End LinearIrr.

End FieldRepr.

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

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

Notation "'Cl" := (Clifford_action _) : action_scope.

Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.

Section DecideRed.

Import MatrixFormula.
Local Notation term := GRing.term.
Local Notation True := GRing.True.
Local Notation And := GRing.And (only parsing).
Local Notation morphAnd := (@big_morph _ _ _ true _ andb).
Local Notation eval := GRing.eval.
Local Notation holds := GRing.holds.
Local Notation qf_form := GRing.qf_form.
Local Notation qf_eval := GRing.qf_eval.

Section Definitions.

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

Definition mxmodule_form (U : 'M[term F]_n) :=
  \big[And/True]_(x \in G) submx_form (mulmx_term U (mx_term (rG x))) U.

Lemma mxmodule_form_qf : forall U, qf_form (mxmodule_form U).

Lemma eval_mxmodule : forall U e,
   qf_eval e (mxmodule_form U) = mxmodule rG (eval_mx e U).

Definition mxnonsimple_form (U : 'M[term F]_n) :=
  let V := vec_mx (row_var F (n * n) 0) in
  let nzV := (~ mxrank_form 0 V)%T in
  let properVU := (submx_form V U /\ ~ submx_form U V)%T in
  (Exists_row_form (n * n) 0 (mxmodule_form V /\ nzV /\ properVU))%T.

End Definitions.

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

Definition mxnonsimple_sat U :=
  GRing.sat (@row_env _ (n * n) [::]) (mxnonsimple_form rG (mx_term U)).

Lemma mxnonsimpleP : forall U,
  U != 0 -> reflect (mxnonsimple rG U) (mxnonsimple_sat U).

Lemma dec_mxsimple_exists : forall U : 'M_n,
  mxmodule rG U -> U != 0 -> {V | mxsimple rG V & V <= U}%MS.

Lemma dec_mx_reducible_semisimple : forall U,
  mxmodule rG U -> mx_completely_reducible rG U -> mxsemisimple rG U.

Lemma DecSocleType : socleType rG.

End DecideRed.

 Change of representation field (by tensoring) 
Section ChangeOfField.

Variables (aF rF : fieldType) (f : {rmorphism aF -> rF}).
Local Notation "A ^f" := (map_mx (GRing.RMorphism.apply f) A) : ring_scope.
Variables (gT : finGroupType) (G : {group gT}).

Section OneRepresentation.

Variables (n : nat) (rG : mx_representation aF G n).
Local Notation rGf := (map_repr f rG).

Lemma map_rfix_mx : forall H, (rfix_mx rG H)^f = rfix_mx rGf H.

Lemma rcent_map : forall A, rcent rGf A^f = rcent rG A.

Lemma rstab_map : forall m (U : 'M_(m, n)), rstab rGf U^f = rstab rG U.

Lemma rstabs_map : forall m (U : 'M_(m, n)), rstabs rGf U^f = rstabs rG U.

Lemma centgmx_map : forall A, centgmx rGf A^f = centgmx rG A.

Lemma mxmodule_map : forall m (U : 'M_(m, n)), mxmodule rGf U^f = mxmodule rG U.

Lemma mxsimple_map : forall U : 'M_n, mxsimple rGf U^f -> mxsimple rG U.

Lemma mx_irr_map : mx_irreducible rGf -> mx_irreducible rG.

Lemma rker_map : rker rGf = rker rG.

Lemma map_mx_faithful : mx_faithful rGf = mx_faithful rG.

Lemma map_mx_abs_irr :
  mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.

End OneRepresentation.

Lemma mx_rsim_map : forall n1 n2 rG1 rG2,
  @mx_rsim _ _ G n1 rG1 n2 rG2 -> mx_rsim (map_repr f rG1) (map_repr f rG2).

Lemma map_section_repr : forall n (rG : mx_representation aF G n) rGf U V,
    forall (modU : mxmodule rG U) (modV : mxmodule rG V),
    forall (modUf : mxmodule rGf U^f) (modVf : mxmodule rGf V^f),
  map_repr f rG =1 rGf ->
  mx_rsim (map_repr f (section_repr modU modV)) (section_repr modUf modVf).

Lemma map_regular_subseries : forall U i,
    forall modU : mx_subseries (regular_repr aF G) U,
    forall modUf : mx_subseries (regular_repr rF G) (map (fun M => M^f) U),
  mx_rsim (map_repr f (subseries_repr i modU)) (subseries_repr i modUf).

Lemma extend_group_splitting_field :
  group_splitting_field aF G -> group_splitting_field rF G.

End ChangeOfField.

 Construction of a splitting field FA of an irreducible representation, for 
 a matrix A in the centraliser of the representation. FA is the row-vector  
 space of the matrix algebra generated by A with basis 1, A, ..., A ^+ d.-1 
 or, equivalently, the polynomials in {poly F} taken mod the (irreducible)  
 minimal polynomial pA of A (of degree d).                                  
 The details of the construction of FA are encapsulated in a submodule.     
Module Import MatrixGenField.

Section GenField.

Variables (F : fieldType) (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variables (rG : mx_representation F G n) (A : 'M[F]_n).

Local Notation d := (degree_mxminpoly A).
Local Notation Ad := (powers_mx A d).
Local Notation pA := (mxminpoly A).
Local Notation irr := mx_irreducible.

Record gen_of (irrG : irr rG) (cGA : centgmx rG A) := Gen {rVval : 'rV[F]_d}.

Hypotheses (irrG : irr rG) (cGA : centgmx rG A).

Notation FA := (gen_of irrG cGA).

Canonical Structure gen_subType :=
  Eval hnf in [newType for rVval by @gen_of_rect irrG cGA].
Definition gen_eqMixin := Eval hnf in [eqMixin of FA by <:].
Canonical Structure gen_eqType := Eval hnf in EqType FA gen_eqMixin.
Definition gen_choiceMixin := [choiceMixin of FA by <:].
Canonical Structure gen_choiceType :=
  Eval hnf in ChoiceType FA gen_choiceMixin.

Definition gen0 := inFA 0.
Definition genN (x : FA) := inFA (- val x).
Definition genD (x y : FA) := inFA (val x + val y).

Lemma gen_addA : associative genD.

Lemma gen_addC : commutative genD.

Lemma gen_add0r : left_id gen0 genD.

Lemma gen_addNr : left_inverse gen0 genN genD.

Definition gen_zmodMixin := ZmodMixin gen_addA gen_addC gen_add0r gen_addNr.
Canonical Structure gen_zmodType := Eval hnf in ZmodType FA gen_zmodMixin.

Definition pval (x : FA) := rVpoly (val x).

Definition mxval (x : FA) := horner_mx A (pval x).

Definition gen (x : F) := inFA (poly_rV x%:P).

Lemma genK : forall x, mxval (gen x) = x%:M.

Lemma mxval_inj : injective mxval.

Lemma mxval0 : mxval 0 = 0.

Lemma mxvalN : {morph mxval : x / - x}.

Lemma mxvalD : {morph mxval : x y / x + y}.

Definition mxval_sum := big_morph mxval mxvalD mxval0.

Definition gen1 := inFA (poly_rV 1).
Definition genM x y := inFA (poly_rV (pval x * pval y %% pA)).
Definition genV x := inFA (poly_rV (mx_inv_horner A (mxval x)^-1)).

Lemma mxval_gen1 : mxval gen1 = 1%:M.

Lemma mxval_genM : {morph mxval : x y / genM x y >-> x *m y}.

Lemma mxval_genV : {morph mxval : x / genV x >-> invmx x}.

Lemma gen_mulA : associative genM.

Lemma gen_mulC : commutative genM.

Lemma gen_mul1r : left_id gen1 genM.

Lemma gen_mulDr : left_distributive genM +%R.

Lemma gen_ntriv : gen1 != 0.

Definition gen_ringMixin :=
  ComRingMixin gen_mulA gen_mulC gen_mul1r gen_mulDr gen_ntriv.

Canonical Structure gen_ringType := Eval hnf in RingType FA gen_ringMixin.
Canonical Structure gen_comRingType := Eval hnf in ComRingType FA gen_mulC.

Lemma mxval1 : mxval 1 = 1%:M.

Lemma mxvalM : {morph mxval : x y / x * y >-> x *m y}.

Lemma mxval_sub : additive mxval.
Canonical Structure mxval_additive := Additive mxval_sub.

Lemma mxval_is_multiplicative : multiplicative mxval.
Canonical Structure mxval_rmorphism := AddRMorphism mxval_is_multiplicative.

Lemma mxval_centg : forall x, centgmx rG (mxval x).

Lemma gen_mulVr : GRing.Field.axiom genV.

Lemma gen_invr0 : genV 0 = 0.

Definition gen_unitRingMixin := FieldUnitMixin gen_mulVr gen_invr0.
Canonical Structure gen_unitRingType :=
  Eval hnf in UnitRingType FA gen_unitRingMixin.
Canonical Structure gen_comUnitRingType :=
  Eval hnf in [comUnitRingType of FA].
Definition gen_fieldMixin :=
  @FieldMixin _ _ _ _ : GRing.Field.mixin_of gen_unitRingType.
Definition gen_idomainMixin := FieldIdomainMixin gen_fieldMixin.
Canonical Structure gen_idomainType :=
  Eval hnf in IdomainType FA gen_idomainMixin.
Canonical Structure gen_fieldType :=
  Eval hnf in FieldType FA gen_fieldMixin.

Lemma mxvalV : {morph mxval : x / x^-1 >-> invmx x}.

Lemma gen_is_rmorphism : rmorphism gen.
Canonical Structure gen_additive := Additive gen_is_rmorphism.
Canonical Structure gen_rmorphism := RMorphism gen_is_rmorphism.

 The generated field contains a root of the minimal polynomial (in some  
 cases we want to use the construction solely for that purpose).         

Definition groot := inFA (poly_rV ('X %% pA)).

Lemma mxval_groot : mxval groot = A.

Lemma mxval_grootX : forall k, mxval (groot ^+ k) = A ^+ k.

Lemma map_mxminpoly_groot : (map_poly gen pA).[groot] = 0.

 Plugging the extension morphism gen into the ext_repr construction   
 yields a (reducible) tensored representation.                           
 An alternative to the above, used in the proof of the p-stability of       
 groups of odd order, is to reconsider the original vector space as a       
 vector space of dimension n / e over FA. This is applicable only if G is   
 the largest group represented on the original vector space (i.e., if we    
 are not studying a representation of G induced by one of a larger group,   
 as in B & G Theorem 2.6 for instance). We can't fully exploit one of the   
 benefits of this approach -- that the type domain for the vector space can 
 remain unchanged -- because we're restricting ourselves to row matrices;   
 we have to use explicit bijections to convert between the two views.       

Definition subbase m (B : 'rV_m) : 'M_(m * d, n) :=
  \matrix_ik mxvec (\matrix_(i, k) (row (B 0 i) (A ^+ k))) 0 ik.

Lemma gen_dim_ex_proof : exists m, existsb B : 'rV_m, row_free (subbase B).

Lemma gen_dim_ub_proof : forall m,
   (existsb B : 'rV_m, row_free (subbase B)) -> (m <= n)%N.

Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
Notation m := gen_dim.

Definition gen_base : 'rV_m := odflt 0 [pick B | row_free (subbase B)].
Definition base := subbase gen_base.

Lemma base_free : row_free base.

Lemma base_full : row_full base.

Lemma gen_dim_factor : (m * d)%N = n.

Lemma gen_dim_gt0 : m > 0.

Section Bijection.

Variable m1 : nat.

Definition in_gen (W : 'M[F]_(m1, n)) : 'M[FA]_(m1, m) :=
  \matrix_(i, j) inFA (row j (vec_mx (row i W *m pinvmx base))).

Definition val_gen (W : 'M[FA]_(m1, m)) : 'M[F]_(m1, n) :=
  \matrix_i (mxvec (\matrix_j val (W i j)) *m base).

Lemma in_genK : cancel in_gen val_gen.

Lemma val_genK : cancel val_gen in_gen.

Lemma in_gen0 : in_gen 0 = 0.

Lemma val_gen0 : val_gen 0 = 0.

Lemma in_genN : {morph in_gen : W / - W}.

Lemma val_genN : {morph val_gen : W / - W}.

Lemma in_genD : {morph in_gen : U V / U + V}.

Lemma val_genD : {morph val_gen : U V / U + V}.

Definition in_gen_sum := big_morph in_gen in_genD in_gen0.
Definition val_gen_sum := big_morph val_gen val_genD val_gen0.

Lemma in_genZ : forall a, {morph in_gen : W / a *: W >-> gen a *: W}.

End Bijection.


Lemma val_gen_rV : forall w : 'rV_m,
  val_gen w = mxvec (\matrix_j val (w 0 j)) *m base.

Section Bijection2.

Variable m1 : nat.

Lemma val_gen_row : forall W (i : 'I_m1), val_gen (row i W) = row i (val_gen W).

Lemma in_gen_row : forall W (i : 'I_m1), in_gen (row i W) = row i (in_gen W).

Lemma row_gen_sum_mxval : forall W (i : 'I_m1),
  row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).

Lemma val_genZ : forall x, {morph @val_gen m1 : W / x *: W >-> W *m mxval x}.

End Bijection2.

Lemma submx_in_gen : forall m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)),
  (U <= V -> in_gen U <= in_gen V)%MS.

Lemma submx_in_gen_eq : forall m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)),
  (V *m A <= V -> (in_gen U <= in_gen V) = (U <= V))%MS.

Definition gen_mx g := \matrix_i in_gen (row (gen_base 0 i) (rG g)).

Let val_genJmx : forall m,
  {in G, forall g, {morph @val_gen m : W / W *m gen_mx g >-> W *m rG g}}.

Lemma gen_mx_repr : mx_repr G gen_mx.
Canonical Structure gen_repr := MxRepresentation gen_mx_repr.
Local Notation rGA := gen_repr.

Lemma val_genJ : forall m,
  {in G, forall g, {morph @val_gen m : W / W *m rGA g >-> W *m rG g}}.

Lemma in_genJ : forall m,
  {in G, forall g, {morph @in_gen m : v / v *m rG g >-> v *m rGA g}}.

Lemma rfix_gen : forall H : {set gT},
  H \subset G -> (rfix_mx rGA H :=: in_gen (rfix_mx rG H))%MS.

Definition rowval_gen m1 U :=
  <<\matrix_ik
      mxvec (\matrix_(i < m1, k < d) (row i (val_gen U) *m A ^+ k)) 0 ik>>%MS.

Lemma submx_rowval_gen : forall m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, m)),
  (U <= rowval_gen V)%MS = (in_gen U <= V)%MS.

Lemma rowval_genK : forall m1 (U : 'M_(m1, m)),
  (in_gen (rowval_gen U) :=: U)%MS.

Lemma rowval_gen_stable : forall m1 (U : 'M_(m1, m)),
  (rowval_gen U *m A <= rowval_gen U)%MS.

Lemma rstab_in_gen : forall m1 (U : 'M_(m1, n)),
  rstab rGA (in_gen U) = rstab rG U.

Lemma rstabs_in_gen : forall m1 (U : 'M_(m1, n)),
  rstabs rG U \subset rstabs rGA (in_gen U).

Lemma rstabs_rowval_gen : forall m1 (U : 'M_(m1, m)),
  rstabs rG (rowval_gen U) = rstabs rGA U.

Lemma mxmodule_rowval_gen : forall m1 (U : 'M_(m1, m)),
  mxmodule rG (rowval_gen U) = mxmodule rGA U.

Lemma gen_mx_irr : mx_irreducible rGA.

Lemma rker_gen : rker rGA = rker rG.

Lemma gen_mx_faithful : mx_faithful rGA = mx_faithful rG.

End GenField.

Section DecideGenField.

Import MatrixFormula.

Variable F : decFieldType.

Local Notation False := GRing.False.
Local Notation True := GRing.True.
Local Notation Bool b := (GRing.Bool b%bool).
Local Notation term := (GRing.term F).
Local Notation form := (GRing.formula F).

Local Notation morphAnd := (@big_morph _ _ _ true _ andb).

Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variables (rG : mx_representation F G n) (A : 'M[F]_n).
Hypotheses (irrG : mx_irreducible rG) (cGA : centgmx rG A).
Local Notation FA := (gen_of irrG cGA).
Local Notation inFA := (Gen irrG cGA).

Local Notation d := (degree_mxminpoly A).
Let d_gt0 : d > 0 := mxminpoly_nonconstant A.
Local Notation Ad := (powers_mx A d).

Let mxT (u : 'rV_d) := vec_mx (mulmx_term u (mx_term Ad)).

Let eval_mxT : forall e u, eval_mx e (mxT u) = mxval (inFA (eval_mx e u)).

Let mulT (u v : 'rV_d) := mulmx_term (mxvec (mulmx_term (mxT u) (mxT v))) Ad'T.

Lemma eval_mulT : forall e u v,
  eval_mx e (mulT u v) = val (inFA (eval_mx e u) * inFA (eval_mx e v)).

Fixpoint gen_term t := match t with
| 'X_k => row_var _ d k
| x%:T => mx_term (val (x : FA))
| n1%:R => mx_term (val (n1%:R : FA))%R
| t1 + t2 => \row_i (gen_term t1 0%R i + gen_term t2 0%R i)
| - t1 => \row_i (- gen_term t1 0%R i)
| t1 *+ n1 => mulmx_term (mx_term n1%:R%:M)%R (gen_term t1)
| t1 * t2 => mulT (gen_term t1) (gen_term t2)
| t1^-1 => gen_term t1
| t1 ^+ n1 => iter n1 (mulT (gen_term t1)) (mx_term (val (1%R : FA)))
end%T.

Definition gen_env (e : seq FA) := row_env (map val e).

Lemma nth_map_rVval : forall (e : seq FA) j, (map val e)`_j = val e`_j.

Lemma set_nth_map_rVval : forall (e : seq FA) j v,
  set_nth 0 (map val e) j v = map val (set_nth 0 e j (inFA v)).

Lemma eval_gen_term : forall e t,
  GRing.rterm t -> eval_mx (gen_env e) (gen_term t) = val (GRing.eval e t).

 WARNING: Coq will core dump if the Notation Bool is used in the match 
 pattern here.                                                         
Fixpoint gen_form f := match f with
| GRing.Bool b => Bool b
| t1 == t2 => mxrank_form 0 (gen_term (t1 - t2))
| GRing.Unit t1 => mxrank_form 1 (gen_term t1)
| f1 /\ f2 => gen_form f1 /\ gen_form f2
| f1 \/ f2 => gen_form f1 \/ gen_form f2
| f1 ==> f2 => gen_form f1 ==> gen_form f2
| ~ f1 => ~ gen_form f1
| ('exists 'X_k, f1) => Exists_row_form d k (gen_form f1)
| ('forall 'X_k, f1) => ~ Exists_row_form d k (~ (gen_form f1))
end%T.

Lemma sat_gen_form : forall e f, GRing.rformula f ->
  reflect (GRing.holds e f) (GRing.sat (gen_env e) (gen_form f)).

Definition gen_sat e f := GRing.sat (gen_env e) (gen_form (GRing.to_rform f)).

Lemma gen_satP : GRing.DecidableField.axiom gen_sat.

Definition gen_decFieldMixin := DecFieldMixin gen_satP.

Canonical Structure gen_decFieldType :=
  Eval hnf in DecFieldType FA gen_decFieldMixin.

End DecideGenField.

Section FiniteGenField.

Variables (F : finFieldType) (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variables (rG : mx_representation F G n) (A : 'M[F]_n).
Hypotheses (irrG : mx_irreducible rG) (cGA : centgmx rG A).
Notation FA := (gen_of irrG cGA).

 This should be [countMixin of FA by <:]
Definition gen_countMixin := (sub_countMixin (gen_subType irrG cGA)).
Canonical Structure gen_countType := Eval hnf in CountType FA gen_countMixin.
Canonical Structure gen_subCountType := Eval hnf in [subCountType of FA].
Definition gen_finMixin := [finMixin of FA by <:].
Canonical Structure gen_finType := Eval hnf in FinType FA gen_finMixin.
Canonical Structure gen_subFinType := Eval hnf in [subFinType of FA].
Canonical Structure gen_finZmodType := Eval hnf in [finZmodType of FA].
Canonical Structure gen_baseFinGroupType :=
  Eval hnf in [baseFinGroupType of FA for +%R].
Canonical Structure gen_finGroupType :=
  Eval hnf in [finGroupType of FA for +%R].
Canonical Structure gen_finRingType := Eval hnf in [finRingType of FA].
Canonical Structure gen_finComRingType := Eval hnf in [finComRingType of FA].
Canonical Structure gen_finUnitRingType := Eval hnf in [finUnitRingType of FA].
Canonical Structure gen_finComUnitRingType :=
   Eval hnf in [finComUnitRingType of FA].
Canonical Structure gen_finIdomainType := Eval hnf in [finIdomainType of FA].
Canonical Structure gen_finFieldType := Eval hnf in [finFieldType of FA].

Lemma card_gen : #|{:FA}| = (#|F| ^ degree_mxminpoly A)%N.

End FiniteGenField.

End MatrixGenField.

Canonical Structure gen_subType.
Canonical Structure gen_eqType.
Canonical Structure gen_choiceType.
Canonical Structure gen_countType.
Canonical Structure gen_subCountType.
Canonical Structure gen_finType.
Canonical Structure gen_subFinType.
Canonical Structure gen_zmodType.
Canonical Structure gen_finZmodType.
Canonical Structure gen_baseFinGroupType.
Canonical Structure gen_finGroupType.
Canonical Structure gen_ringType.
Canonical Structure gen_finRingType.
Canonical Structure gen_comRingType.
Canonical Structure gen_finComRingType.
Canonical Structure gen_unitRingType.
Canonical Structure gen_finUnitRingType.
Canonical Structure gen_comUnitRingType.
Canonical Structure gen_finComUnitRingType.
Canonical Structure gen_idomainType.
Canonical Structure gen_finIdomainType.
Canonical Structure gen_fieldType.
Canonical Structure gen_finFieldType.
Canonical Structure gen_decFieldType.

 Classical splitting and closure field constructions provide convenient     
 packaging for the pointwise construction.                                  
Section BuildSplittingField.

Implicit Type gT : finGroupType.
Implicit Type F : fieldType.

Lemma group_splitting_field_exists : forall gT (G : {group gT}) F,
  classically {Fs : fieldType & {rmorphism F -> Fs}
                              & group_splitting_field Fs G}.

Lemma group_closure_field_exists : forall gT F,
  classically {Fs : fieldType & {rmorphism F -> Fs}
                              & group_closure_field Fs gT}.

End BuildSplittingField.