# Library mathcomp.character.mxrepresentation

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg poly polydiv finset fingroup morphism.
From mathcomp Require Import perm automorphism quotient finalg action zmodp.
From mathcomp Require Import commutator cyclic center pgroup matrix mxalgebra.
From mathcomp Require Import mxpoly.
This file provides linkage between classic Group Theory and commutative algebra -- representation theory. Since general abstract linear algebra is still being sorted out, we develop the required theory here on the assumption that all vector spaces are matrix spaces, indeed that most are row matrix spaces; our representation theory is specialized to the latter case. We provide many definitions and results of representation theory: enveloping algebras, reducible, irreducible and absolutely irreducible representations, representation centralisers, submodules and kernels, simple and semisimple modules, the Schur lemmas, Maschke's theorem, components, socles, homomorphisms and isomorphisms, the Jacobson density theorem, similar representations, the Jordan-Holder theorem, Clifford's theorem and Wedderburn components, regular representations and the Wedderburn structure theorem for semisimple group rings, and the construction of a splitting field of an irreducible representation, and of reduced, tensored, and factored representations. mx_representation F G n == the Structure type for representations of G with n x n matrices with coefficients in F. Note that rG : mx_representation F G n coerces to a function from the element type of G to 'M_n, and conversely all such functions have a Canonical mx_representation. mx_repr G r <-> r : gT -> 'M_n defines a (matrix) group representation on G : {set gT} (Prop predicate). enveloping_algebra_mx rG == a #|G| x (n ^ 2) matrix whose rows are the mxvec encodings of the image of G under rG, and whose row space therefore encodes the enveloping algebra of the representation of G. rker rG == the kernel of the representation of r on G, i.e., the subgroup of elements of G mapped to the identity by rG. mx_faithful rG == the representation rG of G is faithful (its kernel is trivial). rfix_mx rG H == an n x n matrix whose row space is the set of vectors fixed (centralised) by the representation of H by rG. rcent rG A == the subgroup of G whose representation via rG commutes with the square matrix A. rcenter rG == the subgroup of G whose representation via rG consists of scalar matrices. centgmx rG f <=> f commutes with every matrix in the representation of G (i.e., f is a total rG-homomorphism). rstab rG U == the subgroup of G whose representation via r fixes all vectors in U, pointwise. rstabs rG U == the subgroup of G whose representation via r fixes the row space of U globally. mxmodule rG U <=> the row-space of the matrix U is a module (globally invariant) under the representation rG of G. max_submod rG U V <-> U < V and U is not a proper of any proper rG-submodule of V (if both U and V are modules, then U is a maximal proper submodule of V). mx_subseries rG Us <=> Us : seq 'M_n is a list of rG-modules mx_composition_series rG Us <-> Us is an increasing composition series for an rG-module (namely, last 0 Us). mxsimple rG M <-> M is a simple rG-module (i.e., minimal and nontrivial) This is a Prop predicate on square matrices. mxnonsimple rG U <-> U is constructively not a submodule, that is, U contains a proper nontrivial submodule. mxnonsimple_sat rG U == U is not a simple as an rG-module. This is a bool predicate, which requires a decField structure on the scalar field. mxsemisimple rG W <-> W is constructively a direct sum of simple modules. mxsplits rG V U <-> V splits over U in rG, i.e., U has an rG-invariant complement in V. mx_completely_reducible rG V <-> V splits over all its submodules; note that this is only classically equivalent to stating that V is semisimple. mx_irreducible rG <-> the representation rG is irreducible, i.e., the full module 1%:M of rG is simple. mx_absolutely_irreducible rG == the representation rG of G is absolutely irreducible: its enveloping algebra is the full matrix ring. This is only classically equivalent to the more standard ``rG does not reduce in any field extension''. group_splitting_field F G <-> F is a splitting field for the group G: every irreducible representation of G is absolutely irreducible. Any field can be embedded classically into a splitting field. group_closure_field F gT <-> F is a splitting field for every group G : {group gT}, and indeed for any section of such a group. This is a convenient constructive substitute for algebraic closures, that can be constructed classically. dom_hom_mx rG f == a square matrix encoding the set of vectors for which multiplication by the n x n matrix f commutes with the representation of G, i.e., the largest domain on which f is an rG homomorphism. mx_iso rG U V <-> U and V are (constructively) rG-isomorphic; this is a Prop predicate. mx_simple_iso rG U V == U and V are rG-isomorphic if one of them is simple; this is a bool predicate. cyclic_mx rG u == the cyclic rG-module generated by the row vector u annihilator_mx rG u == the annihilator of the row vector u in the enveloping algebra the representation rG. row_hom_mx rG u == the image of u by the set of all rG-homomorphisms on its cyclic module, or, equivalently, the null-space of the annihilator of u. component_mx rG M == when M is a simple rG-module, the component of M in the representation rG, i.e. the module generated by all the (simple) modules rG-isomorphic to M. socleType rG == a Structure that represents the type of all components of rG (more precisely, it coerces to such a type via socle_sort). For sG : socleType, values of type sG (to be exact, socle_sort sG) coerce to square matrices. For any representation rG we can construct sG : socleType rG classically; the socleType structure encapsulates this use of classical logic. DecSocleType rG == a socleType rG structure, for a representation over a decidable field type. DecSocleType rG is opaque. socle_base W == for W : (sG : socleType), a simple module whose component is W; socle_simple W and socle_module W are proofs that socle_base W is a simple module. socle_mult W == the multiplicity of socle_base W in W : sG. := \rank W %/ \rank (socle_base W) Socle sG == the Socle of rG, given sG : socleType rG, i.e., the (direct) sum of all the components of rG. mx_rsim rG rG' <-> rG and rG' are similar representations of the same group G. Note that rG and rG' must then have equal, but not necessarily convertible, degree. submod_repr modU == a representation of G on 'rV_(\rank U) equivalent to the restriction of rG to U (here modU : mxmodule rG U). socle_repr W := submod_repr (socle_module W) val/in_submod rG U == the projections resp. from/onto 'rV_(\rank U), that correspond to submod_repr r G U (these work both on vectors and row spaces). factmod_repr modV == a representation of G on 'rV_(\rank (cokermx V)) that is equivalent to the factor module 'rV_n / V induced by V and rG (here modV : mxmodule rG V). val/in_factmod rG U == the projections for factmod_repr r G U. section_repr modU modV == the restriction to in_factmod V U of the factor representation factmod_repr modV (for modU : mxmodule rG U and modV : mxmodule rG V); section_repr modU modV is irreducible iff max_submod rG U V. subseries_repr modUs i == the representation for the section module in_factmod (0 :: Us)`_i Us`_i, where modUs : mx_subseries rG Us. series_repr compUs i == the representation for the section module in_factmod (0 :: Us)`_i Us`_i, where compUs : mx_composition_series rG Us. The Jordan-Holder theorem asserts the uniqueness of the set of such representations, up to similarity and permutation. regular_repr F G == the regular F-representation of the group G. group_ring F G == a #|G| x #|G|^2 matrix that encodes the free group ring of G -- that is, the enveloping algebra of the regular F-representation of G. gring_index x == the index corresponding to x \in G in the matrix encoding of regular_repr and group_ring. gring_row A == the row vector corresponding to A \in group_ring F G in the regular FG-module. gring_proj x A == the 1 x 1 matrix holding the coefficient of x \in G in (A \in group_ring F G)%MS. gring_mx rG u == the image of a row vector u of the regular FG-module, in the enveloping algebra of another representation rG. gring_op rG A == the image of a matrix of the free group ring of G, in the enveloping algebra of rG. gset_mx F G C == the group sum of C in the free group ring of G -- the sum of the images of all the x \in C in group_ring F G. classg_base F G == a #|classes G| x #|G|^2 matrix whose rows encode the group sums of the conjugacy classes of G -- this is a basis of 'Z(group_ring F G)%MS. irrType F G == a type indexing irreducible representations of G over a field F, provided its characteristic does not divide the order of G; it also indexes Wedderburn subrings. := socleType (regular_repr F G) irr_repr i == the irreducible representation corresponding to the index i : irrType sG := socle_repr i as i coerces to a component matrix. 'n_i, irr_degree i == the degree of irr_repr i; the notation is only active after Open Scope group_ring_scope. linear_irr sG == the set of sG-indices of linear irreducible representations of G. irr_comp sG rG == the sG-index of the unique irreducible representation similar to rG, at least when rG is irreducible and the characteristic is coprime. irr_mode i z == the unique eigenvalue of irr_repr i z, at least when irr_repr i z is scalar (e.g., when z \in 'Z(G)). [1 sG]%irr == the index of the principal representation of G, in sG : irrType F G. The i argument of irr_repr, irr_degree and irr_mode is in the %irr scope. This notation may be replaced locally by an interpretation of 1%irr as [1 sG] for some specific irrType sG. 'R_i, Wedderburn_subring i == the subring (indeed, the component) of the free group ring of G corresponding to the component i : sG of the regular FG-module, where sG : irrType F g. In coprime characteristic the Wedderburn structure theorem asserts that the free group ring is the direct sum of these subrings; as with 'n_i above, the notation is only active in group_ring_scope. 'e_i, Wedderburn_id i == the projection of the identity matrix 1%:M on the Wedderburn subring of i : sG (with sG a socleType). In coprime characteristic this is the identity element of the subring, and the basis of its center if the field F is a splitting field. As 'R_i, 'e_i is in group_ring_scope. subg_repr rG sHG == the restriction to H of the representation rG of G; here sHG : H \subset G. eqg_repr rG eqHG == the representation rG of G viewed a a representation of H; here eqHG : G == H. morphpre_repr f rG == the representation of f @*^-1 G obtained by composing the group morphism f with rG. morphim_repr rGf sGD == the representation of G induced by a representation rGf of f @* G; here sGD : G \subset D where D is the domain of the group morphism f. rconj_repr rG uB == the conjugate representation x |-> B * rG x * B^-1; here uB : B \in unitmx. quo_repr sHK nHG == the representation of G / H induced by rG, given sHK : H \subset rker rG, and nHG : G \subset 'N(H). kquo_repr rG == the representation induced on G / rker rG by rG. map_repr f rG == the representation f \o rG, whose module is the tensor product of the module of rG with the extension field into which f : {rmorphism F -> Fstar} embeds F. 'Cl%act == the transitive action of G on the Wedderburn components of H, with nsGH : H <| G, given by Clifford's theorem. More precisely this is a total action of G on socle_sort sH, where sH : socleType (subg_repr rG (normal_sub sGH)). We build on the MatrixFormula toolkit to define decision procedures for the reducibility property: mxmodule_form rG U == a formula asserting that the interpretation of U is a module of the representation rG. mxnonsimple_form rG U == a formula asserting that the interpretation of U contains a proper nontrivial rG-module. mxnonsimple_sat rG U <=> mxnonsimple_form rG U is satisfied. More involved constructions are encapsulated in two Coq submodules: MatrixGenField == a module that encapsulates the lengthy details of the construction of appropriate extension fields. We assume we have an irreducible representation rG of a group G, and a non-scalar matrix A that centralises rG(G), as this data is readily extracted from the Jacobson density theorem. It then follows from Schur's lemma that the ring generated by A is a field on which the extension of the representation rG of G is reducible. Note that this is equivalent to the more traditional quotient of the polynomial ring by an irreducible polynomial (the minimal polynomial of A), but much better suited to our needs. Here are the main definitions of MatrixGenField; they all have three proofs as arguments: (implicit) rG : mx_repr n G, irrG : mx_irreducible rG and cGA : centgmx rG A. These ensure the validity of the construction and allow us to define Canonical instances; we assume degree_mxminpoly A > 1 (which is equivalent to ~~ is_scalar_mx A) only to prove reducibility. + gen_of irrG cGA == the carrier type of the field generated by A. It is at least equipped with a fieldType structure; we also propagate any decFieldType/finFieldType structures on the original field. + gen irrG cGA == the morphism injecting into gen_of irrG cGA. + groot irrG cGA == the root of mxminpoly A in the gen_of irrG cGA field. + pval x, rVval x, mxval x == the interpretation of x : gen_of irrG cGA as a polynomial, a row vector, and a matrix, respectively. Both irrG and cGA are implicit arguments here. + gen_repr irrG cGA == an alternative to the field extension representation, which consists in reconsidering the original module as a module over the new gen_of field, thereby DIVIDING the original dimension n by the degree of the minimal polynomial of A. This can be simpler than the extension method, is actually required by the proof that odd groups are p-stable (B & G 6.1-2, and Appendix A), but is only applicable if G is the LARGEST group represented by rG (e.g., NOT for B & G 2.6). + gen_dim A == the dimension of gen_repr irrG cGA (only depends on A). + in_gen irrG cGA W == the ROWWISE image of a matrix W : 'M[F]_(m, n), i.e., interpreting W as a sequence of m tow vectors, under the bijection from rG to gen_repr irrG cGA. The sequence length m is a maximal implicit argument passed between the explicit argument cGA and W. + val_gen W == the ROWWISE image of an 'M[gen_of irrG cGA]_(m, gen_dim A) matrix W under the bijection from gen_repr irrG cGA to rG. + rowval_gen W == the ROWSPACE image of W under the bijection from gen_repr irrG cGA to rG, i.e., a 'M[F]_n matrix whose row space is the image of the row space of W. This is the A-ideal generated by val_gen W. + gen_sat e f <=> f : GRing.formula (gen_of irrG cGA) is satisfied in environment e : seq (gen_of irrG cGA), provided F has a decFieldType structure. + gen_env e, gen_term t, gen_form f == interpretations of environments, terms, and RING formulas over gen_of irrG cGA as row vector formulae, used to construct gen_sat.
Set Implicit Arguments.
Declare Scope irrType_scope.
Declare Scope group_ring_scope.
Import GroupScope GRing.Theory.
Local Open Scope ring_scope.
Reserved Notation "''n_' i" (at level 8, i at level 2, format "''n_' i").
Reserved Notation "''R_' i" (at level 8, i at level 2, format "''R_' i").
Reserved Notation "''e_' i" (at level 8, i at level 2, format "''e_' i").
Delimit Scope irrType_scope with irr.
Section RingRepr.
Variable R : comUnitRingType.
Section OneRepresentation.
Variable gT : finGroupType.
Definition mx_repr (G : {set gT}) n (r : gT → 'M[R]_n) :=
r 1%g = 1%:M ∧ {in G &, {morph r : x y / (x × y)%g >-> x ×m y}}.
Structure mx_representation G n :=
MxRepresentation { repr_mx :> gT → 'M_n; _ : mx_repr G repr_mx }.
Variables (G : {group gT}) (n : nat) (rG : mx_representation G n).
Arguments rG _%group_scope : extra scopes.
Lemma repr_mx1 : rG 1 = 1%:M.
Lemma repr_mxM : {in G &, {morph rG : x y / (x × y)%g >-> x ×m y}}.
Lemma repr_mxK m x :
x \in G → cancel ((@mulmx R m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).
Lemma repr_mxKV m x :
x \in G → cancel ((@mulmx R m n n)^~ (rG x^-1)) (mulmx^~ (rG x)).
Lemma repr_mx_unit x : x \in G → rG x \in unitmx.
Lemma repr_mxV : {in G, {morph rG : x / x^-1%g >-> invmx x}}.
This is only used in the group ring construction below, as we only have developped the theory of matrix subalgebras for F-algebras.
Definition enveloping_algebra_mx := \matrix_(i < #|G|) mxvec (rG (enum_val i)).
Section Stabiliser.
Variables (m : nat) (U : 'M[R]_(m, n)).
Definition rstab := [set x in G | U ×m rG x == U].
Lemma rstab_sub : rstab \subset G.
Lemma rstab_group_set : group_set rstab.
Canonical rstab_group := Group rstab_group_set.
End Stabiliser.
Centralizer subgroup and central homomorphisms.
Section CentHom.
Variable f : 'M[R]_n.
Definition rcent := [set x in G | f ×m rG x == rG x ×m f].
Lemma rcent_sub : rcent \subset G.
Lemma rcent_group_set : group_set rcent.
Canonical rcent_group := Group rcent_group_set.
Definition centgmx := G \subset rcent.
Lemma centgmxP : reflect (∀ x, x \in G → f ×m rG x = rG x ×m f) centgmx.
End CentHom.
Representation kernel, and faithful representations.
Definition rker := rstab 1%:M.
Canonical rker_group := Eval hnf in [group of rker].
Lemma rkerP x : reflect (x \in G ∧ rG x = 1%:M) (x \in rker).
Lemma rker_norm : G \subset 'N(rker).
Lemma rker_normal : rker <| G.
Definition mx_faithful := rker \subset [1].
Lemma mx_faithful_inj : mx_faithful → {in G &, injective rG}.
Lemma rker_linear : n = 1 → G^`(1)%g \subset rker.
Representation center.
Definition rcenter := [set g in G | is_scalar_mx (rG g)].
Fact rcenter_group_set : group_set rcenter.
Canonical rcenter_group := Group rcenter_group_set.
Lemma rcenter_normal : rcenter <| G.
End OneRepresentation.
Arguments rkerP {gT G n rG x}.
Section Proper.
Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variable rG : mx_representation G n.
Lemma repr_mxMr : {in G &, {morph rG : x y / (x × y)%g >-> x × y}}.
Lemma repr_mxVr : {in G, {morph rG : x / (x^-1)%g >-> x^-1}}.
Lemma repr_mx_unitr x : x \in G → rG x \is a GRing.unit.
Lemma repr_mxX m : {in G, {morph rG : x / (x ^+ m)%g >-> x ^+ m}}.
End Proper.
Section ChangeGroup.
Variables (gT : finGroupType) (G H : {group gT}) (n : nat).
Variables (rG : mx_representation G n).
Section SubGroup.
Hypothesis sHG : H \subset G.
Lemma subg_mx_repr : mx_repr H rG.
Definition subg_repr := MxRepresentation subg_mx_repr.
Local Notation rH := subg_repr.
Lemma rcent_subg U : rcent rH U = H :&: rcent rG U.
Section Stabiliser.
Variables (m : nat) (U : 'M[R]_(m, n)).
Lemma rstab_subg : rstab rH U = H :&: rstab rG U.
End Stabiliser.
Lemma rker_subg : rker rH = H :&: rker rG.
Lemma subg_mx_faithful : mx_faithful rG → mx_faithful rH.
End SubGroup.
Section SameGroup.
Hypothesis eqGH : G :==: H.
Lemma eqg_repr_proof : H \subset G.
Definition eqg_repr := subg_repr eqg_repr_proof.
Local Notation rH := eqg_repr.
Lemma rcent_eqg U : rcent rH U = rcent rG U.
Section Stabiliser.
Variables (m : nat) (U : 'M[R]_(m, n)).
Lemma rstab_eqg : rstab rH U = rstab rG U.
End Stabiliser.
Lemma rker_eqg : rker rH = rker rG.
Lemma eqg_mx_faithful : mx_faithful rH = mx_faithful rG.
End SameGroup.
End ChangeGroup.
Section Morphpre.
Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Variables (G : {group rT}) (n : nat) (rG : mx_representation G n).
Lemma morphpre_mx_repr : mx_repr (f @*^-1 G) (rG \o f).
Canonical morphpre_repr := MxRepresentation morphpre_mx_repr.
Local Notation rGf := morphpre_repr.
Section Stabiliser.
Variables (m : nat) (U : 'M[R]_(m, n)).
Lemma rstab_morphpre : rstab rGf U = f @*^-1 (rstab rG U).
End Stabiliser.
Lemma rker_morphpre : rker rGf = f @*^-1 (rker rG).
End Morphpre.
Section Morphim.
Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
Variables (n : nat) (rGf : mx_representation (f @* G) n).
Definition morphim_mx of G \subset D := fun x ⇒ rGf (f x).
Hypothesis sGD : G \subset D.
Lemma morphim_mxE x : morphim_mx sGD x = rGf (f x).
Let sG_f'fG : G \subset f @*^-1 (f @* G).
Lemma morphim_mx_repr : mx_repr G (morphim_mx sGD).
Canonical morphim_repr := MxRepresentation morphim_mx_repr.
Local Notation rG := morphim_repr.
Section Stabiliser.
Variables (m : nat) (U : 'M[R]_(m, n)).
Lemma rstab_morphim : rstab rG U = G :&: f @*^-1 rstab rGf U.
End Stabiliser.
Lemma rker_morphim : rker rG = G :&: f @*^-1 (rker rGf).
End Morphim.
Section Conjugate.
Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation G n) (B : 'M[R]_n).
Definition rconj_mx of B \in unitmx := fun x ⇒ B ×m rG x ×m invmx B.
Hypothesis uB : B \in unitmx.
Lemma rconj_mx_repr : mx_repr G (rconj_mx uB).
Canonical rconj_repr := MxRepresentation rconj_mx_repr.
Local Notation rGB := rconj_repr.
Lemma rconj_mxE x : rGB x = B ×m rG x ×m invmx B.
Lemma rconj_mxJ m (W : 'M_(m, n)) x : W ×m rGB x ×m B = W ×m B ×m rG x.
Lemma rcent_conj A : rcent rGB A = rcent rG (invmx B ×m A ×m B).
Lemma rstab_conj m (U : 'M_(m, n)) : rstab rGB U = rstab rG (U ×m B).
Lemma rker_conj : rker rGB = rker rG.
Lemma conj_mx_faithful : mx_faithful rGB = mx_faithful rG.
End Conjugate.
Section Quotient.
Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variable rG : mx_representation G n.
Definition quo_mx (H : {set gT}) of H \subset rker rG & G \subset 'N(H) :=
fun Hx : coset_of H ⇒ rG (repr Hx).
Section SubQuotient.
Variable H : {group gT}.
Hypotheses (krH : H \subset rker rG) (nHG : G \subset 'N(H)).
Let nHGs := subsetP nHG.
Lemma quo_mx_coset x : x \in G → quo_mx krH nHG (coset H x) = rG x.
Lemma quo_mx_repr : mx_repr (G / H)%g (quo_mx krH nHG).
Canonical quo_repr := MxRepresentation quo_mx_repr.
Local Notation rGH := quo_repr.
Lemma quo_repr_coset x : x \in G → rGH (coset H x) = rG x.
Lemma rcent_quo A : rcent rGH A = (rcent rG A / H)%g.
Lemma rstab_quo m (U : 'M_(m, n)) : rstab rGH U = (rstab rG U / H)%g.
Lemma rker_quo : rker rGH = (rker rG / H)%g.
End SubQuotient.
Definition kquo_mx := quo_mx (subxx (rker rG)) (rker_norm rG).
Lemma kquo_mxE : kquo_mx = quo_mx (subxx (rker rG)) (rker_norm rG).
Canonical kquo_repr := @MxRepresentation _ _ _ kquo_mx (quo_mx_repr _ _).
Lemma kquo_repr_coset x :
x \in G → kquo_repr (coset (rker rG) x) = rG x.
Lemma kquo_mx_faithful : mx_faithful kquo_repr.
End Quotient.
Section Regular.
Variables (gT : finGroupType) (G : {group gT}).
Definition gcard := #|G|. (* hides the projections to set *)
Local Notation nG := gcard.
Definition gring_index (x : gT) := enum_rank_in (group1 G) x.
Lemma gring_valK : cancel enum_val gring_index.
Lemma gring_indexK : {in G, cancel gring_index enum_val}.
Definition regular_mx x : 'M[R]_nG :=
\matrix_i delta_mx 0 (gring_index (enum_val i × x)).
Lemma regular_mx_repr : mx_repr G regular_mx.
Canonical regular_repr := MxRepresentation regular_mx_repr.
Local Notation aG := regular_repr.
Definition group_ring := enveloping_algebra_mx aG.
Local Notation R_G := group_ring.
Definition gring_row : 'M[R]_nG → 'rV_nG := row (gring_index 1).
Lemma gring_row_mul A B : gring_row (A ×m B) = gring_row A ×m B.
Definition gring_proj x := row (gring_index x) \o trmx \o gring_row.
Lemma gring_projE : {in G &, ∀ x y, gring_proj x (aG y) = (x == y)%:R}.
Lemma regular_mx_faithful : mx_faithful aG.
Section GringMx.
Variables (n : nat) (rG : mx_representation G n).
Definition gring_mx := vec_mx \o mulmxr (enveloping_algebra_mx rG).
Lemma gring_mxJ a x :
x \in G → gring_mx (a ×m aG x) = gring_mx a ×m rG x.
End GringMx.
Lemma gring_mxK : cancel (gring_mx aG) gring_row.
Section GringOp.
Variables (n : nat) (rG : mx_representation G n).
Definition gring_op := gring_mx rG \o gring_row.
Lemma gring_opE a : gring_op a = gring_mx rG (gring_row a).
Lemma gring_opG x : x \in G → gring_op (aG x) = rG x.
Lemma gring_op1 : gring_op 1%:M = 1%:M.
Lemma gring_opJ A b :
gring_op (A ×m gring_mx aG b) = gring_op A ×m gring_mx rG b.
Lemma gring_op_mx b : gring_op (gring_mx aG b) = gring_mx rG b.
Lemma gring_mxA a b :
gring_mx rG (a ×m gring_mx aG b) = gring_mx rG a ×m gring_mx rG b.
End GringOp.
End Regular.
End RingRepr.
Arguments mx_representation R {gT} G%g n%N.
Arguments mx_repr {R gT} G%g {n%N} r.
Arguments group_ring R {gT} G%g.
Arguments regular_repr R {gT} G%g.
Arguments centgmxP {R gT G n rG f}.
Arguments rkerP {R gT G n rG x}.
Arguments repr_mxK {R gT G%G n%N} rG {m%N} [x%g] Gx.
Arguments repr_mxKV {R gT G%G n%N} rG {m%N} [x%g] Gx.
Arguments gring_valK {gT G%G} i%R : rename.
Arguments gring_indexK {gT G%G} x%g.
Arguments gring_mxK {R gT G%G} v%R : rename.
Section ChangeOfRing.
Variables (aR rR : comUnitRingType) (f : {rmorphism aR → rR}).
Local Notation "A ^f" := (map_mx (GRing.RMorphism.sort f) A) : ring_scope.
Variables (gT : finGroupType) (G : {group gT}).
Lemma map_regular_mx x : (regular_mx aR G x)^f = regular_mx rR G x.
Lemma map_gring_row (A : 'M_#|G|) : (gring_row A)^f = gring_row A^f.
Lemma map_gring_proj x (A : 'M_#|G|) : (gring_proj x A)^f = gring_proj x A^f.
Section OneRepresentation.
Variables (n : nat) (rG : mx_representation aR G n).
Definition map_repr_mx (f0 : aR → rR) rG0 (g : gT) : 'M_n := map_mx f0 (rG0 g).
Lemma map_mx_repr : mx_repr G (map_repr_mx f rG).
Canonical map_repr := MxRepresentation map_mx_repr.
Local Notation rGf := map_repr.
Lemma map_reprE x : rGf x = (rG x)^f.
Lemma map_reprJ m (A : 'M_(m, n)) x : (A ×m rG x)^f = A^f ×m rGf x.
Lemma map_enveloping_algebra_mx :
(enveloping_algebra_mx rG)^f = enveloping_algebra_mx rGf.
Lemma map_gring_mx a : (gring_mx rG a)^f = gring_mx rGf a^f.
Lemma map_gring_op A : (gring_op rG A)^f = gring_op rGf A^f.
End OneRepresentation.
Lemma map_regular_repr : map_repr (regular_repr aR G) =1 regular_repr rR G.
Lemma map_group_ring : (group_ring aR G)^f = group_ring rR G.
Stabilisers, etc, are only mapped properly for fields.
End ChangeOfRing.
Section FieldRepr.
Variable F : fieldType.
Section OneRepresentation.
Variable gT : finGroupType.
Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n).
Arguments rG _%group_scope : extra scopes.
Local Notation E_G := (enveloping_algebra_mx rG).
Lemma repr_mx_free x : x \in G → row_free (rG x).
Section Stabilisers.
Variables (m : nat) (U : 'M[F]_(m, n)).
Definition rstabs := [set x in G | U ×m rG x ≤ U]%MS.
Lemma rstabs_sub : rstabs \subset G.
Lemma rstabs_group_set : group_set rstabs.
Canonical rstabs_group := Group rstabs_group_set.
Lemma rstab_act x m1 (W : 'M_(m1, n)) :
x \in rstab rG U → (W ≤ U)%MS → W ×m rG x = W.
Lemma rstabs_act x m1 (W : 'M_(m1, n)) :
x \in rstabs → (W ≤ U)%MS → (W ×m rG x ≤ U)%MS.
Definition mxmodule := G \subset rstabs.
Lemma mxmoduleP : reflect {in G, ∀ x, U ×m rG x ≤ U}%MS mxmodule.
End Stabilisers.
Arguments mxmoduleP {m U}.
Lemma rstabS m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
(U ≤ V)%MS → rstab rG V \subset rstab rG U.
Lemma eqmx_rstab m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
(U :=: V)%MS → rstab rG U = rstab rG V.
Lemma eqmx_rstabs m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
(U :=: V)%MS → rstabs U = rstabs V.
Lemma eqmx_module m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
(U :=: V)%MS → mxmodule U = mxmodule V.
Lemma mxmodule0 m : mxmodule (0 : 'M_(m, n)).
Lemma mxmodule1 : mxmodule 1%:M.
Lemma mxmodule_trans m1 m2 (U : 'M_(m1, n)) (W : 'M_(m2, n)) x :
mxmodule U → x \in G → (W ≤ U → W ×m rG x ≤ U)%MS.
Lemma mxmodule_eigenvector m (U : 'M_(m, n)) :
mxmodule U → \rank U = 1 →
{u : 'rV_n & {a | (U :=: u)%MS & {in G, ∀ x, u ×m rG x = a x *: u}}}.
Lemma addsmx_module m1 m2 U V :
@mxmodule m1 U → @mxmodule m2 V → mxmodule (U + V)%MS.
Lemma sumsmx_module I r (P : pred I) U :
(∀ i, P i → mxmodule (U i)) → mxmodule (\sum_(i <- r | P i) U i)%MS.
Lemma capmx_module m1 m2 U V :
@mxmodule m1 U → @mxmodule m2 V → mxmodule (U :&: V)%MS.
Lemma bigcapmx_module I r (P : pred I) U :
(∀ i, P i → mxmodule (U i)) → mxmodule (\bigcap_(i <- r | P i) U i)%MS.
Sub- and factor representations induced by a (sub)module.
Section Submodule.
Variable U : 'M[F]_n.
Definition val_submod m : 'M_(m, \rank U) → 'M_(m, n) := mulmxr (row_base U).
Definition in_submod m : 'M_(m, n) → 'M_(m, \rank U) :=
mulmxr (invmx (row_ebase U) ×m pid_mx (\rank U)).
Lemma val_submodE m W : @val_submod m W = W ×m val_submod 1%:M.
Lemma in_submodE m W : @in_submod m W = W ×m in_submod 1%:M.
Lemma val_submod1 : (val_submod 1%:M :=: U)%MS.
Lemma val_submodP m W : (@val_submod m W ≤ U)%MS.
Lemma val_submodK m : cancel (@val_submod m) (@in_submod m).
Lemma val_submod_inj m : injective (@val_submod m).
Lemma val_submodS m1 m2 (V : 'M_(m1, \rank U)) (W : 'M_(m2, \rank U)) :
(val_submod V ≤ val_submod W)%MS = (V ≤ W)%MS.
Lemma in_submodK m W : (W ≤ U)%MS → val_submod (@in_submod m W) = W.
Lemma val_submod_eq0 m W : (@val_submod m W == 0) = (W == 0).
Lemma in_submod_eq0 m W : (@in_submod m W == 0) = (W ≤ U^C)%MS.
Lemma mxrank_in_submod m (W : 'M_(m, n)) :
(W ≤ U)%MS → \rank (in_submod W) = \rank W.
Definition val_factmod m : _ → 'M_(m, n) :=
mulmxr (row_base (cokermx U) ×m row_ebase U).
Definition in_factmod m : 'M_(m, n) → _ := mulmxr (col_base (cokermx U)).
Lemma val_factmodE m W : @val_factmod m W = W ×m val_factmod 1%:M.
Lemma in_factmodE m W : @in_factmod m W = W ×m in_factmod 1%:M.
Lemma val_factmodP m W : (@val_factmod m W ≤ U^C)%MS.
Lemma val_factmodK m : cancel (@val_factmod m) (@in_factmod m).
Lemma val_factmod_inj m : injective (@val_factmod m).
Lemma val_factmodS m1 m2 (V : 'M_(m1, _)) (W : 'M_(m2, _)) :
(val_factmod V ≤ val_factmod W)%MS = (V ≤ W)%MS.
Lemma val_factmod_eq0 m W : (@val_factmod m W == 0) = (W == 0).
Lemma in_factmod_eq0 m (W : 'M_(m, n)) : (in_factmod W == 0) = (W ≤ U)%MS.
Lemma in_factmodK m (W : 'M_(m, n)) :
(W ≤ U^C)%MS → val_factmod (in_factmod W) = W.
Lemma in_factmod_addsK m (W : 'M_(m, n)) :
(in_factmod (U + W)%MS :=: in_factmod W)%MS.
Lemma add_sub_fact_mod m (W : 'M_(m, n)) :
val_submod (in_submod W) + val_factmod (in_factmod W) = W.
Lemma proj_factmodS m (W : 'M_(m, n)) :
(val_factmod (in_factmod W) ≤ U + W)%MS.
Lemma in_factmodsK m (W : 'M_(m, n)) :
(U ≤ W)%MS → (U + val_factmod (in_factmod W) :=: W)%MS.
Lemma mxrank_in_factmod m (W : 'M_(m, n)) :
(\rank (in_factmod W) + \rank U)%N = \rank (U + W).
Definition submod_mx of mxmodule U :=
fun 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 m (W : 'M_(m, n)) x :
(W ≤ U)%MS → in_submod (W ×m rG x) = in_submod W ×m submod_mx Umod x.
Lemma val_submodJ m (W : 'M_(m, \rank U)) x :
x \in G → val_submod (W ×m submod_mx Umod x) = val_submod W ×m rG x.
Lemma submod_mx_repr : mx_repr G (submod_mx Umod).
Canonical submod_repr := MxRepresentation submod_mx_repr.
Lemma in_factmodJ m (W : 'M_(m, n)) x :
x \in G → in_factmod (W ×m rG x) = in_factmod W ×m factmod_mx Umod x.
Lemma val_factmodJ m (W : 'M_(m, \rank (cokermx U))) x :
x \in G →
val_factmod (W ×m factmod_mx Umod x) =
val_factmod (in_factmod (val_factmod W ×m rG x)).
Lemma factmod_mx_repr : mx_repr G (factmod_mx Umod).
Canonical factmod_repr := MxRepresentation factmod_mx_repr.
For character theory.
Lemma mxtrace_sub_fact_mod 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 x : x \in G → (rG x \in E_G)%MS.
Lemma envelop_mx1 : (1%:M \in E_G)%MS.
Lemma envelop_mxP A :
reflect (∃ a, A = \sum_(x in G) a x *: rG x) (A \in E_G)%MS.
Lemma envelop_mxM A B : (A \in E_G → B \in E_G → A ×m B \in E_G)%MS.
Lemma mxmodule_envelop m1 m2 (U : 'M_(m1, n)) (W : 'M_(m2, n)) A :
(mxmodule U → mxvec A ≤ E_G → W ≤ U → W ×m A ≤ U)%MS.
Module homomorphisms; any square matrix f defines a module homomorphism over some domain, namely, dom_hom_mx f.
Definition dom_hom_mx f : 'M_n :=
kermx (lin1_mx (mxvec \o mulmx (cent_mx_fun E_G f) \o lin_mul_row)).
Lemma hom_mxP m f (W : 'M_(m, n)) :
reflect (∀ x, x \in G → W ×m rG x ×m f = W ×m f ×m rG x)
(W ≤ dom_hom_mx f)%MS.
Arguments hom_mxP {m f W}.
Lemma hom_envelop_mxC m f (W : 'M_(m, n)) A :
(W ≤ dom_hom_mx f → A \in E_G → W ×m A ×m f = W ×m f ×m A)%MS.
Lemma dom_hom_invmx f :
f \in unitmx → (dom_hom_mx (invmx f) :=: dom_hom_mx f ×m f)%MS.
Lemma dom_hom_mx_module f : mxmodule (dom_hom_mx f).
Lemma hom_mxmodule m (U : 'M_(m, n)) f :
(U ≤ dom_hom_mx f)%MS → mxmodule U → mxmodule (U ×m f).
Lemma kermx_hom_module m (U : 'M_(m, n)) f :
(U ≤ dom_hom_mx f)%MS → mxmodule U → mxmodule (U :&: kermx f)%MS.
Lemma scalar_mx_hom a m (U : 'M_(m, n)) : (U ≤ dom_hom_mx a%:M)%MS.
Lemma proj_mx_hom (U V : 'M_n) :
(U :&: V = 0)%MS → mxmodule U → mxmodule V →
(U + V ≤ dom_hom_mx (proj_mx U V))%MS.
The subspace fixed by a subgroup H of G; it is a module if H <| G. The definition below is extensionally equivalent to the straightforward \bigcap_(x in H) kermx (rG x - 1%:M) but it avoids the dependency on the choice function; this allows it to commute with ring morphisms.
Definition rfix_mx (H : {set gT}) :=
let commrH := \matrix_(i < #|H|) mxvec (rG (enum_val i) - 1%:M) in
kermx (lin1_mx (mxvec \o mulmx commrH \o lin_mul_row)).
Lemma rfix_mxP m (W : 'M_(m, n)) (H : {set gT}) :
reflect (∀ x, x \in H → W ×m rG x = W) (W ≤ rfix_mx H)%MS.
Arguments rfix_mxP {m W}.
Lemma rfix_mx_id (H : {set gT}) x : x \in H → rfix_mx H ×m rG x = rfix_mx H.
Lemma rfix_mxS (H K : {set gT}) : H \subset K → (rfix_mx K ≤ rfix_mx H)%MS.
Lemma rfix_mx_conjsg (H : {set gT}) x :
x \in G → H \subset G → (rfix_mx (H :^ x) :=: rfix_mx H ×m rG x)%MS.
Lemma norm_sub_rstabs_rfix_mx (H : {set gT}) :
H \subset G → 'N_G(H) \subset rstabs (rfix_mx H).
Lemma normal_rfix_mx_module H : H <| G → mxmodule (rfix_mx H).
Lemma rfix_mx_module : mxmodule (rfix_mx G).
Lemma rfix_mx_rstabC (H : {set gT}) m (U : 'M[F]_(m, n)) :
H \subset G → (H \subset rstab rG U) = (U ≤ rfix_mx H)%MS.
The cyclic module generated by a single vector.
Definition cyclic_mx u := <<E_G ×m lin_mul_row u>>%MS.
Lemma cyclic_mxP u v :
reflect (exists2 A, A \in E_G & v = u ×m A)%MS (v ≤ cyclic_mx u)%MS.
Arguments cyclic_mxP {u v}.
Lemma cyclic_mx_id u : (u ≤ cyclic_mx u)%MS.
Lemma cyclic_mx_eq0 u : (cyclic_mx u == 0) = (u == 0).
Lemma cyclic_mx_module u : mxmodule (cyclic_mx u).
Lemma cyclic_mx_sub m u (W : 'M_(m, n)) :
mxmodule W → (u ≤ W)%MS → (cyclic_mx u ≤ W)%MS.
Lemma hom_cyclic_mx u f :
(u ≤ dom_hom_mx f)%MS → (cyclic_mx u ×m f :=: cyclic_mx (u ×m f))%MS.
The annihilator of a single vector.
Definition annihilator_mx u := (E_G :&: kermx (lin_mul_row u))%MS.
Lemma annihilator_mxP u A :
reflect (A \in E_G ∧ u ×m A = 0)%MS (A \in annihilator_mx u)%MS.
The subspace of homomorphic images of a row vector.
Definition row_hom_mx u :=
(\bigcap_j kermx (vec_mx (row j (annihilator_mx u))))%MS.
Lemma row_hom_mxP u v :
reflect (exists2 f, u ≤ dom_hom_mx f & u ×m f = v)%MS (v ≤ row_hom_mx u)%MS.
Sub-, isomorphic, simple, semisimple and completely reducible modules. All these predicates are intuitionistic (since, e.g., testing simplicity requires a splitting algorithm fo r the mas field). They are all specialized to square matrices, to avoid spurious height parameters. Module isomorphism is an intentional property in general, but it can be decided when one of the two modules is known to be simple.
Variant mx_iso (U V : 'M_n) : Prop :=
MxIso f of f \in unitmx & (U ≤ dom_hom_mx f)%MS & (U ×m f :=: V)%MS.
Lemma eqmx_iso U V : (U :=: V)%MS → mx_iso U V.
Lemma mx_iso_refl U : mx_iso U U.
Lemma mx_iso_sym U V : mx_iso U V → mx_iso V U.
Lemma mx_iso_trans U V W : mx_iso U V → mx_iso V W → mx_iso U W.
Lemma mxrank_iso U V : mx_iso U V → \rank U = \rank V.
Lemma mx_iso_module U V : mx_iso U V → mxmodule U → mxmodule V.
Simple modules (we reserve the term "irreducible" for representations).
Definition mxsimple (V : 'M_n) :=
[/\ mxmodule V, V != 0 &
∀ U : 'M_n, mxmodule U → (U ≤ V)%MS → U != 0 → (V ≤ U)%MS].
Definition mxnonsimple (U : 'M_n) :=
∃ V : 'M_n, [&& mxmodule V, (V ≤ U)%MS, V != 0 & \rank V < \rank U].
Lemma mxsimpleP U :
[/\ mxmodule U, U != 0 & ¬ mxnonsimple U] ↔ mxsimple U.
Lemma mxsimple_module U : mxsimple U → mxmodule U.
Lemma mxsimple_exists m (U : 'M_(m, n)) :
mxmodule U → U != 0 → classically (exists2 V, mxsimple V & V ≤ U)%MS.
Lemma mx_iso_simple U V : mx_iso U V → mxsimple U → mxsimple V.
Lemma mxsimple_cyclic u U :
mxsimple U → u != 0 → (u ≤ U)%MS → (U :=: cyclic_mx u)%MS.
The surjective part of Schur's lemma.
Lemma mx_Schur_onto m (U : 'M_(m, n)) V f :
mxmodule U → mxsimple V → (U ≤ dom_hom_mx f)%MS →
(U ×m f ≤ V)%MS → U ×m f != 0 → (U ×m f :=: V)%MS.
The injective part of Schur's lemma.
Lemma mx_Schur_inj U f :
mxsimple U → (U ≤ dom_hom_mx f)%MS → U ×m f != 0 → (U :&: kermx f)%MS = 0.
The injectve part of Schur's lemma, stated as isomorphism with the image.
Lemma mx_Schur_inj_iso 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 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 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 U V :
mxsimple U → reflect (mx_iso U V) (mxsimple_iso U V).
Lemma mxsimple_iso_simple 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.
Variant mxsemisimple (V : 'M_n) :=
MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
∀ i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
This is a slight generalization of Aschbacher 12.5 for finite sets.
Lemma sum_mxsimple_direct_compl m I W (U : 'M_(m, n)) :
let V := (\sum_(i : I) W i)%MS in
(∀ i : I, mxsimple (W i)) → mxmodule U → (U ≤ V)%MS →
{J : {set I} | let S := U + \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
Lemma sum_mxsimple_direct_sub I W (V : 'M_n) :
(∀ i : I, mxsimple (W i)) → (\sum_i W i :=: V)%MS →
{J : {set I} | let S := \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
Lemma mxsemisimple0 : mxsemisimple 0.
Lemma intro_mxsemisimple (I : Type) r (P : pred I) W V :
(\sum_(i <- r | P i) W i :=: V)%MS →
(∀ i, P i → W i != 0 → mxsimple (W i)) →
mxsemisimple V.
Lemma mxsimple_semisimple U : mxsimple U → mxsemisimple U.
Lemma addsmx_semisimple U V :
mxsemisimple U → mxsemisimple V → mxsemisimple (U + V)%MS.
Lemma sumsmx_semisimple (I : finType) (P : pred I) V :
(∀ i, P i → mxsemisimple (V i)) → mxsemisimple (\sum_(i | P i) V i)%MS.
Lemma eqmx_semisimple U V : (U :=: V)%MS → mxsemisimple U → mxsemisimple V.
Lemma hom_mxsemisimple (V f : 'M_n) :
mxsemisimple V → (V ≤ dom_hom_mx f)%MS → mxsemisimple (V ×m f).
Lemma mxsemisimple_module U : mxsemisimple U → mxmodule U.
Completely reducible modules, and Maeschke's Theorem.
Variant mxsplits (V U : 'M_n) :=
MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W).
Definition mx_completely_reducible V :=
∀ U, mxmodule U → (U ≤ V)%MS → mxsplits V U.
Lemma mx_reducibleS 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 V : mxsemisimple V → mx_completely_reducible V.
Lemma mx_reducible_semisimple V :
mxmodule V → mx_completely_reducible V → classically (mxsemisimple V).
Lemma mxsemisimpleS U V :
mxmodule U → (U ≤ V)%MS → mxsemisimple V → mxsemisimple U.
Lemma hom_mxsemisimple_iso I P U W f :
let V := (\sum_(i : I | P i) W i)%MS in
mxsimple U → (∀ i, P 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.
Definition component_mx_expr (U : 'M[F]_n) :=
(\sum_i cyclic_mx (row i (row_hom_mx (nz_row U))))%MS.
Definition component_mx := locked_with component_mx_key component_mx_expr.
Canonical component_mx_unfoldable := [unlockable fun component_mx].
Variable U : 'M[F]_n.
Hypothesis simU : mxsimple U.
Let u := nz_row U.
Let iso_u := row_hom_mx u.
Let nz_u : u != 0 := nz_row_mxsimple simU.
Let Uu : (u ≤ U)%MS := nz_row_sub U.
Let defU : (U :=: cyclic_mx u)%MS := mxsimple_cyclic simU nz_u Uu.
Local Notation compU := (component_mx U).
Lemma component_mx_module : mxmodule compU.
Lemma genmx_component : <<compU>>%MS = compU.
Lemma component_mx_def : {I : finType & {W : I → 'M_n |
∀ i, mx_iso U (W i) & compU = \sum_i W i}}%MS.
Lemma component_mx_semisimple : mxsemisimple compU.
Lemma mx_iso_component V : mx_iso U V → (V ≤ compU)%MS.
Lemma component_mx_id : (U ≤ compU)%MS.
Lemma hom_component_mx_iso f V :
mxsimple V → (compU ≤ dom_hom_mx f)%MS → (V ≤ compU ×m f)%MS →
mx_iso U V.
Lemma component_mx_iso V : mxsimple V → (V ≤ compU)%MS → mx_iso U V.
Lemma hom_component_mx f :
(compU ≤ dom_hom_mx f)%MS → (compU ×m f ≤ compU)%MS.
End Components.
Lemma component_mx_isoP U V :
mxsimple U → mxsimple V →
reflect (mx_iso U V) (component_mx U == component_mx V).
Lemma component_mx_disjoint U V :
mxsimple U → mxsimple V → component_mx U != component_mx V →
(component_mx U :&: component_mx V = 0)%MS.
Section Socle.
Record socleType := EnumSocle {
socle_base_enum : seq 'M[F]_n;
_ : ∀ M, M \in socle_base_enum → mxsimple M;
_ : ∀ M, mxsimple M → has (mxsimple_iso M) socle_base_enum
}.
Lemma socle_exists : classically socleType.
Section SocleDef.
Variable sG0 : socleType.
Definition socle_enum := map component_mx (socle_base_enum sG0).
Lemma component_socle M : mxsimple M → component_mx M \in socle_enum.
Inductive socle_sort : predArgType := PackSocle W of W \in socle_enum.
Local Notation sG := socle_sort.
Local Notation e0 := (socle_base_enum sG0).
Definition socle_base W := let: PackSocle W _ := W in e0`_(index W socle_enum).
Coercion socle_val W : 'M[F]_n := component_mx (socle_base W).
Definition socle_mult (W : sG) := (\rank W %/ \rank (socle_base W))%N.
Lemma socle_simple W : mxsimple (socle_base W).
Definition socle_module (W : sG) := mxsimple_module (socle_simple W).
Definition socle_repr W := submod_repr (socle_module W).
Lemma nz_socle (W : sG) : W != 0 :> 'M_n.
Lemma socle_mem (W : sG) : (W : 'M_n) \in socle_enum.
Lemma PackSocleK W e0W : @PackSocle W e0W = W :> 'M_n.
Lemma socleP (W W' : sG) : reflect (W = W') (W == W')%MS.
Fact socle_can_subproof :
cancel (fun W ⇒ SeqSub (socle_mem W)) (fun s ⇒ PackSocle (valP s)).
End SocleDef.
Coercion socle_sort : socleType >-> predArgType.
Variable sG : socleType.
Section SubSocle.
Variable P : pred sG.
Notation S := (\sum_(W : sG | P W) socle_val W)%MS.
Lemma subSocle_module : mxmodule S.
Lemma subSocle_semisimple : mxsemisimple S.
Local Notation ssimS := subSocle_semisimple.
Lemma subSocle_iso M :
mxsimple M → (M ≤ S)%MS → {W : sG | P W & mx_iso (socle_base W) M}.
Lemma capmx_subSocle m (M : 'M_(m, n)) :
mxmodule M → (M :&: S :=: \sum_(W : sG | P W) (M :&: W))%MS.
End SubSocle.
Lemma subSocle_direct P : mxdirect (\sum_(W : sG | P W) W).
Definition Socle := (\sum_(W : sG) W)%MS.
Lemma simple_Socle M : mxsimple M → (M ≤ Socle)%MS.
Lemma semisimple_Socle U : mxsemisimple U → (U ≤ Socle)%MS.
Lemma reducible_Socle U :
mxmodule U → mx_completely_reducible U → (U ≤ Socle)%MS.
Lemma genmx_Socle : <<Socle>>%MS = Socle.
Lemma reducible_Socle1 : mx_completely_reducible 1%:M → Socle = 1%:M.
Lemma Socle_module : mxmodule Socle.
Lemma Socle_semisimple : mxsemisimple Socle.
Lemma Socle_direct : mxdirect Socle.
Lemma Socle_iso M : mxsimple M → {W : sG | mx_iso (socle_base W) M}.
End Socle.
Centralizer subgroup and central homomorphisms.
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 m (U : 'M_(m, n)) : centgmx rG f → (U ≤ dom_hom_mx f)%MS.
End CentHom.
(Globally) irreducible, and absolutely irreducible representations. Note that unlike "reducible", "absolutely irreducible" can easily be decided.
Definition mx_irreducible := mxsimple 1%:M.
Lemma mx_irrP :
mx_irreducible ↔ n > 0 ∧ (∀ U, @mxmodule n U → U != 0 → row_full U).
Schur's lemma for endomorphisms.
Lemma mx_Schur :
mx_irreducible → ∀ f, centgmx rG f → f != 0 → f \in unitmx.
Definition mx_absolutely_irreducible := (n > 0) && row_full E_G.
Lemma mx_abs_irrP :
reflect (n > 0 ∧ ∃ a_, ∀ A, A = \sum_(x in G) a_ x A *: rG x)
mx_absolutely_irreducible.
Lemma mx_abs_irr_cent_scalar :
mx_absolutely_irreducible → ∀ A, centgmx rG A → is_scalar_mx A.
Lemma mx_abs_irrW : mx_absolutely_irreducible → mx_irreducible.
Lemma linear_mx_abs_irr : n = 1 → mx_absolutely_irreducible.
Lemma abelian_abs_irr : abelian G → mx_absolutely_irreducible = (n == 1).
End OneRepresentation.
Arguments mxmoduleP {gT G n rG m U}.
Arguments envelop_mxP {gT G n rG A}.
Arguments hom_mxP {gT G n rG m f W}.
Arguments rfix_mxP {gT G n rG m W}.
Arguments cyclic_mxP {gT G n rG u v}.
Arguments annihilator_mxP {gT G n rG u A}.
Arguments row_hom_mxP {gT G n rG u v}.
Arguments mxsimple_isoP {gT G n rG U V}.
Arguments socleP {gT G n rG sG0 W W'}.
Arguments mx_abs_irrP {gT G n rG}.
Arguments val_submod {n U m} W.
Arguments in_submod {n} U {m} W.
Arguments val_submodK {n U m} W : rename.
Arguments in_submodK {n U m} [W] sWU.
Arguments val_submod_inj {n U m} [W1 W2] : rename.
Arguments val_factmod {n U m} W.
Arguments in_factmod {n} U {m} W.
Arguments val_factmodK {n U m} W : rename.
Arguments in_factmodK {n} U {m} [W] sWU.
Arguments val_factmod_inj {n U m} [W1 W2] : rename.
Section Proper.
Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variable rG : mx_representation F G n.
Lemma envelop_mx_ring : mxring (enveloping_algebra_mx rG).
End Proper.
Section JacobsonDensity.
Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variable rG : mx_representation F G n.
Hypothesis irrG : mx_irreducible rG.
Local Notation E_G := (enveloping_algebra_mx rG).
Local Notation Hom_G := 'C(E_G)%MS.
Lemma mx_Jacobson_density : ('C(Hom_G) ≤ E_G)%MS.
Lemma cent_mx_scalar_abs_irr : \rank Hom_G ≤ 1 → mx_absolutely_irreducible rG.
End JacobsonDensity.
Section ChangeGroup.
Variables (gT : finGroupType) (G H : {group gT}) (n : nat).
Variables (rG : mx_representation F G n).
Section SubGroup.
Hypothesis sHG : H \subset G.
Local Notation rH := (subg_repr rG sHG).
Lemma rfix_subg : rfix_mx rH = rfix_mx rG.
Section Stabilisers.
Variables (m : nat) (U : 'M[F]_(m, n)).
Lemma rstabs_subg : rstabs rH U = H :&: rstabs rG U.
Lemma mxmodule_subg : mxmodule rG U → mxmodule rH U.
End Stabilisers.
Lemma mxsimple_subg M : mxmodule rG M → mxsimple rH M → mxsimple rG M.
Lemma subg_mx_irr : mx_irreducible rH → mx_irreducible rG.
Lemma subg_mx_abs_irr :
mx_absolutely_irreducible rH → mx_absolutely_irreducible rG.
End SubGroup.
Section SameGroup.
Hypothesis eqGH : G :==: H.
Local Notation rH := (eqg_repr rG eqGH).
Lemma rfix_eqg : rfix_mx rH = rfix_mx rG.
Section Stabilisers.
Variables (m : nat) (U : 'M[F]_(m, n)).
Lemma rstabs_eqg : rstabs rH U = rstabs rG U.
Lemma mxmodule_eqg : mxmodule rH U = mxmodule rG U.
End Stabilisers.
Lemma mxsimple_eqg M : mxsimple rH M ↔ mxsimple rG M.
Lemma eqg_mx_irr : mx_irreducible rH ↔ mx_irreducible rG.
Lemma eqg_mx_abs_irr :
mx_absolutely_irreducible rH = mx_absolutely_irreducible rG.
End SameGroup.
End ChangeGroup.
Section Morphpre.
Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Variables (G : {group rT}) (n : nat) (rG : mx_representation F G n).
Local Notation rGf := (morphpre_repr f rG).
Section Stabilisers.
Variables (m : nat) (U : 'M[F]_(m, n)).
Lemma rstabs_morphpre : rstabs rGf U = f @*^-1 (rstabs rG U).
Lemma mxmodule_morphpre : G \subset f @* D → mxmodule rGf U = mxmodule rG U.
End Stabilisers.
Lemma rfix_morphpre (H : {set aT}) :
H \subset D → (rfix_mx rGf H :=: rfix_mx rG (f @* H))%MS.
Lemma morphpre_mx_irr :
G \subset f @* D → (mx_irreducible rGf ↔ mx_irreducible rG).
Lemma morphpre_mx_abs_irr :
G \subset f @* D →
mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.
End Morphpre.
Section Morphim.
Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
Variables (n : nat) (rGf : mx_representation F (f @* G) n).
Hypothesis sGD : G \subset D.
Let sG_f'fG : G \subset f @*^-1 (f @* G).
Local Notation rG := (morphim_repr rGf sGD).
Section Stabilisers.
Variables (m : nat) (U : 'M[F]_(m, n)).
Lemma rstabs_morphim : rstabs rG U = G :&: f @*^-1 rstabs rGf U.
Lemma mxmodule_morphim : mxmodule rG U = mxmodule rGf U.
End Stabilisers.
Lemma rfix_morphim (H : {set aT}) :
H \subset D → (rfix_mx rG H :=: rfix_mx rGf (f @* H))%MS.
Lemma mxsimple_morphim M : mxsimple rG M ↔ mxsimple rGf M.
Lemma morphim_mx_irr : (mx_irreducible rG ↔ mx_irreducible rGf).
Lemma morphim_mx_abs_irr :
mx_absolutely_irreducible rG = mx_absolutely_irreducible rGf.
End Morphim.
Section Submodule.
Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation F G n) (U : 'M[F]_n) (Umod : mxmodule rG U).
Local Notation rU := (submod_repr Umod).
Local Notation rU' := (factmod_repr Umod).
Lemma rfix_submod (H : {set gT}) :
H \subset G → (rfix_mx rU H :=: in_submod U (U :&: rfix_mx rG H))%MS.
Lemma rfix_factmod (H : {set gT}) :
H \subset G → (in_factmod U (rfix_mx rG H) ≤ rfix_mx rU' H)%MS.
Lemma rstab_submod m (W : 'M_(m, \rank U)) :
rstab rU W = rstab rG (val_submod W).
Lemma rstabs_submod m (W : 'M_(m, \rank U)) :
rstabs rU W = rstabs rG (val_submod W).
Lemma val_submod_module m (W : 'M_(m, \rank U)) :
mxmodule rG (val_submod W) = mxmodule rU W.
Lemma in_submod_module m (V : 'M_(m, n)) :
(V ≤ U)%MS → mxmodule rU (in_submod U V) = mxmodule rG V.
Lemma rstab_factmod m (W : 'M_(m, n)) :
rstab rG W \subset rstab rU' (in_factmod U W).
Lemma rstabs_factmod m (W : 'M_(m, \rank (cokermx U))) :
rstabs rU' W = rstabs rG (U + val_factmod W)%MS.
Lemma val_factmod_module m (W : 'M_(m, \rank (cokermx U))) :
mxmodule rG (U + val_factmod W)%MS = mxmodule rU' W.
Lemma in_factmod_module m (V : 'M_(m, n)) :
mxmodule rU' (in_factmod U V) = mxmodule rG (U + V)%MS.
Lemma rker_submod : rker rU = rstab rG U.
Lemma rstab_norm : G \subset 'N(rstab rG U).
Lemma rstab_normal : rstab rG U <| G.
Lemma submod_mx_faithful : mx_faithful rU → mx_faithful rG.
Lemma rker_factmod : rker rG \subset rker rU'.
Lemma factmod_mx_faithful : mx_faithful rU' → mx_faithful rG.
Lemma submod_mx_irr : mx_irreducible rU ↔ mxsimple rG U.
End Submodule.
Section Conjugate.
Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation F G n) (B : 'M[F]_n).
Hypothesis uB : B \in unitmx.
Local Notation rGB := (rconj_repr rG uB).
Lemma rfix_conj (H : {set gT}) :
(rfix_mx rGB H :=: B ×m rfix_mx rG H ×m invmx B)%MS.
Lemma rstabs_conj m (U : 'M_(m, n)) : rstabs rGB U = rstabs rG (U ×m B).
Lemma mxmodule_conj m (U : 'M_(m, n)) : mxmodule rGB U = mxmodule rG (U ×m B).
Lemma conj_mx_irr : mx_irreducible rGB ↔ mx_irreducible rG.
End Conjugate.
Section Quotient.
Variables (gT : finGroupType) (G : {group gT}) (n : nat).
Variables (rG : mx_representation F G n) (H : {group gT}).
Hypotheses (krH : H \subset rker rG) (nHG : G \subset 'N(H)).
Let nHGs := subsetP nHG.
Local Notation rGH := (quo_repr krH nHG).
Local Notation E_ r := (enveloping_algebra_mx r).
Lemma quo_mx_quotient : (E_ rGH :=: E_ rG)%MS.
Lemma rfix_quo (K : {group gT}) :
K \subset G → (rfix_mx rGH (K / H)%g :=: rfix_mx rG K)%MS.
Lemma rstabs_quo m (U : 'M_(m, n)) : rstabs rGH U = (rstabs rG U / H)%g.
Lemma mxmodule_quo m (U : 'M_(m, n)) : mxmodule rGH U = mxmodule rG U.
Lemma quo_mx_irr : mx_irreducible rGH ↔ mx_irreducible rG.
End Quotient.
Section SplittingField.
Implicit Type gT : finGroupType.
Definition group_splitting_field gT (G : {group gT}) :=
∀ n (rG : mx_representation F G n),
mx_irreducible rG → mx_absolutely_irreducible rG.
Definition group_closure_field gT :=
∀ G : {group gT}, group_splitting_field G.
Lemma quotient_splitting_field gT (G : {group gT}) (H : {set gT}) :
G \subset 'N(H) → group_splitting_field G → group_splitting_field (G / H).
Lemma coset_splitting_field gT (H : {set gT}) :
group_closure_field gT → group_closure_field (coset_of H).
End SplittingField.
Section Abelian.
Variables (gT : finGroupType) (G : {group gT}).
Lemma mx_faithful_irr_center_cyclic n (rG : mx_representation F G n) :
mx_faithful rG → mx_irreducible rG → cyclic 'Z(G).
Lemma mx_faithful_irr_abelian_cyclic n (rG : mx_representation F G n) :
mx_faithful rG → mx_irreducible rG → abelian G → cyclic G.
Hypothesis splitG : group_splitting_field G.
Lemma mx_irr_abelian_linear n (rG : mx_representation F G n) :
mx_irreducible rG → abelian G → n = 1.
Lemma mxsimple_abelian_linear n (rG : mx_representation F G n) M :
abelian G → mxsimple rG M → \rank M = 1.
Lemma linear_mxsimple n (rG : mx_representation F G n) (M : 'M_n) :
mxmodule rG M → \rank M = 1 → mxsimple rG M.
End Abelian.
Section AbelianQuotient.
Variables (gT : finGroupType) (G : {group gT}).
Variables (n : nat) (rG : mx_representation F G n).
Lemma center_kquo_cyclic : mx_irreducible rG → cyclic 'Z(G / rker rG)%g.
Lemma der1_sub_rker :
group_splitting_field G → mx_irreducible rG →
(G^`(1) \subset rker rG)%g = (n == 1)%N.
End AbelianQuotient.
Section Similarity.
Variables (gT : finGroupType) (G : {group gT}).
Local Notation reprG := (mx_representation F G).
Variant mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop :=
MxReprSim B of n1 = n2 & row_free B
& ∀ x, x \in G → rG1 x ×m B = B ×m rG2 x.
Lemma mxrank_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 → n1 = n2.
Lemma mx_rsim_refl n (rG : reprG n) : mx_rsim rG rG.
Lemma mx_rsim_sym n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 → mx_rsim rG2 rG1.
Lemma mx_rsim_trans n1 n2 n3
(rG1 : reprG n1) (rG2 : reprG n2) (rG3 : reprG n3) :
mx_rsim rG1 rG2 → mx_rsim rG2 rG3 → mx_rsim rG1 rG3.
Lemma mx_rsim_def n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 →
∃ B, exists2 B', B' ×m B = 1%:M &
∀ x, x \in G → rG1 x = B ×m rG2 x ×m B'.
Lemma mx_rsim_iso n (rG : reprG n) (U V : 'M_n)
(modU : mxmodule rG U) (modV : mxmodule rG V) :
mx_rsim (submod_repr modU) (submod_repr modV) ↔ mx_iso rG U V.
Lemma mx_rsim_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 → mx_irreducible rG1 → mx_irreducible rG2.
Lemma mx_rsim_abs_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 →
mx_absolutely_irreducible rG1 = mx_absolutely_irreducible rG2.
Lemma rker_mx_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 → rker rG1 = rker rG2.
Lemma mx_rsim_faithful n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 → mx_faithful rG1 = mx_faithful rG2.
Lemma mx_rsim_factmod n (rG : reprG n) U V
(modU : mxmodule rG U) (modV : mxmodule rG V) :
(U + V :=: 1%:M)%MS → mxdirect (U + V) →
mx_rsim (factmod_repr modV) (submod_repr modU).
Lemma mxtrace_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
mx_rsim rG1 rG2 → {in G, ∀ x, \tr (rG1 x) = \tr (rG2 x)}.
Lemma mx_rsim_scalar n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) x c :
x \in G → mx_rsim rG1 rG2 → rG1 x = c%:M → rG2 x = c%:M.
End Similarity.
Section Socle.
Variables (gT : finGroupType) (G : {group gT}).
Variables (n : nat) (rG : mx_representation F G n) (sG : socleType rG).
Lemma socle_irr (W : sG) : mx_irreducible (socle_repr W).
Lemma socle_rsimP (W1 W2 : sG) :
reflect (mx_rsim (socle_repr W1) (socle_repr W2)) (W1 == W2).
Local Notation mG U := (mxmodule rG U).
Local Notation sr modV := (submod_repr modV).
Lemma mx_rsim_in_submod U V (modU : mG U) (modV : mG V) :
let U' := <<in_submod V U>>%MS in
(U ≤ V)%MS →
∃ modU' : mxmodule (sr modV) U', mx_rsim (sr modU) (sr modU').
Lemma rsim_submod1 U (modU : mG U) : (U :=: 1%:M)%MS → mx_rsim (sr modU) rG.
Lemma mxtrace_submod1 U (modU : mG U) :
(U :=: 1%:M)%MS → {in G, ∀ x, \tr (sr modU x) = \tr (rG x)}.
Lemma mxtrace_dadd_mod U V W (modU : mG U) (modV : mG V) (modW : mG W) :
(U + V :=: W)%MS → mxdirect (U + V) →
{in G, ∀ x, \tr (sr modU x) + \tr (sr modV x) = \tr (sr modW x)}.
Lemma mxtrace_dsum_mod (I : finType) (P : pred I) U W
(modU : ∀ i, mG (U i)) (modW : mG W) :
let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
{in G, ∀ x, \sum_(i | P i) \tr (sr (modU i) x) = \tr (sr modW x)}.
Lemma mxtrace_component U (simU : mxsimple rG U) :
let V := component_mx rG U in
let modV := component_mx_module rG U in let modU := mxsimple_module simU in
{in G, ∀ x, \tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.
Lemma mxtrace_Socle : let modS := Socle_module sG in
{in G, ∀ x,
\tr (sr modS x) = \sum_(W : sG) \tr (socle_repr W x) *+ socle_mult W}.
End Socle.
Section Clifford.
Variables (gT : finGroupType) (G H : {group gT}).
Hypothesis nsHG : H <| G.
Variables (n : nat) (rG : mx_representation F G n).
Let sHG := normal_sub nsHG.
Let nHG := normal_norm nsHG.
Let rH := subg_repr rG sHG.
Lemma Clifford_simple M x : mxsimple rH M → x \in G → mxsimple rH (M ×m rG x).
Lemma Clifford_hom x m (U : 'M_(m, n)) :
x \in 'C_G(H) → (U ≤ dom_hom_mx rH (rG x))%MS.
Lemma Clifford_iso x U : x \in 'C_G(H) → mx_iso rH U (U ×m rG x).
Lemma Clifford_iso2 x U V :
mx_iso rH U V → x \in G → mx_iso rH (U ×m rG x) (V ×m rG x).
Lemma Clifford_componentJ M x :
mxsimple rH M → x \in G →
(component_mx rH (M ×m rG x) :=: component_mx rH M ×m rG x)%MS.
Hypothesis irrG : mx_irreducible rG.
Lemma Clifford_basis M : mxsimple rH M →
{X : {set gT} | X \subset G &
let S := \sum_(x in X) M ×m rG x in S :=: 1%:M ∧ mxdirect S}%MS.
Variable sH : socleType rH.
Definition Clifford_act (W : sH) x :=
let Gx := subgP (subg G x) in
PackSocle (component_socle sH (Clifford_simple (socle_simple W) Gx)).
Let valWact W x : (Clifford_act W x :=: W ×m rG (sgval (subg G x)))%MS.
Fact Clifford_is_action : is_action G Clifford_act.
Definition Clifford_action := Action Clifford_is_action.
Local Notation "'Cl" := Clifford_action (at level 8) : action_scope.
Lemma val_Clifford_act W x : x \in G → ('Cl%act W x :=: W ×m rG x)%MS.
Lemma Clifford_atrans : [transitive G, on [set: sH] | 'Cl].
Lemma Clifford_Socle1 : Socle sH = 1%:M.
Lemma Clifford_rank_components (W : sH) : (#|sH| × \rank W)%N = n.
Theorem Clifford_component_basis M : mxsimple rH M →
{t : nat & {x_ : sH → 'I_t → gT |
∀ W, let sW := (\sum_j M ×m rG (x_ W j))%MS in
[/\ ∀ j, x_ W j \in G, (sW :=: W)%MS & mxdirect sW]}}.
Lemma Clifford_astab : H <*> 'C_G(H) \subset 'C([set: sH] | 'Cl).
Lemma Clifford_astab1 (W : sH) : 'C[W | 'Cl] = rstabs rG W.
Lemma Clifford_rstabs_simple (W : sH) :
mxsimple (subg_repr rG (rstabs_sub rG W)) W.
End Clifford.
Section JordanHolder.
Variables (gT : finGroupType) (G : {group gT}).
Variables (n : nat) (rG : mx_representation F G n).
Local Notation modG := ((mxmodule rG) n).
Lemma section_module (U V : 'M_n) (modU : modG U) (modV : modG V) :
mxmodule (factmod_repr modU) <<in_factmod U V>>%MS.
Definition section_repr U V (modU : modG U) (modV : modG V) :=
submod_repr (section_module modU modV).
Lemma mx_factmod_sub U modU :
mx_rsim (@section_repr U _ modU (mxmodule1 rG)) (factmod_repr modU).
Definition max_submod (U V : 'M_n) :=
(U < V)%MS ∧ (∀ W, ¬ [/\ modG W, U < W & W < V])%MS.
Lemma max_submodP U V (modU : modG U) (modV : modG V) :
(U ≤ V)%MS → (max_submod U V ↔ mx_irreducible (section_repr modU modV)).
Lemma max_submod_eqmx U1 U2 V1 V2 :
(U1 :=: U2)%MS → (V1 :=: V2)%MS → max_submod U1 V1 → max_submod U2 V2.
Definition mx_subseries := all modG.
Definition mx_composition_series V :=
mx_subseries V ∧ (∀ i, i < size V → max_submod (0 :: V)`_i V`_i).
Local Notation mx_series := mx_composition_series.
Fact mx_subseries_module V i : mx_subseries V → mxmodule rG V`_i.
Fact mx_subseries_module' 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 V : mx_composition_series V → path ltmx 0 V.
Lemma max_size_mx_series (V : seq 'M[F]_n) :
path ltmx 0 V → size V ≤ \rank (last 0 V).
Lemma mx_series_repr_irr V i (compV : mx_composition_series V) :
i < size V → mx_irreducible (series_repr i compV).
Lemma mx_series_rcons U V :
mx_series (rcons U V) ↔ [/\ mx_series U, modG V & max_submod (last 0 U) V].
Theorem mx_Schreier U :
mx_subseries U → path ltmx 0 U →
classically (∃ V, [/\ mx_series V, last 0 V :=: 1%:M & subseq U V])%MS.
Lemma mx_second_rsim U V (modU : modG U) (modV : modG V) :
let modI := capmx_module modU modV in let modA := addsmx_module modU modV in
mx_rsim (section_repr modI modU) (section_repr modV modA).
Lemma section_eqmx_add U1 U2 V1 V2 modU1 modU2 modV1 modV2 :
(U1 :=: U2)%MS → (U1 + V1 :=: U2 + V2)%MS →
mx_rsim (@section_repr U1 V1 modU1 modV1) (@section_repr U2 V2 modU2 modV2).
Lemma section_eqmx U1 U2 V1 V2 modU1 modU2 modV1 modV2
(eqU : (U1 :=: U2)%MS) (eqV : (V1 :=: V2)%MS) :
mx_rsim (@section_repr U1 V1 modU1 modV1) (@section_repr U2 V2 modU2 modV2).
Lemma mx_butterfly U V W modU modV modW :
~~ (U == V)%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 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 U V compU compUV i : i < size U →
mx_rsim (@series_repr U i compU) (@series_repr (rcons U V) i compUV).
Let last_mod U (compU : mx_series U) : modG (last 0 U).
Let rsim_last U V modUm modV compUV :
mx_rsim (@section_repr (last 0 U) V modUm modV)
(@series_repr (rcons U V) (size U) compUV).
Local Notation rsimT := mx_rsim_trans.
Local Notation rsimC := mx_rsim_sym.
Lemma mx_JordanHolder U V compU compV :
let m := size U in (last 0 U :=: last 0 V)%MS →
m = size V ∧ (∃ p : 'S_m, ∀ i : 'I_m,
mx_rsim (@series_repr U i compU) (@series_repr V (p i) compV)).
Lemma mx_JordanHolder_max U (m := size U) V compU modV :
(last 0 U :=: 1%:M)%MS → mx_irreducible (@factmod_repr _ G n rG V modV) →
∃ i : 'I_m, mx_rsim (factmod_repr modV) (@series_repr U i compU).
End JordanHolder.
Bind Scope irrType_scope with socle_sort.
Section Regular.
Variables (gT : finGroupType) (G : {group gT}).
Local Notation nG := #|pred_of_set (gval G)|.
Local Notation aG := (regular_repr F G).
Local Notation R_G := (group_ring F G).
Lemma gring_free : row_free R_G.
Lemma gring_op_id A : (A \in R_G)%MS → gring_op aG A = A.
Lemma gring_rowK A : (A \in R_G)%MS → gring_mx aG (gring_row A) = A.
Lemma mem_gring_mx m a (M : 'M_(m, nG)) :
(gring_mx aG a \in M ×m R_G)%MS = (a ≤ M)%MS.
Lemma mem_sub_gring m A (M : 'M_(m, nG)) :
(A \in M ×m R_G)%MS = (A \in R_G)%MS && (gring_row A ≤ M)%MS.
Section GringMx.
Variables (n : nat) (rG : mx_representation F G n).
Lemma gring_mxP a : (gring_mx rG a \in enveloping_algebra_mx rG)%MS.
Lemma gring_opM A B :
(B \in R_G)%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 U (compU : mx_composition_series aG U) :
(last 0 U :=: 1%:M)%MS →
∃ i : 'I_(size U), mx_rsim rG (series_repr i compU).
Hypothesis F'G : [char F]^'.-group G.
Lemma rsim_regular_submod :
{U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (submod_repr modU)}}.
End GringMx.
Definition gset_mx (A : {set gT}) := \sum_(x in A) aG x.
Local Notation tG := #|pred_of_set (classes (gval G))|.
Definition classg_base := \matrix_(k < tG) mxvec (gset_mx (enum_val k)).
Let groupCl : {in G, ∀ x, {subset x ^: G ≤ G}}.
Lemma classg_base_free : row_free classg_base.
Lemma classg_base_center : (classg_base :=: 'Z(R_G))%MS.
Lemma regular_module_ideal m (M : 'M_(m, nG)) :
mxmodule aG M = right_mx_ideal R_G (M ×m R_G).
Definition irrType := socleType aG.
Identity Coercion type_of_irrType : irrType >-> socleType.
Variable sG : irrType.
Definition irr_degree (i : sG) := \rank (socle_base i).
Local Notation "'n_ i" := (irr_degree i) : group_ring_scope.
Local Open Scope group_ring_scope.
Lemma irr_degreeE i : 'n_i = \rank (socle_base i).
Lemma irr_degree_gt0 i : 'n_i > 0.
Definition irr_repr i : mx_representation F G 'n_i := socle_repr i.
Lemma irr_reprE i x : irr_repr i x = submod_mx (socle_module i) x.
Lemma rfix_regular : (rfix_mx aG G :=: gring_row (gset_mx G))%MS.
Lemma principal_comp_subproof : mxsimple aG (rfix_mx aG G).
Fact principal_comp_key : unit.
Definition principal_comp_def :=
PackSocle (component_socle sG principal_comp_subproof).
Definition principal_comp := locked_with principal_comp_key principal_comp_def.
Local Notation "1" := principal_comp : irrType_scope.
Lemma irr1_rfix : (1%irr :=: rfix_mx aG G)%MS.
Lemma rank_irr1 : \rank 1%irr = 1.
Lemma degree_irr1 : 'n_1 = 1.
Definition Wedderburn_subring (i : sG) := <<i ×m R_G>>%MS.
Local Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope.
Let sums_R : (\sum_i 'R_i :=: Socle sG ×m R_G)%MS.
Lemma Wedderburn_ideal i : mx_ideal R_G 'R_i.
Lemma Wedderburn_direct : mxdirect (\sum_i 'R_i)%MS.
Lemma Wedderburn_disjoint i j : i != j → ('R_i :&: 'R_j)%MS = 0.
Lemma Wedderburn_annihilate i j : i != j → ('R_i × 'R_j)%MS = 0.
Lemma Wedderburn_mulmx0 i j A B :
i != j → (A \in 'R_i)%MS → (B \in 'R_j)%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_' i" := (Wedderburn_id i) : group_ring_scope.
Lemma Wedderburn_sum_id : \sum_i 'e_i = 1%:M.
Lemma Wedderburn_id_mem i : ('e_i \in 'R_i)%MS.
Lemma Wedderburn_is_id i : mxring_id 'R_i 'e_i.
Lemma Wedderburn_closed i : ('R_i × 'R_i = 'R_i)%MS.
Lemma Wedderburn_is_ring i : mxring 'R_i.
Lemma Wedderburn_min_ideal m i (E : 'A_(m, nG)) :
E != 0 → (E ≤ 'R_i)%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 (iG j : sG) A :
mx_rsim rG (socle_repr iG) → iG != j → (A \in 'R_j)%MS →
gring_op rG A = 0.
Definition irr_comp := odflt 1%irr [pick i | gring_op rG 'e_i != 0].
Local Notation iG := irr_comp.
Hypothesis irrG : mx_irreducible rG.
Lemma rsim_irr_comp : mx_rsim rG (irr_repr iG).
Lemma irr_comp'_op0 j A : j != iG → (A \in 'R_j)%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 n1 n2 rG1 rG2 :
@mx_rsim _ G n1 rG1 n2 rG2 → irr_comp rG1 = irr_comp rG2.
Lemma irr_reprK i : irr_comp (irr_repr i) = i.
Lemma irr_repr'_op0 i j A :
j != i → (A \in 'R_j)%MS → gring_op (irr_repr i) A = 0.
Lemma op_Wedderburn_id i : gring_op (irr_repr i) 'e_i = 1%:M.
Lemma irr_comp_id (M : 'M_nG) (modM : mxmodule aG M) (iM : sG) :
mxsimple aG M → (M ≤ iM)%MS → irr_comp (submod_repr modM) = iM.
Lemma irr1_repr x : x \in G → irr_repr 1 x = 1%:M.
Hypothesis splitG : group_splitting_field G.
Lemma rank_Wedderburn_subring i : \rank 'R_i = ('n_i ^ 2)%N.
Lemma sum_irr_degree : (\sum_i 'n_i ^ 2 = nG)%N.
Lemma irr_mx_mult i : socle_mult i = 'n_i.
Lemma mxtrace_regular :
{in G, ∀ x, \tr (aG x) = \sum_i \tr (socle_repr i x) *+ 'n_i}.
Definition linear_irr := [set i | 'n_i == 1].
Lemma irr_degree_abelian : abelian G → ∀ i, 'n_i = 1.
Lemma linear_irr_comp i : 'n_i = 1 → (i :=: socle_base i)%MS.
Lemma Wedderburn_subring_center i : ('Z('R_i) :=: mxvec 'e_i)%MS.
Lemma Wedderburn_center :
('Z(R_G) :=: \matrix_(i < #|sG|) mxvec 'e_(enum_val i))%MS.
Lemma card_irr : #|sG| = tG.
Section CenterMode.
Variable i : sG.
Let i0 := Ordinal (irr_degree_gt0 i).
Definition irr_mode x := irr_repr i x i0 i0.
Lemma irr_mode1 : irr_mode 1 = 1.
Lemma irr_center_scalar : {in 'Z(G), ∀ x, irr_repr i x = (irr_mode x)%:M}.
Lemma irr_modeM : {in 'Z(G) &, {morph irr_mode : x y / (x × y)%g >-> x × y}}.
Lemma irr_modeX n : {in 'Z(G), {morph irr_mode : x / (x ^+ n)%g >-> x ^+ n}}.
Lemma irr_mode_unit : {in 'Z(G), ∀ x, irr_mode x \is a GRing.unit}.
Lemma irr_mode_neq0 : {in 'Z(G), ∀ 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 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 (sG : irrType G) :
[char F]^'.-group G → group_splitting_field G →
#|linear_irr sG| = #|G : G^`(1)|%g.
Lemma primitive_root_splitting_abelian (z : F) :
#|G|.-primitive_root z → abelian G → group_splitting_field G.
Lemma cycle_repr_structure x (sG : irrType G) :
G :=: <[x]> → [char F]^'.-group G → group_splitting_field G →
exists2 w : F, #|G|.-primitive_root w &
∃ iphi : 'I_#|G| → sG,
[/\ bijective iphi,
#|sG| = #|G|,
∀ i, irr_mode (iphi i) x = w ^+ i
& ∀ 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.
Arguments rfix_mx {F gT G%g n%N} rG H%g.
Arguments gset_mx F {gT} G%g A%g.
Arguments classg_base F {gT} G%g _%g : extra scopes.
Arguments irrType F {gT} G%g.
Arguments mxmoduleP {F gT G n rG m U}.
Arguments envelop_mxP {F gT G n rG A}.
Arguments hom_mxP {F gT G n rG m f W}.
Arguments mx_Maschke [F gT G n] rG _ [U].
Arguments rfix_mxP {F gT G n rG m W}.
Arguments cyclic_mxP {F gT G n rG u v}.
Arguments annihilator_mxP {F gT G n rG u A}.
Arguments row_hom_mxP {F gT G n rG u v}.
Arguments mxsimple_isoP {F gT G n rG U V}.
Arguments socle_exists [F gT G n].
Arguments socleP {F gT G n rG sG0 W W'}.
Arguments mx_abs_irrP {F gT G n rG}.
Arguments socle_rsimP {F gT G n rG sG W1 W2}.
Arguments val_submod {F n U m} W.
Arguments in_submod {F n} U {m} W.
Arguments val_submodK {F n U m} W : rename.
Arguments in_submodK {F n U m} [W] sWU.
Arguments val_submod_inj {F n U m} [W1 W2] : rename.
Arguments val_factmod {F n U m} W.
Arguments in_factmod {F n} U {m} W.
Arguments val_factmodK {F n U m} W : rename.
Arguments in_factmodK {F n} U {m} [W] sWU.
Arguments val_factmod_inj {F n U m} [W1 W2] : rename.
Notation "'Cl" := (Clifford_action _) : action_scope.
Arguments gring_row {R gT G} A.
Arguments gring_rowK {F gT G} [A] RG_A.
Bind Scope irrType_scope with socle_sort.
Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.
Arguments irr_degree {F gT G%G sG} i%irr.
Arguments irr_repr {F gT G%G sG} i%irr _%g : extra scopes.
Arguments irr_mode {F gT G%G sG} i%irr z%g : rename.
Notation "''n_' i" := (irr_degree i) : group_ring_scope.
Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope.
Notation "''e_' i" := (Wedderburn_id i) : group_ring_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 f := ((big_morph f) 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 U : qf_form (mxmodule_form U).
Lemma eval_mxmodule 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 U :
U != 0 → reflect (mxnonsimple rG U) (mxnonsimple_sat U).
Lemma dec_mxsimple_exists (U : 'M_n) :
mxmodule rG U → U != 0 → {V | mxsimple rG V & V ≤ U}%MS.
Lemma dec_mx_reducible_semisimple 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.sort 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 H : (rfix_mx rG H)^f = rfix_mx rGf H.
Lemma rcent_map A : rcent rGf A^f = rcent rG A.
Lemma rstab_map m (U : 'M_(m, n)) : rstab rGf U^f = rstab rG U.
Lemma rstabs_map m (U : 'M_(m, n)) : rstabs rGf U^f = rstabs rG U.
Lemma centgmx_map A : centgmx rGf A^f = centgmx rG A.
Lemma mxmodule_map m (U : 'M_(m, n)) : mxmodule rGf U^f = mxmodule rG U.
Lemma mxsimple_map (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 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 n (rG : mx_representation aF G n) rGf U V
(modU : mxmodule rG U) (modV : mxmodule rG V)
(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 U i (modU : mx_subseries (regular_repr aF G) U)
(modUf : mx_subseries (regular_repr rF G) [seq M^f | M <- 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.
The type definition must come before the main section so that the Bind Scope directive applies to all lemmas and definition discharged at the of the section.
Record gen_of {F : fieldType} {gT : finGroupType} {G : {group gT}} {n' : nat}
{rG : mx_representation F G n'.+1} {A : 'M[F]_n'.+1}
(irrG : mx_irreducible rG) (cGA : centgmx rG A) :=
Gen {rVval : 'rV[F]_(degree_mxminpoly A)}.
Local Arguments rVval {F gT G%G n'%N rG A%R irrG cGA} x%R : rename.
Bind Scope ring_scope with gen_of.
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).
Let d_gt0 := mxminpoly_nonconstant A.
Local Notation irr := mx_irreducible.
Hypotheses (irrG : irr rG) (cGA : centgmx rG A).
Notation FA := (gen_of irrG cGA).
Let inFA := Gen irrG cGA.
#[export, hnf] HB.instance Definition _ := [isNew for rVval : FA → 'rV_d].
#[export] HB.instance Definition _ := [Choice of FA by <:].
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.
#[export] HB.instance Definition _ := GRing.isZmodule.Build FA
gen_addA gen_addC gen_add0r gen_addNr.
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 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.
#[export] HB.instance Definition _ := GRing.Zmodule_isComRing.Build FA
gen_mulA gen_mulC gen_mul1r gen_mulDr gen_ntriv.
Lemma mxval1 : mxval 1 = 1%:M.
Lemma mxvalM : {morph mxval : x y / x × y >-> x ×m y}.
Lemma mxval_sub : additive mxval.
#[export] HB.instance Definition _ :=
GRing.isAdditive.Build FA 'M[F]_n mxval mxval_sub.
Lemma mxval_is_multiplicative : multiplicative mxval.
#[export] HB.instance Definition _ :=
GRing.isMultiplicative.Build FA 'M[F]_n mxval mxval_is_multiplicative.
Lemma mxval_centg x : centgmx rG (mxval x).
Lemma gen_mulVr x : x != 0 → genV x × x = 1.
Lemma gen_invr0 : genV 0 = 0.
#[export] HB.instance Definition _ := GRing.ComRing_isField.Build FA
gen_mulVr gen_invr0.
Lemma mxvalV : {morph mxval : x / x^-1 >-> invmx x}.
Lemma gen_is_additive : additive gen.
Lemma gen_is_multiplicative : multiplicative gen.
#[export] HB.instance Definition _ := GRing.isAdditive.Build F FA gen
gen_is_additive.
#[export] HB.instance Definition _ := GRing.isMultiplicative.Build F FA gen
gen_is_multiplicative.
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_grootXn 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.
Lemma non_linear_gen_reducible : d > 1 → mxnonsimple (map_repr gen rG) 1%:M.
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 nA (B : 'rV_nA) : 'M_(nA × d, n) :=
\matrix_ik mxvec (\matrix_(i, k) (row (B 0 i) (A ^+ k))) 0 ik.
Lemma gen_dim_ex_proof : ∃ nA, [∃ B : 'rV_nA, row_free (subbase B)].
Lemma gen_dim_ub_proof nA :
[∃ B : 'rV_nA, row_free (subbase B)] → (nA ≤ n)%N.
Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
Notation nA := gen_dim.
Definition gen_base : 'rV_nA := 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 : (nA × d)%N = n.
Lemma gen_dim_gt0 : nA > 0.
Section Bijection.
Variable m : nat.
Definition in_gen (W : 'M[F]_(m, n)) : 'M[FA]_(m, nA) :=
\matrix_(i, j) inFA (row j (vec_mx (row i W ×m pinvmx base))).
Definition val_gen (W : 'M[FA]_(m, nA)) : 'M[F]_(m, 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 a : {morph in_gen : W / a *: W >-> gen a *: W}.
End Bijection.
Lemma val_gen_rV (w : 'rV_nA) :
val_gen w = mxvec (\matrix_j val (w 0 j)) ×m base.
Section Bijection2.
Variable m : nat.
Lemma val_gen_row W (i : 'I_m) : val_gen (row i W) = row i (val_gen W).
Lemma in_gen_row W (i : 'I_m) : in_gen (row i W) = row i (in_gen W).
Lemma row_gen_sum_mxval W (i : 'I_m) :
row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).
Lemma val_genZ x : {morph @val_gen m : W / x *: W >-> W ×m mxval x}.
End Bijection2.
Lemma submx_in_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
(U ≤ V → in_gen U ≤ in_gen V)%MS.
Lemma submx_in_gen_eq 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 m :
{in G, ∀ 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 gen_repr := MxRepresentation gen_mx_repr.
Local Notation rGA := gen_repr.
Lemma val_genJ m :
{in G, ∀ g, {morph @val_gen m : W / W ×m rGA g >-> W ×m rG g}}.
Lemma in_genJ m :
{in G, ∀ g, {morph @in_gen m : v / v ×m rG g >-> v ×m rGA g}}.
Lemma rfix_gen (H : {set gT}) :
H \subset G → (rfix_mx rGA H :=: in_gen (rfix_mx rG H))%MS.
Definition rowval_gen m U :=
<<\matrix_ik
mxvec (\matrix_(i < m, k < d) (row i (val_gen U) ×m A ^+ k)) 0 ik>>%MS.
Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, nA)) :
(U ≤ rowval_gen V)%MS = (in_gen U ≤ V)%MS.
Lemma rowval_genK m (U : 'M_(m, nA)) : (in_gen (rowval_gen U) :=: U)%MS.
Lemma rowval_gen_stable m (U : 'M_(m, nA)) :
(rowval_gen U ×m A ≤ rowval_gen U)%MS.
Lemma rstab_in_gen m (U : 'M_(m, n)) : rstab rGA (in_gen U) = rstab rG U.
Lemma rstabs_in_gen m (U : 'M_(m, n)) :
rstabs rG U \subset rstabs rGA (in_gen U).
Lemma rstabs_rowval_gen m (U : 'M_(m, nA)) :
rstabs rG (rowval_gen U) = rstabs rGA U.
Lemma mxmodule_rowval_gen m (U : 'M_(m, nA)) :
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 f := ((big_morph f) 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 e u : eval_mx e (mxT u) = mxval (inFA (eval_mx e u)).
Let Ad'T := mx_term (pinvmx Ad).
Let mulT (u v : 'rV_d) := mulmx_term (mxvec (mulmx_term (mxT u) (mxT v))) Ad'T.
Lemma eval_mulT 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 (e : seq FA) j : (map val e)`_j = val e`_j.
Lemma set_nth_map_rVval (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 e t :
GRing.rterm t → eval_mx (gen_env e) (gen_term t) = val (GRing.eval e t).
Fixpoint gen_form f := match f with
| 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
| ('∃ 'X_k, f1) ⇒ Exists_row_form d k (gen_form f1)
| ('∀ 'X_k, f1) ⇒ ¬ Exists_row_form d k (¬ (gen_form f1))
end%T.
Lemma sat_gen_form 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)).
FIXME : why this MathCompCompatDecidableField
Lemma gen_satP :
GRing.MathCompCompatDecidableField.DecidableField.axiom gen_sat.
#[export] HB.instance Definition _ := GRing.Field_isDecField.Build FA gen_satP.
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).
#[export] HB.instance Definition _ := [Finite of FA by <:].
#[export] HB.instance Definition _ := [finGroupMixin of FA for +%R].
Lemma card_gen : #|{:FA}| = (#|F| ^ degree_mxminpoly A)%N.
End FiniteGenField.
End MatrixGenField.
Module MatrixGenFieldExports.
End MatrixGenFieldExports.
Export MatrixGenFieldExports.
Bind Scope ring_scope with gen_of.
Arguments rVval {F gT G%G n'%N rG A%R irrG cGA} x%R : rename.
Arguments subbase {F n'} A {nA}.
Arguments in_gen {F gT G n' rG A} irrG cGA {m} W.
Arguments in_genK {F gT G n' rG A} irrG cGA {m} W : rename.
Arguments val_genK {F gT G n' rG A irrG cGA m} W : rename.
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 gT (G : {group gT}) F :
classically {Fs : fieldType & {rmorphism F → Fs}
& group_splitting_field Fs G}.
Lemma group_closure_field_exists gT F :
classically {Fs : fieldType & {rmorphism F → Fs}
& group_closure_field Fs gT}.
Lemma group_closure_closed_field (F : closedFieldType) gT :
group_closure_field F gT.
End BuildSplittingField.