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.
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.
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.
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).
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.
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.
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.
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.
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.
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.
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 *)
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.
Definition group_ring := enveloping_algebra_mx aG.
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}).
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.
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.
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.
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.
\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.
Lemma cyclic_mxP u v :
reflect (exists2 A, A \in E_G & v = u ×m A)%MS (v ≤ cyclic_mx u)%MS.
Arguments cyclic_mxP {u v}.
Lemma cyclic_mx_id u : (u ≤ cyclic_mx u)%MS.
Lemma cyclic_mx_eq0 u : (cyclic_mx u == 0) = (u == 0).
Lemma cyclic_mx_module u : mxmodule (cyclic_mx u).
Lemma cyclic_mx_sub m u (W : 'M_(m, n)) :
mxmodule W → (u ≤ W)%MS → (cyclic_mx u ≤ W)%MS.
Lemma hom_cyclic_mx u f :
(u ≤ dom_hom_mx f)%MS → (cyclic_mx u ×m f :=: cyclic_mx (u ×m f))%MS.
The annihilator of a single vector.
Definition annihilator_mx u := (E_G :&: kermx (lin_mul_row u))%MS.
Lemma annihilator_mxP u A :
reflect (A \in E_G ∧ u ×m A = 0)%MS (A \in annihilator_mx u)%MS.
The subspace of homomorphic images of a row vector.
Definition row_hom_mx u :=
(\bigcap_j kermx (vec_mx (row j (annihilator_mx u))))%MS.
Lemma row_hom_mxP u v :
reflect (exists2 f, u ≤ dom_hom_mx f & u ×m f = v)%MS (v ≤ row_hom_mx u)%MS.
Sub-, isomorphic, simple, semisimple and completely reducible modules.
All these predicates are intuitionistic (since, e.g., testing simplicity
requires a splitting algorithm fo r the mas field). They are all
specialized to square matrices, to avoid spurrious height parameters.
Module isomorphism is an intentional property in general, but it can be
decided when one of the two modules is known to be simple.
Variant mx_iso (U V : 'M_n) : Prop :=
MxIso f of f \in unitmx & (U ≤ dom_hom_mx f)%MS & (U ×m f :=: V)%MS.
Lemma eqmx_iso U V : (U :=: V)%MS → mx_iso U V.
Lemma mx_iso_refl U : mx_iso U U.
Lemma mx_iso_sym U V : mx_iso U V → mx_iso V U.
Lemma mx_iso_trans U V W : mx_iso U V → mx_iso V W → mx_iso U W.
Lemma mxrank_iso U V : mx_iso U V → \rank U = \rank V.
Lemma mx_iso_module U V : mx_iso U V → mxmodule U → mxmodule V.
Simple modules (we reserve the term "irreducible" for representations).
Definition mxsimple (V : 'M_n) :=
[/\ mxmodule V, V != 0 &
∀ U : 'M_n, mxmodule U → (U ≤ V)%MS → U != 0 → (V ≤ U)%MS].
Definition mxnonsimple (U : 'M_n) :=
∃ V : 'M_n, [&& mxmodule V, (V ≤ U)%MS, V != 0 & \rank V < \rank U].
Lemma mxsimpleP U :
[/\ mxmodule U, U != 0 & ¬ mxnonsimple U] ↔ mxsimple U.
Lemma mxsimple_module U : mxsimple U → mxmodule U.
Lemma mxsimple_exists m (U : 'M_(m, n)) :
mxmodule U → U != 0 → classically (exists2 V, mxsimple V & V ≤ U)%MS.
Lemma mx_iso_simple U V : mx_iso U V → mxsimple U → mxsimple V.
Lemma mxsimple_cyclic u U :
mxsimple U → u != 0 → (u ≤ U)%MS → (U :=: cyclic_mx u)%MS.
The surjective part of Schur's lemma.
Lemma mx_Schur_onto m (U : 'M_(m, n)) V f :
mxmodule U → mxsimple V → (U ≤ dom_hom_mx f)%MS →
(U ×m f ≤ V)%MS → U ×m f != 0 → (U ×m f :=: V)%MS.
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.
The injectve part of Schur's lemma, stated as isomorphism with the image.
The isomorphism part of Schur's lemma.
Lemma mx_Schur_iso U V f :
mxsimple U → mxsimple V → (U ≤ dom_hom_mx f)%MS →
(U ×m f ≤ V)%MS → U ×m f != 0 → mx_iso U V.
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.
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.
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.
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.
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.
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).
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.
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.
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.
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).
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).
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).
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.
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.
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}).
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).
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.
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).
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).
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
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).
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.
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.
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.
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).
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).
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).
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.
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.
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}).
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).
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.
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).
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).
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