Library mathcomp.character.mxrepresentation
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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 is not a proper is a proper subset of any
+ proper rG-submodule of V (if both U and V are modules,
+ then U is a maximal proper submodule of V).
+ mx_subseries rG Us <=> Us : seq 'M_n is a list of rG-modules
+ mx_composition_series rG Us <-> Us is an increasing composition series
+ for an rG-module (namely, last 0 Us).
+ mxsimple rG M <-> M is a simple rG-module (i.e., minimal and nontrivial)
+ This is a Prop predicate on square matrices.
+ mxnonsimple rG U <-> U is constructively not a submodule, that is, U
+ contains a proper nontrivial submodule.
+ mxnonsimple_sat rG U == U is not a simple as an rG-module.
+ This is a bool predicate, which requires a decField
+ structure on the scalar field.
+ mxsemisimple rG W <-> W is constructively a direct sum of simple modules.
+ mxsplits rG V U <-> V splits over U in rG, i.e., U has an rG-invariant
+ complement in V.
+ mx_completely_reducible rG V <-> V splits over all its submodules; note
+ that this is only classically equivalent to stating that
+ V is semisimple.
+ mx_irreducible rG <-> the representation rG is irreducible, i.e., the full
+ module 1%:M of rG is simple.
+ mx_absolutely_irreducible rG == the representation rG of G is absolutely
+ irreducible: its enveloping algebra is the full matrix
+ ring. This is only classically equivalent to the more
+ standard ``rG does not reduce in any field extension''.
+ group_splitting_field F G <-> F is a splitting field for the group G:
+ every irreducible representation of G is absolutely
+ irreducible. Any field can be embedded classically into a
+ splitting field.
+ group_closure_field F gT <-> F is a splitting field for every group
+ G : {group gT}, and indeed for any section of such a
+ group. This is a convenient constructive substitute for
+ algebraic closures, that can be constructed classically.
+ dom_hom_mx rG f == a square matrix encoding the set of vectors for which
+ multiplication by the n x n matrix f commutes with the
+ representation of G, i.e., the largest domain on which
+ f is an rG homomorphism.
+ mx_iso rG U V <-> U and V are (constructively) rG-isomorphic; this is
+ a Prop predicate.
+ mx_simple_iso rG U V == U and V are rG-isomorphic if one of them is
+ simple; this is a bool predicate.
+ cyclic_mx rG u == the cyclic rG-module generated by the row vector u
+ annihilator_mx rG u == the annihilator of the row vector u in the
+ enveloping algebra the representation rG.
+ row_hom_mx rG u == the image of u by the set of all rG-homomorphisms on
+ its cyclic module, or, equivalently, the null-space of the
+ annihilator of u.
+ component_mx rG M == when M is a simple rG-module, the component of M in
+ the representation rG, i.e. the module generated by all
+ the (simple) modules rG-isomorphic to M.
+ socleType rG == a Structure that represents the type of all components
+ of rG (more precisely, it coerces to such a type via
+ socle_sort). For sG : socleType, values of type sG (to be
+ exact, socle_sort sG) coerce to square matrices. For any
+ representation rG we can construct sG : socleType rG
+ classically; the socleType structure encapsulates this
+ use of classical logic.
+ DecSocleType rG == a socleType rG structure, for a representation over a
+ decidable field type.
+ socle_base W == for W : (sG : socleType), a simple module whose
+ component is W; socle_simple W and socle_module W are
+ proofs that socle_base W is a simple module.
+ socle_mult W == the multiplicity of socle_base W in W : sG.
+ := \rank W %/ \rank (socle_base W)
+ Socle sG == the Socle of rG, given sG : socleType rG, i.e., the
+ (direct) sum of all the components of rG.
+ mx_rsim rG rG' <-> rG and rG' are similar representations of the same
+ group G. Note that rG and rG' must then have equal, but
+ not necessarily convertible, degree.
+ submod_repr modU == a representation of G on 'rV(\rank U) equivalent to
+ the restriction of rG to U (here modU : mxmodule rG U).
+ socle_repr W := submod_repr (socle_module W)
+ val/in_submod rG U == the projections resp. from/onto 'rV(\rank U),
+ that correspond to submod_repr r G U (these work both on
+ vectors and row spaces).
+ factmod_repr modV == a representation of G on 'rV(\rank (cokermx V)) that
+ is equivalent to the factor module 'rV_n / V induced by V
+ and rG (here modV : mxmodule rG V).
+ val/in_factmod rG U == the projections for factmod_repr r G U.
+ section_repr modU modV == the restriction to in_factmod V U of the factor
+ representation factmod_repr modV (for modU : mxmodule rG U
+ and modV : mxmodule rG V); section_repr modU modV is
+ irreducible iff max_submod rG U V.
+ subseries_repr modUs i == the representation for the section module
+ in_factmod (0 :: Us)`i Us`i, where
+ modUs : mx_subseries rG Us.
+ series_repr compUs i == the representation for the section module
+ in_factmod (0 :: Us)`i Us`i, where
+ compUs : mx_composition_series rG Us. The Jordan-Holder
+ theorem asserts the uniqueness of the set of such
+ representations, up to similarity and permutation.
+ regular_repr F G == the regular F-representation of the group G.
+ group_ring F G == a #|G| x #|G|^2 matrix that encodes the free group
+ ring of G -- that is, the enveloping algebra of the
+ regular F-representation of G.
+ gring_index x == the index corresponding to x \in G in the matrix
+ encoding of regular_repr and group_ring.
+ gring_row A == the row vector corresponding to A \in group_ring F G in
+ the regular FG-module.
+ gring_proj x A == the 1 x 1 matrix holding the coefficient of x \in G in
+ (A \in group_ring F G)%MS.
+ gring_mx rG u == the image of a row vector u of the regular FG-module,
+ in the enveloping algebra of another representation rG.
+ gring_op rG A == the image of a matrix of the free group ring of G,
+ in the enveloping algebra of rG.
+ gset_mx F G C == the group sum of C in the free group ring of G -- the
+ sum of the images of all the x \in C in group_ring F G.
+ classg_base F G == a #|classes G| x #|G|^2 matrix whose rows encode the
+ group sums of the conjugacy classes of G -- this is a
+ basis of 'Z(group_ring F G)%MS.
+ irrType F G == a type indexing irreducible representations of G over a
+ field F, provided its characteristic does not divide the
+ order of G; it also indexes Wedderburn subrings.
+ := socleType (regular_repr F G)
+ irr_repr i == the irreducible representation corresponding to the
+ index i : irrType sG
+ := socle_repr i as i coerces to a component matrix.
+ 'n_i, irr_degree i == the degree of irr_repr i; the notation is only
+ active after Open Scope group_ring_scope.
+ linear_irr sG == the set of sG-indices of linear irreducible
+ representations of G.
+ irr_comp sG rG == the sG-index of the unique irreducible representation
+ similar to rG, at least when rG is irreducible and the
+ characteristic is coprime.
+ irr_mode i z == the unique eigenvalue of irr_repr i z, at least when
+ irr_repr i z is scalar (e.g., when z \in 'Z(G)).
+ [1 sG]%irr == the index of the principal representation of G, in
+ sG : irrType F G. The i argument 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)).
+ More involved constructions are encapsulated in two Coq submodules:
+ MatrixGenField == a module that encapsulates the lengthy details of the
+ construction of appropriate extension fields. We assume we
+ have an irreducible representation r of a group G, and a
+ non-scalar matrix A that centralises an r(G), as this data
+ is readily extracted from the Jacobson density theorem. It
+ then follows from Schur's lemma that the ring generated by
+ A is a field on which the extension of the representation
+ r of G is reducible. Note that this is equivalent to the
+ more traditional quotient of the polynomial ring by an
+ irreducible polynomial (the minimal polynomial of A), but
+ much better suited to our needs.
+ Here are the main definitions of MatrixGenField; they all have three
+ proofs as arguments: rG : mx_repr r G, irrG : mx_irreducible rG, and
+ cGA : centgmx rG A, which ensure the validity of the construction and
+ allow us to define Canonical instances (the ~~ is_scalar_mx A assumption
+ is only needed to prove reducibility).
+ + gen_of irrG cGA == the carrier type of the field generated by A. It is
+ at least equipped with a fieldType structure; we also
+ propagate any decFieldType/finFieldType structures on the
+ original field.
+ + gen irrG cGA == the morphism injecting into gen_of rG irrG cGA.
+ + groot irrG cGA == the root of mxminpoly A in the gen_of field.
+ + gen_repr irrG cGA == an alternative to the field extension
+ representation, which consists in reconsidering the
+ original module as a module over the new gen_of field,
+ thereby DIVIDING the original dimension n by the degree of
+ the minimal polynomial of A. This can be simpler than the
+ extension method, and is actually required by the proof
+ that odd groups are p-stable (B & G 6.1-2, and Appendix A)
+ but is only applicable if G is the LARGEST group
+ represented by rG (e.g., NOT for B & G 2.6).
+ + val_gen/in_gen rG irrG cGA : the bijections from/to the module
+ corresponding to gen_repr.
+ + rowval_gen rG irrG cGA : the projection of row spaces in the module
+ corresponding to gen_repr to row spaces in 'rV_n.
+ We build on the MatrixFormula toolkit to define decision procedures for
+ the reducibility property:
+ + mxmodule_form rG U == a formula asserting that the interpretation of U
+ is a module of the representation rG of G via r.
+ + mxnonsimple_form rG U == a formula asserting that the interpretation
+ of U contains a proper nontrivial rG-module.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory.
+Local Open Scope ring_scope.
+ +
+Reserved Notation "''n_' i" (at level 8, i at level 2, format "''n_' i").
+Reserved Notation "''R_' i" (at level 8, i at level 2, format "''R_' i").
+Reserved Notation "''e_' i" (at level 8, i at level 2, format "''e_' i").
+ +
+Delimit Scope irrType_scope with irr.
+ +
+Section RingRepr.
+ +
+Variable R : comUnitRingType.
+ +
+Section OneRepresentation.
+ +
+Variable gT : finGroupType.
+ +
+Definition mx_repr (G : {set gT}) n (r : gT → 'M[R]_n) :=
+ r 1%g = 1%:M ∧ {in G &, {morph r : x y / (x × y)%g >-> x ×m y}}.
+ +
+Structure mx_representation G n :=
+ MxRepresentation { repr_mx :> gT → 'M_n; _ : mx_repr G repr_mx }.
+ +
+Variables (G : {group gT}) (n : nat) (rG : mx_representation G n).
+ +
+Lemma repr_mx1 : rG 1 = 1%:M.
+ +
+Lemma repr_mxM : {in G &, {morph rG : x y / (x × y)%g >-> x ×m y}}.
+ +
+Lemma repr_mxK m x :
+ x \in G → cancel ((@mulmx _ m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).
+ +
+Lemma repr_mxKV m x :
+ x \in G → cancel ((@mulmx _ 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}}.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory.
+Local Open Scope ring_scope.
+ +
+Reserved Notation "''n_' i" (at level 8, i at level 2, format "''n_' i").
+Reserved Notation "''R_' i" (at level 8, i at level 2, format "''R_' i").
+Reserved Notation "''e_' i" (at level 8, i at level 2, format "''e_' i").
+ +
+Delimit Scope irrType_scope with irr.
+ +
+Section RingRepr.
+ +
+Variable R : comUnitRingType.
+ +
+Section OneRepresentation.
+ +
+Variable gT : finGroupType.
+ +
+Definition mx_repr (G : {set gT}) n (r : gT → 'M[R]_n) :=
+ r 1%g = 1%:M ∧ {in G &, {morph r : x y / (x × y)%g >-> x ×m y}}.
+ +
+Structure mx_representation G n :=
+ MxRepresentation { repr_mx :> gT → 'M_n; _ : mx_repr G repr_mx }.
+ +
+Variables (G : {group gT}) (n : nat) (rG : mx_representation G n).
+ +
+Lemma repr_mx1 : rG 1 = 1%:M.
+ +
+Lemma repr_mxM : {in G &, {morph rG : x y / (x × y)%g >-> x ×m y}}.
+ +
+Lemma repr_mxK m x :
+ x \in G → cancel ((@mulmx _ m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).
+ +
+Lemma repr_mxKV m x :
+ x \in G → cancel ((@mulmx _ 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%N → G^`(1)%g \subset rker.
+ +
+
+
++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%N → 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.
+ +
+ +
+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 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).
+Canonical gring_row_linear := [linear of gring_row].
+ +
+Lemma gring_row_mul A B : gring_row (A ×m B) = gring_row A ×m B.
+ +
+Definition gring_proj x := row (gring_index x) \o trmx \o gring_row.
+Canonical gring_proj_linear x := [linear of gring_proj x].
+ +
+Lemma gring_projE : {in G &, ∀ x y, gring_proj x (aG y) = (x == y)%:R}.
+ +
+Lemma regular_mx_faithful : mx_faithful aG.
+ +
+Section GringMx.
+ +
+Variables (n : nat) (rG : mx_representation G n).
+ +
+Definition gring_mx := vec_mx \o mulmxr (enveloping_algebra_mx rG).
+Canonical gring_mx_linear := [linear of gring_mx].
+ +
+Lemma gring_mxJ a x :
+ x \in G → gring_mx (a ×m aG x) = gring_mx a ×m rG x.
+ +
+End GringMx.
+ +
+Lemma gring_mxK : cancel (gring_mx aG) gring_row.
+ +
+Section GringOp.
+ +
+Variables (n : nat) (rG : mx_representation G n).
+ +
+Definition gring_op := gring_mx rG \o gring_row.
+Canonical gring_op_linear := [linear of gring_op].
+ +
+Lemma gring_opE a : gring_op a = gring_mx rG (gring_row a).
+ +
+Lemma gring_opG x : x \in 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.
+ +
+ +
+ +
+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.
+ +
+
+
++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.
+ +
+ +
+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 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).
+Canonical gring_row_linear := [linear of gring_row].
+ +
+Lemma gring_row_mul A B : gring_row (A ×m B) = gring_row A ×m B.
+ +
+Definition gring_proj x := row (gring_index x) \o trmx \o gring_row.
+Canonical gring_proj_linear x := [linear of gring_proj x].
+ +
+Lemma gring_projE : {in G &, ∀ x y, gring_proj x (aG y) = (x == y)%:R}.
+ +
+Lemma regular_mx_faithful : mx_faithful aG.
+ +
+Section GringMx.
+ +
+Variables (n : nat) (rG : mx_representation G n).
+ +
+Definition gring_mx := vec_mx \o mulmxr (enveloping_algebra_mx rG).
+Canonical gring_mx_linear := [linear of gring_mx].
+ +
+Lemma gring_mxJ a x :
+ x \in G → gring_mx (a ×m aG x) = gring_mx a ×m rG x.
+ +
+End GringMx.
+ +
+Lemma gring_mxK : cancel (gring_mx aG) gring_row.
+ +
+Section GringOp.
+ +
+Variables (n : nat) (rG : mx_representation G n).
+ +
+Definition gring_op := gring_mx rG \o gring_row.
+Canonical gring_op_linear := [linear of gring_op].
+ +
+Lemma gring_opE a : gring_op a = gring_mx rG (gring_row a).
+ +
+Lemma gring_opG x : x \in 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.
+ +
+ +
+ +
+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).
+ +
+ +
+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.
+ +
+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%N →
+ {u : 'rV_n & {a | (U :=: u)%MS & {in G, ∀ x, u ×m rG x = a x *: u}}}.
+ +
+Lemma addsmx_module m1 m2 U V :
+ @mxmodule m1 U → @mxmodule m2 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.
+ +
+
+
++End ChangeOfRing.
+ +
+Section FieldRepr.
+ +
+Variable F : fieldType.
+ +
+Section OneRepresentation.
+ +
+Variable gT : finGroupType.
+ +
+Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n).
+ +
+ +
+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.
+ +
+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%N →
+ {u : 'rV_n & {a | (U :=: u)%MS & {in G, ∀ x, u ×m rG x = a x *: u}}}.
+ +
+Lemma addsmx_module m1 m2 U V :
+ @mxmodule m1 U → @mxmodule m2 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)).
+Canonical val_submod_linear m := [linear of @val_submod m].
+Canonical in_submod_linear m := [linear of @in_submod m].
+ +
+Lemma val_submodE m W : @val_submod m W = W ×m val_submod 1%:M.
+ +
+Lemma in_submodE m W : @in_submod m W = W ×m in_submod 1%:M.
+ +
+Lemma val_submod1 : (val_submod 1%:M :=: U)%MS.
+ +
+Lemma val_submodP m W : (@val_submod m W ≤ U)%MS.
+ +
+Lemma val_submodK m : cancel (@val_submod m) (@in_submod m).
+ +
+Lemma val_submod_inj m : injective (@val_submod m).
+ +
+Lemma val_submodS m1 m2 (V : 'M_(m1, \rank U)) (W : 'M_(m2, \rank U)) :
+ (val_submod V ≤ val_submod W)%MS = (V ≤ W)%MS.
+ +
+Lemma in_submodK m W : (W ≤ U)%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)).
+Canonical val_factmod_linear m := [linear of @val_factmod m].
+Canonical in_factmod_linear m := [linear of @in_factmod m].
+ +
+Lemma val_factmodE m W : @val_factmod m W = W ×m val_factmod 1%:M.
+ +
+Lemma in_factmodE m W : @in_factmod m W = W ×m in_factmod 1%:M.
+ +
+Lemma val_factmodP m W : (@val_factmod m W ≤ U^C)%MS.
+ +
+Lemma val_factmodK m : cancel (@val_factmod m) (@in_factmod m).
+ +
+Lemma val_factmod_inj m : injective (@val_factmod m).
+ +
+Lemma val_factmodS m1 m2 (V : 'M_(m1, _)) (W : 'M_(m2, _)) :
+ (val_factmod V ≤ val_factmod W)%MS = (V ≤ W)%MS.
+ +
+Lemma val_factmod_eq0 m W : (@val_factmod m W == 0) = (W == 0).
+ +
+Lemma in_factmod_eq0 m (W : 'M_(m, n)) : (in_factmod W == 0) = (W ≤ U)%MS.
+ +
+Lemma in_factmodK m (W : 'M_(m, n)) :
+ (W ≤ U^C)%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)).
+Canonical val_submod_linear m := [linear of @val_submod m].
+Canonical in_submod_linear m := [linear of @in_submod m].
+ +
+Lemma val_submodE m W : @val_submod m W = W ×m val_submod 1%:M.
+ +
+Lemma in_submodE m W : @in_submod m W = W ×m in_submod 1%:M.
+ +
+Lemma val_submod1 : (val_submod 1%:M :=: U)%MS.
+ +
+Lemma val_submodP m W : (@val_submod m W ≤ U)%MS.
+ +
+Lemma val_submodK m : cancel (@val_submod m) (@in_submod m).
+ +
+Lemma val_submod_inj m : injective (@val_submod m).
+ +
+Lemma val_submodS m1 m2 (V : 'M_(m1, \rank U)) (W : 'M_(m2, \rank U)) :
+ (val_submod V ≤ val_submod W)%MS = (V ≤ W)%MS.
+ +
+Lemma in_submodK m W : (W ≤ U)%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)).
+Canonical val_factmod_linear m := [linear of @val_factmod m].
+Canonical in_factmod_linear m := [linear of @in_factmod m].
+ +
+Lemma val_factmodE m W : @val_factmod m W = W ×m val_factmod 1%:M.
+ +
+Lemma in_factmodE m W : @in_factmod m W = W ×m in_factmod 1%:M.
+ +
+Lemma val_factmodP m W : (@val_factmod m W ≤ U^C)%MS.
+ +
+Lemma val_factmodK m : cancel (@val_factmod m) (@in_factmod m).
+ +
+Lemma val_factmod_inj m : injective (@val_factmod m).
+ +
+Lemma val_factmodS m1 m2 (V : 'M_(m1, _)) (W : 'M_(m2, _)) :
+ (val_factmod V ≤ val_factmod W)%MS = (V ≤ W)%MS.
+ +
+Lemma val_factmod_eq0 m W : (@val_factmod m W == 0) = (W == 0).
+ +
+Lemma in_factmod_eq0 m (W : 'M_(m, n)) : (in_factmod W == 0) = (W ≤ U)%MS.
+ +
+Lemma in_factmodK m (W : 'M_(m, n)) :
+ (W ≤ U^C)%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.
+ +
+
+
++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.
+ +
+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.
+ +
+
+
++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.
+ +
+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.
+ +
+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.
+ +
+
+
++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.
+ +
+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.
+ +
+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.
+ +
+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.
+ +
+
+
++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.
+ +
+
+
++Definition row_hom_mx u :=
+ (\bigcap_j kermx (vec_mx (row j (annihilator_mx u))))%MS.
+ +
+Lemma row_hom_mxP u v :
+ reflect (exists2 f, u ≤ dom_hom_mx f & u ×m f = v)%MS (v ≤ row_hom_mx u)%MS.
+ +
+
+ Sub-, isomorphic, simple, semisimple and completely reducible modules.
+ All these predicates are intuitionistic (since, e.g., testing simplicity
+ requires a splitting algorithm fo r the mas field). They are all
+ specialized to square matrices, to avoid spurrious height parameters.
+
+
+ Module isomorphism is an intentional property in general, but it can be
+ decided when one of the two modules is known to be simple.
+
+
+
+
+CoInductive mx_iso (U V : 'M_n) : Prop :=
+ MxIso f of f \in unitmx & (U ≤ dom_hom_mx f)%MS & (U ×m f :=: V)%MS.
+ +
+Lemma eqmx_iso U V : (U :=: V)%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.
+ +
+
+
++CoInductive mx_iso (U V : 'M_n) : Prop :=
+ MxIso f of f \in unitmx & (U ≤ dom_hom_mx f)%MS & (U ×m f :=: V)%MS.
+ +
+Lemma eqmx_iso U V : (U :=: V)%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.
+ +
+
+
++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.
+
+
+Lemma mx_Schur_inj U f :
+ mxsimple U → (U ≤ dom_hom_mx f)%MS → U ×m f != 0 → (U :&: kermx f)%MS = 0.
+ +
+
+
++ 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).
+ +
+
+
++ 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.
+ +
+
+
++ 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.
+ +
+
+
++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.
+ +
+CoInductive mxsemisimple (V : 'M_n) :=
+ MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
+ ∀ i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
+ +
+
+
++Implicit Type I : finType.
+ +
+CoInductive mxsemisimple (V : 'M_n) :=
+ MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
+ ∀ i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
+ +
+
+ This is a slight generalization of Aschbacher 12.5 for finite sets.
+
+
+Lemma sum_mxsimple_direct_compl m I W (U : 'M_(m, n)) :
+ let V := (\sum_(i : I) W i)%MS in
+ (∀ i : I, mxsimple (W i)) → mxmodule U → (U ≤ V)%MS →
+ {J : {set I} | let S := U + \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
+ +
+Lemma sum_mxsimple_direct_sub I W (V : 'M_n) :
+ (∀ i : I, mxsimple (W i)) → (\sum_i W i :=: V)%MS →
+ {J : {set I} | let S := \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
+ +
+Lemma mxsemisimple0 : mxsemisimple 0.
+ +
+Lemma intro_mxsemisimple (I : Type) r (P : pred I) W V :
+ (\sum_(i <- r | P i) W i :=: V)%MS →
+ (∀ i, P 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.
+
+
+
+
+CoInductive mxsplits (V U : 'M_n) :=
+ MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W).
+ +
+Definition mx_completely_reducible V :=
+ ∀ U, mxmodule U → (U ≤ V)%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}.
+ +
+
+
++CoInductive mxsplits (V U : 'M_n) :=
+ MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W).
+ +
+Definition mx_completely_reducible V :=
+ ∀ U, mxmodule U → (U ≤ V)%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.
+ +
+Canonical socle_subType := SubType _ _ _ socle_sort_rect PackSocleK.
+Definition socle_eqMixin := Eval hnf in [eqMixin of sG by <:].
+Canonical socle_eqType := Eval hnf in EqType sG socle_eqMixin.
+Definition socle_choiceMixin := Eval hnf in [choiceMixin of sG by <:].
+Canonical socle_choiceType := ChoiceType sG socle_choiceMixin.
+ +
+Lemma socleP (W W' : sG) : reflect (W = W') (W == W')%MS.
+ +
+Fact socle_finType_subproof :
+ cancel (fun W ⇒ SeqSub (socle_mem W)) (fun s ⇒ PackSocle (valP s)).
+ +
+Definition socle_countMixin := CanCountMixin socle_finType_subproof.
+Canonical socle_countType := CountType sG socle_countMixin.
+Canonical socle_subCountType := [subCountType of sG].
+Definition socle_finMixin := CanFinMixin socle_finType_subproof.
+Canonical socle_finType := FinType sG socle_finMixin.
+Canonical socle_subFinType := [subFinType of sG].
+ +
+End SocleDef.
+ +
+Coercion socle_sort : socleType >-> predArgType.
+ +
+Variable sG : socleType.
+ +
+Section SubSocle.
+ +
+Variable P : pred sG.
+Notation S := (\sum_(W : sG | P W) socle_val W)%MS.
+ +
+Lemma subSocle_module : mxmodule S.
+ +
+Lemma subSocle_semisimple : mxsemisimple S.
+ +
+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.
+ +
+
+
++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.
+ +
+Canonical socle_subType := SubType _ _ _ socle_sort_rect PackSocleK.
+Definition socle_eqMixin := Eval hnf in [eqMixin of sG by <:].
+Canonical socle_eqType := Eval hnf in EqType sG socle_eqMixin.
+Definition socle_choiceMixin := Eval hnf in [choiceMixin of sG by <:].
+Canonical socle_choiceType := ChoiceType sG socle_choiceMixin.
+ +
+Lemma socleP (W W' : sG) : reflect (W = W') (W == W')%MS.
+ +
+Fact socle_finType_subproof :
+ cancel (fun W ⇒ SeqSub (socle_mem W)) (fun s ⇒ PackSocle (valP s)).
+ +
+Definition socle_countMixin := CanCountMixin socle_finType_subproof.
+Canonical socle_countType := CountType sG socle_countMixin.
+Canonical socle_subCountType := [subCountType of sG].
+Definition socle_finMixin := CanFinMixin socle_finType_subproof.
+Canonical socle_finType := FinType sG socle_finMixin.
+Canonical socle_subFinType := [subFinType of sG].
+ +
+End SocleDef.
+ +
+Coercion socle_sort : socleType >-> predArgType.
+ +
+Variable sG : socleType.
+ +
+Section SubSocle.
+ +
+Variable P : pred sG.
+Notation S := (\sum_(W : sG | P W) socle_val W)%MS.
+ +
+Lemma subSocle_module : mxmodule S.
+ +
+Lemma subSocle_semisimple : mxsemisimple S.
+ +
+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).
+ +
+
+
++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%N → mx_absolutely_irreducible.
+ +
+Lemma abelian_abs_irr : abelian G → mx_absolutely_irreducible = (n == 1%N).
+ +
+End OneRepresentation.
+ +
+ +
+ +
+ +
+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_groupType H).
+ +
+End SplittingField.
+ +
+Section Abelian.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Lemma mx_faithful_irr_center_cyclic n (rG : mx_representation F G n) :
+ mx_faithful 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%N.
+ +
+Lemma mxsimple_abelian_linear n (rG : mx_representation F G n) M :
+ abelian G → mxsimple rG M → \rank M = 1%N.
+ +
+Lemma linear_mxsimple n (rG : mx_representation F G n) (M : 'M_n) :
+ mxmodule rG M → \rank M = 1%N → mxsimple rG M.
+ +
+End Abelian.
+ +
+Section AbelianQuotient.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Variables (n : nat) (rG : mx_representation F G n).
+ +
+Lemma center_kquo_cyclic : mx_irreducible rG → cyclic 'Z(G / rker rG)%g.
+ +
+Lemma der1_sub_rker :
+ group_splitting_field G → mx_irreducible rG →
+ (G^`(1) \subset rker rG)%g = (n == 1)%N.
+ +
+End AbelianQuotient.
+ +
+Section Similarity.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+CoInductive 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 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).
+ +
+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.
+ +
+ +
+Section Regular.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+ +
+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.
+ +
+ +
+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 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.
+ +
+Lemma irr1_rfix : (1%irr :=: rfix_mx aG G)%MS.
+ +
+Lemma rank_irr1 : \rank 1%irr = 1%N.
+ +
+Lemma degree_irr1 : 'n_1 = 1%N.
+ +
+Definition Wedderburn_subring (i : sG) := <<i ×m R_G>>%MS.
+ +
+ +
+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).
+ +
+ +
+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.
+ +
+
+
++ 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%N → mx_absolutely_irreducible.
+ +
+Lemma abelian_abs_irr : abelian G → mx_absolutely_irreducible = (n == 1%N).
+ +
+End OneRepresentation.
+ +
+ +
+ +
+ +
+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_groupType H).
+ +
+End SplittingField.
+ +
+Section Abelian.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Lemma mx_faithful_irr_center_cyclic n (rG : mx_representation F G n) :
+ mx_faithful 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%N.
+ +
+Lemma mxsimple_abelian_linear n (rG : mx_representation F G n) M :
+ abelian G → mxsimple rG M → \rank M = 1%N.
+ +
+Lemma linear_mxsimple n (rG : mx_representation F G n) (M : 'M_n) :
+ mxmodule rG M → \rank M = 1%N → mxsimple rG M.
+ +
+End Abelian.
+ +
+Section AbelianQuotient.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Variables (n : nat) (rG : mx_representation F G n).
+ +
+Lemma center_kquo_cyclic : mx_irreducible rG → cyclic 'Z(G / rker rG)%g.
+ +
+Lemma der1_sub_rker :
+ group_splitting_field G → mx_irreducible rG →
+ (G^`(1) \subset rker rG)%g = (n == 1)%N.
+ +
+End AbelianQuotient.
+ +
+Section Similarity.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+CoInductive 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 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).
+ +
+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.
+ +
+ +
+Section Regular.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+ +
+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.
+ +
+ +
+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 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.
+ +
+Lemma irr1_rfix : (1%irr :=: rfix_mx aG G)%MS.
+ +
+Lemma rank_irr1 : \rank 1%irr = 1%N.
+ +
+Lemma degree_irr1 : 'n_1 = 1%N.
+ +
+Definition Wedderburn_subring (i : sG) := <<i ×m R_G>>%MS.
+ +
+ +
+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).
+ +
+ +
+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).
+ +
+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].
+ +
+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%N].
+ +
+Lemma irr_degree_abelian : abelian G → ∀ i, 'n_i = 1%N.
+ +
+Lemma linear_irr_comp i : 'n_i = 1%N → (i :=: socle_base i)%MS.
+ +
+Lemma Wedderburn_subring_center i : ('Z('R_i) :=: mxvec 'e_i)%MS.
+ +
+Lemma Wedderburn_center :
+ ('Z(R_G) :=: \matrix_(i < #|sG|) mxvec 'e_(enum_val i))%MS.
+ +
+Lemma card_irr : #|sG| = tG.
+ +
+Section CenterMode.
+ +
+Variable i : sG.
+ +
+Let i0 := Ordinal (irr_degree_gt0 i).
+ +
+Definition irr_mode x := irr_repr i x i0 i0.
+ +
+Lemma irr_mode1 : irr_mode 1 = 1.
+ +
+Lemma irr_center_scalar : {in 'Z(G), ∀ x, irr_repr i x = (irr_mode x)%:M}.
+ +
+Lemma irr_modeM : {in 'Z(G) &, {morph irr_mode : x y / (x × y)%g >-> x × y}}.
+ +
+Lemma irr_modeX n : {in 'Z(G), {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.
+ +
+ +
+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.
+ +
+ +
+ +
+ +
+Notation "'Cl" := (Clifford_action _) : action_scope.
+ +
+Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.
+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.
+ +
+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.
+ +
+
+
++Variables (n : nat) (rG : mx_representation F G n).
+ +
+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].
+ +
+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%N].
+ +
+Lemma irr_degree_abelian : abelian G → ∀ i, 'n_i = 1%N.
+ +
+Lemma linear_irr_comp i : 'n_i = 1%N → (i :=: socle_base i)%MS.
+ +
+Lemma Wedderburn_subring_center i : ('Z('R_i) :=: mxvec 'e_i)%MS.
+ +
+Lemma Wedderburn_center :
+ ('Z(R_G) :=: \matrix_(i < #|sG|) mxvec 'e_(enum_val i))%MS.
+ +
+Lemma card_irr : #|sG| = tG.
+ +
+Section CenterMode.
+ +
+Variable i : sG.
+ +
+Let i0 := Ordinal (irr_degree_gt0 i).
+ +
+Definition irr_mode x := irr_repr i x i0 i0.
+ +
+Lemma irr_mode1 : irr_mode 1 = 1.
+ +
+Lemma irr_center_scalar : {in 'Z(G), ∀ x, irr_repr i x = (irr_mode x)%:M}.
+ +
+Lemma irr_modeM : {in 'Z(G) &, {morph irr_mode : x y / (x × y)%g >-> x × y}}.
+ +
+Lemma irr_modeX n : {in 'Z(G), {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.
+ +
+ +
+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.
+ +
+ +
+ +
+ +
+Notation "'Cl" := (Clifford_action _) : action_scope.
+ +
+Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.
+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.
+ +
+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}).
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Section OneRepresentation.
+ +
+Variables (n : nat) (rG : mx_representation aF G n).
+ +
+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.
+ +
+
+
++ +
+Variables (aF rF : fieldType) (f : {rmorphism aF → rF}).
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Section OneRepresentation.
+ +
+Variables (n : nat) (rG : mx_representation aF G n).
+ +
+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.
+ +
+Section GenField.
+ +
+Variables (F : fieldType) (gT : finGroupType) (G : {group gT}) (n' : nat).
+Variables (rG : mx_representation F G n) (A : 'M[F]_n).
+ +
+Let d_gt0 := mxminpoly_nonconstant A.
+ +
+Record gen_of (irrG : irr rG) (cGA : centgmx rG A) := Gen {rVval : 'rV[F]_d}.
+ +
+Hypotheses (irrG : irr rG) (cGA : centgmx rG A).
+ +
+Notation FA := (gen_of irrG cGA).
+Let inFA := Gen irrG cGA.
+ +
+Canonical gen_subType := Eval hnf in [newType for @rVval irrG cGA].
+Definition gen_eqMixin := Eval hnf in [eqMixin of FA by <:].
+Canonical gen_eqType := Eval hnf in EqType FA gen_eqMixin.
+Definition gen_choiceMixin := [choiceMixin of FA by <:].
+Canonical gen_choiceType := Eval hnf in ChoiceType FA gen_choiceMixin.
+ +
+Definition gen0 := inFA 0.
+Definition genN (x : FA) := inFA (- val x).
+Definition genD (x y : FA) := inFA (val x + val y).
+ +
+Lemma gen_addA : associative genD.
+ +
+Lemma gen_addC : commutative genD.
+ +
+Lemma gen_add0r : left_id gen0 genD.
+ +
+Lemma gen_addNr : left_inverse gen0 genN genD.
+ +
+Definition gen_zmodMixin := ZmodMixin gen_addA gen_addC gen_add0r gen_addNr.
+Canonical gen_zmodType := Eval hnf in ZmodType FA gen_zmodMixin.
+ +
+Definition pval (x : FA) := rVpoly (val x).
+ +
+Definition mxval (x : FA) := horner_mx A (pval x).
+ +
+Definition gen (x : F) := inFA (poly_rV x%:P).
+ +
+Lemma genK x : mxval (gen x) = x%:M.
+ +
+Lemma mxval_inj : injective mxval.
+ +
+Lemma mxval0 : mxval 0 = 0.
+ +
+Lemma mxvalN : {morph mxval : x / - x}.
+ +
+Lemma mxvalD : {morph mxval : x y / x + y}.
+ +
+Definition mxval_sum := big_morph mxval mxvalD mxval0.
+ +
+Definition gen1 := inFA (poly_rV 1).
+Definition genM x y := inFA (poly_rV (pval x × pval y %% pA)).
+Definition genV x := inFA (poly_rV (mx_inv_horner A (mxval x)^-1)).
+ +
+Lemma mxval_gen1 : mxval gen1 = 1%:M.
+ +
+Lemma mxval_genM : {morph mxval : x y / genM x y >-> x ×m y}.
+ +
+Lemma mxval_genV : {morph mxval : x / genV x >-> invmx x}.
+ +
+Lemma gen_mulA : associative genM.
+ +
+Lemma gen_mulC : commutative genM.
+ +
+Lemma gen_mul1r : left_id gen1 genM.
+ +
+Lemma gen_mulDr : left_distributive genM +%R.
+ +
+Lemma gen_ntriv : gen1 != 0.
+ +
+Definition gen_ringMixin :=
+ ComRingMixin gen_mulA gen_mulC gen_mul1r gen_mulDr gen_ntriv.
+Canonical gen_ringType := Eval hnf in RingType FA gen_ringMixin.
+Canonical gen_comRingType := Eval hnf in ComRingType FA gen_mulC.
+ +
+Lemma mxval1 : mxval 1 = 1%:M.
+ +
+Lemma mxvalM : {morph mxval : x y / x × y >-> x ×m y}.
+ +
+Lemma mxval_sub : additive mxval.
+ Canonical mxval_additive := Additive mxval_sub.
+ +
+Lemma mxval_is_multiplicative : multiplicative mxval.
+ Canonical mxval_rmorphism := AddRMorphism mxval_is_multiplicative.
+ +
+Lemma mxval_centg x : centgmx rG (mxval x).
+ +
+Lemma gen_mulVr : GRing.Field.axiom genV.
+ +
+Lemma gen_invr0 : genV 0 = 0.
+ +
+Definition gen_unitRingMixin := FieldUnitMixin gen_mulVr gen_invr0.
+Canonical gen_unitRingType := Eval hnf in UnitRingType FA gen_unitRingMixin.
+Canonical gen_comUnitRingType := Eval hnf in [comUnitRingType of FA].
+Definition gen_fieldMixin :=
+ @FieldMixin _ _ _ _ : GRing.Field.mixin_of gen_unitRingType.
+Definition gen_idomainMixin := FieldIdomainMixin gen_fieldMixin.
+Canonical gen_idomainType := Eval hnf in IdomainType FA gen_idomainMixin.
+Canonical gen_fieldType := Eval hnf in FieldType FA gen_fieldMixin.
+ +
+Lemma mxvalV : {morph mxval : x / x^-1 >-> invmx x}.
+ +
+Lemma gen_is_rmorphism : rmorphism gen.
+Canonical gen_additive := Additive gen_is_rmorphism.
+Canonical gen_rmorphism := RMorphism gen_is_rmorphism.
+ +
+
+
++ +
+Section GenField.
+ +
+Variables (F : fieldType) (gT : finGroupType) (G : {group gT}) (n' : nat).
+Variables (rG : mx_representation F G n) (A : 'M[F]_n).
+ +
+Let d_gt0 := mxminpoly_nonconstant A.
+ +
+Record gen_of (irrG : irr rG) (cGA : centgmx rG A) := Gen {rVval : 'rV[F]_d}.
+ +
+Hypotheses (irrG : irr rG) (cGA : centgmx rG A).
+ +
+Notation FA := (gen_of irrG cGA).
+Let inFA := Gen irrG cGA.
+ +
+Canonical gen_subType := Eval hnf in [newType for @rVval irrG cGA].
+Definition gen_eqMixin := Eval hnf in [eqMixin of FA by <:].
+Canonical gen_eqType := Eval hnf in EqType FA gen_eqMixin.
+Definition gen_choiceMixin := [choiceMixin of FA by <:].
+Canonical gen_choiceType := Eval hnf in ChoiceType FA gen_choiceMixin.
+ +
+Definition gen0 := inFA 0.
+Definition genN (x : FA) := inFA (- val x).
+Definition genD (x y : FA) := inFA (val x + val y).
+ +
+Lemma gen_addA : associative genD.
+ +
+Lemma gen_addC : commutative genD.
+ +
+Lemma gen_add0r : left_id gen0 genD.
+ +
+Lemma gen_addNr : left_inverse gen0 genN genD.
+ +
+Definition gen_zmodMixin := ZmodMixin gen_addA gen_addC gen_add0r gen_addNr.
+Canonical gen_zmodType := Eval hnf in ZmodType FA gen_zmodMixin.
+ +
+Definition pval (x : FA) := rVpoly (val x).
+ +
+Definition mxval (x : FA) := horner_mx A (pval x).
+ +
+Definition gen (x : F) := inFA (poly_rV x%:P).
+ +
+Lemma genK x : mxval (gen x) = x%:M.
+ +
+Lemma mxval_inj : injective mxval.
+ +
+Lemma mxval0 : mxval 0 = 0.
+ +
+Lemma mxvalN : {morph mxval : x / - x}.
+ +
+Lemma mxvalD : {morph mxval : x y / x + y}.
+ +
+Definition mxval_sum := big_morph mxval mxvalD mxval0.
+ +
+Definition gen1 := inFA (poly_rV 1).
+Definition genM x y := inFA (poly_rV (pval x × pval y %% pA)).
+Definition genV x := inFA (poly_rV (mx_inv_horner A (mxval x)^-1)).
+ +
+Lemma mxval_gen1 : mxval gen1 = 1%:M.
+ +
+Lemma mxval_genM : {morph mxval : x y / genM x y >-> x ×m y}.
+ +
+Lemma mxval_genV : {morph mxval : x / genV x >-> invmx x}.
+ +
+Lemma gen_mulA : associative genM.
+ +
+Lemma gen_mulC : commutative genM.
+ +
+Lemma gen_mul1r : left_id gen1 genM.
+ +
+Lemma gen_mulDr : left_distributive genM +%R.
+ +
+Lemma gen_ntriv : gen1 != 0.
+ +
+Definition gen_ringMixin :=
+ ComRingMixin gen_mulA gen_mulC gen_mul1r gen_mulDr gen_ntriv.
+Canonical gen_ringType := Eval hnf in RingType FA gen_ringMixin.
+Canonical gen_comRingType := Eval hnf in ComRingType FA gen_mulC.
+ +
+Lemma mxval1 : mxval 1 = 1%:M.
+ +
+Lemma mxvalM : {morph mxval : x y / x × y >-> x ×m y}.
+ +
+Lemma mxval_sub : additive mxval.
+ Canonical mxval_additive := Additive mxval_sub.
+ +
+Lemma mxval_is_multiplicative : multiplicative mxval.
+ Canonical mxval_rmorphism := AddRMorphism mxval_is_multiplicative.
+ +
+Lemma mxval_centg x : centgmx rG (mxval x).
+ +
+Lemma gen_mulVr : GRing.Field.axiom genV.
+ +
+Lemma gen_invr0 : genV 0 = 0.
+ +
+Definition gen_unitRingMixin := FieldUnitMixin gen_mulVr gen_invr0.
+Canonical gen_unitRingType := Eval hnf in UnitRingType FA gen_unitRingMixin.
+Canonical gen_comUnitRingType := Eval hnf in [comUnitRingType of FA].
+Definition gen_fieldMixin :=
+ @FieldMixin _ _ _ _ : GRing.Field.mixin_of gen_unitRingType.
+Definition gen_idomainMixin := FieldIdomainMixin gen_fieldMixin.
+Canonical gen_idomainType := Eval hnf in IdomainType FA gen_idomainMixin.
+Canonical gen_fieldType := Eval hnf in FieldType FA gen_fieldMixin.
+ +
+Lemma mxvalV : {morph mxval : x / x^-1 >-> invmx x}.
+ +
+Lemma gen_is_rmorphism : rmorphism gen.
+Canonical gen_additive := Additive gen_is_rmorphism.
+Canonical gen_rmorphism := RMorphism gen_is_rmorphism.
+ +
+
+ The generated field contains a root of the minimal polynomial (in some
+ cases we want to use the construction solely for that purpose).
+
+
+
+
+Definition groot := inFA (poly_rV ('X %% pA)).
+ +
+Lemma mxval_groot : mxval groot = A.
+ +
+Lemma mxval_grootX k : mxval (groot ^+ k) = A ^+ k.
+ +
+Lemma map_mxminpoly_groot : (map_poly gen pA).[groot] = 0.
+ +
+
+
++Definition groot := inFA (poly_rV ('X %% pA)).
+ +
+Lemma mxval_groot : mxval groot = A.
+ +
+Lemma mxval_grootX k : mxval (groot ^+ k) = A ^+ k.
+ +
+Lemma map_mxminpoly_groot : (map_poly gen pA).[groot] = 0.
+ +
+
+ Plugging the extension morphism gen into the ext_repr construction
+ yields a (reducible) tensored representation.
+
+
+
+
+ An alternative to the above, used in the proof of the p-stability of
+ groups of odd order, is to reconsider the original vector space as a
+ vector space of dimension n / e over FA. This is applicable only if G is
+ the largest group represented on the original vector space (i.e., if we
+ are not studying a representation of G induced by one of a larger group,
+ as in B & G Theorem 2.6 for instance). We can't fully exploit one of the
+ benefits of this approach -- that the type domain for the vector space can
+ remain unchanged -- because we're restricting ourselves to row matrices;
+ we have to use explicit bijections to convert between the two views.
+
+
+
+
+Definition subbase m (B : 'rV_m) : 'M_(m × d, n) :=
+ \matrix_ik mxvec (\matrix_(i, k) (row (B 0 i) (A ^+ k))) 0 ik.
+ +
+Lemma gen_dim_ex_proof : ∃ m, [∃ B : 'rV_m, row_free (subbase B)].
+ +
+Lemma gen_dim_ub_proof m :
+ [∃ B : 'rV_m, row_free (subbase B)] → (m ≤ n)%N.
+ +
+Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
+Notation m := gen_dim.
+ +
+Definition gen_base : 'rV_m := odflt 0 [pick B | row_free (subbase B)].
+Definition base := subbase gen_base.
+ +
+Lemma base_free : row_free base.
+ +
+Lemma base_full : row_full base.
+ +
+Lemma gen_dim_factor : (m × d)%N = n.
+ +
+Lemma gen_dim_gt0 : m > 0.
+ +
+Section Bijection.
+ +
+Variable m1 : nat.
+ +
+Definition in_gen (W : 'M[F]_(m1, n)) : 'M[FA]_(m1, m) :=
+ \matrix_(i, j) inFA (row j (vec_mx (row i W ×m pinvmx base))).
+ +
+Definition val_gen (W : 'M[FA]_(m1, m)) : 'M[F]_(m1, n) :=
+ \matrix_i (mxvec (\matrix_j val (W i j)) ×m base).
+ +
+Lemma in_genK : cancel in_gen val_gen.
+ +
+Lemma val_genK : cancel val_gen in_gen.
+ +
+Lemma in_gen0 : in_gen 0 = 0.
+ +
+Lemma val_gen0 : val_gen 0 = 0.
+ +
+Lemma in_genN : {morph in_gen : W / - W}.
+ +
+Lemma val_genN : {morph val_gen : W / - W}.
+ +
+Lemma in_genD : {morph in_gen : U V / U + V}.
+ +
+Lemma val_genD : {morph val_gen : U V / U + V}.
+ +
+Definition in_gen_sum := big_morph in_gen in_genD in_gen0.
+Definition val_gen_sum := big_morph val_gen val_genD val_gen0.
+ +
+Lemma in_genZ a : {morph in_gen : W / a *: W >-> gen a *: W}.
+ +
+End Bijection.
+ +
+ +
+Lemma val_gen_rV (w : 'rV_m) :
+ val_gen w = mxvec (\matrix_j val (w 0 j)) ×m base.
+ +
+Section Bijection2.
+ +
+Variable m1 : nat.
+ +
+Lemma val_gen_row W (i : 'I_m1) : val_gen (row i W) = row i (val_gen W).
+ +
+Lemma in_gen_row W (i : 'I_m1) : in_gen (row i W) = row i (in_gen W).
+ +
+Lemma row_gen_sum_mxval W (i : 'I_m1) :
+ row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).
+ +
+Lemma val_genZ x : {morph @val_gen m1 : 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.
+ +
+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 m1 U :=
+ <<\matrix_ik
+ mxvec (\matrix_(i < m1, k < d) (row i (val_gen U) ×m A ^+ k)) 0 ik>>%MS.
+ +
+Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, m)) :
+ (U ≤ rowval_gen V)%MS = (in_gen U ≤ V)%MS.
+ +
+Lemma rowval_genK m1 (U : 'M_(m1, m)) : (in_gen (rowval_gen U) :=: U)%MS.
+ +
+Lemma rowval_gen_stable m1 (U : 'M_(m1, m)) :
+ (rowval_gen U ×m A ≤ rowval_gen U)%MS.
+ +
+Lemma rstab_in_gen m1 (U : 'M_(m1, n)) : rstab rGA (in_gen U) = rstab rG U.
+ +
+Lemma rstabs_in_gen m1 (U : 'M_(m1, n)) :
+ rstabs rG U \subset rstabs rGA (in_gen U).
+ +
+Lemma rstabs_rowval_gen m1 (U : 'M_(m1, m)) :
+ rstabs rG (rowval_gen U) = rstabs rGA U.
+ +
+Lemma mxmodule_rowval_gen m1 (U : 'M_(m1, m)) :
+ mxmodule rG (rowval_gen U) = mxmodule rGA U.
+ +
+Lemma gen_mx_irr : mx_irreducible rGA.
+ +
+Lemma rker_gen : rker rGA = rker rG.
+ +
+Lemma gen_mx_faithful : mx_faithful rGA = mx_faithful rG.
+ +
+End GenField.
+ +
+Section DecideGenField.
+ +
+Import MatrixFormula.
+ +
+Variable F : decFieldType.
+ +
+ +
+ +
+Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
+Variables (rG : mx_representation F G n) (A : 'M[F]_n).
+Hypotheses (irrG : mx_irreducible rG) (cGA : centgmx rG A).
+ +
+Let d_gt0 : d > 0 := mxminpoly_nonconstant A.
+ +
+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).
+ +
+
+
++Definition subbase m (B : 'rV_m) : 'M_(m × d, n) :=
+ \matrix_ik mxvec (\matrix_(i, k) (row (B 0 i) (A ^+ k))) 0 ik.
+ +
+Lemma gen_dim_ex_proof : ∃ m, [∃ B : 'rV_m, row_free (subbase B)].
+ +
+Lemma gen_dim_ub_proof m :
+ [∃ B : 'rV_m, row_free (subbase B)] → (m ≤ n)%N.
+ +
+Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
+Notation m := gen_dim.
+ +
+Definition gen_base : 'rV_m := odflt 0 [pick B | row_free (subbase B)].
+Definition base := subbase gen_base.
+ +
+Lemma base_free : row_free base.
+ +
+Lemma base_full : row_full base.
+ +
+Lemma gen_dim_factor : (m × d)%N = n.
+ +
+Lemma gen_dim_gt0 : m > 0.
+ +
+Section Bijection.
+ +
+Variable m1 : nat.
+ +
+Definition in_gen (W : 'M[F]_(m1, n)) : 'M[FA]_(m1, m) :=
+ \matrix_(i, j) inFA (row j (vec_mx (row i W ×m pinvmx base))).
+ +
+Definition val_gen (W : 'M[FA]_(m1, m)) : 'M[F]_(m1, n) :=
+ \matrix_i (mxvec (\matrix_j val (W i j)) ×m base).
+ +
+Lemma in_genK : cancel in_gen val_gen.
+ +
+Lemma val_genK : cancel val_gen in_gen.
+ +
+Lemma in_gen0 : in_gen 0 = 0.
+ +
+Lemma val_gen0 : val_gen 0 = 0.
+ +
+Lemma in_genN : {morph in_gen : W / - W}.
+ +
+Lemma val_genN : {morph val_gen : W / - W}.
+ +
+Lemma in_genD : {morph in_gen : U V / U + V}.
+ +
+Lemma val_genD : {morph val_gen : U V / U + V}.
+ +
+Definition in_gen_sum := big_morph in_gen in_genD in_gen0.
+Definition val_gen_sum := big_morph val_gen val_genD val_gen0.
+ +
+Lemma in_genZ a : {morph in_gen : W / a *: W >-> gen a *: W}.
+ +
+End Bijection.
+ +
+ +
+Lemma val_gen_rV (w : 'rV_m) :
+ val_gen w = mxvec (\matrix_j val (w 0 j)) ×m base.
+ +
+Section Bijection2.
+ +
+Variable m1 : nat.
+ +
+Lemma val_gen_row W (i : 'I_m1) : val_gen (row i W) = row i (val_gen W).
+ +
+Lemma in_gen_row W (i : 'I_m1) : in_gen (row i W) = row i (in_gen W).
+ +
+Lemma row_gen_sum_mxval W (i : 'I_m1) :
+ row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).
+ +
+Lemma val_genZ x : {morph @val_gen m1 : 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.
+ +
+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 m1 U :=
+ <<\matrix_ik
+ mxvec (\matrix_(i < m1, k < d) (row i (val_gen U) ×m A ^+ k)) 0 ik>>%MS.
+ +
+Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, m)) :
+ (U ≤ rowval_gen V)%MS = (in_gen U ≤ V)%MS.
+ +
+Lemma rowval_genK m1 (U : 'M_(m1, m)) : (in_gen (rowval_gen U) :=: U)%MS.
+ +
+Lemma rowval_gen_stable m1 (U : 'M_(m1, m)) :
+ (rowval_gen U ×m A ≤ rowval_gen U)%MS.
+ +
+Lemma rstab_in_gen m1 (U : 'M_(m1, n)) : rstab rGA (in_gen U) = rstab rG U.
+ +
+Lemma rstabs_in_gen m1 (U : 'M_(m1, n)) :
+ rstabs rG U \subset rstabs rGA (in_gen U).
+ +
+Lemma rstabs_rowval_gen m1 (U : 'M_(m1, m)) :
+ rstabs rG (rowval_gen U) = rstabs rGA U.
+ +
+Lemma mxmodule_rowval_gen m1 (U : 'M_(m1, m)) :
+ mxmodule rG (rowval_gen U) = mxmodule rGA U.
+ +
+Lemma gen_mx_irr : mx_irreducible rGA.
+ +
+Lemma rker_gen : rker rGA = rker rG.
+ +
+Lemma gen_mx_faithful : mx_faithful rGA = mx_faithful rG.
+ +
+End GenField.
+ +
+Section DecideGenField.
+ +
+Import MatrixFormula.
+ +
+Variable F : decFieldType.
+ +
+ +
+ +
+Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
+Variables (rG : mx_representation F G n) (A : 'M[F]_n).
+Hypotheses (irrG : mx_irreducible rG) (cGA : centgmx rG A).
+ +
+Let d_gt0 : d > 0 := mxminpoly_nonconstant A.
+ +
+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).
+ +
+
+ WARNING: Coq will core dump if the Notation Bool is used in the match
+ pattern here.
+
+
+Fixpoint gen_form f := match f with
+| GRing.Bool b ⇒ Bool b
+| t1 == t2 ⇒ mxrank_form 0 (gen_term (t1 - t2))
+| GRing.Unit t1 ⇒ mxrank_form 1 (gen_term t1)
+| f1 ∧ f2 ⇒ gen_form f1 ∧ gen_form f2
+| f1 ∨ f2 ⇒ gen_form f1 ∨ gen_form f2
+| f1 ==> f2 ⇒ gen_form f1 ==> gen_form f2
+| ¬ f1 ⇒ ¬ gen_form f1
+| ('∃ '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)).
+ +
+Lemma gen_satP : GRing.DecidableField.axiom gen_sat.
+ +
+Definition gen_decFieldMixin := DecFieldMixin gen_satP.
+ +
+Canonical gen_decFieldType := Eval hnf in DecFieldType FA gen_decFieldMixin.
+ +
+End DecideGenField.
+ +
+Section FiniteGenField.
+ +
+Variables (F : finFieldType) (gT : finGroupType) (G : {group gT}) (n' : nat).
+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).
+ +
+
+
++| GRing.Bool b ⇒ Bool b
+| t1 == t2 ⇒ mxrank_form 0 (gen_term (t1 - t2))
+| GRing.Unit t1 ⇒ mxrank_form 1 (gen_term t1)
+| f1 ∧ f2 ⇒ gen_form f1 ∧ gen_form f2
+| f1 ∨ f2 ⇒ gen_form f1 ∨ gen_form f2
+| f1 ==> f2 ⇒ gen_form f1 ==> gen_form f2
+| ¬ f1 ⇒ ¬ gen_form f1
+| ('∃ '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)).
+ +
+Lemma gen_satP : GRing.DecidableField.axiom gen_sat.
+ +
+Definition gen_decFieldMixin := DecFieldMixin gen_satP.
+ +
+Canonical gen_decFieldType := Eval hnf in DecFieldType FA gen_decFieldMixin.
+ +
+End DecideGenField.
+ +
+Section FiniteGenField.
+ +
+Variables (F : finFieldType) (gT : finGroupType) (G : {group gT}) (n' : nat).
+Variables (rG : mx_representation F G n) (A : 'M[F]_n).
+Hypotheses (irrG : mx_irreducible rG) (cGA : centgmx rG A).
+Notation FA := (gen_of irrG cGA).
+ +
+
+ This should be [countMixin of FA by <: ]
+
+
+Definition gen_countMixin := (sub_countMixin (gen_subType irrG cGA)).
+Canonical gen_countType := Eval hnf in CountType FA gen_countMixin.
+Canonical gen_subCountType := Eval hnf in [subCountType of FA].
+Definition gen_finMixin := [finMixin of FA by <:].
+Canonical gen_finType := Eval hnf in FinType FA gen_finMixin.
+Canonical gen_subFinType := Eval hnf in [subFinType of FA].
+Canonical gen_finZmodType := Eval hnf in [finZmodType of FA].
+Canonical gen_baseFinGroupType := Eval hnf in [baseFinGroupType of FA for +%R].
+Canonical gen_finGroupType := Eval hnf in [finGroupType of FA for +%R].
+Canonical gen_finRingType := Eval hnf in [finRingType of FA].
+Canonical gen_finComRingType := Eval hnf in [finComRingType of FA].
+Canonical gen_finUnitRingType := Eval hnf in [finUnitRingType of FA].
+Canonical gen_finComUnitRingType := Eval hnf in [finComUnitRingType of FA].
+Canonical gen_finIdomainType := Eval hnf in [finIdomainType of FA].
+Canonical gen_finFieldType := Eval hnf in [finFieldType of FA].
+ +
+Lemma card_gen : #|{:FA}| = (#|F| ^ degree_mxminpoly A)%N.
+ +
+End FiniteGenField.
+ +
+End MatrixGenField.
+ +
+Canonical gen_subType.
+Canonical gen_eqType.
+Canonical gen_choiceType.
+Canonical gen_countType.
+Canonical gen_subCountType.
+Canonical gen_finType.
+Canonical gen_subFinType.
+Canonical gen_zmodType.
+Canonical gen_finZmodType.
+Canonical gen_baseFinGroupType.
+Canonical gen_finGroupType.
+Canonical gen_ringType.
+Canonical gen_finRingType.
+Canonical gen_comRingType.
+Canonical gen_finComRingType.
+Canonical gen_unitRingType.
+Canonical gen_finUnitRingType.
+Canonical gen_comUnitRingType.
+Canonical gen_finComUnitRingType.
+Canonical gen_idomainType.
+Canonical gen_finIdomainType.
+Canonical gen_fieldType.
+Canonical gen_finFieldType.
+Canonical gen_decFieldType.
+ +
+
+
++Canonical gen_countType := Eval hnf in CountType FA gen_countMixin.
+Canonical gen_subCountType := Eval hnf in [subCountType of FA].
+Definition gen_finMixin := [finMixin of FA by <:].
+Canonical gen_finType := Eval hnf in FinType FA gen_finMixin.
+Canonical gen_subFinType := Eval hnf in [subFinType of FA].
+Canonical gen_finZmodType := Eval hnf in [finZmodType of FA].
+Canonical gen_baseFinGroupType := Eval hnf in [baseFinGroupType of FA for +%R].
+Canonical gen_finGroupType := Eval hnf in [finGroupType of FA for +%R].
+Canonical gen_finRingType := Eval hnf in [finRingType of FA].
+Canonical gen_finComRingType := Eval hnf in [finComRingType of FA].
+Canonical gen_finUnitRingType := Eval hnf in [finUnitRingType of FA].
+Canonical gen_finComUnitRingType := Eval hnf in [finComUnitRingType of FA].
+Canonical gen_finIdomainType := Eval hnf in [finIdomainType of FA].
+Canonical gen_finFieldType := Eval hnf in [finFieldType of FA].
+ +
+Lemma card_gen : #|{:FA}| = (#|F| ^ degree_mxminpoly A)%N.
+ +
+End FiniteGenField.
+ +
+End MatrixGenField.
+ +
+Canonical gen_subType.
+Canonical gen_eqType.
+Canonical gen_choiceType.
+Canonical gen_countType.
+Canonical gen_subCountType.
+Canonical gen_finType.
+Canonical gen_subFinType.
+Canonical gen_zmodType.
+Canonical gen_finZmodType.
+Canonical gen_baseFinGroupType.
+Canonical gen_finGroupType.
+Canonical gen_ringType.
+Canonical gen_finRingType.
+Canonical gen_comRingType.
+Canonical gen_finComRingType.
+Canonical gen_unitRingType.
+Canonical gen_finUnitRingType.
+Canonical gen_comUnitRingType.
+Canonical gen_finComUnitRingType.
+Canonical gen_idomainType.
+Canonical gen_finIdomainType.
+Canonical gen_fieldType.
+Canonical gen_finFieldType.
+Canonical gen_decFieldType.
+ +
+
+ Classical splitting and closure field constructions provide convenient
+ packaging for the pointwise construction.
+
+
+Section BuildSplittingField.
+ +
+Implicit Type gT : finGroupType.
+Implicit Type F : fieldType.
+ +
+Lemma group_splitting_field_exists 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.
+
++ +
+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.
+