diff options
Diffstat (limited to 'mathcomp/character/mxrepresentation.v')
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 174 |
1 files changed, 103 insertions, 71 deletions
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 0968347..532b382 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -113,7 +113,7 @@ Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly. (* classically; the socleType structure encapsulates this *) (* use of classical logic. *) (* DecSocleType rG == a socleType rG structure, for a representation over a *) -(* decidable field type. *) +(* 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. *) @@ -219,48 +219,66 @@ Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly. (* 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 r of a group G, and a *) -(* non-scalar matrix A that centralises an r(G), as this data *) +(* 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 *) -(* r of G is reducible. Note that this is equivalent to the *) +(* 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: rG : mx_repr r G, irrG : mx_irreducible rG, and *) -(* cGA : centgmx rG A, which ensure the validity of the construction and *) -(* allow us to define Canonical instances (the ~~ is_scalar_mx A assumption *) -(* is only needed to prove reducibility). *) +(* 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 rG irrG cGA. *) -(* + groot irrG cGA == the root of mxminpoly A in the gen_of 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, and is actually required by the proof *) -(* that odd groups are p-stable (B & G 6.1-2, and Appendix A) *) -(* but is only applicable if G is the LARGEST group *) -(* represented by rG (e.g., NOT for B & G 2.6). *) -(* + val_gen/in_gen rG irrG cGA : the bijections from/to the module *) -(* corresponding to gen_repr. *) -(* + rowval_gen rG irrG cGA : the projection of row spaces in the module *) -(* corresponding to gen_repr to row spaces in 'rV_n. *) -(* We build on the MatrixFormula toolkit to define decision procedures for *) -(* the reducibility property: *) -(* + mxmodule_form rG U == a formula asserting that the interpretation of U *) -(* is a module of the representation rG of G via r. *) -(* + mxnonsimple_form rG U == a formula asserting that the interpretation *) -(* of U contains a proper nontrivial rG-module. *) +(* 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. @@ -4873,6 +4891,8 @@ Qed. End DecideRed. +Prenex Implicits mxmodule_form mxnonsimple_form mxnonsimple_sat. + (* Change of representation field (by tensoring) *) Section ChangeOfField. @@ -5029,7 +5049,18 @@ End ChangeOfField. (* minimal polynomial pA of A (of degree d). *) (* The details of the construction of FA are encapsulated in a submodule. *) Module Import MatrixGenField. - + +(* The type definition must come before the main section so that the Bind *) +(* Scope directive applies to all lemmas and definition discharged at the *) +(* of the section. *) +Record gen_of {F : fieldType} {gT : finGroupType} {G : {group gT}} {n' : nat} + {rG : mx_representation F G n'.+1} {A : 'M[F]_n'.+1} + (irrG : mx_irreducible rG) (cGA : centgmx rG A) := + Gen {rVval : 'rV[F]_(degree_mxminpoly A)}. + +Local Arguments rVval {F gT G%G n'%N rG A%R irrG cGA} x%R : rename. +Bind Scope ring_scope with gen_of. + Section GenField. Variables (F : fieldType) (gT : finGroupType) (G : {group gT}) (n' : nat). @@ -5042,15 +5073,12 @@ Local Notation pA := (mxminpoly A). Let d_gt0 := mxminpoly_nonconstant A. Local Notation irr := mx_irreducible. -Record gen_of (irrG : irr rG) (cGA : centgmx rG A) := Gen {rVval : 'rV[F]_d}. -Prenex Implicits rVval. - Hypotheses (irrG : irr rG) (cGA : centgmx rG A). Notation FA := (gen_of irrG cGA). Let inFA := Gen irrG cGA. -Canonical gen_subType := Eval hnf in [newType for @rVval irrG cGA]. +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 <:]. @@ -5181,7 +5209,8 @@ Lemma gen_invr0 : genV 0 = 0. Proof. by apply: mxval_inj; rewrite mxval_genV !mxval0 -{2}invr0. Qed. Definition gen_unitRingMixin := FieldUnitMixin gen_mulVr gen_invr0. -Canonical gen_unitRingType := Eval hnf in UnitRingType FA gen_unitRingMixin. +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. @@ -5261,37 +5290,37 @@ Qed. (* remain unchanged -- because we're restricting ourselves to row matrices; *) (* we have to use explicit bijections to convert between the two views. *) -Definition subbase m (B : 'rV_m) : 'M_(m * d, n) := +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 : exists m, [exists B : 'rV_m, row_free (subbase B)]. +Lemma gen_dim_ex_proof : exists nA, [exists B : 'rV_nA, row_free (subbase B)]. Proof. by exists 0%N; apply/existsP; exists 0. Qed. -Lemma gen_dim_ub_proof m : - [exists B : 'rV_m, row_free (subbase B)] -> (m <= n)%N. +Lemma gen_dim_ub_proof nA : + [exists B : 'rV_nA, row_free (subbase B)] -> (nA <= n)%N. Proof. -case/existsP=> B /eqnP def_md. -by rewrite (leq_trans _ (rank_leq_col (subbase B))) // def_md leq_pmulr. +case/existsP=> B /eqnP def_nAd. +by rewrite (leq_trans _ (rank_leq_col (subbase B))) // def_nAd leq_pmulr. Qed. Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof. -Notation m := gen_dim. +Notation nA := gen_dim. -Definition gen_base : 'rV_m := odflt 0 [pick B | row_free (subbase B)]. +Definition gen_base : 'rV_nA := odflt 0 [pick B | row_free (subbase B)]. Definition base := subbase gen_base. Lemma base_free : row_free base. Proof. -rewrite /base /gen_base /m; case: pickP => //; case: ex_maxnP => m_max. +rewrite /base /gen_base /nA; case: pickP => //; case: ex_maxnP => nA_max. by case/existsP=> B Bfree _ no_free; rewrite no_free in Bfree. Qed. Lemma base_full : row_full base. Proof. -rewrite /row_full (eqnP base_free) /m; case: ex_maxnP => m. -case/existsP=> /= B /eqnP Bfree m_max; rewrite -Bfree eqn_leq rank_leq_col. +rewrite /row_full (eqnP base_free) /nA; case: ex_maxnP => nA. +case/existsP=> /= B /eqnP Bfree nA_max; rewrite -Bfree eqn_leq rank_leq_col. rewrite -{1}(mxrank1 F n) mxrankS //; apply/row_subP=> j; set u := row _ _. -move/implyP: {m_max}(m_max m.+1); rewrite ltnn implybF. +move/implyP: {nA_max}(nA_max nA.+1); rewrite ltnn implybF. apply: contraR => nBj; apply/existsP. exists (row_mx (const_mx j : 'M_1) B); rewrite -row_leq_rank. pose Bj := Ad *m lin1_mx (mulmx u \o vec_mx). @@ -5303,7 +5332,7 @@ have rBj: \rank Bj = d. rewrite mul0mx /= -mulmxA -mxvalM divff // mxval1 mulmx1. by move/rowP/(_ j)/eqP; rewrite !mxE !eqxx oner_eq0. rewrite {1}mulSn -Bfree -{1}rBj {rBj} -mxrank_disjoint_sum. - rewrite mxrankS // addsmx_sub -[m.+1]/(1 + m)%N; apply/andP; split. + rewrite mxrankS // addsmx_sub -[nA.+1]/(1 + nA)%N; apply/andP; split. apply/row_subP=> k; rewrite row_mul mul_rV_lin1 /=. apply: eq_row_sub (mxvec_index (lshift _ 0) k) _. by rewrite !rowK mxvecK mxvecE mxE row_mxEl mxE -row_mul mul1mx. @@ -5325,20 +5354,20 @@ rewrite !linearZ scalemx_sub //= rowK mxvecK -rowE. by apply: eq_row_sub (mxvec_index i k) _; rewrite rowK mxvecE mxE. Qed. -Lemma gen_dim_factor : (m * d)%N = n. +Lemma gen_dim_factor : (nA * d)%N = n. Proof. by rewrite -(eqnP base_free) (eqnP base_full). Qed. -Lemma gen_dim_gt0 : m > 0. +Lemma gen_dim_gt0 : nA > 0. Proof. by case: posnP gen_dim_factor => // ->. Qed. Section Bijection. -Variable m1 : nat. +Variable m : nat. -Definition in_gen (W : 'M[F]_(m1, n)) : 'M[FA]_(m1, m) := +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]_(m1, m)) : 'M[F]_(m1, n) := +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. @@ -5394,24 +5423,24 @@ End Bijection. Prenex Implicits val_genK in_genK. -Lemma val_gen_rV (w : 'rV_m) : +Lemma val_gen_rV (w : 'rV_nA) : val_gen w = mxvec (\matrix_j val (w 0 j)) *m base. Proof. by apply/rowP=> j; rewrite mxE. Qed. Section Bijection2. -Variable m1 : nat. +Variable m : nat. -Lemma val_gen_row W (i : 'I_m1) : val_gen (row i W) = row i (val_gen W). +Lemma val_gen_row W (i : 'I_m) : val_gen (row i W) = row i (val_gen W). Proof. rewrite val_gen_rV rowK; congr (mxvec _ *m _). by apply/matrixP=> j k; rewrite !mxE. Qed. -Lemma in_gen_row W (i : 'I_m1) : in_gen (row i W) = row i (in_gen W). +Lemma in_gen_row W (i : 'I_m) : in_gen (row i W) = row i (in_gen W). Proof. by apply: (canLR val_genK); rewrite val_gen_row in_genK. Qed. -Lemma row_gen_sum_mxval W (i : 'I_m1) : +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)). Proof. rewrite -val_gen_row [row i W]row_sum_delta val_gen_sum. @@ -5431,7 +5460,7 @@ apply/row_matrixP=> j'; rewrite rowK !mxE mulr_natr rowE mul_delta_mx_cond. by rewrite !mulrb (fun_if rVval). Qed. -Lemma val_genZ x : {morph @val_gen m1 : W / x *: W >-> W *m mxval x}. +Lemma val_genZ x : {morph @val_gen m : W / x *: W >-> W *m mxval x}. Proof. move=> W; apply/row_matrixP=> i; rewrite row_mul !row_gen_sum_mxval. by rewrite mulmx_suml; apply: eq_bigr => j _; rewrite mxE mulrC mxvalM row_mul. @@ -5502,11 +5531,11 @@ rewrite -[rfix_mx rGA H]val_genK; apply: submx_in_gen. by apply/rfix_mxP=> g Hg; rewrite -val_genJ ?rfix_mx_id ?sHG. Qed. -Definition rowval_gen m1 U := +Definition rowval_gen m U := <<\matrix_ik - mxvec (\matrix_(i < m1, k < d) (row i (val_gen U) *m A ^+ k)) 0 ik>>%MS. + 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, m)) : +Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, nA)) : (U <= rowval_gen V)%MS = (in_gen U <= V)%MS. Proof. rewrite genmxE; apply/idP/idP=> sUV. @@ -5523,40 +5552,40 @@ rewrite !linearZ scalemx_sub {u}//= rowK mxvecK val_gen_row. by apply: (eq_row_sub (mxvec_index i k)); rewrite rowK mxvecE mxE. Qed. -Lemma rowval_genK m1 (U : 'M_(m1, m)) : (in_gen (rowval_gen U) :=: U)%MS. +Lemma rowval_genK m (U : 'M_(m, nA)) : (in_gen (rowval_gen U) :=: U)%MS. Proof. apply/eqmxP; rewrite -submx_rowval_gen submx_refl /=. by rewrite -{1}[U]val_genK submx_in_gen // submx_rowval_gen val_genK. Qed. -Lemma rowval_gen_stable m1 (U : 'M_(m1, m)) : +Lemma rowval_gen_stable m (U : 'M_(m, nA)) : (rowval_gen U *m A <= rowval_gen U)%MS. Proof. rewrite -[A]mxval_groot -{1}[_ U]in_genK -val_genZ. by rewrite submx_rowval_gen val_genK scalemx_sub // rowval_genK. Qed. -Lemma rstab_in_gen m1 (U : 'M_(m1, n)) : rstab rGA (in_gen U) = rstab rG U. +Lemma rstab_in_gen m (U : 'M_(m, n)) : rstab rGA (in_gen U) = rstab rG U. Proof. apply/setP=> x; rewrite !inE; case Gx: (x \in G) => //=. by rewrite -in_genJ // (inj_eq (can_inj in_genK)). Qed. -Lemma rstabs_in_gen m1 (U : 'M_(m1, n)) : +Lemma rstabs_in_gen m (U : 'M_(m, n)) : rstabs rG U \subset rstabs rGA (in_gen U). Proof. apply/subsetP=> x; rewrite !inE => /andP[Gx nUx]. by rewrite -in_genJ Gx // submx_in_gen. Qed. -Lemma rstabs_rowval_gen m1 (U : 'M_(m1, m)) : +Lemma rstabs_rowval_gen m (U : 'M_(m, nA)) : rstabs rG (rowval_gen U) = rstabs rGA U. Proof. apply/setP=> x; rewrite !inE; case Gx: (x \in G) => //=. by rewrite submx_rowval_gen in_genJ // (eqmxMr _ (rowval_genK U)). Qed. -Lemma mxmodule_rowval_gen m1 (U : 'M_(m1, m)) : +Lemma mxmodule_rowval_gen m (U : 'M_(m, nA)) : mxmodule rG (rowval_gen U) = mxmodule rGA U. Proof. by rewrite /mxmodule rstabs_rowval_gen. Qed. @@ -5582,11 +5611,6 @@ Proof. by rewrite /mx_faithful rker_gen. Qed. End GenField. -Arguments in_gen {F gT G n' rG A} irrG cGA {m1} W. -Arguments val_gen {F gT G n' rG A} irrG cGA {m1} W. -Arguments in_genK {F gT G n' rG A} irrG cGA {m1} W : rename. -Arguments val_genK {F gT G n' rG A} irrG cGA {m1} W : rename. - Section DecideGenField. Import MatrixFormula. @@ -5674,10 +5698,8 @@ elim: n1 => [|n1 IHn1] /=; first by rewrite eval_mx_term. by rewrite eval_mulT exprS IH1 IHn1. Qed. -(* WARNING: Coq will core dump if the Notation Bool is used in the match *) -(* pattern here. *) Fixpoint gen_form f := match f with -| GRing.Bool b => Bool b +| 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 @@ -5764,6 +5786,16 @@ End FiniteGenField. End MatrixGenField. +Bind Scope ring_scope with gen_of. +Arguments rVval {F gT G%G n'%N rG A%R irrG cGA} x%R : rename. +Prenex Implicits gen_of Gen rVval pval mxval gen groot. +Arguments subbase {F n'} A {nA}. +Prenex Implicits gen_dim gen_base base val_gen gen_mx rowval_gen. +Arguments in_gen {F gT G n' rG A} irrG cGA {m} W. +Arguments in_genK {F gT G n' rG A} irrG cGA {m} W : rename. +Arguments val_genK {F gT G n' rG A irrG cGA m} W : rename. +Prenex Implicits gen_env gen_term gen_form gen_sat. + Canonical gen_subType. Canonical gen_eqType. Canonical gen_choiceType. |