Library mathcomp.character.mxrepresentation
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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. DecSocleType rG is opaque.
- socle_base W == for W : (sG : socleType), a simple module whose
- component is W; socle_simple W and socle_module W are
- proofs that socle_base W is a simple module.
- socle_mult W == the multiplicity of socle_base W in W : sG.
- := \rank W %/ \rank (socle_base W)
- Socle sG == the Socle of rG, given sG : socleType rG, i.e., the
- (direct) sum of all the components of rG.
- mx_rsim rG rG' <-> rG and rG' are similar representations of the same
- group G. Note that rG and rG' must then have equal, but
- not necessarily convertible, degree.
- submod_repr modU == a representation of G on 'rV(\rank U) equivalent to
- the restriction of rG to U (here modU : mxmodule rG U).
- socle_repr W := submod_repr (socle_module W)
- val/in_submod rG U == the projections resp. from/onto 'rV(\rank U),
- that correspond to submod_repr r G U (these work both on
- vectors and row spaces).
- factmod_repr modV == a representation of G on 'rV(\rank (cokermx V)) that
- is equivalent to the factor module 'rV_n / V induced by V
- and rG (here modV : mxmodule rG V).
- val/in_factmod rG U == the projections for factmod_repr r G U.
- section_repr modU modV == the restriction to in_factmod V U of the factor
- representation factmod_repr modV (for modU : mxmodule rG U
- and modV : mxmodule rG V); section_repr modU modV is
- irreducible iff max_submod rG U V.
- subseries_repr modUs i == the representation for the section module
- in_factmod (0 :: Us)`i Us`i, where
- modUs : mx_subseries rG Us.
- series_repr compUs i == the representation for the section module
- in_factmod (0 :: Us)`i Us`i, where
- compUs : mx_composition_series rG Us. The Jordan-Holder
- theorem asserts the uniqueness of the set of such
- representations, up to similarity and permutation.
- regular_repr F G == the regular F-representation of the group G.
- group_ring F G == a #|G| x #|G|^2 matrix that encodes the free group
- ring of G -- that is, the enveloping algebra of the
- regular F-representation of G.
- gring_index x == the index corresponding to x \in G in the matrix
- encoding of regular_repr and group_ring.
- gring_row A == the row vector corresponding to A \in group_ring F G in
- the regular FG-module.
- gring_proj x A == the 1 x 1 matrix holding the coefficient of x \in G in
- (A \in group_ring F G)%MS.
- gring_mx rG u == the image of a row vector u of the regular FG-module,
- in the enveloping algebra of another representation rG.
- gring_op rG A == the image of a matrix of the free group ring of G,
- in the enveloping algebra of rG.
- gset_mx F G C == the group sum of C in the free group ring of G -- the
- sum of the images of all the x \in C in group_ring F G.
- classg_base F G == a #|classes G| x #|G|^2 matrix whose rows encode the
- group sums of the conjugacy classes of G -- this is a
- basis of 'Z(group_ring F G)%MS.
- irrType F G == a type indexing irreducible representations of G over a
- field F, provided its characteristic does not divide the
- order of G; it also indexes Wedderburn subrings.
- := socleType (regular_repr F G)
- irr_repr i == the irreducible representation corresponding to the
- index i : irrType sG
- := socle_repr i as i coerces to a component matrix.
- 'n_i, irr_degree i == the degree of irr_repr i; the notation is only
- active after Open Scope group_ring_scope.
- linear_irr sG == the set of sG-indices of linear irreducible
- representations of G.
- irr_comp sG rG == the sG-index of the unique irreducible representation
- similar to rG, at least when rG is irreducible and the
- characteristic is coprime.
- irr_mode i z == the unique eigenvalue of irr_repr i z, at least when
- irr_repr i z is scalar (e.g., when z \in 'Z(G)).
- [1 sG]%irr == the index of the principal representation of G, in
- sG : irrType F G. The i argument of irr_repr, irr_degree
- and irr_mode is in the %irr scope. This notation may be
- replaced locally by an interpretation of 1%irr as [1 sG]
- for some specific irrType sG.
- 'R_i, Wedderburn_subring i == the subring (indeed, the component) of the
- free group ring of G corresponding to the component i : sG
- of the regular FG-module, where sG : irrType F g. In
- coprime characteristic the Wedderburn structure theorem
- asserts that the free group ring is the direct sum of
- these subrings; as with 'n_i above, the notation is only
- active in group_ring_scope.
- 'e_i, Wedderburn_id i == the projection of the identity matrix 1%:M on the
- Wedderburn subring of i : sG (with sG a socleType). In
- coprime characteristic this is the identity element of
- the subring, and the basis of its center if the field F is
- a splitting field. As 'R_i, 'e_i is in group_ring_scope.
- subg_repr rG sHG == the restriction to H of the representation rG of G;
- here sHG : H \subset G.
- eqg_repr rG eqHG == the representation rG of G viewed a a representation
- of H; here eqHG : G == H.
- morphpre_repr f rG == the representation of f @*^-1 G obtained by
- composing the group morphism f with rG.
- morphim_repr rGf sGD == the representation of G induced by a
- representation rGf of f @* G; here sGD : G \subset D where
- D is the domain of the group morphism f.
- rconj_repr rG uB == the conjugate representation x |-> B * rG x * B^-1;
- here uB : B \in unitmx.
- quo_repr sHK nHG == the representation of G / H induced by rG, given
- sHK : H \subset rker rG, and nHG : G \subset 'N(H).
- kquo_repr rG == the representation induced on G / rker rG by rG.
- map_repr f rG == the representation f \o rG, whose module is the tensor
- product of the module of rG with the extension field into
- which f : {rmorphism F -> Fstar} embeds F.
- 'Cl%act == the transitive action of G on the Wedderburn components of
- H, with nsGH : H <| G, given by Clifford's theorem. More
- precisely this is a total action of G on socle_sort sH,
- where sH : socleType (subg_repr rG (normal_sub sGH)).
- We build on the MatrixFormula toolkit to define decision procedures for
- the reducibility property:
- mxmodule_form rG U == a formula asserting that the interpretation of U is
- a module of the representation rG.
- mxnonsimple_form rG U == a formula asserting that the interpretation of U
- contains a proper nontrivial rG-module.
- mxnonsimple_sat rG U <=> mxnonsimple_form rG U is satisfied.
- More involved constructions are encapsulated in two Coq submodules:
- MatrixGenField == a module that encapsulates the lengthy details of the
- construction of appropriate extension fields. We assume we
- have an irreducible representation rG of a group G, and a
- non-scalar matrix A that centralises rG(G), as this data
- is readily extracted from the Jacobson density theorem. It
- then follows from Schur's lemma that the ring generated by
- A is a field on which the extension of the representation
- rG of G is reducible. Note that this is equivalent to the
- more traditional quotient of the polynomial ring by an
- irreducible polynomial (the minimal polynomial of A), but
- much better suited to our needs.
- Here are the main definitions of MatrixGenField; they all have three
- proofs as arguments: (implicit) rG : mx_repr n G, irrG : mx_irreducible rG
- and cGA : centgmx rG A. These ensure the validity of the construction and
- allow us to define Canonical instances; we assume degree_mxminpoly A > 1
- (which is equivalent to ~~ is_scalar_mx A) only to prove reducibility.
- + gen_of irrG cGA == the carrier type of the field generated by A. It is
- at least equipped with a fieldType structure; we also
- propagate any decFieldType/finFieldType structures on the
- original field.
- + gen irrG cGA == the morphism injecting into gen_of irrG cGA.
- + groot irrG cGA == the root of mxminpoly A in the gen_of irrG cGA field.
- + pval x, rVval x, mxval x == the interpretation of x : gen_of irrG cGA
- as a polynomial, a row vector, and a matrix, respectively.
- Both irrG and cGA are implicit arguments here.
- + gen_repr irrG cGA == an alternative to the field extension
- representation, which consists in reconsidering the
- original module as a module over the new gen_of field,
- thereby DIVIDING the original dimension n by the degree of
- the minimal polynomial of A. This can be simpler than the
- extension method, is actually required by the proof that
- odd groups are p-stable (B & G 6.1-2, and Appendix A), but
- is only applicable if G is the LARGEST group represented
- by rG (e.g., NOT for B & G 2.6).
- + gen_dim A == the dimension of gen_repr irrG cGA (only depends on A).
- + in_gen irrG cGA W == the ROWWISE image of a matrix W : 'M[F](m, n),
- i.e., interpreting W as a sequence of m tow vectors,
- under the bijection from rG to gen_repr irrG cGA.
- The sequence length m is a maximal implicit argument
- passed between the explicit argument cGA and W.
- + val_gen W == the ROWWISE image of an 'M[gen_of irrG cGA](m, gen_dim A)
- matrix W under the bijection from gen_repr irrG cGA to rG.
- + rowval_gen W == the ROWSPACE image of W under the bijection from
- gen_repr irrG cGA to rG, i.e., a 'M[F]_n matrix whose row
- space is the image of the row space of W.
- This is the A-ideal generated by val_gen W.
- + gen_sat e f <=> f : GRing.formula (gen_of irrG cGA) is satisfied in
- environment e : seq (gen_of irrG cGA), provided F has a
- decFieldType structure.
- + gen_env e, gen_term t, gen_form f == interpretations of environments,
- terms, and RING formulas over gen_of irrG cGA as row
- vector formulae, used to construct gen_sat.
-
-
-
-
-Set Implicit Arguments.
- -
-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 R m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).
- -
-Lemma repr_mxKV m x :
- x \in G → cancel ((@mulmx R m n n)^~ (rG x^-1)) (mulmx^~ (rG x)).
- -
-Lemma repr_mx_unit x : x \in G → rG x \in unitmx.
- -
-Lemma repr_mxV : {in G, {morph rG : x / x^-1%g >-> invmx x}}.
- -
-
-
--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 R m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).
- -
-Lemma repr_mxKV m x :
- x \in G → cancel ((@mulmx R m n n)^~ (rG x^-1)) (mulmx^~ (rG x)).
- -
-Lemma repr_mx_unit x : x \in G → rG x \in unitmx.
- -
-Lemma repr_mxV : {in G, {morph rG : x / x^-1%g >-> invmx x}}.
- -
-
- This is only used in the group ring construction below, as we only have
- developped the theory of matrix subalgebras for F-algebras.
-
-
-Definition enveloping_algebra_mx := \matrix_(i < #|G|) mxvec (rG (enum_val i)).
- -
-Section Stabiliser.
- -
-Variables (m : nat) (U : 'M[R]_(m, n)).
- -
-Definition rstab := [set x in G | U ×m rG x == U].
- -
-Lemma rstab_sub : rstab \subset G.
- -
-Lemma rstab_group_set : group_set rstab.
-Canonical rstab_group := Group rstab_group_set.
- -
-End Stabiliser.
- -
-
-
-- -
-Section Stabiliser.
- -
-Variables (m : nat) (U : 'M[R]_(m, n)).
- -
-Definition rstab := [set x in G | U ×m rG x == U].
- -
-Lemma rstab_sub : rstab \subset G.
- -
-Lemma rstab_group_set : group_set rstab.
-Canonical rstab_group := Group rstab_group_set.
- -
-End Stabiliser.
- -
-
- Centralizer subgroup and central homomorphisms.
-
-
-Section CentHom.
- -
-Variable f : 'M[R]_n.
- -
-Definition rcent := [set x in G | f ×m rG x == rG x ×m f].
- -
-Lemma rcent_sub : rcent \subset G.
- -
-Lemma rcent_group_set : group_set rcent.
-Canonical rcent_group := Group rcent_group_set.
- -
-Definition centgmx := G \subset rcent.
- -
-Lemma centgmxP : reflect (∀ x, x \in G → f ×m rG x = rG x ×m f) centgmx.
- -
-End CentHom.
- -
-
-
-- -
-Variable f : 'M[R]_n.
- -
-Definition rcent := [set x in G | f ×m rG x == rG x ×m f].
- -
-Lemma rcent_sub : rcent \subset G.
- -
-Lemma rcent_group_set : group_set rcent.
-Canonical rcent_group := Group rcent_group_set.
- -
-Definition centgmx := G \subset rcent.
- -
-Lemma centgmxP : reflect (∀ x, x \in G → f ×m rG x = rG x ×m f) centgmx.
- -
-End CentHom.
- -
-
- Representation kernel, and faithful representations.
-
-
-
-
-Definition rker := rstab 1%:M.
-Canonical rker_group := Eval hnf in [group of rker].
- -
-Lemma rkerP x : reflect (x \in G ∧ rG x = 1%:M) (x \in rker).
- -
-Lemma rker_norm : G \subset 'N(rker).
- -
-Lemma rker_normal : rker <| G.
- -
-Definition mx_faithful := rker \subset [1].
- -
-Lemma mx_faithful_inj : mx_faithful → {in G &, injective rG}.
- -
-Lemma rker_linear : n = 1%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.
-
-
-
-
-Variant mx_iso (U V : 'M_n) : Prop :=
- MxIso f of f \in unitmx & (U ≤ dom_hom_mx f)%MS & (U ×m f :=: V)%MS.
- -
-Lemma eqmx_iso U V : (U :=: V)%MS → mx_iso U V.
- -
-Lemma mx_iso_refl U : mx_iso U U.
- -
-Lemma mx_iso_sym U V : mx_iso U V → mx_iso V U.
- -
-Lemma mx_iso_trans U V W : mx_iso U V → mx_iso V W → mx_iso U W.
- -
-Lemma mxrank_iso U V : mx_iso U V → \rank U = \rank V.
- -
-Lemma mx_iso_module U V : mx_iso U V → mxmodule U → mxmodule V.
- -
-
-
--Variant mx_iso (U V : 'M_n) : Prop :=
- MxIso f of f \in unitmx & (U ≤ dom_hom_mx f)%MS & (U ×m f :=: V)%MS.
- -
-Lemma eqmx_iso U V : (U :=: V)%MS → mx_iso U V.
- -
-Lemma mx_iso_refl U : mx_iso U U.
- -
-Lemma mx_iso_sym U V : mx_iso U V → mx_iso V U.
- -
-Lemma mx_iso_trans U V W : mx_iso U V → mx_iso V W → mx_iso U W.
- -
-Lemma mxrank_iso U V : mx_iso U V → \rank U = \rank V.
- -
-Lemma mx_iso_module U V : mx_iso U V → mxmodule U → mxmodule V.
- -
-
- Simple modules (we reserve the term "irreducible" for representations).
-
-
-
-
-Definition mxsimple (V : 'M_n) :=
- [/\ mxmodule V, V != 0 &
- ∀ U : 'M_n, mxmodule U → (U ≤ V)%MS → U != 0 → (V ≤ U)%MS].
- -
-Definition mxnonsimple (U : 'M_n) :=
- ∃ V : 'M_n, [&& mxmodule V, (V ≤ U)%MS, V != 0 & \rank V < \rank U].
- -
-Lemma mxsimpleP U :
- [/\ mxmodule U, U != 0 & ¬ mxnonsimple U] ↔ mxsimple U.
- -
-Lemma mxsimple_module U : mxsimple U → mxmodule U.
- -
-Lemma mxsimple_exists m (U : 'M_(m, n)) :
- mxmodule U → U != 0 → classically (exists2 V, mxsimple V & V ≤ U)%MS.
- -
-Lemma mx_iso_simple U V : mx_iso U V → mxsimple U → mxsimple V.
- -
-Lemma mxsimple_cyclic u U :
- mxsimple U → u != 0 → (u ≤ U)%MS → (U :=: cyclic_mx u)%MS.
- -
-
-
--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.
- -
-Variant mxsemisimple (V : 'M_n) :=
- MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
- ∀ i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
- -
-
-
--Implicit Type I : finType.
- -
-Variant mxsemisimple (V : 'M_n) :=
- MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
- ∀ i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
- -
-
- This is a slight generalization of Aschbacher 12.5 for finite sets.
-
-
-Lemma sum_mxsimple_direct_compl m I W (U : 'M_(m, n)) :
- let V := (\sum_(i : I) W i)%MS in
- (∀ i : I, mxsimple (W i)) → mxmodule U → (U ≤ V)%MS →
- {J : {set I} | let S := U + \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
- -
-Lemma sum_mxsimple_direct_sub I W (V : 'M_n) :
- (∀ i : I, mxsimple (W i)) → (\sum_i W i :=: V)%MS →
- {J : {set I} | let S := \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
- -
-Lemma mxsemisimple0 : mxsemisimple 0.
- -
-Lemma intro_mxsemisimple (I : Type) r (P : pred I) W V :
- (\sum_(i <- r | P i) W i :=: V)%MS →
- (∀ i, P i → W i != 0 → mxsimple (W i)) →
- mxsemisimple V.
- -
-Lemma mxsimple_semisimple U : mxsimple U → mxsemisimple U.
- -
-Lemma addsmx_semisimple U V :
- mxsemisimple U → mxsemisimple V → mxsemisimple (U + V)%MS.
- -
-Lemma sumsmx_semisimple (I : finType) (P : pred I) V :
- (∀ i, P i → mxsemisimple (V i)) → mxsemisimple (\sum_(i | P i) V i)%MS.
- -
-Lemma eqmx_semisimple U V : (U :=: V)%MS → mxsemisimple U → mxsemisimple V.
- -
-Lemma hom_mxsemisimple (V f : 'M_n) :
- mxsemisimple V → (V ≤ dom_hom_mx f)%MS → mxsemisimple (V ×m f).
- -
-Lemma mxsemisimple_module U : mxsemisimple U → mxmodule U.
- -
-
-
-- let V := (\sum_(i : I) W i)%MS in
- (∀ i : I, mxsimple (W i)) → mxmodule U → (U ≤ V)%MS →
- {J : {set I} | let S := U + \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
- -
-Lemma sum_mxsimple_direct_sub I W (V : 'M_n) :
- (∀ i : I, mxsimple (W i)) → (\sum_i W i :=: V)%MS →
- {J : {set I} | let S := \sum_(i in J) W i in S :=: V ∧ mxdirect S}%MS.
- -
-Lemma mxsemisimple0 : mxsemisimple 0.
- -
-Lemma intro_mxsemisimple (I : Type) r (P : pred I) W V :
- (\sum_(i <- r | P i) W i :=: V)%MS →
- (∀ i, P i → W i != 0 → mxsimple (W i)) →
- mxsemisimple V.
- -
-Lemma mxsimple_semisimple U : mxsimple U → mxsemisimple U.
- -
-Lemma addsmx_semisimple U V :
- mxsemisimple U → mxsemisimple V → mxsemisimple (U + V)%MS.
- -
-Lemma sumsmx_semisimple (I : finType) (P : pred I) V :
- (∀ i, P i → mxsemisimple (V i)) → mxsemisimple (\sum_(i | P i) V i)%MS.
- -
-Lemma eqmx_semisimple U V : (U :=: V)%MS → mxsemisimple U → mxsemisimple V.
- -
-Lemma hom_mxsemisimple (V f : 'M_n) :
- mxsemisimple V → (V ≤ dom_hom_mx f)%MS → mxsemisimple (V ×m f).
- -
-Lemma mxsemisimple_module U : mxsemisimple U → mxmodule U.
- -
-
- Completely reducible modules, and Maeschke's Theorem.
-
-
-
-
-Variant mxsplits (V U : 'M_n) :=
- MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W).
- -
-Definition mx_completely_reducible V :=
- ∀ U, mxmodule U → (U ≤ V)%MS → mxsplits V U.
- -
-Lemma mx_reducibleS U V :
- mxmodule U → (U ≤ V)%MS →
- mx_completely_reducible V → mx_completely_reducible U.
- -
-Lemma mx_Maschke : [char F]^'.-group G → mx_completely_reducible 1%:M.
- -
-Lemma mxsemisimple_reducible V : mxsemisimple V → mx_completely_reducible V.
- -
-Lemma mx_reducible_semisimple V :
- mxmodule V → mx_completely_reducible V → classically (mxsemisimple V).
- -
-Lemma mxsemisimpleS U V :
- mxmodule U → (U ≤ V)%MS → mxsemisimple V → mxsemisimple U.
- -
-Lemma hom_mxsemisimple_iso I P U W f :
- let V := (\sum_(i : I | P i) W i)%MS in
- mxsimple U → (∀ i, P i → W i != 0 → mxsimple (W i)) →
- (V ≤ dom_hom_mx f)%MS → (U ≤ V ×m f)%MS →
- {i | P i & mx_iso (W i) U}.
- -
-
-
--Variant mxsplits (V U : 'M_n) :=
- MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W).
- -
-Definition mx_completely_reducible V :=
- ∀ U, mxmodule U → (U ≤ V)%MS → mxsplits V U.
- -
-Lemma mx_reducibleS U V :
- mxmodule U → (U ≤ V)%MS →
- mx_completely_reducible V → mx_completely_reducible U.
- -
-Lemma mx_Maschke : [char F]^'.-group G → mx_completely_reducible 1%:M.
- -
-Lemma mxsemisimple_reducible V : mxsemisimple V → mx_completely_reducible V.
- -
-Lemma mx_reducible_semisimple V :
- mxmodule V → mx_completely_reducible V → classically (mxsemisimple V).
- -
-Lemma mxsemisimpleS U V :
- mxmodule U → (U ≤ V)%MS → mxsemisimple V → mxsemisimple U.
- -
-Lemma hom_mxsemisimple_iso I P U W f :
- let V := (\sum_(i : I | P i) W i)%MS in
- mxsimple U → (∀ i, P i → W i != 0 → mxsimple (W i)) →
- (V ≤ dom_hom_mx f)%MS → (U ≤ V ×m f)%MS →
- {i | P i & mx_iso (W i) U}.
- -
-
- The component associated to a given irreducible module.
-
-
-
-
-Section Components.
- -
-Fact component_mx_key : unit.
-Definition component_mx_expr (U : 'M[F]_n) :=
- (\sum_i cyclic_mx (row i (row_hom_mx (nz_row U))))%MS.
-Definition component_mx := locked_with component_mx_key component_mx_expr.
-Canonical component_mx_unfoldable := [unlockable fun component_mx].
- -
-Variable U : 'M[F]_n.
-Hypothesis simU : mxsimple U.
- -
-Let u := nz_row U.
-Let iso_u := row_hom_mx u.
-Let nz_u : u != 0 := nz_row_mxsimple simU.
-Let Uu : (u ≤ U)%MS := nz_row_sub U.
-Let defU : (U :=: cyclic_mx u)%MS := mxsimple_cyclic simU nz_u Uu.
- -
-Lemma component_mx_module : mxmodule compU.
- -
-Lemma genmx_component : <<compU>>%MS = compU.
- -
-Lemma component_mx_def : {I : finType & {W : I → 'M_n |
- ∀ i, mx_iso U (W i) & compU = \sum_i W i}}%MS.
- -
-Lemma component_mx_semisimple : mxsemisimple compU.
- -
-Lemma mx_iso_component V : mx_iso U V → (V ≤ compU)%MS.
- -
-Lemma component_mx_id : (U ≤ compU)%MS.
- -
-Lemma hom_component_mx_iso f V :
- mxsimple V → (compU ≤ dom_hom_mx f)%MS → (V ≤ compU ×m f)%MS →
- mx_iso U V.
- -
-Lemma component_mx_iso V : mxsimple V → (V ≤ compU)%MS → mx_iso U V.
- -
-Lemma hom_component_mx f :
- (compU ≤ dom_hom_mx f)%MS → (compU ×m f ≤ compU)%MS.
- -
-End Components.
- -
-Lemma component_mx_isoP U V :
- mxsimple U → mxsimple V →
- reflect (mx_iso U V) (component_mx U == component_mx V).
- -
-Lemma component_mx_disjoint U V :
- mxsimple U → mxsimple V → component_mx U != component_mx V →
- (component_mx U :&: component_mx V = 0)%MS.
- -
-Section Socle.
- -
-Record socleType := EnumSocle {
- socle_base_enum : seq 'M[F]_n;
- _ : ∀ M, M \in socle_base_enum → mxsimple M;
- _ : ∀ M, mxsimple M → has (mxsimple_iso M) socle_base_enum
-}.
- -
-Lemma socle_exists : classically socleType.
- -
-Section SocleDef.
- -
-Variable sG0 : socleType.
- -
-Definition socle_enum := map component_mx (socle_base_enum sG0).
- -
-Lemma component_socle M : mxsimple M → component_mx M \in socle_enum.
- -
-Inductive socle_sort : predArgType := PackSocle W of W \in socle_enum.
- -
- -
-Definition socle_base W := let: PackSocle W _ := W in e0`_(index W socle_enum).
- -
-Coercion socle_val W : 'M[F]_n := component_mx (socle_base W).
- -
-Definition socle_mult (W : sG) := (\rank W %/ \rank (socle_base W))%N.
- -
-Lemma socle_simple W : mxsimple (socle_base W).
- -
-Definition socle_module (W : sG) := mxsimple_module (socle_simple W).
- -
-Definition socle_repr W := submod_repr (socle_module W).
- -
-Lemma nz_socle (W : sG) : W != 0 :> 'M_n.
- -
-Lemma socle_mem (W : sG) : (W : 'M_n) \in socle_enum.
- -
-Lemma PackSocleK W e0W : @PackSocle W e0W = W :> 'M_n.
- -
-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}).
- -
-Variant mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop :=
- MxReprSim B of n1 = n2 & row_free B
- & ∀ x, x \in G → rG1 x ×m B = B ×m rG2 x.
- -
-Lemma mxrank_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → n1 = n2.
- -
-Lemma mx_rsim_refl n (rG : reprG n) : mx_rsim rG rG.
- -
-Lemma mx_rsim_sym n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → mx_rsim rG2 rG1.
- -
-Lemma mx_rsim_trans n1 n2 n3
- (rG1 : reprG n1) (rG2 : reprG n2) (rG3 : reprG n3) :
- mx_rsim rG1 rG2 → mx_rsim rG2 rG3 → mx_rsim rG1 rG3.
- -
-Lemma mx_rsim_def n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 →
- ∃ B, exists2 B', B' ×m B = 1%:M &
- ∀ x, x \in G → rG1 x = B ×m rG2 x ×m B'.
- -
-Lemma mx_rsim_iso n (rG : reprG n) (U V : 'M_n)
- (modU : mxmodule rG U) (modV : mxmodule rG V) :
- mx_rsim (submod_repr modU) (submod_repr modV) ↔ mx_iso rG U V.
- -
-Lemma mx_rsim_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → mx_irreducible rG1 → mx_irreducible rG2.
- -
-Lemma mx_rsim_abs_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 →
- mx_absolutely_irreducible rG1 = mx_absolutely_irreducible rG2.
- -
-Lemma rker_mx_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → rker rG1 = rker rG2.
- -
-Lemma mx_rsim_faithful n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → mx_faithful rG1 = mx_faithful rG2.
- -
-Lemma mx_rsim_factmod n (rG : reprG n) U V
- (modU : mxmodule rG U) (modV : mxmodule rG V) :
- (U + V :=: 1%:M)%MS → mxdirect (U + V) →
- mx_rsim (factmod_repr modV) (submod_repr modU).
- -
-Lemma mxtrace_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → {in G, ∀ x, \tr (rG1 x) = \tr (rG2 x)}.
- -
-Lemma mx_rsim_scalar n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) x c :
- x \in G → mx_rsim rG1 rG2 → rG1 x = c%:M → rG2 x = c%:M.
- -
-End Similarity.
- -
-Section Socle.
- -
-Variables (gT : finGroupType) (G : {group gT}).
-Variables (n : nat) (rG : mx_representation F G n) (sG : socleType rG).
- -
-Lemma socle_irr (W : sG) : mx_irreducible (socle_repr W).
- -
-Lemma socle_rsimP (W1 W2 : sG) :
- reflect (mx_rsim (socle_repr W1) (socle_repr W2)) (W1 == W2).
- -
- -
-Lemma mx_rsim_in_submod U V (modU : mG U) (modV : mG V) :
- let U' := <<in_submod V U>>%MS in
- (U ≤ V)%MS →
- ∃ modU' : mxmodule (sr modV) U', mx_rsim (sr modU) (sr modU').
- -
-Lemma rsim_submod1 U (modU : mG U) : (U :=: 1%:M)%MS → mx_rsim (sr modU) rG.
- -
-Lemma mxtrace_submod1 U (modU : mG U) :
- (U :=: 1%:M)%MS → {in G, ∀ x, \tr (sr modU x) = \tr (rG x)}.
- -
-Lemma mxtrace_dadd_mod U V W (modU : mG U) (modV : mG V) (modW : mG W) :
- (U + V :=: W)%MS → mxdirect (U + V) →
- {in G, ∀ x, \tr (sr modU x) + \tr (sr modV x) = \tr (sr modW x)}.
- -
-Lemma mxtrace_dsum_mod (I : finType) (P : pred I) U W
- (modU : ∀ i, mG (U i)) (modW : mG W) :
- let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
- {in G, ∀ x, \sum_(i | P i) \tr (sr (modU i) x) = \tr (sr modW x)}.
- -
-Lemma mxtrace_component U (simU : mxsimple rG U) :
- let V := component_mx rG U in
- let modV := component_mx_module rG U in let modU := mxsimple_module simU in
- {in G, ∀ x, \tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.
- -
-Lemma mxtrace_Socle : let modS := Socle_module sG in
- {in G, ∀ x,
- \tr (sr modS x) = \sum_(W : sG) \tr (socle_repr W x) *+ socle_mult W}.
- -
-End Socle.
- -
-Section Clifford.
- -
-Variables (gT : finGroupType) (G H : {group gT}).
-Hypothesis nsHG : H <| G.
-Variables (n : nat) (rG : mx_representation F G n).
-Let sHG := normal_sub nsHG.
-Let nHG := normal_norm nsHG.
-Let rH := subg_repr rG sHG.
- -
-Lemma Clifford_simple M x : mxsimple rH M → x \in G → mxsimple rH (M ×m rG x).
- -
-Lemma Clifford_hom x m (U : 'M_(m, n)) :
- x \in 'C_G(H) → (U ≤ dom_hom_mx rH (rG x))%MS.
- -
-Lemma Clifford_iso x U : x \in 'C_G(H) → mx_iso rH U (U ×m rG x).
- -
-Lemma Clifford_iso2 x U V :
- mx_iso rH U V → x \in G → mx_iso rH (U ×m rG x) (V ×m rG x).
- -
-Lemma Clifford_componentJ M x :
- mxsimple rH M → x \in G →
- (component_mx rH (M ×m rG x) :=: component_mx rH M ×m rG x)%MS.
- -
-Hypothesis irrG : mx_irreducible rG.
- -
-Lemma Clifford_basis M : mxsimple rH M →
- {X : {set gT} | X \subset G &
- let S := \sum_(x in X) M ×m rG x in S :=: 1%:M ∧ mxdirect S}%MS.
- -
-Variable sH : socleType rH.
- -
-Definition Clifford_act (W : sH) x :=
- let Gx := subgP (subg G x) in
- PackSocle (component_socle sH (Clifford_simple (socle_simple W) Gx)).
- -
-Let valWact W x : (Clifford_act W x :=: W ×m rG (sgval (subg G x)))%MS.
- -
-Fact Clifford_is_action : is_action G Clifford_act.
- -
-Definition Clifford_action := Action Clifford_is_action.
- -
- -
-Lemma val_Clifford_act W x : x \in G → ('Cl%act W x :=: W ×m rG x)%MS.
- -
-Lemma Clifford_atrans : [transitive G, on [set: sH] | 'Cl].
- -
-Lemma Clifford_Socle1 : Socle sH = 1%:M.
- -
-Lemma Clifford_rank_components (W : sH) : (#|sH| × \rank W)%N = n.
- -
-Theorem Clifford_component_basis M : mxsimple rH M →
- {t : nat & {x_ : sH → 'I_t → gT |
- ∀ W, let sW := (\sum_j M ×m rG (x_ W j))%MS in
- [/\ ∀ j, x_ W j \in G, (sW :=: W)%MS & mxdirect sW]}}.
- -
-Lemma Clifford_astab : H <*> 'C_G(H) \subset 'C([set: sH] | 'Cl).
- -
-Lemma Clifford_astab1 (W : sH) : 'C[W | 'Cl] = rstabs rG W.
- -
-Lemma Clifford_rstabs_simple (W : sH) :
- mxsimple (subg_repr rG (rstabs_sub rG W)) W.
- -
-End Clifford.
- -
-Section JordanHolder.
- -
-Variables (gT : finGroupType) (G : {group gT}).
-Variables (n : nat) (rG : mx_representation F G n).
- -
-Lemma section_module (U V : 'M_n) (modU : modG U) (modV : modG V) :
- mxmodule (factmod_repr modU) <<in_factmod U V>>%MS.
- -
-Definition section_repr U V (modU : modG U) (modV : modG V) :=
- submod_repr (section_module modU modV).
- -
-Lemma mx_factmod_sub U modU :
- mx_rsim (@section_repr U _ modU (mxmodule1 rG)) (factmod_repr modU).
- -
-Definition max_submod (U V : 'M_n) :=
- (U < V)%MS ∧ (∀ W, ¬ [/\ modG W, U < W & W < V])%MS.
- -
-Lemma max_submodP U V (modU : modG U) (modV : modG V) :
- (U ≤ V)%MS → (max_submod U V ↔ mx_irreducible (section_repr modU modV)).
- -
-Lemma max_submod_eqmx U1 U2 V1 V2 :
- (U1 :=: U2)%MS → (V1 :=: V2)%MS → max_submod U1 V1 → max_submod U2 V2.
- -
-Definition mx_subseries := all modG.
- -
-Definition mx_composition_series V :=
- mx_subseries V ∧ (∀ i, i < size V → max_submod (0 :: V)`_i V`_i).
- -
-Fact mx_subseries_module V i : mx_subseries V → mxmodule rG V`_i.
- -
-Fact mx_subseries_module' V i : mx_subseries V → mxmodule rG (0 :: V)`_i.
- -
-Definition subseries_repr V i (modV : all modG V) :=
- section_repr (mx_subseries_module' i modV) (mx_subseries_module i modV).
- -
-Definition series_repr V i (compV : mx_composition_series V) :=
- subseries_repr i (proj1 compV).
- -
-Lemma mx_series_lt V : mx_composition_series V → path ltmx 0 V.
- -
-Lemma max_size_mx_series (V : seq 'M[F]_n) :
- path ltmx 0 V → size V ≤ \rank (last 0 V).
- -
-Lemma mx_series_repr_irr V i (compV : mx_composition_series V) :
- i < size V → mx_irreducible (series_repr 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}).
- -
-Variant mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop :=
- MxReprSim B of n1 = n2 & row_free B
- & ∀ x, x \in G → rG1 x ×m B = B ×m rG2 x.
- -
-Lemma mxrank_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → n1 = n2.
- -
-Lemma mx_rsim_refl n (rG : reprG n) : mx_rsim rG rG.
- -
-Lemma mx_rsim_sym n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → mx_rsim rG2 rG1.
- -
-Lemma mx_rsim_trans n1 n2 n3
- (rG1 : reprG n1) (rG2 : reprG n2) (rG3 : reprG n3) :
- mx_rsim rG1 rG2 → mx_rsim rG2 rG3 → mx_rsim rG1 rG3.
- -
-Lemma mx_rsim_def n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 →
- ∃ B, exists2 B', B' ×m B = 1%:M &
- ∀ x, x \in G → rG1 x = B ×m rG2 x ×m B'.
- -
-Lemma mx_rsim_iso n (rG : reprG n) (U V : 'M_n)
- (modU : mxmodule rG U) (modV : mxmodule rG V) :
- mx_rsim (submod_repr modU) (submod_repr modV) ↔ mx_iso rG U V.
- -
-Lemma mx_rsim_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → mx_irreducible rG1 → mx_irreducible rG2.
- -
-Lemma mx_rsim_abs_irr n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 →
- mx_absolutely_irreducible rG1 = mx_absolutely_irreducible rG2.
- -
-Lemma rker_mx_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → rker rG1 = rker rG2.
- -
-Lemma mx_rsim_faithful n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → mx_faithful rG1 = mx_faithful rG2.
- -
-Lemma mx_rsim_factmod n (rG : reprG n) U V
- (modU : mxmodule rG U) (modV : mxmodule rG V) :
- (U + V :=: 1%:M)%MS → mxdirect (U + V) →
- mx_rsim (factmod_repr modV) (submod_repr modU).
- -
-Lemma mxtrace_rsim n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
- mx_rsim rG1 rG2 → {in G, ∀ x, \tr (rG1 x) = \tr (rG2 x)}.
- -
-Lemma mx_rsim_scalar n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) x c :
- x \in G → mx_rsim rG1 rG2 → rG1 x = c%:M → rG2 x = c%:M.
- -
-End Similarity.
- -
-Section Socle.
- -
-Variables (gT : finGroupType) (G : {group gT}).
-Variables (n : nat) (rG : mx_representation F G n) (sG : socleType rG).
- -
-Lemma socle_irr (W : sG) : mx_irreducible (socle_repr W).
- -
-Lemma socle_rsimP (W1 W2 : sG) :
- reflect (mx_rsim (socle_repr W1) (socle_repr W2)) (W1 == W2).
- -
- -
-Lemma mx_rsim_in_submod U V (modU : mG U) (modV : mG V) :
- let U' := <<in_submod V U>>%MS in
- (U ≤ V)%MS →
- ∃ modU' : mxmodule (sr modV) U', mx_rsim (sr modU) (sr modU').
- -
-Lemma rsim_submod1 U (modU : mG U) : (U :=: 1%:M)%MS → mx_rsim (sr modU) rG.
- -
-Lemma mxtrace_submod1 U (modU : mG U) :
- (U :=: 1%:M)%MS → {in G, ∀ x, \tr (sr modU x) = \tr (rG x)}.
- -
-Lemma mxtrace_dadd_mod U V W (modU : mG U) (modV : mG V) (modW : mG W) :
- (U + V :=: W)%MS → mxdirect (U + V) →
- {in G, ∀ x, \tr (sr modU x) + \tr (sr modV x) = \tr (sr modW x)}.
- -
-Lemma mxtrace_dsum_mod (I : finType) (P : pred I) U W
- (modU : ∀ i, mG (U i)) (modW : mG W) :
- let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
- {in G, ∀ x, \sum_(i | P i) \tr (sr (modU i) x) = \tr (sr modW x)}.
- -
-Lemma mxtrace_component U (simU : mxsimple rG U) :
- let V := component_mx rG U in
- let modV := component_mx_module rG U in let modU := mxsimple_module simU in
- {in G, ∀ x, \tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.
- -
-Lemma mxtrace_Socle : let modS := Socle_module sG in
- {in G, ∀ x,
- \tr (sr modS x) = \sum_(W : sG) \tr (socle_repr W x) *+ socle_mult W}.
- -
-End Socle.
- -
-Section Clifford.
- -
-Variables (gT : finGroupType) (G H : {group gT}).
-Hypothesis nsHG : H <| G.
-Variables (n : nat) (rG : mx_representation F G n).
-Let sHG := normal_sub nsHG.
-Let nHG := normal_norm nsHG.
-Let rH := subg_repr rG sHG.
- -
-Lemma Clifford_simple M x : mxsimple rH M → x \in G → mxsimple rH (M ×m rG x).
- -
-Lemma Clifford_hom x m (U : 'M_(m, n)) :
- x \in 'C_G(H) → (U ≤ dom_hom_mx rH (rG x))%MS.
- -
-Lemma Clifford_iso x U : x \in 'C_G(H) → mx_iso rH U (U ×m rG x).
- -
-Lemma Clifford_iso2 x U V :
- mx_iso rH U V → x \in G → mx_iso rH (U ×m rG x) (V ×m rG x).
- -
-Lemma Clifford_componentJ M x :
- mxsimple rH M → x \in G →
- (component_mx rH (M ×m rG x) :=: component_mx rH M ×m rG x)%MS.
- -
-Hypothesis irrG : mx_irreducible rG.
- -
-Lemma Clifford_basis M : mxsimple rH M →
- {X : {set gT} | X \subset G &
- let S := \sum_(x in X) M ×m rG x in S :=: 1%:M ∧ mxdirect S}%MS.
- -
-Variable sH : socleType rH.
- -
-Definition Clifford_act (W : sH) x :=
- let Gx := subgP (subg G x) in
- PackSocle (component_socle sH (Clifford_simple (socle_simple W) Gx)).
- -
-Let valWact W x : (Clifford_act W x :=: W ×m rG (sgval (subg G x)))%MS.
- -
-Fact Clifford_is_action : is_action G Clifford_act.
- -
-Definition Clifford_action := Action Clifford_is_action.
- -
- -
-Lemma val_Clifford_act W x : x \in G → ('Cl%act W x :=: W ×m rG x)%MS.
- -
-Lemma Clifford_atrans : [transitive G, on [set: sH] | 'Cl].
- -
-Lemma Clifford_Socle1 : Socle sH = 1%:M.
- -
-Lemma Clifford_rank_components (W : sH) : (#|sH| × \rank W)%N = n.
- -
-Theorem Clifford_component_basis M : mxsimple rH M →
- {t : nat & {x_ : sH → 'I_t → gT |
- ∀ W, let sW := (\sum_j M ×m rG (x_ W j))%MS in
- [/\ ∀ j, x_ W j \in G, (sW :=: W)%MS & mxdirect sW]}}.
- -
-Lemma Clifford_astab : H <*> 'C_G(H) \subset 'C([set: sH] | 'Cl).
- -
-Lemma Clifford_astab1 (W : sH) : 'C[W | 'Cl] = rstabs rG W.
- -
-Lemma Clifford_rstabs_simple (W : sH) :
- mxsimple (subg_repr rG (rstabs_sub rG W)) W.
- -
-End Clifford.
- -
-Section JordanHolder.
- -
-Variables (gT : finGroupType) (G : {group gT}).
-Variables (n : nat) (rG : mx_representation F G n).
- -
-Lemma section_module (U V : 'M_n) (modU : modG U) (modV : modG V) :
- mxmodule (factmod_repr modU) <<in_factmod U V>>%MS.
- -
-Definition section_repr U V (modU : modG U) (modV : modG V) :=
- submod_repr (section_module modU modV).
- -
-Lemma mx_factmod_sub U modU :
- mx_rsim (@section_repr U _ modU (mxmodule1 rG)) (factmod_repr modU).
- -
-Definition max_submod (U V : 'M_n) :=
- (U < V)%MS ∧ (∀ W, ¬ [/\ modG W, U < W & W < V])%MS.
- -
-Lemma max_submodP U V (modU : modG U) (modV : modG V) :
- (U ≤ V)%MS → (max_submod U V ↔ mx_irreducible (section_repr modU modV)).
- -
-Lemma max_submod_eqmx U1 U2 V1 V2 :
- (U1 :=: U2)%MS → (V1 :=: V2)%MS → max_submod U1 V1 → max_submod U2 V2.
- -
-Definition mx_subseries := all modG.
- -
-Definition mx_composition_series V :=
- mx_subseries V ∧ (∀ i, i < size V → max_submod (0 :: V)`_i V`_i).
- -
-Fact mx_subseries_module V i : mx_subseries V → mxmodule rG V`_i.
- -
-Fact mx_subseries_module' V i : mx_subseries V → mxmodule rG (0 :: V)`_i.
- -
-Definition subseries_repr V i (modV : all modG V) :=
- section_repr (mx_subseries_module' i modV) (mx_subseries_module i modV).
- -
-Definition series_repr V i (compV : mx_composition_series V) :=
- subseries_repr i (proj1 compV).
- -
-Lemma mx_series_lt V : mx_composition_series V → path ltmx 0 V.
- -
-Lemma max_size_mx_series (V : seq 'M[F]_n) :
- path ltmx 0 V → size V ≤ \rank (last 0 V).
- -
-Lemma mx_series_repr_irr V i (compV : mx_composition_series V) :
- i < size V → mx_irreducible (series_repr 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.
-
-
-
-
- The type definition must come before the main section so that the Bind
- Scope directive applies to all lemmas and definition discharged at the
- of the section.
-
-
-Record gen_of {F : fieldType} {gT : finGroupType} {G : {group gT}} {n' : nat}
- {rG : mx_representation F G n'.+1} {A : 'M[F]_n'.+1}
- (irrG : mx_irreducible rG) (cGA : centgmx rG A) :=
- Gen {rVval : 'rV[F]_(degree_mxminpoly A)}.
- -
- -
-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.
- -
-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 : FA → 'rV_d].
-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.
- -
-
-
-- {rG : mx_representation F G n'.+1} {A : 'M[F]_n'.+1}
- (irrG : mx_irreducible rG) (cGA : centgmx rG A) :=
- Gen {rVval : 'rV[F]_(degree_mxminpoly A)}.
- -
- -
-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.
- -
-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 : FA → 'rV_d].
-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 nA (B : 'rV_nA) : 'M_(nA × d, n) :=
- \matrix_ik mxvec (\matrix_(i, k) (row (B 0 i) (A ^+ k))) 0 ik.
- -
-Lemma gen_dim_ex_proof : ∃ nA, [∃ B : 'rV_nA, row_free (subbase B)].
- -
-Lemma gen_dim_ub_proof nA :
- [∃ B : 'rV_nA, row_free (subbase B)] → (nA ≤ n)%N.
- -
-Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
-Notation nA := gen_dim.
- -
-Definition gen_base : 'rV_nA := odflt 0 [pick B | row_free (subbase B)].
-Definition base := subbase gen_base.
- -
-Lemma base_free : row_free base.
- -
-Lemma base_full : row_full base.
- -
-Lemma gen_dim_factor : (nA × d)%N = n.
- -
-Lemma gen_dim_gt0 : nA > 0.
- -
-Section Bijection.
- -
-Variable m : nat.
- -
-Definition in_gen (W : 'M[F]_(m, n)) : 'M[FA]_(m, nA) :=
- \matrix_(i, j) inFA (row j (vec_mx (row i W ×m pinvmx base))).
- -
-Definition val_gen (W : 'M[FA]_(m, nA)) : 'M[F]_(m, n) :=
- \matrix_i (mxvec (\matrix_j val (W i j)) ×m base).
- -
-Lemma in_genK : cancel in_gen val_gen.
- -
-Lemma val_genK : cancel val_gen in_gen.
- -
-Lemma in_gen0 : in_gen 0 = 0.
- -
-Lemma val_gen0 : val_gen 0 = 0.
- -
-Lemma in_genN : {morph in_gen : W / - W}.
- -
-Lemma val_genN : {morph val_gen : W / - W}.
- -
-Lemma in_genD : {morph in_gen : U V / U + V}.
- -
-Lemma val_genD : {morph val_gen : U V / U + V}.
- -
-Definition in_gen_sum := big_morph in_gen in_genD in_gen0.
-Definition val_gen_sum := big_morph val_gen val_genD val_gen0.
- -
-Lemma in_genZ a : {morph in_gen : W / a *: W >-> gen a *: W}.
- -
-End Bijection.
- -
- -
-Lemma val_gen_rV (w : 'rV_nA) :
- val_gen w = mxvec (\matrix_j val (w 0 j)) ×m base.
- -
-Section Bijection2.
- -
-Variable m : nat.
- -
-Lemma val_gen_row W (i : 'I_m) : val_gen (row i W) = row i (val_gen W).
- -
-Lemma in_gen_row W (i : 'I_m) : in_gen (row i W) = row i (in_gen W).
- -
-Lemma row_gen_sum_mxval W (i : 'I_m) :
- row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).
- -
-Lemma val_genZ x : {morph @val_gen m : W / x *: W >-> W ×m mxval x}.
- -
-End Bijection2.
- -
-Lemma submx_in_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
- (U ≤ V → in_gen U ≤ in_gen V)%MS.
- -
-Lemma submx_in_gen_eq m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
- (V ×m A ≤ V → (in_gen U ≤ in_gen V) = (U ≤ V))%MS.
- -
-Definition gen_mx g := \matrix_i in_gen (row (gen_base 0 i) (rG g)).
- -
-Let val_genJmx m :
- {in G, ∀ g, {morph @val_gen m : W / W ×m gen_mx g >-> W ×m rG g}}.
- -
-Lemma gen_mx_repr : mx_repr G gen_mx.
-Canonical gen_repr := MxRepresentation gen_mx_repr.
- -
-Lemma val_genJ m :
- {in G, ∀ g, {morph @val_gen m : W / W ×m rGA g >-> W ×m rG g}}.
- -
-Lemma in_genJ m :
- {in G, ∀ g, {morph @in_gen m : v / v ×m rG g >-> v ×m rGA g}}.
- -
-Lemma rfix_gen (H : {set gT}) :
- H \subset G → (rfix_mx rGA H :=: in_gen (rfix_mx rG H))%MS.
- -
-Definition rowval_gen m U :=
- <<\matrix_ik
- mxvec (\matrix_(i < m, k < d) (row i (val_gen U) ×m A ^+ k)) 0 ik>>%MS.
- -
-Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, nA)) :
- (U ≤ rowval_gen V)%MS = (in_gen U ≤ V)%MS.
- -
-Lemma rowval_genK m (U : 'M_(m, nA)) : (in_gen (rowval_gen U) :=: U)%MS.
- -
-Lemma rowval_gen_stable m (U : 'M_(m, nA)) :
- (rowval_gen U ×m A ≤ rowval_gen U)%MS.
- -
-Lemma rstab_in_gen m (U : 'M_(m, n)) : rstab rGA (in_gen U) = rstab rG U.
- -
-Lemma rstabs_in_gen m (U : 'M_(m, n)) :
- rstabs rG U \subset rstabs rGA (in_gen U).
- -
-Lemma rstabs_rowval_gen m (U : 'M_(m, nA)) :
- rstabs rG (rowval_gen U) = rstabs rGA U.
- -
-Lemma mxmodule_rowval_gen m (U : 'M_(m, nA)) :
- mxmodule rG (rowval_gen U) = mxmodule rGA U.
- -
-Lemma gen_mx_irr : mx_irreducible rGA.
- -
-Lemma rker_gen : rker rGA = rker rG.
- -
-Lemma gen_mx_faithful : mx_faithful rGA = mx_faithful rG.
- -
-End GenField.
- -
-Section DecideGenField.
- -
-Import MatrixFormula.
- -
-Variable F : decFieldType.
- -
- -
- -
-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).
- -
-Fixpoint gen_form f := match f with
-| Bool b ⇒ Bool b
-| t1 == t2 ⇒ mxrank_form 0 (gen_term (t1 - t2))
-| GRing.Unit t1 ⇒ mxrank_form 1 (gen_term t1)
-| f1 ∧ f2 ⇒ gen_form f1 ∧ gen_form f2
-| f1 ∨ f2 ⇒ gen_form f1 ∨ gen_form f2
-| f1 ==> f2 ⇒ gen_form f1 ==> gen_form f2
-| ¬ f1 ⇒ ¬ gen_form f1
-| ('∃ 'X_k, f1) ⇒ Exists_row_form d k (gen_form f1)
-| ('∀ 'X_k, f1) ⇒ ¬ Exists_row_form d k (¬ (gen_form f1))
-end%T.
- -
-Lemma sat_gen_form e f : GRing.rformula f →
- reflect (GRing.holds e f) (GRing.sat (gen_env e) (gen_form f)).
- -
-Definition gen_sat e f := GRing.sat (gen_env e) (gen_form (GRing.to_rform f)).
- -
-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).
- -
-
-
--Definition subbase nA (B : 'rV_nA) : 'M_(nA × d, n) :=
- \matrix_ik mxvec (\matrix_(i, k) (row (B 0 i) (A ^+ k))) 0 ik.
- -
-Lemma gen_dim_ex_proof : ∃ nA, [∃ B : 'rV_nA, row_free (subbase B)].
- -
-Lemma gen_dim_ub_proof nA :
- [∃ B : 'rV_nA, row_free (subbase B)] → (nA ≤ n)%N.
- -
-Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
-Notation nA := gen_dim.
- -
-Definition gen_base : 'rV_nA := odflt 0 [pick B | row_free (subbase B)].
-Definition base := subbase gen_base.
- -
-Lemma base_free : row_free base.
- -
-Lemma base_full : row_full base.
- -
-Lemma gen_dim_factor : (nA × d)%N = n.
- -
-Lemma gen_dim_gt0 : nA > 0.
- -
-Section Bijection.
- -
-Variable m : nat.
- -
-Definition in_gen (W : 'M[F]_(m, n)) : 'M[FA]_(m, nA) :=
- \matrix_(i, j) inFA (row j (vec_mx (row i W ×m pinvmx base))).
- -
-Definition val_gen (W : 'M[FA]_(m, nA)) : 'M[F]_(m, n) :=
- \matrix_i (mxvec (\matrix_j val (W i j)) ×m base).
- -
-Lemma in_genK : cancel in_gen val_gen.
- -
-Lemma val_genK : cancel val_gen in_gen.
- -
-Lemma in_gen0 : in_gen 0 = 0.
- -
-Lemma val_gen0 : val_gen 0 = 0.
- -
-Lemma in_genN : {morph in_gen : W / - W}.
- -
-Lemma val_genN : {morph val_gen : W / - W}.
- -
-Lemma in_genD : {morph in_gen : U V / U + V}.
- -
-Lemma val_genD : {morph val_gen : U V / U + V}.
- -
-Definition in_gen_sum := big_morph in_gen in_genD in_gen0.
-Definition val_gen_sum := big_morph val_gen val_genD val_gen0.
- -
-Lemma in_genZ a : {morph in_gen : W / a *: W >-> gen a *: W}.
- -
-End Bijection.
- -
- -
-Lemma val_gen_rV (w : 'rV_nA) :
- val_gen w = mxvec (\matrix_j val (w 0 j)) ×m base.
- -
-Section Bijection2.
- -
-Variable m : nat.
- -
-Lemma val_gen_row W (i : 'I_m) : val_gen (row i W) = row i (val_gen W).
- -
-Lemma in_gen_row W (i : 'I_m) : in_gen (row i W) = row i (in_gen W).
- -
-Lemma row_gen_sum_mxval W (i : 'I_m) :
- row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).
- -
-Lemma val_genZ x : {morph @val_gen m : W / x *: W >-> W ×m mxval x}.
- -
-End Bijection2.
- -
-Lemma submx_in_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
- (U ≤ V → in_gen U ≤ in_gen V)%MS.
- -
-Lemma submx_in_gen_eq m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
- (V ×m A ≤ V → (in_gen U ≤ in_gen V) = (U ≤ V))%MS.
- -
-Definition gen_mx g := \matrix_i in_gen (row (gen_base 0 i) (rG g)).
- -
-Let val_genJmx m :
- {in G, ∀ g, {morph @val_gen m : W / W ×m gen_mx g >-> W ×m rG g}}.
- -
-Lemma gen_mx_repr : mx_repr G gen_mx.
-Canonical gen_repr := MxRepresentation gen_mx_repr.
- -
-Lemma val_genJ m :
- {in G, ∀ g, {morph @val_gen m : W / W ×m rGA g >-> W ×m rG g}}.
- -
-Lemma in_genJ m :
- {in G, ∀ g, {morph @in_gen m : v / v ×m rG g >-> v ×m rGA g}}.
- -
-Lemma rfix_gen (H : {set gT}) :
- H \subset G → (rfix_mx rGA H :=: in_gen (rfix_mx rG H))%MS.
- -
-Definition rowval_gen m U :=
- <<\matrix_ik
- mxvec (\matrix_(i < m, k < d) (row i (val_gen U) ×m A ^+ k)) 0 ik>>%MS.
- -
-Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, nA)) :
- (U ≤ rowval_gen V)%MS = (in_gen U ≤ V)%MS.
- -
-Lemma rowval_genK m (U : 'M_(m, nA)) : (in_gen (rowval_gen U) :=: U)%MS.
- -
-Lemma rowval_gen_stable m (U : 'M_(m, nA)) :
- (rowval_gen U ×m A ≤ rowval_gen U)%MS.
- -
-Lemma rstab_in_gen m (U : 'M_(m, n)) : rstab rGA (in_gen U) = rstab rG U.
- -
-Lemma rstabs_in_gen m (U : 'M_(m, n)) :
- rstabs rG U \subset rstabs rGA (in_gen U).
- -
-Lemma rstabs_rowval_gen m (U : 'M_(m, nA)) :
- rstabs rG (rowval_gen U) = rstabs rGA U.
- -
-Lemma mxmodule_rowval_gen m (U : 'M_(m, nA)) :
- mxmodule rG (rowval_gen U) = mxmodule rGA U.
- -
-Lemma gen_mx_irr : mx_irreducible rGA.
- -
-Lemma rker_gen : rker rGA = rker rG.
- -
-Lemma gen_mx_faithful : mx_faithful rGA = mx_faithful rG.
- -
-End GenField.
- -
-Section DecideGenField.
- -
-Import MatrixFormula.
- -
-Variable F : decFieldType.
- -
- -
- -
-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).
- -
-Fixpoint gen_form f := match f with
-| Bool b ⇒ Bool b
-| t1 == t2 ⇒ mxrank_form 0 (gen_term (t1 - t2))
-| GRing.Unit t1 ⇒ mxrank_form 1 (gen_term t1)
-| f1 ∧ f2 ⇒ gen_form f1 ∧ gen_form f2
-| f1 ∨ f2 ⇒ gen_form f1 ∨ gen_form f2
-| f1 ==> f2 ⇒ gen_form f1 ==> gen_form f2
-| ¬ f1 ⇒ ¬ gen_form f1
-| ('∃ 'X_k, f1) ⇒ Exists_row_form d k (gen_form f1)
-| ('∀ 'X_k, f1) ⇒ ¬ Exists_row_form d k (¬ (gen_form f1))
-end%T.
- -
-Lemma sat_gen_form e f : GRing.rformula f →
- reflect (GRing.holds e f) (GRing.sat (gen_env e) (gen_form f)).
- -
-Definition gen_sat e f := GRing.sat (gen_env e) (gen_form (GRing.to_rform f)).
- -
-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.
-