diff options
| author | Cyril Cohen | 2015-07-17 18:03:31 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2015-07-17 18:03:31 +0200 |
| commit | 532de9b68384a114c6534a0736ed024c900447f9 (patch) | |
| tree | e100a6a7839bf7548ab8a9e053033f8eef3c7492 /mathcomp/character | |
| parent | f180c539a00fd83d8b3b5fd2d5710eb16e971e2e (diff) | |
Updating files + reorganizing everything
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/Make | 2 | ||||
| -rw-r--r-- | mathcomp/character/all_character.v (renamed from mathcomp/character/all.v) | 0 | ||||
| -rw-r--r-- | mathcomp/character/character.v | 1075 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 129 | ||||
| -rw-r--r-- | mathcomp/character/finfield.v | 29 | ||||
| -rw-r--r-- | mathcomp/character/inertia.v | 45 | ||||
| -rw-r--r-- | mathcomp/character/integral_char.v | 47 | ||||
| -rw-r--r-- | mathcomp/character/mxabelem.v | 58 | ||||
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 275 | ||||
| -rw-r--r-- | mathcomp/character/vcharacter.v | 69 |
10 files changed, 867 insertions, 862 deletions
diff --git a/mathcomp/character/Make b/mathcomp/character/Make index 646641d..6d1f18c 100644 --- a/mathcomp/character/Make +++ b/mathcomp/character/Make @@ -1,4 +1,4 @@ -all.v +all_character.v character.v classfun.v finfield.v diff --git a/mathcomp/character/all.v b/mathcomp/character/all_character.v index 927d9a0..927d9a0 100644 --- a/mathcomp/character/all.v +++ b/mathcomp/character/all_character.v diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 166fcc5..146d965 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -1,27 +1,17 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg poly finalg zmodp cyclic. -From mathcomp.algebra -Require Import matrix mxalgebra mxpoly vector ssrnum. -From mathcomp.solvable -Require Import commutator center pgroup nilpotent sylow abelian. -From mathcomp.field -Require Import algC. -Require Import mxrepresentation classfun. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import GroupScope GRing.Theory Num.Theory. -Local Open Scope ring_scope. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg poly finset gproduct. +From mathcomp +Require Import fingroup morphism perm automorphism quotient finalg action. +From mathcomp +Require Import zmodp commutator cyclic center pgroup nilpotent sylow abelian. +From mathcomp +Require Import matrix mxalgebra mxpoly mxrepresentation vector ssrnum algC. +From mathcomp +Require Import classfun. (******************************************************************************) (* This file contains the basic notions of character theory, based on Isaacs. *) @@ -78,6 +68,13 @@ Local Open Scope ring_scope. (* class_Iirr xG == the index of xG \in classes G, in Iirr G. *) (******************************************************************************) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import GroupScope GRing.Theory Num.Theory. +Local Open Scope ring_scope. + Local Notation algCF := [fieldType of algC]. Section AlgC. @@ -333,9 +330,9 @@ rewrite !big_cons /= in dxW defW *. rewrite 2!(big_nth i) !big_mkord /= in IHe dxW defW. set Wi := (\sum_i _)%MS in defW dxW IHe. rewrite -mxdirectE mxdirect_addsE !mxdirectE eqxx /= -/Wi in dxW. -have modWi: mxmodule rG Wi by exact: sumsmx_module. +have modWi: mxmodule rG Wi by apply: sumsmx_module. case/andP: dxW; move/(IHe Wi modWi) {IHe}; move/(_ (eqmx_refl _))=> rsimWi. -by move/eqP; move/mxdirect_addsP=> dxUiWi; exact: mx_rsim_dadd (rsimU i) rsimWi. +by move/eqP; move/mxdirect_addsP=> dxUiWi; apply: mx_rsim_dadd (rsimU i) rsimWi. Qed. Definition muln_grepr rW k := \big[dadd_grepr/grepr0]_(i < k) rW. @@ -348,7 +345,7 @@ Proof. set M := socle_base W => modW rsimM. have simM: mxsimple rG M := socle_simple W. have rankM_gt0: (\rank M > 0)%N by rewrite lt0n mxrank_eq0; case: simM. -have [I /= U_I simU]: mxsemisimple rG W by exact: component_mx_semisimple. +have [I /= U_I simU]: mxsemisimple rG W by apply: component_mx_semisimple. pose U (i : 'I_#|I|) := U_I (enum_val i). have reindexI := reindex _ (onW_bij I (enum_val_bij I)). rewrite mxdirectE /= !reindexI -mxdirectE /= => defW dxW. @@ -360,8 +357,8 @@ have ->: socle_mult W = #|I|. rewrite -defW (mxdirectP dxW) /= -sum_nat_const reindexI /=. by apply: eq_bigr => i _; rewrite -(mxrank_iso (isoU i)). have modU: mxmodule rG (U _) := mxsimple_module (simU _). -suff: mx_rsim (submod_repr (modU _)) rW by exact: mx_rsim_dsum defW dxW. -by move=> i; apply: mx_rsim_trans (mx_rsim_sym _) rsimM; exact/mx_rsim_iso. +suff: mx_rsim (submod_repr (modU _)) rW by apply: mx_rsim_dsum defW dxW. +by move=> i; apply: mx_rsim_trans (mx_rsim_sym _) rsimM; apply/mx_rsim_iso. Qed. End DsumRepr. @@ -466,7 +463,7 @@ have [defS dxS]: (S :=: 1%:M)%MS /\ mxdirect S. rewrite /soc; case: pickP => [W' | /(_ Wi)] /= /eqP // eqWi. apply/eqP/socle_rsimP. apply: mx_rsim_trans (rsim_irr_comp iG C'G (socle_irr _)) (mx_rsim_sym _). - by rewrite [irr_comp _ _]eqWi; exact: rsim_irr_comp (socle_irr _). + by rewrite [irr_comp _ _]eqWi; apply: rsim_irr_comp (socle_irr _). have bij_irr: {on [pred i | soc i], bijective standard_irr}. exists (odflt W0 \o soc) => [Wi _ | i]; first by rewrite /= irrK. by rewrite inE /soc /=; case: pickP => //= Wi; move/eqP. @@ -485,7 +482,7 @@ apply: mx_rsim_dsum (modW) _ defS dxS _ => i. rewrite /W /standard_irr_coef /modW /soc; case: pickP => [Wi|_] /=; last first. rewrite /muln_grepr big_ord0. by exists 0 => [||x _]; rewrite ?mxrank0 ?mulmx0 ?mul0mx. -by move/eqP=> <-; apply: mx_rsim_socle; exact: rsim_irr_comp (socle_irr Wi). +by move/eqP=> <-; apply: mx_rsim_socle; apply: rsim_irr_comp (socle_irr Wi). Qed. End StandardRepr. @@ -560,7 +557,7 @@ Lemma NirrE : Nirr G = #|classes G|. Proof. by rewrite /pred_Nirr (cardD1 [1]) classes1. Qed. Fact Iirr_cast : Nirr G = #|sG|. -Proof. by rewrite NirrE ?card_irr ?algC'G //; exact: groupC. Qed. +Proof. by rewrite NirrE ?card_irr ?algC'G //; apply: groupC. Qed. Let offset := cast_ord (esym Iirr_cast) (enum_rank [1 sG]%irr). @@ -790,7 +787,7 @@ Lemma irr_reprP xi : (xi \in irr G). Proof. apply: (iffP (irrP xi)) => [[i ->] | [[n rG] irr_rG ->]]. - by exists (Representation 'Chi_i); [exact: socle_irr | rewrite irrRepr]. + by exists (Representation 'Chi_i); [apply: socle_irr | rewrite irrRepr]. exists (irr_of_socle (irr_comp sG rG)); rewrite -irrRepr irr_of_socleK /=. exact/cfRepr_sim/rsim_irr_comp. Qed. @@ -799,7 +796,7 @@ Qed. Lemma Wedderburn_id_expansion i : 'e_i = #|G|%:R^-1 *: \sum_(x in G) 'chi_i 1%g * 'chi_i x^-1%g *: aG x. Proof. -have Rei: ('e_i \in 'R_i)%MS by exact: Wedderburn_id_mem. +have Rei: ('e_i \in 'R_i)%MS by apply: Wedderburn_id_mem. have /envelop_mxP[a def_e]: ('e_i \in R_G)%MS; last rewrite -/aG in def_e. by move: Rei; rewrite genmxE mem_sub_gring => /andP[]. apply: canRL (scalerK (neq0CG _)) _; rewrite def_e linear_sum /=. @@ -932,20 +929,21 @@ Section AutChar. Variables (gT : finGroupType) (G : {group gT}). Implicit Type u : {rmorphism algC -> algC}. +Implicit Type chi : 'CF(G). Lemma cfRepr_map u n (rG : mx_representation algCF G n) : cfRepr (map_repr u rG) = cfAut u (cfRepr rG). Proof. by apply/cfun_inP=> x Gx; rewrite !cfunE Gx map_reprE trace_map_mx. Qed. -Lemma cfAut_char u (chi : 'CF(G)) : - chi \is a character -> cfAut u chi \is a character. +Lemma cfAut_char u chi : (cfAut u chi \is a character) = (chi \is a character). Proof. -case/char_reprP=> rG ->; apply/char_reprP. +without loss /char_reprP[rG ->]: u chi / chi \is a character. + by move=> IHu; apply/idP/idP=> ?; first rewrite -(cfAutK u chi); rewrite IHu. +rewrite cfRepr_char; apply/char_reprP. by exists (Representation (map_repr u rG)); rewrite cfRepr_map. Qed. -Lemma cfConjC_char (chi : 'CF(G)) : - chi \is a character -> chi^*%CF \is a character. +Lemma cfConjC_char chi : (chi^*%CF \is a character) = (chi \is a character). Proof. exact: cfAut_char. Qed. Lemma cfAut_char1 u (chi : 'CF(G)) : @@ -1037,7 +1035,7 @@ Qed. Lemma lin_char_irr : xi \in irr G. Proof. case/andP: CFxi => /char_reprP[rG ->]; rewrite cfRepr1 pnatr_eq1 => /eqP n1. -by apply/irr_reprP; exists rG => //; exact/mx_abs_irrW/linear_mx_abs_irr. +by apply/irr_reprP; exists rG => //; apply/mx_abs_irrW/linear_mx_abs_irr. Qed. Lemma mul_conjC_lin_char : xi * xi^*%CF = 1. @@ -1052,12 +1050,6 @@ Proof. by apply/unitrPr; exists xi^*%CF; apply: mul_conjC_lin_char. Qed. Lemma invr_lin_char : xi^-1 = xi^*%CF. Proof. by rewrite -[_^-1]mulr1 -mul_conjC_lin_char mulKr ?lin_char_unitr. Qed. -Lemma cfAut_lin_char u : cfAut u xi \is a linear_char. -Proof. by rewrite qualifE cfunE lin_char1 rmorph1 cfAut_char ?lin_charW /=. Qed. - -Lemma cfConjC_lin_char : xi^*%CF \is a linear_char. -Proof. exact: cfAut_lin_char. Qed. - Lemma fful_lin_char_inj : cfaithful xi -> {in G &, injective xi}. Proof. move=> fful_phi x y Gx Gy xi_xy; apply/eqP; rewrite eq_mulgV1 -in_set1. @@ -1068,6 +1060,14 @@ Qed. End OneChar. +Lemma cfAut_lin_char u (xi : 'CF(G)) : + (cfAut u xi \is a linear_char) = (xi \is a linear_char). +Proof. by rewrite qualifE cfAut_char; apply/andb_id2l=> /cfAut_char1->. Qed. + +Lemma cfConjC_lin_char (xi : 'CF(G)) : + (xi^*%CF \is a linear_char) = (xi \is a linear_char). +Proof. exact: cfAut_lin_char. Qed. + Lemma card_Iirr_abelian : abelian G -> #|Iirr G| = #|G|. Proof. by rewrite card_ord NirrE card_classes_abelian => /eqP. Qed. @@ -1079,7 +1079,7 @@ Lemma char_abelianP : Proof. apply: (iffP idP) => [cGG i | CF_G]. rewrite qualifE irr_char /= irr1_degree. - by rewrite irr_degree_abelian //; last exact: groupC. + by rewrite irr_degree_abelian //; last apply: groupC. rewrite card_classes_abelian -NirrE -eqC_nat -irr_sum_square //. rewrite -{1}[Nirr G]card_ord -sumr_const; apply/eqP/eq_bigr=> i _. by rewrite lin_char1 ?expr1n ?CF_G. @@ -1115,173 +1115,6 @@ End Linear. Prenex Implicits linear_char. -Section Restrict. - -Variable (gT : finGroupType) (G H : {group gT}). - -Lemma cfRepr_sub n (rG : mx_representation algCF G n) (sHG : H \subset G) : - cfRepr (subg_repr rG sHG) = 'Res[H] (cfRepr rG). -Proof. -by apply/cfun_inP => x Hx; rewrite cfResE // !cfunE Hx (subsetP sHG). -Qed. - -Lemma cfRes_char chi : chi \is a character -> 'Res[H, G] chi \is a character. -Proof. -have [sHG | not_sHG] := boolP (H \subset G). - by case/char_reprP=> rG ->; rewrite -(cfRepr_sub rG sHG) cfRepr_char. -by move/Cnat_char1=> Nchi1; rewrite cfResEout // rpredZ_Cnat ?rpred1. -Qed. - -Lemma cfRes_eq0 phi : phi \is a character -> ('Res[H, G] phi == 0) = (phi == 0). -Proof. by move=> Nchi; rewrite -!char1_eq0 ?cfRes_char // cfRes1. Qed. - -Lemma cfRes_lin_char chi : - chi \is a linear_char -> 'Res[H, G] chi \is a linear_char. -Proof. by case/andP=> Nchi; rewrite qualifE cfRes_char ?cfRes1. Qed. - -Lemma Res_irr_neq0 i : 'Res[H, G] 'chi_i != 0. -Proof. by rewrite cfRes_eq0 ?irr_neq0 ?irr_char. Qed. - -Lemma cfRes_lin_lin (chi : 'CF(G)) : - chi \is a character -> 'Res[H] chi \is a linear_char -> chi \is a linear_char. -Proof. by rewrite !qualifE cfRes1 => -> /andP[]. Qed. - -Lemma cfRes_irr_irr chi : - chi \is a character -> 'Res[H] chi \in irr H -> chi \in irr G. -Proof. -have [sHG /char_reprP[rG ->] | not_sHG Nchi] := boolP (H \subset G). - rewrite -(cfRepr_sub _ sHG) => /irr_reprP[rH irrH def_rH]; apply/irr_reprP. - suffices /subg_mx_irr: mx_irreducible (subg_repr rG sHG) by exists rG. - by apply: mx_rsim_irr irrH; exact/cfRepr_rsimP/eqP. -rewrite cfResEout // => /irrP[j Dchi_j]; apply/lin_char_irr/cfRes_lin_lin=> //. -suffices j0: j = 0 by rewrite cfResEout // Dchi_j j0 irr0 rpred1. -apply: contraNeq (irr1_neq0 j) => nz_j. -have:= xcfun_id j 0; rewrite -Dchi_j cfunE xcfunZl -irr0 xcfun_id eqxx => ->. -by rewrite (negPf nz_j). -Qed. - -Definition Res_Iirr (A B : {set gT}) i := cfIirr ('Res[B, A] 'chi_i). - -Lemma Res_Iirr0 : Res_Iirr H (0 : Iirr G) = 0. -Proof. by rewrite /Res_Iirr irr0 rmorph1 -irr0 irrK. Qed. - -Lemma lin_Res_IirrE i : 'chi[G]_i 1%g = 1 -> 'chi_(Res_Iirr H i) = 'Res 'chi_i. -Proof. -move=> chi1; rewrite cfIirrE ?lin_char_irr ?cfRes_lin_char //. -by rewrite qualifE irr_char /= chi1. -Qed. - -End Restrict. - -Arguments Scope Res_Iirr [_ group_scope group_scope ring_scope]. - -Section Morphim. - -Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}). -Implicit Type chi : 'CF(f @* G). - -Lemma cfRepr_morphim n (rfG : mx_representation algCF (f @* G) n) sGD : - cfRepr (morphim_repr rfG sGD) = cfMorph (cfRepr rfG). -Proof. -apply/cfun_inP=> x Gx; have Dx: x \in D := subsetP sGD x Gx. -by rewrite cfMorphE // !cfunE ?mem_morphim ?Gx. -Qed. - -Lemma cfMorph_char chi : chi \is a character -> cfMorph chi \is a character. -Proof. -have [sGD /char_reprP[rG ->] | outGD Nchi] := boolP (G \subset D); last first. - by rewrite cfMorphEout // rpredZ_Cnat ?rpred1 ?Cnat_char1. -apply/char_reprP; exists (Representation (morphim_repr rG sGD)). -by rewrite cfRepr_morphim. -Qed. - -Lemma cfMorph_lin_char chi : - chi \is a linear_char -> cfMorph chi \is a linear_char. -Proof. by case/andP=> Nchi; rewrite qualifE cfMorph_char ?cfMorph1. Qed. - -Lemma cfMorph_irr chi : - G \subset D -> chi \in irr (f @* G) -> cfMorph chi \in irr G. -Proof. -move=> sGD /irr_reprP[rG irrG ->]; apply/irr_reprP. -exists (Representation (morphim_repr rG sGD)); first exact/morphim_mx_irr. -apply/cfun_inP=> x Gx; rewrite !cfunElock /= sGD Gx. -by rewrite mem_morphim ?(subsetP sGD). -Qed. - -Definition morph_Iirr i := cfIirr (cfMorph 'chi[f @* G]_i). - -Lemma morph_Iirr0 : morph_Iirr 0 = 0. -Proof. by rewrite /morph_Iirr irr0 rmorph1 -irr0 irrK. Qed. - -Hypothesis sGD : G \subset D. - -Lemma morph_IirrE i : 'chi_(morph_Iirr i) = cfMorph 'chi_i. -Proof. by rewrite cfIirrE ?cfMorph_irr ?mem_irr. Qed. - -Lemma morph_Iirr_inj : injective morph_Iirr. -Proof. -by move=> i j eq_ij; apply/irr_inj/cfMorph_inj; rewrite // -!morph_IirrE eq_ij. -Qed. - -Lemma morph_Iirr_eq0 i : (morph_Iirr i == 0) = (i == 0). -Proof. by rewrite -!irr_eq1 morph_IirrE cfMorph_eq1. Qed. - -End Morphim. - -Section Isom. - -Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}). -Variables (R : {group rT}) (isoGR : isom G R f). -Implicit Type chi : 'CF(G). - -Lemma cfIsom_char chi : chi \is a character -> cfIsom isoGR chi \is a character. -Proof. -by move=> Nchi; rewrite [cfIsom _]locked_withE cfMorph_char ?cfRes_char. -Qed. - -Lemma cfIsom_lin_char chi : - chi \is a linear_char -> cfIsom isoGR chi \is a linear_char. -Proof. by case/andP=> Nchi; rewrite qualifE cfIsom_char ?cfIsom1. Qed. - -Lemma cfIsom_irr chi : chi \in irr G -> cfIsom isoGR chi \in irr R. -Proof. -move=> irr_chi; rewrite [cfIsom _]locked_withE cfMorph_irr //. -by rewrite (isom_im (isom_sym isoGR)) cfRes_id. -Qed. - -Definition isom_Iirr i := cfIirr (cfIsom isoGR 'chi_i). - -Lemma isom_IirrE i : 'chi_(isom_Iirr i) = cfIsom isoGR 'chi_i. -Proof. by rewrite cfIirrE ?cfIsom_irr ?mem_irr. Qed. - -Lemma isom_Iirr_inj : injective isom_Iirr. -Proof. -by move=> i j eqij; apply/irr_inj/(cfIsom_inj isoGR); rewrite -!isom_IirrE eqij. -Qed. - -Lemma isom_Iirr_eq0 i : (isom_Iirr i == 0) = (i == 0). -Proof. by rewrite -!irr_eq1 isom_IirrE cfIsom_eq1. Qed. - -Lemma isom_Iirr0 : isom_Iirr 0 = 0. -Proof. by apply/eqP; rewrite isom_Iirr_eq0. Qed. - -End Isom. - -Implicit Arguments isom_Iirr_inj [aT rT G f R x1 x2]. - -Section IsomInv. - -Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}). -Variables (R : {group rT}) (isoGR : isom G R f). - -Lemma isom_IirrK : cancel (isom_Iirr isoGR) (isom_Iirr (isom_sym isoGR)). -Proof. by move=> i; apply: irr_inj; rewrite !isom_IirrE cfIsomK. Qed. - -Lemma isom_IirrKV : cancel (isom_Iirr (isom_sym isoGR)) (isom_Iirr isoGR). -Proof. by move=> i; apply: irr_inj; rewrite !isom_IirrE cfIsomKV. Qed. - -End IsomInv. - Section OrthogonalityRelations. Variables aT gT : finGroupType. @@ -1303,9 +1136,9 @@ have [I U W simU W1 dxW]: mxsemisimple rG 1%:M. rewrite -(reducible_Socle1 (DecSocleType rG) (mx_Maschke _ (algC'G G))). exact: Socle_semisimple. have linU i: \rank (U i) = 1%N. - by apply: mxsimple_abelian_linear cGG (simU i); exact: groupC. + by apply: mxsimple_abelian_linear cGG (simU i); apply: groupC. have castI: f = #|I|. - by rewrite -(mxrank1 algCF f) -W1 (eqnP dxW) /= -sum1_card; exact/eq_bigr. + by rewrite -(mxrank1 algCF f) -W1 (eqnP dxW) /= -sum1_card; apply/eq_bigr. pose B := \matrix_j nz_row (U (enum_val (cast_ord castI j))). have rowU i: (nz_row (U i) :=: U i)%MS. apply/eqmxP; rewrite -(geq_leqif (mxrank_leqif_eq (nz_row_sub _))) linU. @@ -1417,8 +1250,8 @@ Proof. by move=> xG GxG; rewrite /c cast_ordKV enum_rankK_in. Qed. Lemma reindex_irr_class R idx (op : @Monoid.com_law R idx) F : \big[op/idx]_(xG in classes G) F xG = \big[op/idx]_i F (c i). Proof. -rewrite (reindex c); first by apply: eq_bigl => i; exact: enum_valP. -by exists iC; [apply: in1W; exact: irr_classK | exact: class_IirrK]. +rewrite (reindex c); first by apply: eq_bigl => i; apply: enum_valP. +by exists iC; [apply: in1W; apply: irr_classK | apply: class_IirrK]. Qed. (* The explicit value of the inverse is needed for the proof of the second *) @@ -1451,10 +1284,10 @@ transitivity ((#|'C_G[repr (y ^: G)]|%:R *: (X' *m X)) i_y i_x). rewrite scalemxAl !mxE; apply: eq_bigr => k _; rewrite !mxE mulrC -!mulrA. by rewrite !class_IirrK ?mem_classes // !cfun_repr mulVKf ?neq0CG. rewrite mulmx1C // !mxE -!divg_index !(index_cent1, =^~ indexgI). -rewrite (class_transr (mem_repr y _)) ?class_refl // mulr_natr. +rewrite (class_eqP (mem_repr y _)) ?class_refl // mulr_natr. rewrite (can_in_eq class_IirrK) ?mem_classes //. have [-> | not_yGx] := altP eqP; first by rewrite class_refl. -by rewrite [x \in _](contraNF _ not_yGx) // => /class_transr->. +by rewrite [x \in _](contraNF _ not_yGx) // => /class_eqP->. Qed. Lemma eq_irr_mem_classP x y : @@ -1638,24 +1471,435 @@ Qed. End InnerProduct. +Section IrrConstt. + +Variable (gT : finGroupType) (G H : {group gT}). + +Lemma char1_ge_norm (chi : 'CF(G)) x : + chi \is a character -> `|chi x| <= chi 1%g. +Proof. +case/char_reprP=> rG ->; case Gx: (x \in G); last first. + by rewrite cfunE cfRepr1 Gx normr0 ler0n. +by have [e [_ _ []]] := repr_rsim_diag rG Gx. +Qed. + +Lemma max_cfRepr_norm_scalar n (rG : mx_representation algCF G n) x : + x \in G -> `|cfRepr rG x| = cfRepr rG 1%g -> + exists2 c, `|c| = 1 & rG x = c%:M. +Proof. +move=> Gx; have [e [[B uB def_x] [_ e1] [-> _] _]] := repr_rsim_diag rG Gx. +rewrite cfRepr1 -[n in n%:R]card_ord -sumr_const -(eq_bigr _ (in1W e1)). +case/normC_sum_eq1=> [i _ | c /eqP norm_c_1 def_e]; first by rewrite e1. +have{def_e} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. +by exists c => //; rewrite def_x def_e diag_const_mx scalar_mxC mulmxKV. +Qed. + +Lemma max_cfRepr_mx1 n (rG : mx_representation algCF G n) x : + x \in G -> cfRepr rG x = cfRepr rG 1%g -> rG x = 1%:M. +Proof. +move=> Gx kerGx; have [|c _ def_x] := @max_cfRepr_norm_scalar n rG x Gx. + by rewrite kerGx cfRepr1 normr_nat. +move/eqP: kerGx; rewrite cfRepr1 cfunE Gx {rG}def_x mxtrace_scalar. +case: n => [_|n]; first by rewrite ![_%:M]flatmx0. +rewrite mulrb -subr_eq0 -mulrnBl -mulr_natl mulf_eq0 pnatr_eq0 /=. +by rewrite subr_eq0 => /eqP->. +Qed. + +Definition irr_constt (B : {set gT}) phi := [pred i | '[phi, 'chi_i]_B != 0]. + +Lemma irr_consttE i phi : (i \in irr_constt phi) = ('[phi, 'chi_i]_G != 0). +Proof. by []. Qed. + +Lemma constt_charP (i : Iirr G) chi : + chi \is a character -> + reflect (exists2 chi', chi' \is a character & chi = 'chi_i + chi') + (i \in irr_constt chi). +Proof. +move=> Nchi; apply: (iffP idP) => [i_in_chi| [chi' Nchi' ->]]; last first. + rewrite inE /= cfdotDl cfdot_irr eqxx -(eqP (Cnat_cfdot_char_irr i Nchi')). + by rewrite -natrD pnatr_eq0. +exists (chi - 'chi_i); last by rewrite addrC subrK. +apply/forallP=> j; rewrite coord_cfdot cfdotBl cfdot_irr. +have [<- | _] := eqP; last by rewrite subr0 Cnat_cfdot_char_irr. +have := i_in_chi; rewrite inE /= -(eqP (Cnat_cfdot_char_irr i Nchi)) pnatr_eq0. +by case: (truncC _) => // n _; rewrite mulrSr addrK ?isNatC_nat. +Qed. + +Lemma cfun_sum_constt (phi : 'CF(G)) : + phi = \sum_(i in irr_constt phi) '[phi, 'chi_i] *: 'chi_i. +Proof. +rewrite {1}[phi]cfun_sum_cfdot (bigID [pred i | '[phi, 'chi_i] == 0]) /=. +by rewrite big1 ?add0r // => i /eqP->; rewrite scale0r. +Qed. + +Lemma neq0_has_constt (phi : 'CF(G)) : + phi != 0 -> exists i, i \in irr_constt phi. +Proof. +move=> nz_phi; apply/existsP; apply: contra nz_phi => /pred0P phi0. +by rewrite [phi]cfun_sum_constt big_pred0. +Qed. + +Lemma constt_irr i : irr_constt 'chi[G]_i =i pred1 i. +Proof. +by move=> j; rewrite !inE cfdot_irr pnatr_eq0 (eq_sym j); case: (i == j). +Qed. + +Lemma char1_ge_constt (i : Iirr G) chi : + chi \is a character -> i \in irr_constt chi -> 'chi_i 1%g <= chi 1%g. +Proof. +move=> {chi} _ /constt_charP[// | chi Nchi ->]. +by rewrite cfunE addrC -subr_ge0 addrK char1_ge0. +Qed. + +Lemma constt_ortho_char (phi psi : 'CF(G)) i j : + phi \is a character -> psi \is a character -> + i \in irr_constt phi -> j \in irr_constt psi -> + '[phi, psi] = 0 -> '['chi_i, 'chi_j] = 0. +Proof. +move=> _ _ /constt_charP[//|phi1 Nphi1 ->] /constt_charP[//|psi1 Npsi1 ->]. +rewrite cfdot_irr; case: eqP => // -> /eqP/idPn[]. +rewrite cfdotDl !cfdotDr cfnorm_irr -addrA gtr_eqF ?ltr_paddr ?ltr01 //. +by rewrite Cnat_ge0 ?rpredD ?Cnat_cfdot_char ?irr_char. +Qed. + +End IrrConstt. + +Arguments Scope irr_constt [_ group_scope cfun_scope]. + +Section Kernel. + +Variable (gT : finGroupType) (G : {group gT}). +Implicit Types (phi chi xi : 'CF(G)) (H : {group gT}). + +Lemma cfker_repr n (rG : mx_representation algCF G n) : + cfker (cfRepr rG) = rker rG. +Proof. +apply/esym/setP=> x; rewrite inE mul1mx /=. +case Gx: (x \in G); last by rewrite inE Gx. +apply/eqP/idP=> Kx; last by rewrite max_cfRepr_mx1 // cfker1. +rewrite inE Gx; apply/forallP=> y; rewrite !cfunE !mulrb groupMl //. +by case: ifP => // Gy; rewrite repr_mxM // Kx mul1mx. +Qed. + +Lemma cfkerEchar chi : + chi \is a character -> cfker chi = [set x in G | chi x == chi 1%g]. +Proof. +move=> Nchi; apply/setP=> x; apply/idP/setIdP=> [Kx | [Gx /eqP chi_x]]. + by rewrite (subsetP (cfker_sub chi)) // cfker1. +case/char_reprP: Nchi => rG -> in chi_x *; rewrite inE Gx; apply/forallP=> y. +rewrite !cfunE groupMl // !mulrb; case: ifP => // Gy. +by rewrite repr_mxM // max_cfRepr_mx1 ?mul1mx. +Qed. + +Lemma cfker_nzcharE chi : + chi \is a character -> chi != 0 -> cfker chi = [set x | chi x == chi 1%g]. +Proof. +move=> Nchi nzchi; apply/setP=> x; rewrite cfkerEchar // !inE andb_idl //. +by apply: contraLR => /cfun0-> //; rewrite eq_sym char1_eq0. +Qed. + +Lemma cfkerEirr i : cfker 'chi[G]_i = [set x | 'chi_i x == 'chi_i 1%g]. +Proof. by rewrite cfker_nzcharE ?irr_char ?irr_neq0. Qed. + +Lemma cfker_irr0 : cfker 'chi[G]_0 = G. +Proof. by rewrite irr0 cfker_cfun1. Qed. + +Lemma cfaithful_reg : cfaithful (cfReg G). +Proof. +apply/subsetP=> x; rewrite cfkerEchar ?cfReg_char // !inE !cfRegE eqxx. +by case/andP=> _; apply: contraLR => /negbTE->; rewrite eq_sym neq0CG. +Qed. + +Lemma cfkerE chi : + chi \is a character -> + cfker chi = G :&: \bigcap_(i in irr_constt chi) cfker 'chi_i. +Proof. +move=> Nchi; rewrite cfkerEchar //; apply/setP=> x; rewrite !inE. +apply: andb_id2l => Gx; rewrite {1 2}[chi]cfun_sum_constt !sum_cfunE. +apply/eqP/bigcapP=> [Kx i Ci | Kx]; last first. + by apply: eq_bigr => i /Kx Kx_i; rewrite !cfunE cfker1. +rewrite cfkerEirr inE /= -(inj_eq (mulfI Ci)). +have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {i Ci} i _. +have chi_i_ge0: 0 <= '[chi, 'chi_i]. + by rewrite Cnat_ge0 ?Cnat_cfdot_char_irr. +by rewrite !cfunE normrM (normr_idP _) ?ler_wpmul2l ?char1_ge_norm ?irr_char. +Qed. + +Lemma TI_cfker_irr : \bigcap_i cfker 'chi[G]_i = [1]. +Proof. +apply/trivgP; apply: subset_trans cfaithful_reg; rewrite cfkerE ?cfReg_char //. +rewrite subsetI (bigcap_min 0) //=; last by rewrite cfker_irr0. +by apply/bigcapsP=> i _; rewrite bigcap_inf. +Qed. + +Lemma cfker_constt i chi : + chi \is a character -> i \in irr_constt chi -> + cfker chi \subset cfker 'chi[G]_i. +Proof. by move=> Nchi Ci; rewrite cfkerE ?subIset ?(bigcap_min i) ?orbT. Qed. + +Section KerLin. + +Variable xi : 'CF(G). +Hypothesis lin_xi : xi \is a linear_char. +Let Nxi: xi \is a character. Proof. by have [] := andP lin_xi. Qed. + +Lemma lin_char_der1 : G^`(1)%g \subset cfker xi. +Proof. +rewrite gen_subG /=; apply/subsetP=> _ /imset2P[x y Gx Gy ->]. +rewrite cfkerEchar // inE groupR //= !lin_charM ?lin_charV ?in_group //. +by rewrite mulrCA mulKf ?mulVf ?lin_char_neq0 // lin_char1. +Qed. + +Lemma cforder_lin_char : #[xi]%CF = exponent (G / cfker xi)%g. +Proof. +apply/eqP; rewrite eqn_dvd; apply/andP; split. + apply/dvdn_cforderP=> x Gx; rewrite -lin_charX // -cfQuoEker ?groupX //. + rewrite morphX ?(subsetP (cfker_norm xi)) //= expg_exponent ?mem_quotient //. + by rewrite cfQuo1 ?cfker_normal ?lin_char1. +have abGbar: abelian (G / cfker xi) := sub_der1_abelian lin_char_der1. +have [_ /morphimP[x Nx Gx ->] ->] := exponent_witness (abelian_nil abGbar). +rewrite order_dvdn -morphX //= coset_id cfkerEchar // !inE groupX //=. +by rewrite lin_charX ?lin_char1 // (dvdn_cforderP _ _ _). +Qed. + +Lemma cforder_lin_char_dvdG : #[xi]%CF %| #|G|. +Proof. +by rewrite cforder_lin_char (dvdn_trans (exponent_dvdn _)) ?dvdn_morphim. +Qed. + +Lemma cforder_lin_char_gt0 : (0 < #[xi]%CF)%N. +Proof. by rewrite cforder_lin_char exponent_gt0. Qed. + +End KerLin. + +End Kernel. + +Section Restrict. + +Variable (gT : finGroupType) (G H : {group gT}). + +Lemma cfRepr_sub n (rG : mx_representation algCF G n) (sHG : H \subset G) : + cfRepr (subg_repr rG sHG) = 'Res[H] (cfRepr rG). +Proof. +by apply/cfun_inP => x Hx; rewrite cfResE // !cfunE Hx (subsetP sHG). +Qed. + +Lemma cfRes_char chi : chi \is a character -> 'Res[H, G] chi \is a character. +Proof. +have [sHG | not_sHG] := boolP (H \subset G). + by case/char_reprP=> rG ->; rewrite -(cfRepr_sub rG sHG) cfRepr_char. +by move/Cnat_char1=> Nchi1; rewrite cfResEout // rpredZ_Cnat ?rpred1. +Qed. + +Lemma cfRes_eq0 phi : phi \is a character -> ('Res[H, G] phi == 0) = (phi == 0). +Proof. by move=> Nchi; rewrite -!char1_eq0 ?cfRes_char // cfRes1. Qed. + +Lemma cfRes_lin_char chi : + chi \is a linear_char -> 'Res[H, G] chi \is a linear_char. +Proof. by case/andP=> Nchi; rewrite qualifE cfRes_char ?cfRes1. Qed. + +Lemma Res_irr_neq0 i : 'Res[H, G] 'chi_i != 0. +Proof. by rewrite cfRes_eq0 ?irr_neq0 ?irr_char. Qed. + +Lemma cfRes_lin_lin (chi : 'CF(G)) : + chi \is a character -> 'Res[H] chi \is a linear_char -> chi \is a linear_char. +Proof. by rewrite !qualifE cfRes1 => -> /andP[]. Qed. + +Lemma cfRes_irr_irr chi : + chi \is a character -> 'Res[H] chi \in irr H -> chi \in irr G. +Proof. +have [sHG /char_reprP[rG ->] | not_sHG Nchi] := boolP (H \subset G). + rewrite -(cfRepr_sub _ sHG) => /irr_reprP[rH irrH def_rH]; apply/irr_reprP. + suffices /subg_mx_irr: mx_irreducible (subg_repr rG sHG) by exists rG. + by apply: mx_rsim_irr irrH; apply/cfRepr_rsimP/eqP. +rewrite cfResEout // => /irrP[j Dchi_j]; apply/lin_char_irr/cfRes_lin_lin=> //. +suffices j0: j = 0 by rewrite cfResEout // Dchi_j j0 irr0 rpred1. +apply: contraNeq (irr1_neq0 j) => nz_j. +have:= xcfun_id j 0; rewrite -Dchi_j cfunE xcfunZl -irr0 xcfun_id eqxx => ->. +by rewrite (negPf nz_j). +Qed. + +Definition Res_Iirr (A B : {set gT}) i := cfIirr ('Res[B, A] 'chi_i). + +Lemma Res_Iirr0 : Res_Iirr H (0 : Iirr G) = 0. +Proof. by rewrite /Res_Iirr irr0 rmorph1 -irr0 irrK. Qed. + +Lemma lin_Res_IirrE i : 'chi[G]_i 1%g = 1 -> 'chi_(Res_Iirr H i) = 'Res 'chi_i. +Proof. +move=> chi1; rewrite cfIirrE ?lin_char_irr ?cfRes_lin_char //. +by rewrite qualifE irr_char /= chi1. +Qed. + +End Restrict. + +Arguments Scope Res_Iirr [_ group_scope group_scope ring_scope]. + +Section MoreConstt. + +Variables (gT : finGroupType) (G H : {group gT}). + +Lemma constt_Ind_Res i j : + i \in irr_constt ('Ind[G] 'chi_j) = (j \in irr_constt ('Res[H] 'chi_i)). +Proof. by rewrite !irr_consttE cfdotC conjC_eq0 -cfdot_Res_l. Qed. + +Lemma cfdot_Res_ge_constt i j psi : + psi \is a character -> j \in irr_constt psi -> + '['Res[H, G] 'chi_j, 'chi_i] <= '['Res[H] psi, 'chi_i]. +Proof. +move=> {psi} _ /constt_charP[// | psi Npsi ->]. +rewrite linearD cfdotDl addrC -subr_ge0 addrK Cnat_ge0 //=. +by rewrite Cnat_cfdot_char_irr // cfRes_char. +Qed. + +Lemma constt_Res_trans j psi : + psi \is a character -> j \in irr_constt psi -> + {subset irr_constt ('Res[H, G] 'chi_j) <= irr_constt ('Res[H] psi)}. +Proof. +move=> Npsi Cj i; apply: contraNneq; rewrite eqr_le => {1}<-. +rewrite cfdot_Res_ge_constt ?Cnat_ge0 ?Cnat_cfdot_char_irr //. +by rewrite cfRes_char ?irr_char. +Qed. + +End MoreConstt. + +Section Morphim. + +Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}). +Implicit Type chi : 'CF(f @* G). + +Lemma cfRepr_morphim n (rfG : mx_representation algCF (f @* G) n) sGD : + cfRepr (morphim_repr rfG sGD) = cfMorph (cfRepr rfG). +Proof. +apply/cfun_inP=> x Gx; have Dx: x \in D := subsetP sGD x Gx. +by rewrite cfMorphE // !cfunE ?mem_morphim ?Gx. +Qed. + +Lemma cfMorph_char chi : chi \is a character -> cfMorph chi \is a character. +Proof. +have [sGD /char_reprP[rfG ->] | outGD Nchi] := boolP (G \subset D); last first. + by rewrite cfMorphEout // rpredZ_Cnat ?rpred1 ?Cnat_char1. +apply/char_reprP; exists (Representation (morphim_repr rfG sGD)). +by rewrite cfRepr_morphim. +Qed. + +Lemma cfMorph_lin_char chi : + chi \is a linear_char -> cfMorph chi \is a linear_char. +Proof. by case/andP=> Nchi; rewrite qualifE cfMorph1 cfMorph_char. Qed. + +Lemma cfMorph_charE chi : + G \subset D -> (cfMorph chi \is a character) = (chi \is a character). +Proof. +move=> sGD; apply/idP/idP=> [/char_reprP[[n rG] /=Dfchi] | /cfMorph_char//]. +pose H := 'ker_G f; have kerH: H \subset rker rG. + by rewrite -cfker_repr -Dfchi cfker_morph // setIS // ker_sub_pre. +have nHG: G \subset 'N(H) by rewrite normsI // (subset_trans sGD) ?ker_norm. +have [h injh im_h] := first_isom_loc f sGD; rewrite -/H in h injh im_h. +have DfG: invm injh @*^-1 (G / H) == (f @* G)%g by rewrite morphpre_invm im_h. +pose rfG := eqg_repr (morphpre_repr _ (quo_repr kerH nHG)) DfG. +apply/char_reprP; exists (Representation rfG). +apply/cfun_inP=> _ /morphimP[x Dx Gx ->]; rewrite -cfMorphE // Dfchi !cfunE Gx. +pose xH := coset H x; have GxH: xH \in (G / H)%g by apply: mem_quotient. +suffices Dfx: f x = h xH by rewrite mem_morphim //= Dfx invmE ?quo_repr_coset. +by apply/set1_inj; rewrite -?morphim_set1 ?im_h ?(subsetP nHG) ?sub1set. +Qed. + +Lemma cfMorph_lin_charE chi : + G \subset D -> (cfMorph chi \is a linear_char) = (chi \is a linear_char). +Proof. by rewrite qualifE cfMorph1 => /cfMorph_charE->. Qed. + +Lemma cfMorph_irr chi : + G \subset D -> (cfMorph chi \in irr G) = (chi \in irr (f @* G)). +Proof. by move=> sGD; rewrite !irrEchar cfMorph_charE // cfMorph_iso. Qed. + +Definition morph_Iirr i := cfIirr (cfMorph 'chi[f @* G]_i). + +Lemma morph_Iirr0 : morph_Iirr 0 = 0. +Proof. by rewrite /morph_Iirr irr0 rmorph1 -irr0 irrK. Qed. + +Hypothesis sGD : G \subset D. + +Lemma morph_IirrE i : 'chi_(morph_Iirr i) = cfMorph 'chi_i. +Proof. by rewrite cfIirrE ?cfMorph_irr ?mem_irr. Qed. + +Lemma morph_Iirr_inj : injective morph_Iirr. +Proof. +by move=> i j eq_ij; apply/irr_inj/cfMorph_inj; rewrite // -!morph_IirrE eq_ij. +Qed. + +Lemma morph_Iirr_eq0 i : (morph_Iirr i == 0) = (i == 0). +Proof. by rewrite -!irr_eq1 morph_IirrE cfMorph_eq1. Qed. + +End Morphim. + +Section Isom. + +Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}). +Variables (R : {group rT}) (isoGR : isom G R f). +Implicit Type chi : 'CF(G). + +Lemma cfIsom_char chi : + (cfIsom isoGR chi \is a character) = (chi \is a character). +Proof. +rewrite [cfIsom _]locked_withE cfMorph_charE //. +by rewrite (isom_im (isom_sym _)) cfRes_id. +Qed. + +Lemma cfIsom_lin_char chi : + (cfIsom isoGR chi \is a linear_char) = (chi \is a linear_char). +Proof. by rewrite qualifE cfIsom_char cfIsom1. Qed. + +Lemma cfIsom_irr chi : (cfIsom isoGR chi \in irr R) = (chi \in irr G). +Proof. by rewrite !irrEchar cfIsom_char cfIsom_iso. Qed. + +Definition isom_Iirr i := cfIirr (cfIsom isoGR 'chi_i). + +Lemma isom_IirrE i : 'chi_(isom_Iirr i) = cfIsom isoGR 'chi_i. +Proof. by rewrite cfIirrE ?cfIsom_irr ?mem_irr. Qed. + +Lemma isom_Iirr_inj : injective isom_Iirr. +Proof. +by move=> i j eqij; apply/irr_inj/(cfIsom_inj isoGR); rewrite -!isom_IirrE eqij. +Qed. + +Lemma isom_Iirr_eq0 i : (isom_Iirr i == 0) = (i == 0). +Proof. by rewrite -!irr_eq1 isom_IirrE cfIsom_eq1. Qed. + +Lemma isom_Iirr0 : isom_Iirr 0 = 0. +Proof. by apply/eqP; rewrite isom_Iirr_eq0. Qed. + +End Isom. + +Implicit Arguments isom_Iirr_inj [aT rT G f R x1 x2]. + +Section IsomInv. + +Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}). +Variables (R : {group rT}) (isoGR : isom G R f). + +Lemma isom_IirrK : cancel (isom_Iirr isoGR) (isom_Iirr (isom_sym isoGR)). +Proof. by move=> i; apply: irr_inj; rewrite !isom_IirrE cfIsomK. Qed. + +Lemma isom_IirrKV : cancel (isom_Iirr (isom_sym isoGR)) (isom_Iirr isoGR). +Proof. by move=> i; apply: irr_inj; rewrite !isom_IirrE cfIsomKV. Qed. + +End IsomInv. + Section Sdprod. Variables (gT : finGroupType) (K H G : {group gT}). Hypothesis defG : K ><| H = G. +Let nKG: G \subset 'N(K). Proof. by have [/andP[]] := sdprod_context defG. Qed. Lemma cfSdprod_char chi : - chi \is a character -> cfSdprod defG chi \is a character. -Proof. by move=> Nchi; rewrite unlock cfMorph_char ?cfIsom_char. Qed. + (cfSdprod defG chi \is a character) = (chi \is a character). +Proof. by rewrite unlock cfMorph_charE // cfIsom_char. Qed. Lemma cfSdprod_lin_char chi : - chi \is a linear_char -> cfSdprod defG chi \is a linear_char. -Proof. by move=> Nphi; rewrite unlock cfMorph_lin_char ?cfIsom_lin_char. Qed. + (cfSdprod defG chi \is a linear_char) = (chi \is a linear_char). +Proof. by rewrite qualifE cfSdprod_char cfSdprod1. Qed. -Lemma cfSdprod_irr chi : chi \in irr H -> cfSdprod defG chi \in irr G. -Proof. -have [/andP[_ nKG] _ _ _ _] := sdprod_context defG. -by move=> Nphi; rewrite unlock cfMorph_irr ?cfIsom_irr. -Qed. +Lemma cfSdprod_irr chi : (cfSdprod defG chi \in irr G) = (chi \in irr H). +Proof. by rewrite !irrEchar cfSdprod_char cfSdprod_iso. Qed. Definition sdprod_Iirr j := cfIirr (cfSdprod defG 'chi_j). @@ -1707,17 +1951,17 @@ Lemma cfDprodKr_abelian i : abelian K -> cancel (cfDprod KxH 'chi_i) 'Res. Proof. by move=> cKK; apply: cfDprodKr; apply/lin_char1/char_abelianP. Qed. Lemma cfDprodl_char phi : - phi \is a character -> cfDprodl KxH phi \is a character. + (cfDprodl KxH phi \is a character) = (phi \is a character). Proof. exact: cfSdprod_char. Qed. Lemma cfDprodr_char psi : - psi \is a character -> cfDprodr KxH psi \is a character. + (cfDprodr KxH psi \is a character) = (psi \is a character). Proof. exact: cfSdprod_char. Qed. Lemma cfDprod_char phi psi : phi \is a character -> psi \is a character -> cfDprod KxH phi psi \is a character. -Proof. by move=> /cfDprodl_char Nphi /cfDprodr_char; apply: rpredM. Qed. +Proof. by move=> Nphi Npsi; rewrite rpredM ?cfDprodl_char ?cfDprodr_char. Qed. Lemma cfDprod_eq1 phi psi : phi \is a character -> psi \is a character -> @@ -1732,22 +1976,22 @@ by rewrite !rmorph1. Qed. Lemma cfDprodl_lin_char phi : - phi \is a linear_char -> cfDprodl KxH phi \is a linear_char. + (cfDprodl KxH phi \is a linear_char) = (phi \is a linear_char). Proof. exact: cfSdprod_lin_char. Qed. Lemma cfDprodr_lin_char psi : - psi \is a linear_char -> cfDprodr KxH psi \is a linear_char. + (cfDprodr KxH psi \is a linear_char) = (psi \is a linear_char). Proof. exact: cfSdprod_lin_char. Qed. Lemma cfDprod_lin_char phi psi : phi \is a linear_char -> psi \is a linear_char -> cfDprod KxH phi psi \is a linear_char. -Proof. by move=> /cfDprodl_lin_char Lphi /cfDprodr_lin_char; apply: rpredM. Qed. +Proof. by move=> Nphi Npsi; rewrite rpredM ?cfSdprod_lin_char. Qed. -Lemma cfDprodl_irr chi : chi \in irr K -> cfDprodl KxH chi \in irr G. +Lemma cfDprodl_irr chi : (cfDprodl KxH chi \in irr G) = (chi \in irr K). Proof. exact: cfSdprod_irr. Qed. -Lemma cfDprodr_irr chi : chi \in irr H -> cfDprodr KxH chi \in irr G. +Lemma cfDprodr_irr chi : (cfDprodr KxH chi \in irr G) = (chi \in irr H). Proof. exact: cfSdprod_irr. Qed. Definition dprodl_Iirr i := cfIirr (cfDprodl KxH 'chi_i). @@ -1834,10 +2078,10 @@ Qed. Definition inv_dprod_Iirr i := iinv (dprod_Iirr_onto i). Lemma dprod_IirrK : cancel dprod_Iirr inv_dprod_Iirr. -Proof. by move=> p; exact: (iinv_f dprod_Iirr_inj). Qed. +Proof. by move=> p; apply: (iinv_f dprod_Iirr_inj). Qed. Lemma inv_dprod_IirrK : cancel inv_dprod_Iirr dprod_Iirr. -Proof. by move=> i; exact: f_iinv. Qed. +Proof. by move=> i; apply: f_iinv. Qed. Lemma inv_dprod_Iirr0 : inv_dprod_Iirr 0 = (0, 0). Proof. by apply/(canLR dprod_IirrK); rewrite dprod_Iirr0. Qed. @@ -1862,7 +2106,11 @@ Proof. by move=> Pi; rewrite -(bigdprodWY defG) (bigD1 i) ?joing_subl. Qed. Lemma cfBigdprodi_char i (phi : 'CF(A i)) : phi \is a character -> cfBigdprodi defG phi \is a character. -Proof. by move=> Nphi; rewrite cfDprodl_char ?cfRes_char. Qed. +Proof. by move=> Nphi; rewrite cfDprodl_char cfRes_char. Qed. + +Lemma cfBigdprodi_charE i (phi : 'CF(A i)) : + P i -> (cfBigdprodi defG phi \is a character) = (phi \is a character). +Proof. by move=> Pi; rewrite cfDprodl_char Pi cfRes_id. Qed. Lemma cfBigdprod_char phi : (forall i, P i -> phi i \is a character) -> @@ -1875,6 +2123,10 @@ Lemma cfBigdprodi_lin_char i (phi : 'CF(A i)) : phi \is a linear_char -> cfBigdprodi defG phi \is a linear_char. Proof. by move=> Lphi; rewrite cfDprodl_lin_char ?cfRes_lin_char. Qed. +Lemma cfBigdprodi_lin_charE i (phi : 'CF(A i)) : + P i -> (cfBigdprodi defG phi \is a linear_char) = (phi \is a linear_char). +Proof. by move=> Pi; rewrite qualifE cfBigdprodi_charE // cfBigdprodi1. Qed. + Lemma cfBigdprod_lin_char phi : (forall i, P i -> phi i \is a linear_char) -> cfBigdprod defG phi \is a linear_char. @@ -1883,8 +2135,8 @@ by move=> Lphi; apply/rpred_prod=> i /Lphi; apply: cfBigdprodi_lin_char. Qed. Lemma cfBigdprodi_irr i chi : - P i -> chi \in irr (A i) -> cfBigdprodi defG chi \in irr G. -Proof. by move=> Pi Nchi; rewrite cfDprodl_irr // Pi cfRes_id. Qed. + P i -> (cfBigdprodi defG chi \in irr G) = (chi \in irr (A i)). +Proof. by move=> Pi; rewrite !irrEchar cfBigdprodi_charE ?cfBigdprodi_iso. Qed. Lemma cfBigdprod_irr chi : (forall i, P i -> chi i \in irr (A i)) -> cfBigdprod defG chi \in irr G. @@ -1946,7 +2198,7 @@ Lemma conjC_charAut u (chi : 'CF(G)) x : Proof. have [Gx | /cfun0->] := boolP (x \in G); last by rewrite !rmorph0. case/char_reprP=> rG ->; have [e [_ [en1 _] [-> _] _]] := repr_rsim_diag rG Gx. -by rewrite !rmorph_sum; apply: eq_bigr => i _; exact: aut_unity_rootC (en1 i). +by rewrite !rmorph_sum; apply: eq_bigr => i _; apply: aut_unity_rootC (en1 i). Qed. Lemma conjC_irrAut u i x : (u ('chi[G]_i x))^* = u ('chi_i x)^*. @@ -1960,17 +2212,17 @@ Lemma cfdot_aut_irr u phi i : '[cfAut u phi, cfAut u 'chi[G]_i] = u '[phi, 'chi_i]. Proof. exact: cfdot_aut_char (irr_char i). Qed. -Lemma cfAut_irr u chi : chi \in irr G -> cfAut u chi \in irr G. +Lemma cfAut_irr u chi : (cfAut u chi \in irr G) = (chi \in irr G). Proof. -case/irrP=> i ->; rewrite irrEchar cfAut_char ?irr_char //=. -by rewrite cfdot_aut_irr // cfdot_irr eqxx rmorph1. +rewrite !irrEchar cfAut_char; apply/andb_id2l=> /cfdot_aut_char->. +exact: fmorph_eq1. Qed. Lemma cfConjC_irr i : (('chi_i)^*)%CF \in irr G. -Proof. by rewrite cfAut_irr ?mem_irr. Qed. +Proof. by rewrite cfAut_irr mem_irr. Qed. Lemma irr_aut_closed u : cfAut_closed u (irr G). -Proof. exact: cfAut_irr. Qed. +Proof. by move=> chi; rewrite /= cfAut_irr. Qed. Definition aut_Iirr u i := cfIirr (cfAut u 'chi[G]_i). @@ -2002,255 +2254,10 @@ Proof. by move=> i j eq_ij; apply/irr_inj/(cfAut_inj u); rewrite -!aut_IirrE eq_ij. Qed. -Lemma char_aut u (chi : 'CF(G)) : - (cfAut u chi \is a character) = (chi \is a character). -Proof. -apply/idP/idP=> [Nuchi|]; last exact: cfAut_char. -rewrite [chi]cfun_sum_cfdot rpred_sum // => i _. -rewrite rpredZ_Cnat ?irr_char // -(Cnat_aut u) -cfdot_aut_irr. -by rewrite -aut_IirrE Cnat_cfdot_char_irr. -Qed. - -Lemma irr_aut u chi : (cfAut u chi \in irr G) = (chi \in irr G). -Proof. -rewrite !irrEchar char_aut; apply/andb_id2l=> /cfdot_aut_char->. -by rewrite fmorph_eq1. -Qed. - End Aut. -Section IrrConstt. - -Variable (gT : finGroupType) (G H : {group gT}). - -Lemma char1_ge_norm (chi : 'CF(G)) x : - chi \is a character -> `|chi x| <= chi 1%g. -Proof. -case/char_reprP=> rG ->; case Gx: (x \in G); last first. - by rewrite cfunE cfRepr1 Gx normr0 ler0n. -by have [e [_ _ []]] := repr_rsim_diag rG Gx. -Qed. - -Lemma max_cfRepr_norm_scalar n (rG : mx_representation algCF G n) x : - x \in G -> `|cfRepr rG x| = cfRepr rG 1%g -> - exists2 c, `|c| = 1 & rG x = c%:M. -Proof. -move=> Gx; have [e [[B uB def_x] [_ e1] [-> _] _]] := repr_rsim_diag rG Gx. -rewrite cfRepr1 -[n in n%:R]card_ord -sumr_const -(eq_bigr _ (in1W e1)). -case/normC_sum_eq1=> [i _ | c /eqP norm_c_1 def_e]; first by rewrite e1. -have{def_e} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. -by exists c => //; rewrite def_x def_e diag_const_mx scalar_mxC mulmxKV. -Qed. - -Lemma max_cfRepr_mx1 n (rG : mx_representation algCF G n) x : - x \in G -> cfRepr rG x = cfRepr rG 1%g -> rG x = 1%:M. -Proof. -move=> Gx kerGx; have [|c _ def_x] := @max_cfRepr_norm_scalar n rG x Gx. - by rewrite kerGx cfRepr1 normr_nat. -move/eqP: kerGx; rewrite cfRepr1 cfunE Gx {rG}def_x mxtrace_scalar. -case: n => [_|n]; first by rewrite ![_%:M]flatmx0. -rewrite mulrb -subr_eq0 -mulrnBl -mulr_natl mulf_eq0 pnatr_eq0 /=. -by rewrite subr_eq0 => /eqP->. -Qed. - -Definition irr_constt (B : {set gT}) phi := [pred i | '[phi, 'chi_i]_B != 0]. - -Lemma irr_consttE i phi : (i \in irr_constt phi) = ('[phi, 'chi_i]_G != 0). -Proof. by []. Qed. - -Lemma constt_charP (i : Iirr G) chi : - chi \is a character -> - reflect (exists2 chi', chi' \is a character & chi = 'chi_i + chi') - (i \in irr_constt chi). -Proof. -move=> Nchi; apply: (iffP idP) => [i_in_chi| [chi' Nchi' ->]]; last first. - rewrite inE /= cfdotDl cfdot_irr eqxx -(eqP (Cnat_cfdot_char_irr i Nchi')). - by rewrite -natrD pnatr_eq0. -exists (chi - 'chi_i); last by rewrite addrC subrK. -apply/forallP=> j; rewrite coord_cfdot cfdotBl cfdot_irr. -have [<- | _] := eqP; last by rewrite subr0 Cnat_cfdot_char_irr. -have := i_in_chi; rewrite inE /= -(eqP (Cnat_cfdot_char_irr i Nchi)) pnatr_eq0. -by case: (truncC _) => // n _; rewrite mulrSr addrK ?isNatC_nat. -Qed. - -Lemma cfun_sum_constt (phi : 'CF(G)) : - phi = \sum_(i in irr_constt phi) '[phi, 'chi_i] *: 'chi_i. -Proof. -rewrite {1}[phi]cfun_sum_cfdot (bigID [pred i | '[phi, 'chi_i] == 0]) /=. -by rewrite big1 ?add0r // => i /eqP->; rewrite scale0r. -Qed. - -Lemma neq0_has_constt (phi : 'CF(G)) : - phi != 0 -> exists i, i \in irr_constt phi. -Proof. -move=> nz_phi; apply/existsP; apply: contra nz_phi => /pred0P phi0. -by rewrite [phi]cfun_sum_constt big_pred0. -Qed. - -Lemma constt_irr i : irr_constt 'chi[G]_i =i pred1 i. -Proof. -by move=> j; rewrite !inE cfdot_irr pnatr_eq0 (eq_sym j); case: (i == j). -Qed. - -Lemma char1_ge_constt (i : Iirr G) chi : - chi \is a character -> i \in irr_constt chi -> 'chi_i 1%g <= chi 1%g. -Proof. -move=> {chi} _ /constt_charP[// | chi Nchi ->]. -by rewrite cfunE addrC -subr_ge0 addrK char1_ge0. -Qed. - -Lemma constt_ortho_char (phi psi : 'CF(G)) i j : - phi \is a character -> psi \is a character -> - i \in irr_constt phi -> j \in irr_constt psi -> - '[phi, psi] = 0 -> '['chi_i, 'chi_j] = 0. -Proof. -move=> _ _ /constt_charP[//|phi1 Nphi1 ->] /constt_charP[//|psi1 Npsi1 ->]. -rewrite cfdot_irr; case: eqP => // -> /eqP/idPn[]. -rewrite cfdotDl !cfdotDr cfnorm_irr -addrA gtr_eqF ?ltr_paddr ?ltr01 //. -by rewrite Cnat_ge0 ?rpredD ?Cnat_cfdot_char ?irr_char. -Qed. - -End IrrConstt. - -Arguments Scope irr_constt [_ group_scope cfun_scope]. Implicit Arguments aut_Iirr_inj [gT G x1 x2]. -Section MoreConstt. - -Variables (gT : finGroupType) (G H : {group gT}). - -Lemma constt_Ind_Res i j : - i \in irr_constt ('Ind[G] 'chi_j) = (j \in irr_constt ('Res[H] 'chi_i)). -Proof. by rewrite !irr_consttE cfdotC conjC_eq0 -cfdot_Res_l. Qed. - -Lemma cfdot_Res_ge_constt i j psi : - psi \is a character -> j \in irr_constt psi -> - '['Res[H, G] 'chi_j, 'chi_i] <= '['Res[H] psi, 'chi_i]. -Proof. -move=> {psi} _ /constt_charP[// | psi Npsi ->]. -rewrite linearD cfdotDl addrC -subr_ge0 addrK Cnat_ge0 //=. -by rewrite Cnat_cfdot_char_irr // cfRes_char. -Qed. - -Lemma constt_Res_trans j psi : - psi \is a character -> j \in irr_constt psi -> - {subset irr_constt ('Res[H, G] 'chi_j) <= irr_constt ('Res[H] psi)}. -Proof. -move=> Npsi Cj i; apply: contraNneq; rewrite eqr_le => {1}<-. -rewrite cfdot_Res_ge_constt ?Cnat_ge0 ?Cnat_cfdot_char_irr //. -by rewrite cfRes_char ?irr_char. -Qed. - -End MoreConstt. - -Section Kernel. - -Variable (gT : finGroupType) (G : {group gT}). -Implicit Types (phi chi xi : 'CF(G)) (H : {group gT}). - -Lemma cfker_repr n (rG : mx_representation algCF G n) : - cfker (cfRepr rG) = rker rG. -Proof. -apply/esym/setP=> x; rewrite inE mul1mx /=. -case Gx: (x \in G); last by rewrite inE Gx. -apply/eqP/idP=> Kx; last by rewrite max_cfRepr_mx1 // cfker1. -rewrite inE Gx; apply/forallP=> y; rewrite !cfunE !mulrb groupMl //. -by case: ifP => // Gy; rewrite repr_mxM // Kx mul1mx. -Qed. - -Lemma cfkerEchar chi : - chi \is a character -> cfker chi = [set x in G | chi x == chi 1%g]. -Proof. -move=> Nchi; apply/setP=> x; apply/idP/setIdP=> [Kx | [Gx /eqP chi_x]]. - by rewrite (subsetP (cfker_sub chi)) // cfker1. -case/char_reprP: Nchi => rG -> in chi_x *; rewrite inE Gx; apply/forallP=> y. -rewrite !cfunE groupMl // !mulrb; case: ifP => // Gy. -by rewrite repr_mxM // max_cfRepr_mx1 ?mul1mx. -Qed. - -Lemma cfker_nzcharE chi : - chi \is a character -> chi != 0 -> cfker chi = [set x | chi x == chi 1%g]. -Proof. -move=> Nchi nzchi; apply/setP=> x; rewrite cfkerEchar // !inE andb_idl //. -by apply: contraLR => /cfun0-> //; rewrite eq_sym char1_eq0. -Qed. - -Lemma cfkerEirr i : cfker 'chi[G]_i = [set x | 'chi_i x == 'chi_i 1%g]. -Proof. by rewrite cfker_nzcharE ?irr_char ?irr_neq0. Qed. - -Lemma cfker_irr0 : cfker 'chi[G]_0 = G. -Proof. by rewrite irr0 cfker_cfun1. Qed. - -Lemma cfaithful_reg : cfaithful (cfReg G). -Proof. -apply/subsetP=> x; rewrite cfkerEchar ?cfReg_char // !inE !cfRegE eqxx. -by case/andP=> _; apply: contraLR => /negbTE->; rewrite eq_sym neq0CG. -Qed. - -Lemma cfkerE chi : - chi \is a character -> - cfker chi = G :&: \bigcap_(i in irr_constt chi) cfker 'chi_i. -Proof. -move=> Nchi; rewrite cfkerEchar //; apply/setP=> x; rewrite !inE. -apply: andb_id2l => Gx; rewrite {1 2}[chi]cfun_sum_constt !sum_cfunE. -apply/eqP/bigcapP=> [Kx i Ci | Kx]; last first. - by apply: eq_bigr => i /Kx Kx_i; rewrite !cfunE cfker1. -rewrite cfkerEirr inE /= -(inj_eq (mulfI Ci)). -have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {i Ci} i _. -have chi_i_ge0: 0 <= '[chi, 'chi_i]. - by rewrite Cnat_ge0 ?Cnat_cfdot_char_irr. -by rewrite !cfunE normrM (normr_idP _) ?ler_wpmul2l ?char1_ge_norm ?irr_char. -Qed. - -Lemma TI_cfker_irr : \bigcap_i cfker 'chi[G]_i = [1]. -Proof. -apply/trivgP; apply: subset_trans cfaithful_reg; rewrite cfkerE ?cfReg_char //. -rewrite subsetI (bigcap_min 0) //=; last by rewrite cfker_irr0. -by apply/bigcapsP=> i _; rewrite bigcap_inf. -Qed. - -Lemma cfker_constt i chi : - chi \is a character -> i \in irr_constt chi -> - cfker chi \subset cfker 'chi[G]_i. -Proof. by move=> Nchi Ci; rewrite cfkerE ?subIset ?(bigcap_min i) ?orbT. Qed. - -Section KerLin. - -Variable xi : 'CF(G). -Hypothesis lin_xi : xi \is a linear_char. -Let Nxi: xi \is a character. Proof. by have [] := andP lin_xi. Qed. - -Lemma lin_char_der1 : G^`(1)%g \subset cfker xi. -Proof. -rewrite gen_subG /=; apply/subsetP=> _ /imset2P[x y Gx Gy ->]. -rewrite cfkerEchar // inE groupR //= !lin_charM ?lin_charV ?in_group //. -by rewrite mulrCA mulKf ?mulVf ?lin_char_neq0 // lin_char1. -Qed. - -Lemma cforder_lin_char : #[xi]%CF = exponent (G / cfker xi)%g. -Proof. -apply/eqP; rewrite eqn_dvd; apply/andP; split. - apply/dvdn_cforderP=> x Gx; rewrite -lin_charX // -cfQuoEker ?groupX //. - rewrite morphX ?(subsetP (cfker_norm xi)) //= expg_exponent ?mem_quotient //. - by rewrite cfQuo1 ?cfker_normal ?lin_char1. -have abGbar: abelian (G / cfker xi) := sub_der1_abelian lin_char_der1. -have [_ /morphimP[x Nx Gx ->] ->] := exponent_witness (abelian_nil abGbar). -rewrite order_dvdn -morphX //= coset_id cfkerEchar // !inE groupX //=. -by rewrite lin_charX ?lin_char1 // (dvdn_cforderP _ _ _). -Qed. - -Lemma cforder_lin_char_dvdG : #[xi]%CF %| #|G|. -Proof. -by rewrite cforder_lin_char (dvdn_trans (exponent_dvdn _)) ?dvdn_morphim. -Qed. - -Lemma cforder_lin_char_gt0 : (0 < #[xi]%CF)%N. -Proof. by rewrite cforder_lin_char exponent_gt0. Qed. - -End KerLin. - -End Kernel. - Section Coset. Variable (gT : finGroupType). @@ -2260,27 +2267,18 @@ Implicit Types G H : {group gT}. Lemma cfQuo_char G H (chi : 'CF(G)) : chi \is a character -> (chi / H)%CF \is a character. Proof. -move=> Nchi; case KchiH: (H \subset cfker chi); last first. +move=> Nchi; without loss kerH: / H \subset cfker chi. + move/contraNF=> IHchi; apply/wlog_neg=> N'chiH. suffices ->: (chi / H)%CF = (chi 1%g)%:A. by rewrite rpredZ_Cnat ?Cnat_char1 ?rpred1. - by apply/cfunP=> x; rewrite cfunE cfun1E mulr_natr cfunElock KchiH. -have sHG := subset_trans KchiH (cfker_sub _). -pose N := 'N_G(H); pose phi := 'Res[N] chi. -have nsHN: H <| N by [rewrite normal_subnorm]; have [sHN nHN] := andP nsHN. -have{Nchi} Nphi: phi \is a character by apply: cfRes_char. -have KphiH: H \subset cfker phi. - apply/subsetP=> x Hx; have [Kx Nx] := (subsetP KchiH x Hx, subsetP sHN x Hx). - by rewrite cfkerEchar // inE Nx cfRes1 cfResE ?subsetIl //= cfker1. -pose psi := 'Res[(N / H)%g] (chi / H)%CF. -have ->: (chi / H)%CF = 'Res psi by rewrite /psi quotientInorm !cfRes_id. -have{KchiH} ->: psi = (phi / H)%CF. - apply/cfun_inP => _ /morphimP[x nHx Nx ->]; have [Gx _] := setIP Nx. - rewrite cfResE ?mem_quotient ?quotientS ?subsetIl // cfQuoEnorm //. - by rewrite cfQuoE ?cfResE ?subsetIl. -have [rG Dphi] := char_reprP Nphi; rewrite {phi Nphi}Dphi cfker_repr in KphiH *. -apply/cfRes_char/char_reprP; exists (Representation (quo_repr KphiH nHN)). -apply/cfun_inP=> _ /morphimP[x nHx Nx ->]; rewrite cfQuoE ?cfker_repr //=. -by rewrite !cfunE Nx quo_repr_coset ?mem_quotient. + by apply/cfunP=> x; rewrite cfunE cfun1E mulr_natr cfunElock IHchi. +without loss nsHG: G chi Nchi kerH / H <| G. + move=> IHchi; have nsHN := normalSG (subset_trans kerH (cfker_sub chi)). + by rewrite cfQuoInorm ?(cfRes_char, IHchi) ?sub_cfker_Res // ?normal_sub. +have [rG Dchi] := char_reprP Nchi; rewrite Dchi cfker_repr in kerH. +apply/char_reprP; exists (Representation (quo_repr kerH (normal_norm nsHG))). +apply/cfun_inP=> _ /morphimP[x nHx Gx ->]; rewrite Dchi cfQuoE ?cfker_repr //=. +by rewrite !cfunE Gx quo_repr_coset ?mem_quotient. Qed. Lemma cfQuo_lin_char G H (chi : 'CF(G)) : @@ -2295,8 +2293,26 @@ Lemma cfMod_lin_char G H (chi : 'CF(G / H)) : chi \is a linear_char -> (chi %% H)%CF \is a linear_char. Proof. exact: cfMorph_lin_char. Qed. +Lemma cfMod_charE G H (chi : 'CF(G / H)) : + H <| G -> (chi %% H \is a character)%CF = (chi \is a character). +Proof. by case/andP=> _; apply: cfMorph_charE. Qed. + +Lemma cfMod_lin_charE G H (chi : 'CF(G / H)) : + H <| G -> (chi %% H \is a linear_char)%CF = (chi \is a linear_char). +Proof. by case/andP=> _; apply: cfMorph_lin_charE. Qed. + +Lemma cfQuo_charE G H (chi : 'CF(G)) : + H <| G -> H \subset cfker chi -> + (chi / H \is a character)%CF = (chi \is a character). +Proof. by move=> nsHG kerH; rewrite -cfMod_charE ?cfQuoK. Qed. + +Lemma cfQuo_lin_charE G H (chi : 'CF(G)) : + H <| G -> H \subset cfker chi -> + (chi / H \is a linear_char)%CF = (chi \is a linear_char). +Proof. by move=> nsHG kerH; rewrite -cfMod_lin_charE ?cfQuoK. Qed. + Lemma cfMod_irr G H chi : - H <| G -> chi \in irr (G / H) -> (chi %% H)%CF \in irr G. + H <| G -> (chi %% H \in irr G)%CF = (chi \in irr (G / H)). Proof. by case/andP=> _; apply: cfMorph_irr. Qed. Definition mod_Iirr G H i := cfIirr ('chi[G / H]_i %% H)%CF. @@ -2312,16 +2328,9 @@ Lemma mod_Iirr_eq0 G H i : Proof. by case/andP=> _ /morph_Iirr_eq0->. Qed. Lemma cfQuo_irr G H chi : - H <| G -> H \subset cfker chi -> chi \in irr G -> - (chi / H)%CF \in irr (G / H). -Proof. -move=> nsHG sHK /irr_reprP[rG irrG Dchi]; have [sHG nHG] := andP nsHG. -have sHKr: H \subset rker rG by rewrite -cfker_repr -Dchi. -apply/irr_reprP; exists (Representation (quo_repr sHKr nHG)). - exact/quo_mx_irr. -apply/cfun_inP=> _ /morphimP[x Nx Gx ->]. -by rewrite cfQuoE //= Dchi !cfunE Gx quo_repr_coset ?mem_quotient. -Qed. + H <| G -> H \subset cfker chi -> + ((chi / H)%CF \in irr (G / H)) = (chi \in irr G). +Proof. by move=> nsHG kerH; rewrite -cfMod_irr ?cfQuoK. Qed. Definition quo_Iirr G H i := cfIirr ('chi[G]_i / H)%CF. @@ -2359,7 +2368,7 @@ Qed. Lemma mod_Iirr_bij H G : H <| G -> {on [pred i | H \subset cfker 'chi_i], bijective (@mod_Iirr G H)}. Proof. -by exists (quo_Iirr H) => [i _ | i]; [exact: mod_IirrK | exact: quo_IirrK]. +by exists (quo_Iirr H) => [i _ | i]; [apply: mod_IirrK | apply: quo_IirrK]. Qed. Lemma sum_norm_irr_quo H G x : @@ -2394,7 +2403,7 @@ Qed. End Coset. -Section Derive. +Section DerivedGroup. Variable gT : finGroupType. Implicit Types G H : {group gT}. @@ -2405,7 +2414,7 @@ Proof. apply/idP/idP=> [|sG'K]; first by apply: lin_char_der1. have nsG'G: G^`(1) <| G := der_normal 1 G. rewrite qualifE irr_char -[i](quo_IirrK nsG'G) // mod_IirrE //=. -by rewrite cfModE // morph1 lin_char1 //; exact/char_abelianP/der_abelian. +by rewrite cfModE // morph1 lin_char1 //; apply/char_abelianP/der_abelian. Qed. Lemma subGcfker G i : (G \subset cfker 'chi[G]_i) = (i == 0). @@ -2447,7 +2456,7 @@ by apply: eq_card => i; rewrite !inE mod_IirrE ?cfker_mod. (* Alternative: use the equivalent result in modular representation theory transitivity #|@socle_of_Iirr _ G @^-1: linear_irr _|; last first. rewrite (on_card_preimset (socle_of_Iirr_bij _)). - by rewrite card_linear_irr ?algC'G; last exact: groupC. + by rewrite card_linear_irr ?algC'G; last apply: groupC. by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. *) Qed. @@ -2466,7 +2475,7 @@ Qed. (* A combinatorial group isommorphic to the linear characters. *) Lemma lin_char_group G : - {linG : finGroupType & {cF : linG -> 'CF(G) | + {linG : finGroupType & {cF : linG -> 'CF(G) | [/\ injective cF, #|linG| = #|G : G^`(1)|, forall u, cF u \is a linear_char & forall phi, phi \is a linear_char -> exists u, phi = cF u] @@ -2542,7 +2551,7 @@ rewrite (bigID (fun i => H \subset cfker 'chi[G]_i)) //= addrC addKr. by apply: sumr_ge0 => i _; rewrite normCK mul_conjC_ge0. Qed. -End Derive. +End DerivedGroup. Implicit Arguments irr_prime_injP [gT G i]. @@ -2789,7 +2798,7 @@ have [-> | nz_chi] := eqVneq chi 0. by apply/subsetP=> x /setIdP[Gx _]; rewrite inE Gx /= !cfunE. have [xi Lxi def_chi] := cfcenter_Res chi. set Z := ('Z(_))%CF in xi Lxi def_chi *. -have sZG: Z \subset G by exact: cfcenter_sub. +have sZG: Z \subset G by apply: cfcenter_sub. have ->: cfker chi = cfker xi. rewrite -(setIidPr (normal_sub (cfker_center_normal _))) -/Z. rewrite !cfkerEchar // ?lin_charW //= -/Z. @@ -2797,7 +2806,7 @@ have ->: cfker chi = cfker xi. rewrite (subsetP sZG) //= -!(cfResE chi sZG) ?group1 // def_chi !cfunE. by rewrite (inj_eq (mulfI _)) ?char1_eq0. have: abelian (Z / cfker xi) by rewrite sub_der1_abelian ?lin_char_der1. -have [rG irrG ->] := irr_reprP _ (lin_char_irr Lxi); rewrite cfker_repr. +have /irr_reprP[rG irrG ->] := lin_char_irr Lxi; rewrite cfker_repr. apply: mx_faithful_irr_abelian_cyclic (kquo_mx_faithful rG) _. exact/quo_mx_irr. Qed. @@ -2824,7 +2833,7 @@ apply/subsetP=> _ /setIP[/morphimP[x /= _ Gx ->] cGx]; rewrite mem_quotient //=. rewrite -irrRepr cfker_repr cfcenter_repr inE Gx in cGx *. apply: mx_abs_irr_cent_scalar 'Chi_i _ _ _. by apply: groupC; apply: socle_irr. -have nKG: G \subset 'N(rker 'Chi_i) by exact: rker_norm. +have nKG: G \subset 'N(rker 'Chi_i) by apply: rker_norm. (* GG -- locking here is critical to prevent Coq kernel divergence. *) apply/centgmxP=> y Gy; rewrite [eq]lock -2?(quo_repr_coset (subxx _) nKG) //. move: (quo_repr _ _) => rG; rewrite -2?repr_mxM ?mem_quotient // -lock. @@ -2915,10 +2924,10 @@ Lemma pgroup_cyclic_faithful (p : nat) : p.-group G -> cyclic 'Z(G) -> exists i, cfaithful 'chi[G]_i. Proof. pose Z := 'Ohm_1('Z(G)) => pG cycZG; have nilG := pgroup_nil pG. -have [-> | ntG] := eqsVneq G [1]; first by exists 0; exact: cfker_sub. +have [-> | ntG] := eqsVneq G [1]; first by exists 0; apply: cfker_sub. have{pG} [[p_pr _ _] pZ] := (pgroup_pdiv pG ntG, pgroupS (center_sub G) pG). have ntZ: 'Z(G) != [1] by rewrite center_nil_eq1. -have{pZ} oZ: #|Z| = p by exact: Ohm1_cyclic_pgroup_prime. +have{pZ} oZ: #|Z| = p by apply: Ohm1_cyclic_pgroup_prime. apply/existsP; apply: contraR ntZ; rewrite negb_exists => /forallP-not_ffulG. rewrite -Ohm1_eq1 -subG1 /= -/Z -(TI_cfker_irr G); apply/bigcapsP=> i _. rewrite prime_meetG ?oZ // setIC meet_Ohm1 // meet_center_nil ?cfker_normal //. @@ -2973,7 +2982,7 @@ move=> sHG Nchi nzchi; rewrite !cfker_nzcharE ?cfInd_char ?cfInd_eq0 //. apply/setP=> x; rewrite inE cfIndE // (can2_eq (mulVKf _) (mulKf _)) ?neq0CG //. rewrite cfInd1 // mulrA -natrM Lagrange // mulr_natl -sumr_const. apply/eqP/bigcapP=> [/normC_sum_upper ker_chiG_x y Gy | ker_chiG_x]. - by rewrite mem_conjg inE ker_chiG_x ?groupV // => z _; exact: char1_ge_norm. + by rewrite mem_conjg inE ker_chiG_x ?groupV // => z _; apply: char1_ge_norm. by apply: eq_bigr => y /groupVr/ker_chiG_x; rewrite mem_conjgV inE => /eqP. Qed. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 32eeabb..3b3d894 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -1,25 +1,23 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg poly finalg zmodp cyclic vector ssrnum matrix vector. -From mathcomp.solvable -Require Import commutator center pgroup sylow. -From mathcomp.field -Require Import falgebra algC algnum. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg poly finset. +From mathcomp +Require Import fingroup morphism perm automorphism quotient finalg action. +From mathcomp +Require Import gproduct zmodp commutator cyclic center pgroup sylow. +From mathcomp +Require Import matrix vector falgebra ssrnum algC algnum. (******************************************************************************) (* This file contains the basic theory of class functions: *) (* 'CF(G) == the type of class functions on G : {group gT}, i.e., *) (* which map gT to the type algC of complex algebraics, *) (* have support in G, and are constant on each conjugacy *) -(* class of G. 'CF(G) implements the algebraType interface *) -(* of finite-dimensional F-algebras. *) +(* class of G. 'CF(G) implements the FalgType interface of *) +(* finite-dimensional F-algebras. *) (* The identity 1 : 'CF(G) is the indicator function of G, *) (* and (later) the principal character. *) (* --> The %CF scope (cfun_scope) is bound to the 'CF(_) types. *) @@ -28,7 +26,7 @@ Require Import falgebra algC algnum. (* phi x == the image of x : gT under phi : 'CF(G). *) (* #[phi]%CF == the multiplicative order of phi : 'CF(G). *) (* cfker phi == the kernel of phi : 'CF(G); note that cfker phi <| G. *) -(* cfaithful phi <=> phi : 'CF(G) is faithful (has a trivial kernel). *) +(* cfaithful phi <=> phi : 'CF(G) is faithful (has a trivial kernel). *) (* '1_A == the indicator function of A as a function of 'CF(G). *) (* (Provided A <| G; G is determined by the context.) *) (* phi^*%CF == the function conjugate to phi : 'CF(G). *) @@ -52,10 +50,10 @@ Require Import falgebra algC algnum. (* whose range is contained in CR. *) (* cfReal phi <=> phi is real, i.e., phi^* == phi. *) (* cfAut_closed u S <-> S : seq 'CF(G) is closed under conjugation by u. *) -(* conjC_closed S <-> S : seq 'CF(G) is closed under complex conjugation. *) +(* cfConjC_closed S <-> S : seq 'CF(G) is closed under complex conjugation. *) (* conjC_subset S1 S2 <-> S1 : seq 'CF(G) represents a subset of S2 closed *) (* under complex conjugation. *) -(* := [/\ uniq S1, {subset S1 <= S2} & conjC_closed S1]. *) +(* := [/\ uniq S1, {subset S1 <= S2} & cfConjC_closed S1]. *) (* 'Res[H] phi == the restriction of phi : 'CF(G) to a function of 'CF(H) *) (* 'Res[H, G] phi 'Res[H] phi x = phi x if x \in H (when H \subset G), *) (* 'Res phi 'Res[H] phi x = 0 if x \notin H. The syntax variants *) @@ -88,7 +86,7 @@ Require Import falgebra algC algnum. (* cfBigdprodi defG phi == for phi : 'CF(A i) s.t. P i, the class function *) (* of 'CF(G) that maps x to phi x_i, where x_i is the *) (* (A i)-component of x : G. *) -(* cfBigdprodi defG phi == for phi : forall i, 'CF(A i), the class function *) +(* cfBigdprod defG phi == for phi : forall i, 'CF(A i), the class function *) (* of 'CF(G) that maps x to \prod_(i | P i) phi i x_i, *) (* where x_i is the (A i)-component of x : G. *) (******************************************************************************) @@ -181,7 +179,7 @@ Lemma cfunP phi psi : phi =1 psi <-> phi = psi. Proof. by split=> [/ffunP/val_inj | ->]. Qed. Lemma cfun0gen phi x : x \notin G -> phi x = 0. -Proof. by case: phi => f fP; case: (andP fP) => _ /supportP; exact. Qed. +Proof. by case: phi => f fP; case: (andP fP) => _ /supportP; apply. Qed. Lemma cfun_in_genP phi psi : {in G, phi =1 psi} -> phi = psi. Proof. @@ -335,8 +333,8 @@ Proof. by apply/cfunP=> x; rewrite !cfunE rmorphM. Qed. Lemma cfAut_is_rmorphism : rmorphism cfAut. Proof. -by do 2?split=> [phi psi|]; last exact: cfAut_cfun1i; - apply/cfunP=> x; rewrite !cfunE (rmorphB, rmorphM). +by do 2?split=> [phi psi|]; apply/cfunP=> x; + rewrite ?cfAut_cfun1i // !cfunE (rmorphB, rmorphM). Qed. Canonical cfAut_additive := Additive cfAut_is_rmorphism. Canonical cfAut_rmorphism := RMorphism cfAut_is_rmorphism. @@ -409,7 +407,7 @@ Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. Notation "1" := (@GRing.one (cfun_ringType _)) (only parsing) : cfun_scope. Notation "phi ^*" := (cfAut conjC phi) : cfun_scope. -Notation conjC_closed := (cfAut_closed conjC). +Notation cfConjC_closed := (cfAut_closed conjC). Prenex Implicits cfReal. (* Workaround for overeager projection reduction. *) Notation eqcfP := (@eqP (cfun_eqType _) _ _) (only parsing). @@ -482,7 +480,7 @@ Lemma cfunJ phi x y : y \in G -> phi (x ^ y) = phi x. Proof. by rewrite -{1}(genGid G) => /(cfunJgen phi)->. Qed. Lemma cfun_repr phi x : phi (repr (x ^: G)) = phi x. -Proof. by have [y Gy ->] := repr_class G x; exact: cfunJ. Qed. +Proof. by have [y Gy ->] := repr_class G x; apply: cfunJ. Qed. Lemma cfun_inP phi psi : {in G, phi =1 psi} -> phi = psi. Proof. by rewrite -{1}genGid => /cfun_in_genP. Qed. @@ -500,7 +498,7 @@ Lemma eq_mul_cfuni A phi : A <| G -> {in A, phi * '1_A =1 phi}. Proof. by move=> nsAG x Ax; rewrite cfunE cfuniE // Ax mulr1. Qed. Lemma eq_cfuni A : A <| G -> {in A, '1_A =1 (1 : 'CF(G))}. -Proof. by rewrite -['1_A]mul1r; exact: eq_mul_cfuni. Qed. +Proof. by rewrite -['1_A]mul1r; apply: eq_mul_cfuni. Qed. Lemma cfuniG : '1_G = 1. Proof. by rewrite -[G in '1_G]genGid. Qed. @@ -556,12 +554,12 @@ apply/cfun_inP=> x Gx; rewrite sum_cfunE (bigD1 (x ^: G)) ?mem_classes //=. rewrite cfunE cfun_repr cfun_classE Gx class_refl mulr1. rewrite big1 ?addr0 // => _ /andP[/imsetP[y Gy ->]]; apply: contraNeq. rewrite cfunE cfun_repr cfun_classE Gy mulf_eq0 => /norP[_]. -by rewrite pnatr_eq0 -lt0n lt0b => /class_transr->. +by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->. Qed. Implicit Arguments cfun_onP [A phi]. Lemma cfun_on0 A phi x : phi \in 'CF(G, A) -> x \notin A -> phi x = 0. -Proof. by move/cfun_onP; exact. Qed. +Proof. by move/cfun_onP; apply. Qed. Lemma sum_by_classes (R : ringType) (F : gT -> R) : {in G &, forall g h, F (g ^ h) = F g} -> @@ -571,7 +569,7 @@ move=> FJ; rewrite {1}(partition_big _ _ ((@mem_classes gT)^~ G)) /=. apply: eq_bigr => _ /imsetP[x Gx ->]; have [y Gy ->] := repr_class G x. rewrite mulr_natl -sumr_const FJ {y Gy}//; apply/esym/eq_big=> y /=. apply/idP/andP=> [xGy | [Gy /eqP<-]]; last exact: class_refl. - by rewrite (class_transr xGy) (subsetP (class_subG Gx (subxx _))). + by rewrite (class_eqP xGy) (subsetP (class_subG Gx (subxx _))). by case/imsetP=> z Gz ->; rewrite FJ. Qed. @@ -587,7 +585,7 @@ apply: contraNeq; rewrite b_i !cfunE mulf_eq0 => /norP[_]. rewrite -(inj_eq enum_val_inj). have /setIdP[/imsetP[x _ ->] _] := enum_valP i; rewrite cfun_repr. have /setIdP[/imsetP[y Gy ->] _] := enum_valP j; rewrite cfun_classE Gy. -by rewrite pnatr_eq0 -lt0n lt0b => /class_transr->. +by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->. Qed. Lemma dim_cfun : \dim 'CF(G) = #|classes G|. @@ -895,7 +893,7 @@ Proof. by rewrite -cfdot_conjC cfConjCK. Qed. Lemma cfnorm_ge0 phi : 0 <= '[phi]. Proof. -by rewrite mulr_ge0 ?invr_ge0 ?ler0n ?sumr_ge0 // => x _; exact: mul_conjC_ge0. +by rewrite mulr_ge0 ?invr_ge0 ?ler0n ?sumr_ge0 // => x _; apply: mul_conjC_ge0. Qed. Lemma cfnorm_eq0 phi : ('[phi] == 0) = (phi == 0). @@ -903,7 +901,7 @@ Proof. apply/idP/eqP=> [|->]; last by rewrite cfdot0r. rewrite mulf_eq0 invr_eq0 (negbTE (neq0CG G)) /= => /eqP/psumr_eq0P phi0. apply/cfun_inP=> x Gx; apply/eqP; rewrite cfunE -mul_conjC_eq0. -by rewrite phi0 // => y _; exact: mul_conjC_ge0. +by rewrite phi0 // => y _; apply: mul_conjC_ge0. Qed. Lemma cfnorm_gt0 phi : ('[phi] > 0) = (phi != 0). @@ -995,7 +993,7 @@ Lemma orthogonal_cons phi R S : Proof. by rewrite /orthogonal /= andbT. Qed. Lemma orthoP phi psi : reflect ('[phi, psi] = 0) (orthogonal phi psi). -Proof. by rewrite /orthogonal /= !andbT; exact: eqP. Qed. +Proof. by rewrite /orthogonal /= !andbT; apply: eqP. Qed. Lemma orthogonalP S R : reflect {in S & R, forall phi psi, '[phi, psi] = 0} (orthogonal S R). @@ -1028,7 +1026,7 @@ Lemma eq_orthogonal R1 R2 S1 S2 : R1 =i R2 -> S1 =i S2 -> orthogonal R1 S1 = orthogonal R2 S2. Proof. move=> eqR eqS; rewrite [orthogonal _ _](eq_all_r eqR). -by apply: eq_all => psi /=; exact: eq_all_r. +by apply: eq_all => psi /=; apply: eq_all_r. Qed. Lemma orthogonal_catl R1 R2 S : @@ -1083,7 +1081,7 @@ Qed. Lemma orthogonal_oppr S R : orthogonal S (map -%R R) = orthogonal S R. Proof. wlog suffices IH: S R / orthogonal S R -> orthogonal S (map -%R R). - apply/idP/idP=> /IH; rewrite ?mapK //; exact: opprK. + by apply/idP/idP=> /IH; rewrite ?mapK //; apply: opprK. move/orthogonalP=> oSR; apply/orthogonalP=> xi1 _ Sxi1 /mapP[xi2 Rxi2 ->]. by rewrite cfdotNr oSR ?oppr0. Qed. @@ -1104,7 +1102,7 @@ have [opS | not_opS] := allP; last first. by rewrite opS ?mem_head 1?mem_behead // (memPnC notSp). rewrite (contra (opS _)) /= ?cfnorm_eq0 //. apply: (iffP IH) => [] [uniqS oSS]; last first. - by split=> //; apply: sub_in2 oSS => psi Spsi; exact: mem_behead. + by split=> //; apply: sub_in2 oSS => psi Spsi; apply: mem_behead. split=> // psi xi; rewrite !inE => /predU1P[-> // | Spsi]. by case/predU1P=> [-> | /opS] /eqP. case/predU1P=> [-> _ | Sxi /oSS-> //]. @@ -1134,14 +1132,14 @@ Lemma sub_pairwise_orthogonal S1 S2 : Proof. move=> sS12 uniqS1 /pairwise_orthogonalP[/andP[notS2_0 _] oS2]. apply/pairwise_orthogonalP; rewrite /= (contra (sS12 0)) //. -by split=> //; exact: sub_in2 oS2. +by split=> //; apply: sub_in2 oS2. Qed. Lemma orthogonal_free S : pairwise_orthogonal S -> free S. Proof. case/pairwise_orthogonalP=> [/=/andP[notS0 uniqS] oSS]. rewrite -(in_tupleE S); apply/freeP => a aS0 i. -have S_i: S`_i \in S by exact: mem_nth. +have S_i: S`_i \in S by apply: mem_nth. have /eqP: '[S`_i, 0]_G = 0 := cfdot0r _. rewrite -{2}aS0 raddf_sum /= (bigD1 i) //= big1 => [|j neq_ji]; last 1 first. by rewrite cfdotZr oSS ?mulr0 ?mem_nth // eq_sym nth_uniq. @@ -1202,7 +1200,7 @@ Lemma sub_orthonormal S1 S2 : {subset S1 <= S2} -> uniq S1 -> orthonormal S2 -> orthonormal S1. Proof. move=> sS12 uniqS1 /orthonormalP[_ oS1]. -by apply/orthonormalP; split; last exact: sub_in2 sS12 _ _. +by apply/orthonormalP; split; last apply: sub_in2 sS12 _ _. Qed. Lemma orthonormal2P phi psi : @@ -1214,7 +1212,7 @@ by apply: (iffP and3P) => [] []; do 3!move/eqP->. Qed. Lemma conjC_pair_orthogonal S chi : - conjC_closed S -> ~~ has cfReal S -> pairwise_orthogonal S -> chi \in S -> + cfConjC_closed S -> ~~ has cfReal S -> pairwise_orthogonal S -> chi \in S -> pairwise_orthogonal (chi :: chi^*%CF). Proof. move=> ccS /hasPn nrS oSS Schi; apply: sub_pairwise_orthogonal oSS. @@ -1225,6 +1223,16 @@ Qed. Lemma cfdot_real_conjC phi psi : cfReal phi -> '[phi, psi^*]_G = '[phi, psi]^*. Proof. by rewrite -cfdot_conjC => /eqcfP->. Qed. +Lemma extend_cfConjC_subset S X phi : + cfConjC_closed S -> ~~ has cfReal S -> phi \in S -> phi \notin X -> + cfConjC_subset X S -> cfConjC_subset [:: phi, phi^* & X]%CF S. +Proof. +move=> ccS nrS Sphi X'phi [uniqX /allP-sXS ccX]. +split; last 1 [by apply/allP; rewrite /= Sphi ccS | apply/allP]; rewrite /= inE. + by rewrite negb_or X'phi eq_sym (hasPn nrS) // (contra (ccX _)) ?cfConjCK. +by rewrite cfConjCK !mem_head orbT; apply/allP=> xi Xxi; rewrite !inE ccX ?orbT. +Qed. + (* Note: other isometry lemmas, and the dot product lemmas for orthogonal *) (* and orthonormal sequences are in vcharacter, because we need the 'Z[S] *) (* notation for the isometry domains. Alternatively, this could be moved to *) @@ -1291,7 +1299,22 @@ Lemma sub_iso_to U1 U2 W1 W2 tau : {subset U2 <= U1} -> {subset W1 <= W2} -> {in U1, isometry tau, to W1} -> {in U2, isometry tau, to W2}. Proof. -by move=> sU sW [Itau Wtau]; split=> [|u /sU/Wtau/sW //]; exact: sub_in2 Itau. +by move=> sU sW [Itau Wtau]; split=> [|u /sU/Wtau/sW //]; apply: sub_in2 Itau. +Qed. + +Lemma isometry_of_free S f : + free S -> {in S &, isometry f} -> + {tau : {linear 'CF(L) -> 'CF(G)} | + {in S, tau =1 f} & {in <<S>>%VS &, isometry tau}}. +Proof. +move=> freeS If; have defS := free_span freeS. +have [tau /(_ freeS (size_map f S))Dtau] := linear_of_free S (map f S). +have{Dtau} Dtau: {in S, tau =1 f}. + by move=> _ /(nthP 0)[i ltiS <-]; rewrite -!(nth_map 0 0) ?Dtau. +exists tau => // _ _ /defS[a -> _] /defS[b -> _]. +rewrite !{1}linear_sum !{1}cfdot_suml; apply/eq_big_seq=> xi1 Sxi1. +rewrite !{1}cfdot_sumr; apply/eq_big_seq=> xi2 Sxi2. +by rewrite !linearZ /= !Dtau // !cfdotZl !cfdotZr If. Qed. Lemma isometry_of_cfnorm S tauS : @@ -1302,16 +1325,15 @@ Lemma isometry_of_cfnorm S tauS : Proof. move=> oS oT eq_nST; have freeS := orthogonal_free oS. have eq_sz: size tauS = size S by have:= congr1 size eq_nST; rewrite !size_map. -have [tau /(_ freeS eq_sz) defT] := linear_of_free S tauS. -rewrite -[S]/(tval (in_tuple S)). -exists tau => // u v /coord_span-> /coord_span->; rewrite !raddf_sum /=. +have [tau defT] := linear_of_free S tauS; rewrite -[S]/(tval (in_tuple S)). +exists tau => [|u v /coord_span-> /coord_span->]; rewrite ?raddf_sum ?defT //=. apply: eq_bigr => i _ /=; rewrite linearZ !cfdotZr !cfdot_suml; congr (_ * _). apply: eq_bigr => j _ /=; rewrite linearZ !cfdotZl; congr (_ * _). -rewrite -!((nth_map _ 0) tau) // defT; have [-> | neq_ji] := eqVneq j i. - by rewrite -!['[_]]((nth_map _ 0) cfnorm) ?eq_sz // eq_nST. +rewrite -!(nth_map 0 0 tau) ?{}defT //; have [-> | neq_ji] := eqVneq j i. + by rewrite -!['[_]](nth_map 0 0 cfnorm) ?eq_sz // eq_nST. have{oS} [/=/andP[_ uS] oS] := pairwise_orthogonalP oS. have{oT} [/=/andP[_ uT] oT] := pairwise_orthogonalP oT. -by rewrite oS ?oT ?mem_nth ? nth_uniq ?eq_sz. +by rewrite oS ?oT ?mem_nth ?nth_uniq ?eq_sz. Qed. Lemma isometry_raddf_inj U (tau : {additive 'CF(L) -> 'CF(G)}) : @@ -1628,7 +1650,7 @@ Local Notation "phi %% 'B'" := (cfMod phi) (at level 40) : cfun_scope. (* stronger results are needed. *) Lemma cfModE phi x : B <| G -> x \in G -> (phi %% B)%CF x = phi (coset B x). -Proof. by move/normal_norm=> nBG; exact: cfMorphE. Qed. +Proof. by move/normal_norm=> nBG; apply: cfMorphE. Qed. Lemma cfMod1 phi : (phi %% B)%CF 1%g = phi 1%g. Proof. exact: cfMorph1. Qed. @@ -2115,7 +2137,7 @@ apply: eq_bigr => _ /morphimP[x Dx Gx ->]. rewrite -(card_rcoset _ x) mulr_natl -sumr_const. apply/eq_big => [y | y /andP[Gy /eqP <-]]; last by rewrite !cfMorphE. rewrite mem_rcoset inE groupMr ?groupV // -mem_rcoset. -by apply: andb_id2l => /(subsetP sGD) Dy; exact: sameP eqP (rcoset_kerP f _ _). +by apply: andb_id2l => /(subsetP sGD) Dy; apply: sameP eqP (rcoset_kerP f _ _). Qed. Lemma cfIsom_iso rT G (R : {group rT}) (f : {morphism G >-> rT}) : @@ -2374,11 +2396,14 @@ Proof. exact: raddfZ_Cnat. Qed. Lemma cfAutZ_Cint z phi : z \in Cint -> (z *: phi)^u = z *: phi^u. Proof. exact: raddfZ_Cint. Qed. +Lemma cfAutK : cancel (@cfAut gT G u) (cfAut (algC_invaut_rmorphism u)). +Proof. by move=> phi; apply/cfunP=> x; rewrite !cfunE /= algC_autK. Qed. + +Lemma cfAutVK : cancel (cfAut (algC_invaut_rmorphism u)) (@cfAut gT G u). +Proof. by move=> phi; apply/cfunP=> x; rewrite !cfunE /= algC_invautK. Qed. + Lemma cfAut_inj : injective (@cfAut gT G u). -Proof. -move=> phi psi /cfunP eqfg; apply/cfunP=> x. -by have := eqfg x; rewrite !cfunE => /fmorph_inj. -Qed. +Proof. exact: can_inj cfAutK. Qed. Lemma cfAut_eq1 phi : (cfAut u phi == 1) = (phi == 1). Proof. by rewrite rmorph_eq1 //; apply: cfAut_inj. Qed. @@ -2460,6 +2485,8 @@ Proof. by rewrite rmorphM /= cfAutDprodl cfAutDprodr. Qed. End FieldAutomorphism. +Implicit Arguments cfAutK [[gT] [G]]. +Implicit Arguments cfAutVK [[gT] [G]]. Implicit Arguments cfAut_inj [gT G x1 x2]. Definition conj_cfRes := cfAutRes conjC. diff --git a/mathcomp/character/finfield.v b/mathcomp/character/finfield.v index 05b4a31..467449a 100644 --- a/mathcomp/character/finfield.v +++ b/mathcomp/character/finfield.v @@ -1,23 +1,14 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype tuple bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism action. -From mathcomp.algebra -Require Import ssralg poly polydiv finalg zmodp cyclic. -From mathcomp.algebra -Require Import matrix vector. -From mathcomp.solvable -Require Import center pgroup abelian. -From mathcomp.field -Require Import falgebra fieldext separable galois. -Require Import mxabelem. - -From mathcomp.algebra Require ssrnum ssrint. -From mathcomp.field Require algC cyclotomic. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype div. +From mathcomp +Require Import tuple bigop prime finset fingroup ssralg poly polydiv. +From mathcomp +Require Import morphism action finalg zmodp cyclic center pgroup abelian. +From mathcomp +Require Import matrix mxabelem vector falgebra fieldext separable galois. +Require ssrnum ssrint algC cyclotomic. (******************************************************************************) (* Additional constructions and results on finite fields. *) @@ -498,7 +489,7 @@ have [p p_pr charRp]: exists2 p, prime p & p \in [char R]. rewrite big_seq; elim/big_rec: _ => [|[p m] /= n]; first by rewrite oner_eq0. case/mem_prime_decomp=> p_pr _ _ IHn. elim: m => [|m IHm]; rewrite ?mul1n {IHn}// expnS -mulnA natrM. - by case/eqP/domR/orP=> //; exists p; last exact/andP. + by case/eqP/domR/orP=> //; exists p; last apply/andP. pose Rp := PrimeCharType charRp; pose L : {vspace Rp} := fullv. pose G := [set: {unit R}]; pose ofG : {unit R} -> Rp := val. pose projG (E : {vspace Rp}) := [preim ofG of E]. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 9a795e8..c6ddf44 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -1,20 +1,17 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg ssrnum zmodp cyclic matrix mxalgebra vector. -From mathcomp.solvable -Require Import center commutator gseries nilpotent pgroup sylow maximal. -From mathcomp.solvable +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq path choice div. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg ssrnum finset fingroup. +From mathcomp +Require Import morphism perm automorphism quotient action zmodp cyclic center. +From mathcomp +Require Import gproduct commutator gseries nilpotent pgroup sylow maximal. +From mathcomp Require Import frobenius. -From mathcomp.field -Require Import algC. -Require Import mxrepresentation classfun character. +From mathcomp +Require Import matrix mxalgebra mxrepresentation vector algC classfun character. Set Implicit Arguments. Unset Strict Implicit. @@ -105,7 +102,7 @@ Qed. (* Isaacs' 6.1.b *) Lemma cfConjgM L phi : G <| L -> {in L &, forall y z, phi ^ (y * z) = (phi ^ y) ^ z}%CF. -Proof. by case/andP=> _ /subsetP nGL; exact: sub_in2 (cfConjgMnorm phi). Qed. +Proof. by case/andP=> _ /subsetP nGL; apply: sub_in2 (cfConjgMnorm phi). Qed. Lemma cfConjgJ1 phi : (phi ^ 1)%CF = phi. Proof. by apply/cfunP=> x; rewrite cfConjgE ?group1 // invg1 conjg1. Qed. @@ -403,7 +400,7 @@ apply: (iffP imageP) => [[_ /rcosetsP[y Ay ->] ->] | [y Ay ->]]. by case: repr_rcosetP => z /setIdP[Az _]; exists (z * y)%g; rewrite ?groupM. without loss nHy: y Ay / y \in 'N(H). have [nHy | /cfConjgEout->] := boolP (y \in 'N(H)); first exact. - by move/(_ 1%g); rewrite !group1 !cfConjgJ1; exact. + by move/(_ 1%g); rewrite !group1 !cfConjgJ1; apply. exists ('I_A[phi] :* y); first by rewrite -rcosetE mem_imset. case: repr_rcosetP => z /setIP[_ /setIdP[nHz /eqP Tz]]. by rewrite cfConjgMnorm ?Tz. @@ -414,25 +411,25 @@ Proof. move=> xi; apply/cfclassP/cfclassP=> [[x /setIP[Gx _] ->] | [x Gx ->]]. by exists x. have [Nx | /cfConjgEout-> //] := boolP (x \in 'N(H)). - by exists x; first exact/setIP. + by exists x; first apply/setIP. by exists 1%g; rewrite ?group1 ?cfConjgJ1. Qed. Lemma cfclass_refl phi : phi \in (phi ^: G)%CF. Proof. by apply/cfclassP; exists 1%g => //; rewrite cfConjgJ1. Qed. -Lemma cfclass_transl phi psi : +Lemma cfclass_transr phi psi : (psi \in phi ^: G)%CF -> (phi ^: G =i psi ^: G)%CF. Proof. rewrite -cfclassInorm; case/cfclassP=> x Gx -> xi; rewrite -!cfclassInorm. -have nHN: {subset 'N_G(H) <= 'N(H)} by apply/subsetP; exact: subsetIr. +have nHN: {subset 'N_G(H) <= 'N(H)} by apply/subsetP; apply: subsetIr. apply/cfclassP/cfclassP=> [[y Gy ->] | [y Gy ->]]. by exists (x^-1 * y)%g; rewrite -?cfConjgMnorm ?groupM ?groupV ?nHN // mulKVg. by exists (x * y)%g; rewrite -?cfConjgMnorm ?groupM ?nHN. Qed. Lemma cfclass_sym phi psi : (psi \in phi ^: G)%CF = (phi \in psi ^: G)%CF. -Proof. by apply/idP/idP=> /cfclass_transl <-; exact: cfclass_refl. Qed. +Proof. by apply/idP/idP=> /cfclass_transr <-; apply: cfclass_refl. Qed. Lemma cfclass_uniq phi : H <| G -> uniq (phi ^: G)%CF. Proof. @@ -440,7 +437,7 @@ move=> nsHG; rewrite map_inj_in_uniq ?enum_uniq // => Ty Tz; rewrite !mem_enum. move=> {Ty}/rcosetsP[y Gy ->] {Tz}/rcosetsP[z Gz ->] /eqP. case: repr_rcosetP => u Iphi_u; case: repr_rcosetP => v Iphi_v. have [[Gu _] [Gv _]] := (setIdP Iphi_u, setIdP Iphi_v). -rewrite cfConjg_eqE ?groupM // => /rcoset_transl. +rewrite cfConjg_eqE ?groupM // => /rcoset_eqP. by rewrite !rcosetM (rcoset_id Iphi_v) (rcoset_id Iphi_u). Qed. @@ -466,7 +463,7 @@ Lemma eq_cfclass_IirrE i j : (cfclass_Iirr G j == cfclass_Iirr G i) = (j \in cfclass_Iirr G i). Proof. apply/eqP/idP=> [<- | iGj]; first by rewrite cfclass_IirrE cfclass_refl. -by apply/setP=> k; rewrite !cfclass_IirrE in iGj *; apply/esym/cfclass_transl. +by apply/setP=> k; rewrite !cfclass_IirrE in iGj *; apply/esym/cfclass_transr. Qed. Lemma im_cfclass_Iirr i : @@ -1581,7 +1578,7 @@ apply: contraR => notKx; apply/cards1P; exists 1%g; apply/esym/eqP. rewrite eqEsubset !(sub1set, inE) classes1 /= conjs1g eqxx /=. apply/subsetP=> _ /setIP[/imsetP[y Ky ->] /afix1P /= cyKx]. have /imsetP[z Kz def_yx]: y ^ x \in y ^: K. - by rewrite -cyKx; apply: mem_imset; exact: class_refl. + by rewrite -cyKx; apply: mem_imset; apply: class_refl. rewrite inE classG_eq1; apply: contraR notKx => nty. rewrite -(groupMr x (groupVr Kz)). apply: (subsetP (regK y _)); first exact/setD1P. @@ -1606,7 +1603,7 @@ Proof. have [_ _ nsKG _] := Frobenius_kerP frobGK; have [sKG nKG] := andP nsKG. apply: (iffP idP) => [not_chijK1 | [i nzi ->]]; last first. by rewrite cfker_Ind_irr ?sub_gcore // subGcfker. -have /neq0_has_constt[i chijKi]: 'Res[K] 'chi_j != 0 by exact: Res_irr_neq0. +have /neq0_has_constt[i chijKi]: 'Res[K] 'chi_j != 0 by apply: Res_irr_neq0. have nz_i: i != 0. by apply: contraNneq not_chijK1 => i0; rewrite constt0_Res_cfker // -i0. have /irrP[k def_chik] := irr_induced_Frobenius_ker nz_i. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 14ae4fc..1770335 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -1,19 +1,18 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg poly polydiv finalg zmodp cyclic matrix mxalgebra mxpoly. -From mathcomp.solvable -Require Import commutator center pgroup sylow gseries nilpotent abelian. -From mathcomp.algebra -Require Import ssrnum ssrint polydiv rat matrix mxalgebra intdiv mxpoly vector. -From mathcomp.field -Require Import fieldext separable galois algC cyclotomic algnum falgebra. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg poly finset. +From mathcomp +Require Import fingroup morphism perm automorphism quotient action finalg zmodp. +From mathcomp +Require Import commutator cyclic center pgroup sylow gseries nilpotent abelian. +From mathcomp +Require Import ssrnum ssrint polydiv rat matrix mxalgebra intdiv mxpoly. +From mathcomp +Require Import vector falgebra fieldext separable galois algC cyclotomic algnum. +From mathcomp Require Import mxrepresentation classfun character. (******************************************************************************) @@ -31,7 +30,7 @@ Require Import mxrepresentation classfun character. (* gring_classM_coef_set A B z == the set of all (x, y) in setX A B such *) (* that x * y = z; if A and B are respectively the ith and jth *) (* conjugacy class of G, and z is in the kth conjugacy class, then *) -(* gring_classM_coef i j k is exactly the cadinal of this set. *) +(* gring_classM_coef i j k is exactly the cardinal of this set. *) (* 'omega_i[A] == the mode of 'chi[G]_i on (A \in 'Z(group_ring algC G))%MS, *) (* i.e., the z such that gring_op 'Chi_i A = z%:M. *) (******************************************************************************) @@ -73,7 +72,7 @@ exists (SplittingFieldType _ _ Qn_ax). apply: separable_Xn_sub_1; rewrite -(fmorph_eq0 QnC) rmorph_nat. by rewrite pnatr_eq0 -lt0n cardG_gt0. exists QnC => [// nuQn|]. - by exact: (extend_algC_subfield_aut QnC [rmorphism of nuQn]). + by apply: (extend_algC_subfield_aut QnC [rmorphism of nuQn]). rewrite span_seq1 in genQn. exists w => // hT H phi Nphi x x_dv_n. apply: sig_eqW; have [rH ->] := char_reprP Nphi. @@ -146,7 +145,7 @@ rewrite scaler_sumr; apply: eq_bigr => g Kk_g; rewrite scaler_nat. rewrite (set_gring_classM_coef _ _ Kk_g) -sumr_const; apply: eq_big => [] [x y]. rewrite !inE /= dKi dKj /h1 /h2 /=; apply: andb_id2r => /eqP ->. have /imsetP[zk Gzk dKk] := enum_valP k; rewrite dKk in Kk_g. - by rewrite (class_transr Kk_g) -dKk enum_valK_in eqxx andbT. + by rewrite (class_eqP Kk_g) -dKk enum_valK_in eqxx andbT. by rewrite /h2 /= => /andP[_ /eqP->]. Qed. @@ -179,7 +178,7 @@ exact/unity_rootP. Qed. Lemma Aint_irr i x : 'chi[G]_i x \in Aint. -Proof. by apply: Aint_char; exact: irr_char. Qed. +Proof. exact/Aint_char/irr_char. Qed. Local Notation R_G := (group_ring algCfield G). Local Notation a := gring_classM_coef. @@ -240,9 +239,9 @@ Qed. Lemma Aint_gring_mode_class_sum k : 'omega_i['K_k] \in Aint. Proof. move: k; pose X := [tuple 'omega_i['K_k] | k < #|classes G| ]. -have memX k: 'omega_i['K_k] \in X by apply: map_f; exact: mem_enum. +have memX k: 'omega_i['K_k] \in X by apply: image_f. have S_P := Cint_spanP X; set S := Cint_span X in S_P. -have S_X: {subset X <= S} by exact: mem_Cint_span. +have S_X: {subset X <= S} by apply: mem_Cint_span. have S_1: 1 \in S. apply: S_X; apply/codomP; exists (enum_rank_in (classes1 G) 1%g). rewrite (@gring_mode_class_sum_eq _ 1%g) ?enum_rankK_in ?classes1 //. @@ -383,7 +382,7 @@ rewrite ltnS => leGn piGle2; have [simpleG | ] := boolP (simple G); last first. exact: solvable1. rewrite [N == G]eqEproper sNG eqbF_neg !negbK => ltNG /and3P[grN]. case/isgroupP: grN => {N}N -> in sNG ltNG *; rewrite /= genGid => ntN nNG. - have nsNG: N <| G by exact/andP. + have nsNG: N <| G by apply/andP. have dv_le_pi m: (m %| #|G| -> size (primes m) <= 2)%N. move=> m_dv_G; apply: leq_trans piGle2. by rewrite uniq_leq_size ?primes_uniq //; apply: pi_of_dvd. @@ -498,7 +497,7 @@ move=> a /= Kg1 Kg2 Kg; rewrite mulrAC; apply: canRL (mulfK (neq0CG G)) _. transitivity (\sum_j (#|G| * a j)%:R *+ (j == k) : algC). by rewrite (bigD1 k) //= eqxx -natrM mulnC big1 ?addr0 // => j /negPf->. have defK (j : 'I_#|classes G|) x: x \in enum_val j -> enum_val j = x ^: G. - by have /imsetP[y Gy ->] := enum_valP j => /class_transr. + by have /imsetP[y Gy ->] := enum_valP j => /class_eqP. have Gg: g \in G. by case/imsetP: (enum_valP k) Kg => x Gx -> /imsetP[y Gy ->]; apply: groupJ. transitivity (\sum_j \sum_i 'omega_i['K_j] * 'chi_i 1%g * ('chi_i g)^* *+ a j). @@ -680,7 +679,7 @@ have{Qpi1} Zpi1: pi1 \in Cint. have{pi1 Zpi1} pi2_ge1: 1 <= pi2. have ->: pi2 = `|pi1| ^+ 2. by rewrite (big_morph Num.norm (@normrM _) (@normr1 _)) -prodrXl. - by rewrite Cint_normK // sqr_Cint_ge1 //; exact/prodf_neq0. + by rewrite Cint_normK // sqr_Cint_ge1 //; apply/prodf_neq0. have Sgt0: (#|S| > 0)%N by rewrite (cardD1 g) [g \in S]Sg. rewrite -mulr_natr -ler_pdivl_mulr ?ltr0n //. have n2chi_ge0 s: s \in S -> 0 <= `|chi s| ^+ 2 by rewrite exprn_ge0 ?normr_ge0. @@ -693,7 +692,7 @@ Theorem nonlinear_irr_vanish gT (G : {group gT}) i : 'chi[G]_i 1%g > 1 -> exists2 x, x \in G & 'chi_i x = 0. Proof. move=> chi1gt1; apply/exists_eq_inP; apply: contraFT (ltr_geF chi1gt1). -rewrite negb_exists_in => /forall_inP nz_chi. +rewrite negb_exists_in => /forall_inP-nz_chi. rewrite -(norm_Cnat (Cnat_irr1 i)) -(@expr_le1 _ 2) ?normr_ge0 //. rewrite -(ler_add2r (#|G|%:R * '['chi_i])) {1}cfnorm_irr mulr1. rewrite (cfnormE (cfun_onG _)) mulVKf ?neq0CG // (big_setD1 1%g) //=. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 377cb72..8685796 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -1,18 +1,15 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime finset. -From mathcomp.fingroup +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg poly finset. +From mathcomp Require Import fingroup morphism perm automorphism quotient gproduct action. -From mathcomp.algebra -Require Import ssralg poly finalg zmodp cyclic matrix mxalgebra. -From mathcomp.solvable -Require Import commutator center pgroup gseries nilpotent. -From mathcomp.solvable -Require Import sylow maximal abelian. -Require Import mxrepresentation. +From mathcomp +Require Import finalg zmodp commutator cyclic center pgroup gseries nilpotent. +From mathcomp +Require Import sylow maximal abelian matrix mxalgebra mxrepresentation. (******************************************************************************) (* This file completes the theory developed in mxrepresentation.v with the *) @@ -145,7 +142,7 @@ Proof. by rewrite inE. Qed. Fact rowg_group_set m A : group_set (@rowg m A). Proof. -by apply/group_setP; split=> [|u v]; rewrite !inE ?sub0mx //; exact: addmx_sub. +by apply/group_setP; split=> [|u v]; rewrite !inE ?sub0mx //; apply: addmx_sub. Qed. Canonical rowg_group m A := Group (@rowg_group_set m A). @@ -157,7 +154,7 @@ Lemma rowgS m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) : Proof. apply/subsetP/idP=> sAB => [| u]. by apply/row_subP=> i; have:= sAB (row i A); rewrite !inE row_sub => ->. -by rewrite !inE => suA; exact: submx_trans sAB. +by rewrite !inE => suA; apply: submx_trans sAB. Qed. Lemma eq_rowg m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) : @@ -214,8 +211,8 @@ Proof. by apply/eqP; rewrite -submx0 -(rowg0 0) rowgK sub0mx. Qed. Lemma rowg_mx_eq0 (L : {group rVn}) : (rowg_mx L == 0) = (L :==: 1%g). Proof. -rewrite -trivg_rowg; apply/idP/idP=> [|/eqP->]; last by rewrite rowg_mx1 rowg0. -by rewrite !(sameP eqP trivgP); apply: subset_trans; exact: sub_rowg_mx. +rewrite -trivg_rowg; apply/idP/eqP=> [|->]; last by rewrite rowg_mx1 rowg0. +exact/contraTeq/subG1_contra/sub_rowg_mx. Qed. Lemma rowgI m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) : @@ -312,7 +309,7 @@ Lemma astabs_rowg_repr m (A : 'M_(m, n)) : 'N(rowg A | 'MR rG) = rstabs rG A. Proof. apply/setP=> x; rewrite !inE /=; apply: andb_id2l => Gx. apply/subsetP/idP=> nAx => [|u]; last first. - rewrite !inE mx_repr_actE // => Au; exact: (submx_trans (submxMr _ Au)). + by rewrite !inE mx_repr_actE // => Au; apply: (submx_trans (submxMr _ Au)). apply/row_subP=> i; move/implyP: (nAx (row i A)). by rewrite !inE row_sub mx_repr_actE //= row_mul. Qed. @@ -449,13 +446,13 @@ Variables p n : nat. Local Notation rVn := 'rV['F_p]_n. Lemma rowg_mxK (L : {group rVn}) : rowg (rowg_mx L) = L. -Proof. by apply: stable_rowg_mxK; exact: mx_Fp_stable. Qed. +Proof. by apply: stable_rowg_mxK; apply: mx_Fp_stable. Qed. Lemma rowg_mxSK (L : {set rVn}) (M : {group rVn}) : (rowg_mx L <= rowg_mx M)%MS = (L \subset M). Proof. apply/idP/idP; last exact: rowg_mxS. -by rewrite -rowgS rowg_mxK; apply: subset_trans; exact: sub_rowg_mx. +by rewrite -rowgS rowg_mxK; apply/subset_trans/sub_rowg_mx. Qed. Lemma mxrank_rowg (L : {group rVn}) : @@ -508,7 +505,7 @@ Proof. by case/misomP: (xchooseP ab_rV_P). Qed. Lemma abelem_rV_injm : 'injm ErV. Proof. by case/isomP: abelem_rV_isom. Qed. Lemma abelem_rV_inj : {in E &, injective ErV}. -Proof. by apply/injmP; exact: abelem_rV_injm. Qed. +Proof. by apply/injmP; apply: abelem_rV_injm. Qed. Lemma im_abelem_rV : ErV @* E = setT. Proof. by case/isomP: abelem_rV_isom. Qed. @@ -701,7 +698,7 @@ Qed. Lemma abelem_mx_irrP : reflect (mx_irreducible rG) (minnormal E G). Proof. -by rewrite -[E in minnormal E G]im_rVabelem -rowg1; exact: mxsimple_abelemP. +by rewrite -[E in minnormal E G]im_rVabelem -rowg1; apply: mxsimple_abelemP. Qed. Lemma rfix_abelem (H : {set gT}) : @@ -850,7 +847,7 @@ Let p_gt1 := prime_gt1 p_pr. Let oZp := card_center_extraspecial pS esS. Let modIp' (i : 'I_p.-1) : (i.+1 %% p = i.+1)%N. -Proof. by case: i => i; rewrite /= -ltnS prednK //; exact: modn_small. Qed. +Proof. by case: i => i; rewrite /= -ltnS prednK //; apply: modn_small. Qed. (* This is Aschbacher (34.9), parts (1)-(4). *) Theorem extraspecial_repr_structure (sS : irrType F S) : @@ -873,7 +870,7 @@ have nb_irr: #|sS| = (p ^ n.*2 + p.-1)%N. pose Zcl := classes S ::&: 'Z(S). have cardZcl: #|Zcl| = p. transitivity #|[set [set z] | z in 'Z(S)]|; last first. - by rewrite card_imset //; exact: set1_inj. + by rewrite card_imset //; apply: set1_inj. apply: eq_card => zS; apply/setIdP/imsetP=> [[] | [z]]. case/imsetP=> z Sz ->{zS} szSZ. have Zz: z \in 'Z(S) by rewrite (subsetP szSZ) ?class_refl. @@ -900,7 +897,7 @@ have nb_irr: #|sS| = (p ^ n.*2 + p.-1)%N. apply: contra notZxS => Zxy; rewrite -{1}(lcoset_id Sy) class_lcoset. rewrite ((_ ^: _ =P [set x ^ y])%g _) ?sub1set // eq_sym eqEcard. rewrite sub1set class_refl cards1 -index_cent1 (setIidPl _) ?indexgg //. - by rewrite sub_cent1; apply: subsetP Zxy; exact: subsetIr. + by rewrite sub_cent1; apply: subsetP Zxy; apply: subsetIr. rewrite sum_nat_dep_const mulnC eqn_pmul2l //; move/eqP <-. rewrite addSnnS prednK // -cardZcl -[card _](cardsID Zcl) /= addnC. by congr (_ + _)%N; apply: eq_card => t; rewrite !inE andbC // andbAC andbb. @@ -954,11 +951,10 @@ have alpha_i_z i: ((alpha ^+ ephi i) z = z ^+ i.+1)%g. by rewrite autE ?cycle_id //= val_Zp_nat ozp ?modIp'. have rphiP i: S :==: autm (groupX (ephi i) Aut_alpha) @* S by rewrite im_autm. pose rphi i := morphim_repr (eqg_repr phi (rphiP i)) (subxx S). -have rphi_irr i: mx_irreducible (rphi i). - by apply/morphim_mx_irr; exact/eqg_mx_irr. +have rphi_irr i: mx_irreducible (rphi i) by apply/morphim_mx_irr/eqg_mx_irr. have rphi_fful i: mx_faithful (rphi i). rewrite /mx_faithful rker_morphim rker_eqg. - by rewrite (trivgP (fful_nlin _ nlin_i0)) morphpreIdom; exact: injm_autm. + by rewrite (trivgP (fful_nlin _ nlin_i0)) morphpreIdom; apply: injm_autm. have rphi_z i: rphi i z = (w ^+ i.+1)%:M. by rewrite /rphi [phi]lock /= /morphim_mx autmE alpha_i_z -lock phi_ze. pose iphi i := irr_comp sS (rphi i); pose phi_ i := irr_repr (iphi i). @@ -1021,7 +1017,7 @@ suffices IH V: mxsimple rS V -> mx_iso rZ U V -> - split=> [|/= V simV isoUV]. by case/andP: (IH U simU (mx_iso_refl _ _)) => /eqP. by case/andP: (IH V simV isoUV) => _ /(mxsimple_isoP simU). -move=> simV isoUV; wlog sS: / irrType F S by exact: socle_exists. +move=> simV isoUV; wlog sS: / irrType F S by apply: socle_exists. have [[_ defS'] prZ] := esS. have{prZ} ntZ: 'Z(S) :!=: 1%g by case: eqP prZ => // ->; rewrite cards1. have [_ [iphi]] := extraspecial_repr_structure sS. @@ -1030,13 +1026,13 @@ have [modU nzU _]:= simU; pose rU := submod_repr modU. have nlinU: \rank U != 1%N. apply/eqP=> /(rker_linear rU); apply/negP; rewrite /rker rstab_submod. by rewrite (eqmx_rstab _ (val_submod1 _)) (eqP ffulU) defS' subG1. -have irrU: mx_irreducible rU by exact/submod_mx_irr. +have irrU: mx_irreducible rU by apply/submod_mx_irr. have rsimU := rsim_irr_comp sS F'S irrU. set iU := irr_comp sS rU in rsimU; have [_ degU _ _]:= rsimU. have phiUP: iU \in codom iphi by rewrite im_phi !inE -degU. rewrite degU -(f_iinv phiUP) dim_phi eqxx /=; apply/(mxsimple_isoP simU). have [modV _ _]:= simV; pose rV := submod_repr modV. -have irrV: mx_irreducible rV by exact/submod_mx_irr. +have irrV: mx_irreducible rV by apply/submod_mx_irr. have rsimV := rsim_irr_comp sS F'S irrV. set iV := irr_comp sS rV in rsimV; have [_ degV _ _]:= rsimV. have phiVP: iV \in codom iphi by rewrite im_phi !inE -degV -(mxrank_iso isoUV). @@ -1045,7 +1041,7 @@ have [z Zz ntz]:= trivgPn _ ntZ. have [|w prim_w phi_z] := phiZ z; first by rewrite 2!inE ntz. suffices eqjUV: jU == jV. apply/(mx_rsim_iso modU modV); apply: mx_rsim_trans rsimU _. - by rewrite -(f_iinv phiUP) -/jU (eqP eqjUV) f_iinv; exact: mx_rsim_sym. + by rewrite -(f_iinv phiUP) -/jU (eqP eqjUV) f_iinv; apply: mx_rsim_sym. have rsimUV: mx_rsim (subg_repr (phi jU) sZS) (subg_repr (phi jV) sZS). have [bU _ bUfree bUhom] := mx_rsim_sym rsimU. have [bV _ bVfree bVhom] := rsimV. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index e947fe0..7ceae6e 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -1,15 +1,13 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg poly polydiv finalg zmodp cyclic matrix mxalgebra mxpoly. -From mathcomp.solvable -Require Import commutator center pgroup. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg poly polydiv finset. +From mathcomp +Require Import fingroup morphism perm automorphism quotient finalg action zmodp. +From mathcomp +Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly. (******************************************************************************) (* This file provides linkage between classic Group Theory and commutative *) @@ -308,7 +306,7 @@ Qed. Lemma repr_mxKV m x : x \in G -> cancel ((@mulmx _ m n n)^~ (rG x^-1)) (mulmx^~ (rG x)). -Proof. by rewrite -groupV -{3}[x]invgK; exact: repr_mxK. Qed. +Proof. by rewrite -groupV -{3}[x]invgK; apply: repr_mxK. Qed. Lemma repr_mx_unit x : x \in G -> rG x \in unitmx. Proof. by move=> Gx; case/mulmx1_unit: (repr_mxKV Gx 1%:M). Qed. @@ -923,7 +921,7 @@ Proof. by case/setIdP=> _ /eqP cUx /submxP[w ->]; rewrite -mulmxA cUx. Qed. Lemma rstabs_act x m1 (W : 'M_(m1, n)) : x \in rstabs -> (W <= U)%MS -> (W *m rG x <= U)%MS. Proof. -by case/setIdP=> [_ nUx] sWU; apply: submx_trans nUx; exact: submxMr. +by case/setIdP=> [_ nUx] sWU; apply: submx_trans nUx; apply: submxMr. Qed. Definition mxmodule := G \subset rstabs. @@ -964,7 +962,7 @@ Proof. by apply/mxmoduleP=> x _; rewrite submx1. Qed. 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. Proof. -by move=> modU Gx sWU; apply: submx_trans (mxmoduleP modU x Gx); exact: submxMr. +by move=> modU Gx sWU; apply: submx_trans (mxmoduleP modU x Gx); apply: submxMr. Qed. Lemma mxmodule_eigenvector m (U : 'M_(m, n)) : @@ -989,7 +987,7 @@ Qed. Lemma sumsmx_module I r (P : pred I) U : (forall i, P i -> mxmodule (U i)) -> mxmodule (\sum_(i <- r | P i) U i)%MS. Proof. -by move=> modU; elim/big_ind: _; [exact: mxmodule0 | exact: addsmx_module | ]. +by move=> modU; elim/big_ind: _; [apply: mxmodule0 | apply: addsmx_module | ]. Qed. Lemma capmx_module m1 m2 U V : @@ -1002,7 +1000,7 @@ Qed. Lemma bigcapmx_module I r (P : pred I) U : (forall i, P i -> mxmodule (U i)) -> mxmodule (\bigcap_(i <- r | P i) U i)%MS. Proof. -by move=> modU; elim/big_ind: _; [exact: mxmodule1 | exact: capmx_module | ]. +by move=> modU; elim/big_ind: _; [apply: mxmodule1 | apply: capmx_module | ]. Qed. (* Sub- and factor representations induced by a (sub)module. *) @@ -1023,7 +1021,7 @@ Lemma in_submodE m W : @in_submod m W = W *m in_submod 1%:M. Proof. by rewrite mulmxA mulmx1. Qed. Lemma val_submod1 : (val_submod 1%:M :=: U)%MS. -Proof. by rewrite /val_submod /= mul1mx; exact: eq_row_base. Qed. +Proof. by rewrite /val_submod /= mul1mx; apply: eq_row_base. Qed. Lemma val_submodP m W : (@val_submod m W <= U)%MS. Proof. by rewrite mulmx_sub ?eq_row_base. Qed. @@ -1128,7 +1126,7 @@ Lemma in_factmod_addsK m (W : 'M_(m, n)) : (in_factmod (U + W)%MS :=: in_factmod W)%MS. Proof. apply: eqmx_trans (addsmxMr _ _ _) _. -by rewrite ((_ *m _ =P 0) _) ?in_factmod_eq0 //; exact: adds0mx. +by rewrite ((_ *m _ =P 0) _) ?in_factmod_eq0 //; apply: adds0mx. Qed. Lemma add_sub_fact_mod m (W : 'M_(m, n)) : @@ -1151,7 +1149,7 @@ Lemma in_factmodsK m (W : 'M_(m, n)) : (U <= W)%MS -> (U + val_factmod (in_factmod W) :=: W)%MS. Proof. move/addsmx_idPr; apply: eqmx_trans (eqmx_sym _). -by rewrite -{1}[W]add_sub_fact_mod; apply: addsmx_addKl; exact: val_submodP. +by rewrite -{1}[W]add_sub_fact_mod; apply: addsmx_addKl; apply: val_submodP. Qed. Lemma mxrank_in_factmod m (W : 'M_(m, n)) : @@ -1245,7 +1243,7 @@ Lemma envelop_mxP A : reflect (exists a, A = \sum_(x in G) a x *: rG x) (A \in E_G)%MS. Proof. have G_1 := group1 G; have bijG := enum_val_bij_in G_1. -set h := enum_val in bijG; have Gh: h _ \in G by exact: enum_valP. +set h := enum_val in bijG; have Gh: h _ \in G by apply: enum_valP. apply: (iffP submxP) => [[u defA] | [a ->]]. exists (fun x => u 0 (enum_rank_in G_1 x)); apply: (can_inj mxvecK). rewrite defA mulmx_sum_row linear_sum (reindex h) //=. @@ -1374,7 +1372,7 @@ Proof. exact/rfix_mxP. Qed. Lemma rfix_mxS (H K : {set gT}) : H \subset K -> (rfix_mx K <= rfix_mx H)%MS. Proof. -by move=> sHK; apply/rfix_mxP=> x Hx; exact: rfix_mxP (subsetP sHK x Hx). +by move=> sHK; apply/rfix_mxP=> x Hx; apply: rfix_mxP (subsetP sHK x Hx). Qed. Lemma rfix_mx_conjsg (H : {set gT}) x : @@ -1437,7 +1435,7 @@ Proof. by apply/cyclic_mxP; exists 1%:M; rewrite ?mulmx1 ?envelop_mx1. Qed. Lemma cyclic_mx_eq0 u : (cyclic_mx u == 0) = (u == 0). Proof. rewrite -!submx0; apply/idP/idP. - by apply: submx_trans; exact: cyclic_mx_id. + by apply: submx_trans; apply: cyclic_mx_id. move/submx0null->; rewrite genmxE; apply/row_subP=> i. by rewrite row_mul mul_rV_lin1 /= mul0mx ?sub0mx. Qed. @@ -1529,7 +1527,7 @@ Lemma mx_iso_sym U V : mx_iso U V -> mx_iso V U. Proof. case=> f injf homUf defV; exists (invmx f); first by rewrite unitmx_inv. by rewrite dom_hom_invmx // -defV submxMr. -by rewrite -[U](mulmxK injf); exact: eqmxMr (eqmx_sym _). +by rewrite -[U](mulmxK injf); apply: eqmxMr (eqmx_sym _). Qed. Lemma mx_iso_trans U V W : mx_iso U V -> mx_iso V W -> mx_iso U W. @@ -1537,7 +1535,7 @@ Proof. case=> f injf homUf defV [g injg homVg defW]. exists (f *m g); first by rewrite unitmx_mul injf. by apply/hom_mxP=> x Gx; rewrite !mulmxA 2?(hom_mxP _) ?defV. -by rewrite mulmxA; exact: eqmx_trans (eqmxMr g defV) defW. +by rewrite mulmxA; apply: eqmx_trans (eqmxMr g defV) defW. Qed. Lemma mxrank_iso U V : mx_iso U V -> \rank U = \rank V. @@ -1545,7 +1543,7 @@ Proof. by case=> f injf _ <-; rewrite mxrankMfree ?row_free_unit. Qed. Lemma mx_iso_module U V : mx_iso U V -> mxmodule U -> mxmodule V. Proof. -by case=> f _ homUf defV; rewrite -(eqmx_module defV); exact: hom_mxmodule. +by case=> f _ homUf defV; rewrite -(eqmx_module defV); apply: hom_mxmodule. Qed. (* Simple modules (we reserve the term "irreducible" for representations). *) @@ -1562,7 +1560,7 @@ Lemma mxsimpleP U : Proof. do [split => [] [modU nzU simU]; split] => // [V modV sVU nzV | [V]]. apply/idPn; rewrite -(ltn_leqif (mxrank_leqif_sup sVU)) => ltVU. - by case: simU; exists V; exact/and4P. + by case: simU; exists V; apply/and4P. by case/and4P=> modV sVU nzV; apply/negP; rewrite -leqNgt mxrankS ?simU. Qed. @@ -1578,7 +1576,7 @@ have genU := genmxE U; apply simU; exists <<U>>%MS; last by rewrite genU. apply/mxsimpleP; split; rewrite ?(eqmx_eq0 genU) ?(eqmx_module genU) //. case=> V; rewrite !genU=> /and4P[modV sVU nzV ltVU]; case: notF. apply: IHr nzV _ => // [|[W simW sWV]]; first exact: leq_trans ltVU _. -by apply: simU; exists W => //; exact: submx_trans sWV sVU. +by apply: simU; exists W => //; apply: submx_trans sWV sVU. Qed. Lemma mx_iso_simple U V : mx_iso U V -> mxsimple U -> mxsimple V. @@ -1663,19 +1661,19 @@ apply: (iffP and3P) => [[modV] | isoUV]; last first. by case: (mx_iso_simple isoUV simU). have [f injf homUf defV] := isoUV; apply/rowV0Pn; exists (u *m f). rewrite sub_capmx -defV submxMr //. - by apply/row_hom_mxP; exists f; first exact: (submx_trans Uu). + by apply/row_hom_mxP; exists f; first apply: (submx_trans Uu). by rewrite -(mul0mx _ f) (can_eq (mulmxK injf)) nz_u. case/rowV0Pn=> v; rewrite sub_capmx => /andP[Vv]. case/row_hom_mxP => f homMf def_v nz_v eqrUV. pose uG := cyclic_mx u; pose vG := cyclic_mx v. -have def_vG: (uG *m f :=: vG)%MS by rewrite /vG -def_v; exact: hom_cyclic_mx. -have defU: (U :=: uG)%MS by exact: mxsimple_cyclic. +have def_vG: (uG *m f :=: vG)%MS by rewrite /vG -def_v; apply: hom_cyclic_mx. +have defU: (U :=: uG)%MS by apply: mxsimple_cyclic. have mod_uG: mxmodule uG by rewrite cyclic_mx_module. have homUf: (U <= dom_hom_mx f)%MS. by rewrite defU cyclic_mx_sub ?dom_hom_mx_module. have isoUf: mx_iso U (U *m f). apply: mx_Schur_inj_iso => //; apply: contra nz_v; rewrite -!submx0. - by rewrite (eqmxMr f defU) def_vG; exact: submx_trans (cyclic_mx_id v). + by rewrite (eqmxMr f defU) def_vG; apply: submx_trans (cyclic_mx_id v). apply: mx_iso_trans (isoUf) (eqmx_iso _); apply/eqmxP. have sUfV: (U *m f <= V)%MS by rewrite (eqmxMr f defU) def_vG cyclic_mx_sub. by rewrite -mxrank_leqif_eq ?eqn_leq 1?mxrankS // -(mxrank_iso isoUf). @@ -1684,7 +1682,7 @@ Qed. Lemma mxsimple_iso_simple U V : mxsimple_iso U V -> mxsimple U -> mxsimple V. Proof. -by move=> isoUV simU; apply: mx_iso_simple (simU); exact/mxsimple_isoP. +by move=> isoUV simU; apply: mx_iso_simple (simU); apply/mxsimple_isoP. Qed. (* For us, "semisimple" means "sum of simple modules"; this is classically, *) @@ -1713,7 +1711,7 @@ exists J; split=> //; apply/eqmxP; rewrite addsmx_sub sUV; apply/andP; split. by apply/sumsmx_subP=> i Ji; rewrite (sumsmx_sup i). rewrite -/(V_ J); apply/sumsmx_subP=> i _. case Ji: (i \in J). - by apply: submx_trans (addsmxSr _ _); exact: (sumsmx_sup i). + by apply: submx_trans (addsmxSr _ _); apply: (sumsmx_sup i). have [modWi nzWi simWi] := simW i. rewrite (sameP capmx_idPl eqmxP) simWi ?capmxSl ?capmx_module ?addsmx_module //. apply: contraFT (Ji); rewrite negbK => dxWiUVJ. @@ -1754,7 +1752,7 @@ rewrite addsmxC big1 ?adds0mx_id => [|i /andP[_ /eqP] //]. set tI := 'I_(_); set r_ := nth _ _ => defV. have{simW} simWr (i : tI) : mxsimple (W (r_ i)). case: i => m /=; set Pr := fun i => _ => lt_m_r /=. - suffices: (Pr (r_ m)) by case/andP; exact: simW. + suffices: (Pr (r_ m)) by case/andP; apply: simW. apply: all_nthP m lt_m_r; apply/all_filterP. by rewrite -filter_predI; apply: eq_filter => i; rewrite /= andbb. have [J []] := sum_mxsimple_direct_sub simWr defV. @@ -1763,7 +1761,7 @@ case: (set_0Vmem J) => [-> V0 | [j0 Jj0]]. pose K := {j | j \in J}; pose k0 : K := Sub j0 Jj0. have bij_KJ: {on J, bijective (sval : K -> _)}. by exists (insubd k0) => [k _ | j Jj]; rewrite ?valKd ?insubdK. -have J_K (k : K) : sval k \in J by exact: valP k. +have J_K (k : K) : sval k \in J by apply: valP k. rewrite mxdirectE /= !(reindex _ bij_KJ) !(eq_bigl _ _ J_K) -mxdirectE /= -/tI. exact: MxSemisimple. Qed. @@ -1779,7 +1777,7 @@ Lemma addsmx_semisimple U V : Proof. case=> [I W /= simW defU _] [J T /= simT defV _]. have defUV: (\sum_ij sum_rect (fun _ => 'M_n) W T ij :=: U + V)%MS. - by rewrite big_sumType /=; exact: adds_eqmx. + by rewrite big_sumType /=; apply: adds_eqmx. by apply: intro_mxsemisimple defUV _; case=> /=. Qed. @@ -1792,7 +1790,7 @@ Qed. Lemma eqmx_semisimple U V : (U :=: V)%MS -> mxsemisimple U -> mxsemisimple V. Proof. -by move=> eqUV [I W S simW defU dxS]; exists I W => //; exact: eqmx_trans eqUV. +by move=> eqUV [I W S simW defU dxS]; exists I W => //; apply: eqmx_trans eqUV. Qed. Lemma hom_mxsemisimple (V f : 'M_n) : @@ -1800,7 +1798,7 @@ Lemma hom_mxsemisimple (V f : 'M_n) : Proof. case=> I W /= simW defV _; rewrite -defV => /sumsmx_subP homWf. have{defV} defVf: (\sum_i W i *m f :=: V *m f)%MS. - by apply: eqmx_trans (eqmx_sym _) (eqmxMr f defV); exact: sumsmxMr. + by apply: eqmx_trans (eqmx_sym _) (eqmxMr f defV); apply: sumsmxMr. apply: (intro_mxsemisimple defVf) => i _ nzWf. by apply: mx_iso_simple (simW i); apply: mx_Schur_inj_iso; rewrite ?homWf. Qed. @@ -1872,7 +1870,7 @@ Proof. move=> modV redV [] // nssimV; move: {-1}_.+1 (ltnSn (\rank V)) => r leVr. elim: r => // r IHr in V leVr modV redV nssimV. have [V0 | nzV] := eqVneq V 0. - by rewrite nssimV ?V0 //; exact: mxsemisimple0. + by rewrite nssimV ?V0 //; apply: mxsemisimple0. apply (mxsimple_exists modV nzV) => [[U simU sUV]]; have [modU nzU _] := simU. have [W modW defUW dxUW] := redV U modU sUV. have sWV: (W <= V)%MS by rewrite -defUW addsmxSr. @@ -1964,7 +1962,7 @@ rewrite [in compU]unlock; apply/genmxP/andP; split; last first. by apply/sumsmx_subP => i _; rewrite (sumsmx_sup (sval i)). apply/sumsmx_subP => i _. case i0: (r_nz i); first by rewrite (sumsmx_sup (Sub i i0)). -by move/negbFE: i0; rewrite -cyclic_mx_eq0 => /eqP->; exact: sub0mx. +by move/negbFE: i0; rewrite -cyclic_mx_eq0 => /eqP->; apply: sub0mx. Qed. Lemma component_mx_semisimple : mxsemisimple compU. @@ -2027,7 +2025,7 @@ move=> simU simV; apply: (iffP eqP) => isoUV. by apply: component_mx_iso; rewrite ?isoUV ?component_mx_id. rewrite -(genmx_component U) -(genmx_component V); apply/genmxP. wlog suffices: U V simU simV isoUV / (component_mx U <= component_mx V)%MS. - by move=> IH; rewrite !IH //; exact: mx_iso_sym. + by move=> IH; rewrite !IH //; apply: mx_iso_sym. have [I [W isoWU ->]] := component_mx_def simU. apply/sumsmx_subP => i _; apply: mx_iso_component => //. exact: mx_iso_trans (mx_iso_sym isoUV) (isoWU i). @@ -2041,7 +2039,7 @@ move=> simU simV neUV; apply: contraNeq neUV => ntUV. apply: (mxsimple_exists _ ntUV) => [|[W simW]]. by rewrite capmx_module ?component_mx_module. rewrite sub_capmx => /andP[sWU sWV]; apply/component_mx_isoP=> //. -by apply: mx_iso_trans (_ : mx_iso U W) (mx_iso_sym _); exact: component_mx_iso. +by apply: mx_iso_trans (_ : mx_iso U W) (mx_iso_sym _); apply: component_mx_iso. Qed. Section Socle. @@ -2054,7 +2052,7 @@ Record socleType := EnumSocle { Lemma socle_exists : classically socleType. Proof. -pose V : 'M[F]_n := 0; have: mxsemisimple V by exact: mxsemisimple0. +pose V : 'M[F]_n := 0; have: mxsemisimple V by apply: mxsemisimple0. have: n - \rank V < n.+1 by rewrite mxrank0 subn0. elim: _.+1 V => // n' IHn' V; rewrite ltnS => le_nV_n' ssimV. case=> // maxV; apply: (maxV); have [I /= U simU defV _] := ssimV. @@ -2063,12 +2061,12 @@ suffices sMV: (M <= V)%MS. rewrite -defV -(mulmx1 (\sum_i _)%MS) in sMV. have [//| i _] := hom_mxsemisimple_iso simM _ (scalar_mx_hom _ _) sMV. move/mx_iso_sym=> isoM; apply/hasP. - exists (U i); [exact: codom_f | exact/mxsimple_isoP]. + by exists (U i); [apply: codom_f | apply/mxsimple_isoP]. have ssimMV := addsmx_semisimple (mxsimple_semisimple simM) ssimV. apply: contraLR isT => nsMV; apply: IHn' ssimMV _ maxV. apply: leq_trans le_nV_n'; rewrite ltn_sub2l //. rewrite ltn_neqAle rank_leq_row andbT -[_ == _]sub1mx. - apply: contra nsMV; apply: submx_trans; exact: submx1. + by apply: contra nsMV; apply: submx_trans; apply: submx1. rewrite (ltn_leqif (mxrank_leqif_sup _)) ?addsmxSr //. by rewrite addsmx_sub submx_refl andbT. Qed. @@ -2083,7 +2081,7 @@ Lemma component_socle M : mxsimple M -> component_mx M \in socle_enum. Proof. rewrite /socle_enum; case: sG0 => e0 /= sim_e mem_e simM. have /hasP[M' e0M' isoMM'] := mem_e M simM; apply/mapP; exists M' => //. -by apply/eqP/component_mx_isoP; [|exact: sim_e | exact/mxsimple_isoP]. +by apply/eqP/component_mx_isoP; [|apply: sim_e | apply/mxsimple_isoP]. Qed. Inductive socle_sort : predArgType := PackSocle W of W \in socle_enum. @@ -2110,7 +2108,7 @@ Definition socle_repr W := submod_repr (socle_module W). Lemma nz_socle (W : sG) : W != 0 :> 'M_n. Proof. have simW := socle_simple W; have [_ nzW _] := simW; apply: contra nzW. -by rewrite -!submx0; exact: submx_trans (component_mx_id simW). +by rewrite -!submx0; apply: submx_trans (component_mx_id simW). Qed. Lemma socle_mem (W : sG) : (W : 'M_n) \in socle_enum. @@ -2129,7 +2127,7 @@ 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. -Proof. by rewrite (sameP genmxP eqP) !{1}genmx_component; exact: (W =P _). Qed. +Proof. by rewrite (sameP genmxP eqP) !{1}genmx_component; apply: (W =P _). Qed. Fact socle_finType_subproof : cancel (fun W => SeqSub (socle_mem W)) (fun s => PackSocle (valP s)). @@ -2154,7 +2152,7 @@ Variable P : pred sG. Notation S := (\sum_(W : sG | P W) socle_val W)%MS. Lemma subSocle_module : mxmodule S. -Proof. by rewrite sumsmx_module // => W _; exact: component_mx_module. Qed. +Proof. by rewrite sumsmx_module // => W _; apply: component_mx_module. Qed. Lemma subSocle_semisimple : mxsemisimple S. Proof. @@ -2203,7 +2201,7 @@ Proof. apply/mxdirect_sumsP=> W _; apply/eqP. rewrite -submx0 capmx_subSocle ?component_mx_module //. apply/sumsmx_subP=> W' /andP[_ neWW']. -by rewrite capmxC component_mx_disjoint //; exact: socle_simple. +by rewrite capmxC component_mx_disjoint //; apply: socle_simple. Qed. Definition Socle := (\sum_(W : sG) W)%MS. @@ -2216,7 +2214,7 @@ Qed. Lemma semisimple_Socle U : mxsemisimple U -> (U <= Socle)%MS. Proof. -by case=> I M /= simM <- _; apply/sumsmx_subP=> i _; exact: simple_Socle. +by case=> I M /= simM <- _; apply/sumsmx_subP=> i _; apply: simple_Socle. Qed. Lemma reducible_Socle U : @@ -2273,7 +2271,7 @@ by rewrite -mulmxA -cGf // mulmxA mulmx_ker mul0mx. Qed. Lemma centgmx_hom m (U : 'M_(m, n)) : centgmx rG f -> (U <= dom_hom_mx f)%MS. -Proof. by rewrite -row_full_dom_hom -sub1mx; exact: submx_trans (submx1 _). Qed. +Proof. by rewrite -row_full_dom_hom -sub1mx; apply: submx_trans (submx1 _). Qed. End CentHom. @@ -2307,7 +2305,7 @@ Lemma mx_abs_irrP : mx_absolutely_irreducible. Proof. have G_1 := group1 G; have bijG := enum_val_bij_in G_1. -set h := enum_val in bijG; have Gh : h _ \in G by exact: enum_valP. +set h := enum_val in bijG; have Gh : h _ \in G by apply: enum_valP. rewrite /mx_absolutely_irreducible; case: (n > 0); last by right; case. apply: (iffP row_fullP) => [[E' E'G] | [_ [a_ a_G]]]. split=> //; exists (fun x B => (mxvec B *m E') 0 (enum_rank_in G_1 x)) => B. @@ -2391,7 +2389,7 @@ Variable rG : mx_representation F G n. Lemma envelop_mx_ring : mxring (enveloping_algebra_mx rG). Proof. -apply/andP; split; first by apply/mulsmx_subP; exact: envelop_mxM. +apply/andP; split; first by apply/mulsmx_subP; apply: envelop_mxM. apply/mxring_idP; exists 1%:M; split=> *; rewrite ?mulmx1 ?mul1mx //. by rewrite -mxrank_eq0 mxrank1. exact: envelop_mx1. @@ -2500,17 +2498,17 @@ Lemma rstabs_subg : rstabs rH U = H :&: rstabs rG U. Proof. by apply/setP=> x; rewrite !inE andbA -in_setI (setIidPl sHG). Qed. Lemma mxmodule_subg : mxmodule rG U -> mxmodule rH U. -Proof. by rewrite /mxmodule rstabs_subg subsetI subxx; exact: subset_trans. Qed. +Proof. by rewrite /mxmodule rstabs_subg subsetI subxx; apply: subset_trans. Qed. End Stabilisers. Lemma mxsimple_subg M : mxmodule rG M -> mxsimple rH M -> mxsimple rG M. Proof. -by move=> modM [_ nzM minM]; split=> // U /mxmodule_subg; exact: minM. +by move=> modM [_ nzM minM]; split=> // U /mxmodule_subg; apply: minM. Qed. Lemma subg_mx_irr : mx_irreducible rH -> mx_irreducible rG. -Proof. by apply: mxsimple_subg; exact: mxmodule1. Qed. +Proof. by apply: mxsimple_subg; apply: mxmodule1. Qed. Lemma subg_mx_abs_irr : mx_absolutely_irreducible rH -> mx_absolutely_irreducible rG. @@ -2734,7 +2732,7 @@ by rewrite val_factmod_module (eqmx_module _ (in_factmod_addsK _ _)). Qed. Lemma rker_submod : rker rU = rstab rG U. -Proof. by rewrite /rker rstab_submod; exact: eqmx_rstab (val_submod1 U). Qed. +Proof. by rewrite /rker rstab_submod; apply: eqmx_rstab (val_submod1 U). Qed. Lemma rstab_norm : G \subset 'N(rstab rG U). Proof. by rewrite -rker_submod rker_norm. Qed. @@ -2807,7 +2805,7 @@ Proof. have Bfree: row_free B by rewrite row_free_unit. split => /mx_irrP[n_gt0 irrG]; apply/mx_irrP; split=> // U. rewrite -[U](mulmxKV uB) -mxmodule_conj -mxrank_eq0 /row_full mxrankMfree //. - by rewrite mxrank_eq0; exact: irrG. + by rewrite mxrank_eq0; apply: irrG. rewrite -mxrank_eq0 /row_full -(mxrankMfree _ Bfree) mxmodule_conj mxrank_eq0. exact: irrG. Qed. @@ -2882,7 +2880,7 @@ Lemma quotient_splitting_field gT (G : {group gT}) (H : {set gT}) : G \subset 'N(H) -> group_splitting_field G -> group_splitting_field (G / H). Proof. move=> nHG splitG n rGH irrGH. -by rewrite -(morphim_mx_abs_irr _ nHG) splitG //; exact/morphim_mx_irr. +by rewrite -(morphim_mx_abs_irr _ nHG) splitG //; apply/morphim_mx_irr. Qed. Lemma coset_splitting_field gT (H : {set gT}) : @@ -2890,7 +2888,7 @@ Lemma coset_splitting_field gT (H : {set gT}) : Proof. move=> split_gT Gbar; have ->: Gbar = (coset H @*^-1 Gbar / H)%G. by apply: val_inj; rewrite /= /quotient morphpreK ?sub_im_coset. -by apply: quotient_splitting_field; [exact: subsetIl | exact: split_gT]. +by apply: quotient_splitting_field; [apply: subsetIl | apply: split_gT]. Qed. End SplittingField. @@ -2958,9 +2956,9 @@ Lemma der1_sub_rker : group_splitting_field G -> mx_irreducible rG -> (G^`(1) \subset rker rG)%g = (n == 1)%N. Proof. -move=> splitG irrG; apply/idP/idP; last by move/eqP; exact: rker_linear. +move=> splitG irrG; apply/idP/idP; last by move/eqP; apply: rker_linear. move/sub_der1_abelian; move/(abelian_abs_irr (kquo_repr rG))=> <-. -by apply: (quotient_splitting_field (rker_norm _) splitG); exact/quo_mx_irr. +by apply: (quotient_splitting_field (rker_norm _) splitG); apply/quo_mx_irr. Qed. End AbelianQuotient. @@ -3086,7 +3084,7 @@ Proof. move=> addUV dxUV. have eqUV: \rank U = \rank (cokermx V). by rewrite mxrank_coker -{3}(mxrank1 F n) -addUV (mxdirectP dxUV) addnK. -have{dxUV} dxUV: (U :&: V = 0)%MS by exact/mxdirect_addsP. +have{dxUV} dxUV: (U :&: V = 0)%MS by apply/mxdirect_addsP. exists (in_submod U (val_factmod 1%:M *m proj_mx U V)) => // [|x Gx]. rewrite /row_free -{6}eqUV -[_ == _]sub1mx -val_submodS val_submod1. rewrite in_submodK ?proj_mx_sub // -{1}[U](proj_mx_id dxUV) //. @@ -3121,13 +3119,13 @@ 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). -Proof. by apply/submod_mx_irr; exact: socle_simple. Qed. +Proof. by apply/submod_mx_irr; apply: socle_simple. Qed. Lemma socle_rsimP (W1 W2 : sG) : reflect (mx_rsim (socle_repr W1) (socle_repr W2)) (W1 == W2). Proof. have [simW1 simW2] := (socle_simple W1, socle_simple W2). -by apply: (iffP (component_mx_isoP simW1 simW2)); move/mx_rsim_iso; exact. +by apply: (iffP (component_mx_isoP simW1 simW2)); move/mx_rsim_iso; apply. Qed. Local Notation mG U := (mxmodule rG U). @@ -3160,7 +3158,7 @@ Qed. Lemma mxtrace_submod1 U (modU : mG U) : (U :=: 1%:M)%MS -> {in G, forall x, \tr (sr modU x) = \tr (rG x)}. -Proof. by move=> defU; exact: mxtrace_rsim (rsim_submod1 modU defU). Qed. +Proof. by move=> defU; apply: mxtrace_rsim (rsim_submod1 modU defU). Qed. Lemma mxtrace_dadd_mod U V W (modU : mG U) (modV : mG V) (modW : mG W) : (U + V :=: W)%MS -> mxdirect (U + V) -> @@ -3213,9 +3211,9 @@ have isoW i: mx_iso rG U (W i). have ->: (\rank V %/ \rank U)%N = #|I|. symmetry; rewrite -(mulnK #|I| rankU_gt0); congr (_ %/ _)%N. rewrite -defV (mxdirectP dxV) /= -sum_nat_const. - by apply: eq_bigr => i _; exact: mxrank_iso. + by apply: eq_bigr => i _; apply: mxrank_iso. rewrite -sumr_const; apply: eq_bigr => i _; symmetry. -by apply: mxtrace_rsim Gx; apply/mx_rsim_iso; exact: isoW. +by apply: mxtrace_rsim Gx; apply/mx_rsim_iso; apply: isoW. Qed. Lemma mxtrace_Socle : let modS := Socle_module sG in @@ -3271,7 +3269,7 @@ Lemma Clifford_iso2 x U V : Proof. case=> [f injf homUf defV] Gx; have Gx' := groupVr Gx. pose fx := rG (x^-1)%g *m f *m rG x; exists fx; last 1 first. -- by rewrite !mulmxA repr_mxK //; exact: eqmxMr. +- by rewrite !mulmxA repr_mxK //; apply: eqmxMr. - by rewrite !unitmx_mul andbC !repr_mx_unit. apply/hom_mxP=> h Hh; have Gh := subsetP sHG h Hh. rewrite -(mulmxA U) -repr_mxM // conjgCV repr_mxM ?groupJ // !mulmxA. @@ -3287,10 +3285,10 @@ set simH := mxsimple rH; set cH := component_mx rH. have actG: {in G, forall y M, simH M -> cH M *m rG y <= cH (M *m rG y)}%MS. move=> {M} y Gy /= M simM; have [I [U isoU def_cHM]] := component_mx_def simM. rewrite /cH def_cHM sumsmxMr; apply/sumsmx_subP=> i _. - by apply: mx_iso_component; [exact: Clifford_simple | exact: Clifford_iso2]. + by apply: mx_iso_component; [apply: Clifford_simple | apply: Clifford_iso2]. move=> simM Gx; apply/eqmxP; rewrite actG // -/cH. rewrite -{1}[cH _](repr_mxKV rG Gx) submxMr // -{2}[M](repr_mxK rG Gx). -by rewrite actG ?groupV //; exact: Clifford_simple. +by rewrite actG ?groupV //; apply: Clifford_simple. Qed. Hypothesis irrG : mx_irreducible rG. @@ -3300,7 +3298,7 @@ Lemma Clifford_basis M : mxsimple rH M -> let S := \sum_(x in X) M *m rG x in S :=: 1%:M /\ mxdirect S}%MS. Proof. move=> simM. have simMG (g : [subg G]) : mxsimple rH (M *m rG (val g)). - by case: g => x Gx; exact: Clifford_simple. + by case: g => x Gx; apply: Clifford_simple. have [|XG [defX1 dxX1]] := sum_mxsimple_direct_sub simMG (_ : _ :=: 1%:M)%MS. apply/eqmxP; case irrG => _ _ ->; rewrite ?submx1 //; last first. rewrite -submx0; apply/sumsmx_subP; move/(_ 1%g (erefl _)); apply: negP. @@ -3333,7 +3331,8 @@ Proof. split=> [x W W' eqWW' | W x y Gx Gy]. pose Gx := subgP (subg G x); apply/socleP; apply/eqmxP. rewrite -(repr_mxK rG Gx W) -(repr_mxK rG Gx W'); apply: eqmxMr. - apply: eqmx_trans (eqmx_sym _) (valWact _ _); rewrite -eqWW'; exact: valWact. + apply: eqmx_trans (eqmx_sym _) (valWact _ _). + by rewrite -eqWW'; apply: valWact. apply/socleP; rewrite !{1}valWact 2!{1}(eqmxMr _ (valWact _ _)). by rewrite !subgK ?groupM ?repr_mxM ?mulmxA ?andbb. Qed. @@ -3361,7 +3360,7 @@ have Gx := sXG x Xx; apply/imsetP; exists x => //; apply/socleP/eqmxP/eqmx_sym. apply: eqmx_trans (val_Clifford_act _ Gx) _; rewrite PackSocleK. apply: eqmx_trans (eqmx_sym (Clifford_componentJ simM Gx)) _. apply/eqmxP; rewrite (sameP genmxP eqP) !{1}genmx_component. -by apply/component_mx_isoP=> //; exact: Clifford_simple. +by apply/component_mx_isoP=> //; apply: Clifford_simple. Qed. Lemma Clifford_Socle1 : Socle sH = 1%:M. @@ -3431,15 +3430,15 @@ Proof. rewrite join_subG !subsetI sHG subsetIl /=; apply/andP; split. apply/subsetP=> h Hh; have Gh := subsetP sHG h Hh; rewrite inE. apply/subsetP=> W _; have simW := socle_simple W; have [modW _ _] := simW. - have simWh: mxsimple rH (socle_base W *m rG h) by exact: Clifford_simple. + have simWh: mxsimple rH (socle_base W *m rG h) by apply: Clifford_simple. rewrite inE -val_eqE /= PackSocleK eq_sym. apply/component_mx_isoP; rewrite ?subgK //; apply: component_mx_iso => //. by apply: submx_trans (component_mx_id simW); move/mxmoduleP: modW => ->. apply/subsetP=> z cHz; have [Gz _] := setIP cHz; rewrite inE. apply/subsetP=> W _; have simW := socle_simple W; have [modW _ _] := simW. -have simWz: mxsimple rH (socle_base W *m rG z) by exact: Clifford_simple. +have simWz: mxsimple rH (socle_base W *m rG z) by apply: Clifford_simple. rewrite inE -val_eqE /= PackSocleK eq_sym. -by apply/component_mx_isoP; rewrite ?subgK //; exact: Clifford_iso. +by apply/component_mx_isoP; rewrite ?subgK //; apply: Clifford_iso. Qed. Lemma Clifford_astab1 (W : sH) : 'C[W | 'Cl] = rstabs rG W. @@ -3592,7 +3591,7 @@ split=> [ [/andP[modU modV] maxU] | [[modU maxU] modV maxV]]. by split=> // i ltiU; have:= maxU i (ltnW ltiU); rewrite !nth_rcons leqW ltiU. rewrite modV; split=> // i; rewrite !nth_rcons ltnS leq_eqVlt. case: eqP => [-> _ | /= _ ltiU]; first by rewrite ltnn ?eqxx -last_nth. -by rewrite ltiU; exact: maxU. +by rewrite ltiU; apply: maxU. Qed. Theorem mx_Schreier U : @@ -3620,7 +3619,7 @@ set U' := take i U; set U'' := drop _ U; case/and3P=> incU' ltUi incU''. split=> // W [modW ltUW ltWV]; case: notF. apply: {IH_U}(IH_U (U' ++ W :: Ui :: U'')) noV; last 2 first. - by rewrite /mx_subseries -drop_nth // all_cat /= modW -all_cat defU. -- by rewrite cat_path /= -defU'i; exact/and4P. +- by rewrite cat_path /= -defU'i; apply/and4P. - by rewrite -drop_nth // size_cat /= addnS -size_cat defU addSnnS. by rewrite (subseq_trans sU0U) // -defU cat_subseq // -drop_nth ?subseq_cons. Qed. @@ -3686,7 +3685,7 @@ Qed. 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). -Proof. by apply: section_eqmx_add => //; exact: adds_eqmx. Qed. +Proof. by apply: section_eqmx_add => //; apply: adds_eqmx. Qed. Lemma mx_butterfly U V W modU modV modW : ~~ (U == V)%MS -> max_submod U W -> max_submod V W -> @@ -3696,16 +3695,16 @@ Lemma mx_butterfly U V W modU modV modW : Proof. move=> neUV maxU maxV modUV; have{neUV maxU} defW: (U + V :=: W)%MS. wlog{neUV modUV} ltUV: U V modU modV maxU maxV / ~~ (V <= U)%MS. - by case/nandP: neUV => ?; first rewrite addsmxC; exact. + by case/nandP: neUV => ?; first rewrite addsmxC; apply. apply/eqmxP/idPn=> neUVW; case: maxU => ltUW; case/(_ (U + V)%MS). rewrite addsmx_module // ltmxE ltmxEneq neUVW addsmxSl !addsmx_sub. by have [ltVW _] := maxV; rewrite submx_refl andbT ltUV !ltmxW. have sUV_U := capmxSl U V; have sVW: (V <= W)%MS by rewrite -defW addsmxSr. set goal := mx_rsim _ _; suffices{maxV} simUV: goal. split=> //; apply/(max_submodP modUV modU sUV_U). - by apply: mx_rsim_irr simUV _; exact/max_submodP. + by apply: mx_rsim_irr simUV _; apply/max_submodP. apply: {goal}mx_rsim_sym. -by apply: mx_rsim_trans (mx_second_rsim modU modV) _; exact: section_eqmx. +by apply: mx_rsim_trans (mx_second_rsim modU modV) _; apply: section_eqmx. Qed. Lemma mx_JordanHolder_exists U V : @@ -3719,7 +3718,7 @@ case eqUV: (last 0 U == V)%MS. by rewrite andbC; move/eqmx0P->; exists [::]. rewrite last_rcons; move/eqmxP=> eqU'V; case/mx_series_rcons=> compU _ maxUm'. exists (rcons U' V); last by rewrite last_rcons. - apply/mx_series_rcons; split => //; exact: max_submod_eqmx maxUm'. + by apply/mx_series_rcons; split => //; apply: max_submod_eqmx maxUm'. set Um' := last 0 U in maxUm eqUV; have [modU _] := compU. have modUm': modG Um' by rewrite /Um' (last_nth 0) mx_subseries_module'. have [|||W compW lastW] := IHU (V :&: Um')%MS; rewrite ?capmx_module //. @@ -3771,12 +3770,12 @@ have [eqUVm' | neqUVm'] := altP (@eqmxP _ _ _ _ Um' Vm'). split; first by rewrite szV. exists (lift_perm i_m i_m p) => i; case: (unliftP i_m i) => [j|] ->{i}. apply: rsimT (rsimC _) (rsimT (sim_p j) _). - by rewrite lift_max; exact: rsim_rcons. + by rewrite lift_max; apply: rsim_rcons. by rewrite lift_perm_lift lift_max; apply: rsim_rcons; rewrite -szV. have simUVm := section_eqmx modUm' modVm' modUm modVm eqUVm' eqUVm. apply: rsimT (rsimC _) (rsimT simUVm _); first exact: rsim_last. - by rewrite lift_perm_id /= szV; exact: rsim_last. -have maxVUm: max_submod Vm' Um by exact: max_submod_eqmx (eqmx_sym _) maxVm. + by rewrite lift_perm_id /= szV; apply: rsim_last. +have maxVUm: max_submod Vm' Um by apply: max_submod_eqmx (eqmx_sym _) maxVm. have:= mx_butterfly modUm' modVm' modUm neqUVm' maxUm maxVUm. move: (capmx_module _ _); set Wm := (Um' :&: Vm')%MS => modWm [maxWUm simWVm]. have:= mx_butterfly modVm' modUm' modUm _ maxVUm maxUm. @@ -3795,19 +3794,19 @@ rewrite !permM; case: (unliftP i_m i) => [j {simWUm}|] ->{i}; last first. rewrite lift_perm_id tpermL lift_perm_lift lift_max {simWVm}. apply: rsimT (rsimT (pWV j_m) _); last by apply: rsim_rcons; rewrite -szV. apply: rsimT (rsimC _) {simWUm}(rsimT simWUm _); first exact: rsim_last. - by rewrite -lastW in modWm *; exact: rsim_last. + by rewrite -lastW in modWm *; apply: rsim_last. apply: rsimT (rsimC _) {pUW}(rsimT (pUW j) _). - by rewrite lift_max; exact: rsim_rcons. + by rewrite lift_max; apply: rsim_rcons. rewrite lift_perm_lift; case: (unliftP j_m (pU j)) => [k|] ->{j pU}. rewrite tpermD ?(inj_eq (@lift_inj _ _)) ?neq_lift //. rewrite lift_perm_lift !lift_max; set j := lift j_m k. have ltjW: j < size W by have:= ltn_ord k; rewrite -(lift_max k) /= {1 3}szW. apply: rsimT (rsimT (pWV j) _); last by apply: rsim_rcons; rewrite -szV. - by apply: rsimT (rsimC _) (rsim_rcons compW _ _); first exact: rsim_rcons. + by apply: rsimT (rsimC _) (rsim_rcons compW _ _); first apply: rsim_rcons. apply: rsimT {simWVm}(rsimC (rsimT simWVm _)) _. - by rewrite -lastW in modWm *; exact: rsim_last. + by rewrite -lastW in modWm *; apply: rsim_last. rewrite tpermR lift_perm_id /= szV. -by apply: rsimT (rsim_last modVm' modVm _); exact: section_eqmx. +by apply: rsimT (rsim_last modVm' modVm _); apply: section_eqmx. Qed. Lemma mx_JordanHolder_max U (m := size U) V compU modV : @@ -3818,7 +3817,7 @@ rewrite {}/m; set Um := last 0 U => Um1 irrV. have modUm: modG Um := last_mod compU; have simV := rsimC (mx_factmod_sub modV). have maxV: max_submod V Um. move/max_submodP: (mx_rsim_irr simV irrV) => /(_ (submx1 _)). - by apply: max_submod_eqmx; last exact: eqmx_sym. + by apply: max_submod_eqmx; last apply: eqmx_sym. have [W compW lastW] := mx_JordanHolder_exists compU modV maxV. have compWU: mx_series (rcons W Um) by apply/mx_series_rcons; rewrite lastW. have:= mx_JordanHolder compU compWU; rewrite last_rcons size_rcons. @@ -3920,7 +3919,7 @@ Proof. move=> lastU; have [V [modV simGV]] := rsim_regular_factmod. have irrV := mx_rsim_irr simGV irrG. have [i simVU] := mx_JordanHolder_max compU lastU irrV. -exists i; exact: mx_rsim_trans simGV simVU. +by exists i; apply: mx_rsim_trans simGV simVU. Qed. Hypothesis F'G : [char F]^'.-group G. @@ -3943,7 +3942,7 @@ Local Notation tG := #|pred_of_set (classes (gval G))|. Definition classg_base := \matrix_(k < tG) mxvec (gset_mx (enum_val k)). Let groupCl : {in G, forall x, {subset x ^: G <= G}}. -Proof. by move=> x Gx; apply: subsetP; exact: class_subG. Qed. +Proof. by move=> x Gx; apply: subsetP; apply: class_subG. Qed. Lemma classg_base_free : row_free classg_base. Proof. @@ -3960,7 +3959,7 @@ rewrite rowK !linearZ /= mxvecK -(inj_eq enum_val_inj) def_k eq_sym. have [z Gz ->] := imsetP (enum_valP k'). move/eqP=> not_Gxz; rewrite linear_sum big1 ?scaler0 //= => y zGy. rewrite gring_projE ?(groupCl Gz zGy) //. -by case: eqP zGy => // <- /class_transr. +by case: eqP zGy => // <- /class_eqP. Qed. Lemma classg_base_center : (classg_base :=: 'Z(R_G))%MS. @@ -4080,7 +4079,7 @@ Qed. Lemma degree_irr1 : 'n_1 = 1%N. Proof. apply/eqP; rewrite eqn_leq irr_degree_gt0 -rank_irr1. -by rewrite mxrankS ?component_mx_id //; exact: socle_simple. +by rewrite mxrankS ?component_mx_id //; apply: socle_simple. Qed. Definition Wedderburn_subring (i : sG) := <<i *m R_G>>%MS. @@ -4144,7 +4143,7 @@ Qed. Hypothesis F'G : [char F]^'.-group G. Lemma irr_mx_sum : (\sum_(i : sG) i = 1%:M)%MS. -Proof. by apply: reducible_Socle1; exact: mx_Maschke. Qed. +Proof. by apply: reducible_Socle1; apply: mx_Maschke. Qed. Lemma Wedderburn_sum : (\sum_i 'R_i :=: R_G)%MS. Proof. by apply: eqmx_trans sums_R _; rewrite /Socle irr_mx_sum mul1mx. Qed. @@ -4195,7 +4194,7 @@ Qed. Lemma Wedderburn_is_ring i : mxring 'R_i. Proof. rewrite /mxring /left_mx_ideal Wedderburn_closed submx_refl. -by apply/mxring_idP; exists 'e_i; exact: Wedderburn_is_id. +by apply/mxring_idP; exists 'e_i; apply: Wedderburn_is_id. Qed. Lemma Wedderburn_min_ideal m i (E : 'A_(m, nG)) : @@ -4249,7 +4248,7 @@ transitivity (f *m in_submod _ (val_submod 1%:M *m A) *m f'). rewrite (_ : _ *m A = 0) ?(linear0, mul0mx) //. apply/row_matrixP=> i; rewrite row_mul row0 -[row _ _]gring_mxK -gring_row_mul. rewrite (Wedderburn_mulmx0 ne_iG_j) ?linear0 // genmxE mem_gring_mx. -by rewrite (row_subP _) // val_submod1 component_mx_id //; exact: socle_simple. +by rewrite (row_subP _) // val_submod1 component_mx_id //; apply: socle_simple. Qed. Definition irr_comp := odflt 1%irr [pick i | gring_op rG 'e_i != 0]. @@ -4285,7 +4284,7 @@ by move/eqP: (G0 j). Qed. Lemma irr_comp'_op0 j A : j != iG -> (A \in 'R_j)%MS -> gring_op rG A = 0. -Proof. by rewrite eq_sym; exact: not_rsim_op0 rsim_irr_comp. Qed. +Proof. by rewrite eq_sym; apply: not_rsim_op0 rsim_irr_comp. Qed. Lemma irr_comp_envelop : ('R_iG *m lin_mx (gring_op rG) :=: E_G)%MS. Proof. @@ -4311,7 +4310,7 @@ case/sub_sumsmxP=> e ->; rewrite linear_sum mulmx_suml summx_sub // => j _. rewrite -(in_submodK (submxMl _ (M j))); move: (in_submod _ _) => v. have modMj: mxmodule aG (M j) by apply: mx_iso_module (isoM j) _; case: simMi. have rsimMj: mx_rsim rG (submod_repr modMj). - by apply: mx_rsim_trans rsim_irr_comp _; exact/mx_rsim_iso. + by apply: mx_rsim_trans rsim_irr_comp _; apply/mx_rsim_iso. have [f [f' _ hom_f]] := mx_rsim_def (mx_rsim_sym rsimMj); rewrite submx0. have <-: (gring_mx aG (val_submod (v *m (f *m gring_op rG A *m f')))) = 0. by rewrite (eqP opA0) !(mul0mx, linear0). @@ -4352,13 +4351,13 @@ Qed. Lemma irr_reprK i : irr_comp (irr_repr i) = i. Proof. apply/eqP; apply/component_mx_isoP; try exact: socle_simple. -by move/mx_rsim_iso: (rsim_irr_comp (socle_irr i)); exact: mx_iso_sym. +by move/mx_rsim_iso: (rsim_irr_comp (socle_irr i)); apply: mx_iso_sym. Qed. Lemma irr_repr'_op0 i j A : j != i -> (A \in 'R_j)%MS -> gring_op (irr_repr i) A = 0. Proof. -by move=> neq_ij /irr_comp'_op0-> //; [exact: socle_irr | rewrite irr_reprK]. +by move=> neq_ij /irr_comp'_op0-> //; [apply: socle_irr | rewrite irr_reprK]. Qed. Lemma op_Wedderburn_id i : gring_op (irr_repr i) 'e_i = 1%:M. @@ -4380,7 +4379,7 @@ Lemma irr1_repr x : x \in G -> irr_repr 1 x = 1%:M. Proof. move=> Gx; suffices: x \in rker (irr_repr 1) by case/rkerP. apply: subsetP x Gx; rewrite rker_submod rfix_mx_rstabC // -irr1_rfix. -by apply: component_mx_id; exact: socle_simple. +by apply: component_mx_id; apply: socle_simple. Qed. Hypothesis splitG : group_splitting_field G. @@ -4415,7 +4414,7 @@ Qed. Definition linear_irr := [set i | 'n_i == 1%N]. Lemma irr_degree_abelian : abelian G -> forall i, 'n_i = 1%N. -Proof. by move=> cGG i; exact: mxsimple_abelian_linear (socle_simple i). Qed. +Proof. by move=> cGG i; apply: mxsimple_abelian_linear (socle_simple i). Qed. Lemma linear_irr_comp i : 'n_i = 1%N -> (i :=: socle_base i)%MS. Proof. @@ -4539,25 +4538,25 @@ Lemma card_linear_irr (sG : irrType G) : #|linear_irr sG| = #|G : G^`(1)|%g. Proof. move=> F'G splitG; apply/eqP. -wlog sGq: / irrType (G / G^`(1))%G by exact: socle_exists. +wlog sGq: / irrType (G / G^`(1))%G by apply: socle_exists. have [_ nG'G] := andP (der_normal 1 G); apply/eqP; rewrite -card_quotient //. -have cGqGq: abelian (G / G^`(1))%g by exact: sub_der1_abelian. -have F'Gq: [char F]^'.-group (G / G^`(1))%g by exact: morphim_pgroup. +have cGqGq: abelian (G / G^`(1))%g by apply: sub_der1_abelian. +have F'Gq: [char F]^'.-group (G / G^`(1))%g by apply: morphim_pgroup. have splitGq: group_splitting_field (G / G^`(1))%G. exact: quotient_splitting_field. rewrite -(sum_irr_degree sGq) // -sum1_card. pose rG (j : sGq) := morphim_repr (socle_repr j) nG'G. -have irrG j: mx_irreducible (rG j) by apply/morphim_mx_irr; exact: socle_irr. +have irrG j: mx_irreducible (rG j) by apply/morphim_mx_irr; apply: socle_irr. rewrite (reindex (fun j => irr_comp sG (rG j))) /=. apply: eq_big => [j | j _]; last by rewrite irr_degree_abelian. have [_ lin_j _ _] := rsim_irr_comp sG F'G (irrG j). by rewrite inE -lin_j -irr_degreeE irr_degree_abelian. pose sGlin := {i | i \in linear_irr sG}. have sG'k (i : sGlin) : G^`(1)%g \subset rker (irr_repr (val i)). - by case: i => i /=; rewrite !inE => lin; rewrite rker_linear //=; exact/eqP. + by case: i => i /=; rewrite !inE => lin; rewrite rker_linear //=; apply/eqP. pose h' u := irr_comp sGq (quo_repr (sG'k u) nG'G). have irrGq u: mx_irreducible (quo_repr (sG'k u) nG'G). - by apply/quo_mx_irr; exact: socle_irr. + by apply/quo_mx_irr; apply: socle_irr. exists (fun i => oapp h' [1 sGq]%irr (insub i)) => [j | i] lin_i. rewrite (insubT (mem _) lin_i) /=; apply/esym/eqP/socle_rsimP. apply: mx_rsim_trans (rsim_irr_comp sGq F'Gq (irrGq _)). @@ -4585,7 +4584,7 @@ case: (pickP [pred x in G | ~~ is_scalar_mx (rG x)]) => [x | scalG]. rewrite big_nat_recr //= rmorphM mxrankMfree {IHi}//. rewrite row_free_unit rmorphB /= horner_mx_X horner_mx_C. rewrite (mx_Schur irrG) ?subr_eq0 //; last first. - by apply: contraNneq nscal_rGx => ->; exact: scalar_mx_is_scalar. + by apply: contraNneq nscal_rGx => ->; apply: scalar_mx_is_scalar. rewrite -memmx_cent_envelop linearB. rewrite addmx_sub ?eqmx_opp ?scalar_mx_cent //= memmx_cent_envelop. by apply/centgmxP=> j Zh_j; rewrite -!repr_mxM // (centsP cGG). @@ -4628,13 +4627,13 @@ have /hasP[w _ prim_w]: has #[x].-primitive_root (map r (enum sG)). by rewrite size_map -cardE card_sG. by apply/allP=> _ /mapP[W _ ->]; rewrite unity_rootE rx1. have iphi'P := prim_rootP prim_w (rx1 _); pose iphi' := sval (iphi'P _). -have def_r W: r W = w ^+ iphi' W by exact: svalP (iphi'P W). +have def_r W: r W = w ^+ iphi' W by apply: svalP (iphi'P W). have inj_iphi': injective iphi'. by move=> i j eq_ij; apply: inj_r; rewrite !def_r eq_ij. have iphiP: codom iphi' =i 'I_#[x]. by apply/subset_cardP; rewrite ?subset_predT // card_ord card_image. pose iphi i := iinv (iphiP i); exists w => //; exists iphi. -have iphiK: cancel iphi iphi' by move=> i; exact: f_iinv. +have iphiK: cancel iphi iphi' by move=> i; apply: f_iinv. have r_iphi i: r (iphi i) = w ^+ i by rewrite def_r iphiK. split=> // [|i]; last by rewrite scalX r_iphi. by exists iphi' => // W; rewrite /iphi iinv_f. @@ -4645,7 +4644,7 @@ Lemma splitting_cyclic_primitive_root : classically {z : F | #|G|.-primitive_root z}. Proof. case/cyclicP=> x defG F'G splitF; case=> // IH. -wlog sG: / irrType G by exact: socle_exists. +wlog sG: / irrType G by apply: socle_exists. have [w prim_w _] := cycle_repr_structure sG defG F'G splitF. by apply: IH; exists w. Qed. @@ -4761,10 +4760,10 @@ Lemma dec_mxsimple_exists (U : 'M_n) : Proof. elim: {U}_.+1 {-2}U (ltnSn (\rank U)) => // m IHm U leUm modU nzU. have [nsimU | simU] := mxnonsimpleP nzU; last first. - by exists U; first exact/mxsimpleP. + by exists U; first apply/mxsimpleP. move: (xchooseP nsimU); move: (xchoose _) => W /and4P[modW sWU nzW ltWU]. case: (IHm W) => // [|V simV sVW]; first exact: leq_trans ltWU _. -by exists V; last exact: submx_trans sVW sWU. +by exists V; last apply: submx_trans sVW sWU. Qed. Lemma dec_mx_reducible_semisimple U : @@ -4815,7 +4814,7 @@ case haveU: (mx_sat (exU 0%N (fun U => mxmodule_form rG U /\ ~ meetUVf _ U)%T)). by rewrite andbC -sub_capmx. case/andP=> nzU tiUV; have [M simM sMU] := dec_mxsimple_exists modU nzU. apply: (IHm (M :: Ms)) => [|M']; last first. - by case/predU1P=> [-> //|]; exact: simMs. + by case/predU1P=> [-> //|]; apply: simMs. have [_ nzM _] := simM. suffices ltVMV: \rank V < \rank (span (M :: Ms)). rewrite (leq_trans _ Ms_ge_n) // ltn_sub2l ?(leq_trans ltVMV) //. @@ -4834,12 +4833,12 @@ have sMV: (M <= V)%MS. apply: contra not_sMV => /and3P[nzW Vw Mw]. have{Vw Mw} [sWV sWM]: (W <= V /\ W <= M)%MS. rewrite !cyclic_mx_sub ?(submx_trans (nz_row_sub _)) //. - by rewrite sumsmx_module // => M' _; exact: component_mx_module. + by rewrite sumsmx_module // => M' _; apply: component_mx_module. by rewrite (submx_trans _ sWV) // minM ?cyclic_mx_module. -wlog sG: / socleType rG by exact: socle_exists. +wlog sG: / socleType rG by apply: socle_exists. have sVS: (V <= \sum_(W : sG | has (fun Mi => Mi <= W) Ms) W)%MS. rewrite [V](big_nth 0) big_mkord; apply/sumsmx_subP=> i _. - set Mi := Ms`_i; have MsMi: Mi \in Ms by exact: mem_nth. + set Mi := Ms`_i; have MsMi: Mi \in Ms by apply: mem_nth. have simMi := simMs _ MsMi; have S_Mi := component_socle sG simMi. rewrite (sumsmx_sup (PackSocle S_Mi)) ?PackSocleK //. by apply/hasP; exists Mi; rewrite ?component_mx_id. @@ -4874,12 +4873,12 @@ Qed. Lemma rcent_map A : rcent rGf A^f = rcent rG A. Proof. -by apply/setP=> x; rewrite !inE -!map_mxM inj_eq //; exact: map_mx_inj. +by apply/setP=> x; rewrite !inE -!map_mxM inj_eq //; apply: map_mx_inj. Qed. Lemma rstab_map m (U : 'M_(m, n)) : rstab rGf U^f = rstab rG U. Proof. -by apply/setP=> x; rewrite !inE -!map_mxM inj_eq //; exact: map_mx_inj. +by apply/setP=> x; rewrite !inE -!map_mxM inj_eq //; apply: map_mx_inj. Qed. Lemma rstabs_map m (U : 'M_(m, n)) : rstabs rGf U^f = rstabs rG U. @@ -4967,7 +4966,7 @@ have mf_i V: nth 0^f (mf V) i = (V`_i)^f. case: (ltnP i (size V)) => [ltiV | leVi]; first exact: nth_map. by rewrite !nth_default ?size_map. rewrite -(map_mx0 f) mf_i (mf_i (0 :: U)) => modUi'f modUif modUi' modUi. -by apply: map_section_repr; exact: map_regular_repr. +by apply: map_section_repr; apply: map_regular_repr. Qed. Lemma extend_group_splitting_field : @@ -4978,7 +4977,7 @@ have modU0: all ((mxmodule (regular_repr aF G)) #|G|) [::] by []. apply: (mx_Schreier modU0 _) => // [[U [compU lastU _]]]; have [modU _]:= compU. pose Uf := map ((map_mx f) _ _) U. have{lastU} lastUf: (last 0 Uf :=: 1%:M)%MS. - by rewrite -(map_mx0 f) -(map_mx1 f) last_map; exact/map_eqmx. + by rewrite -(map_mx0 f) -(map_mx1 f) last_map; apply/map_eqmx. have modUf: mx_subseries (regular_repr rF G) Uf. rewrite /mx_subseries all_map; apply: etrans modU; apply: eq_all => Ui /=. rewrite -mxmodule_map; apply: eq_subset_r => x. @@ -4986,7 +4985,7 @@ have modUf: mx_subseries (regular_repr rF G) Uf. have absUf i: i < size U -> mx_absolutely_irreducible (subseries_repr i modUf). move=> lt_i_U; rewrite -(mx_rsim_abs_irr (map_regular_subseries i modU _)). rewrite map_mx_abs_irr; apply: splitG. - by apply: mx_rsim_irr (mx_series_repr_irr compU lt_i_U); exact: section_eqmx. + by apply: mx_rsim_irr (mx_series_repr_irr compU lt_i_U); apply: section_eqmx. have compUf: mx_composition_series (regular_repr rF G) Uf. split=> // i; rewrite size_map => ltiU. move/max_submodP: (mx_abs_irrW (absUf i ltiU)); apply. @@ -4994,7 +4993,7 @@ have compUf: mx_composition_series (regular_repr rF G) Uf. by rewrite map_submx // ltmxW // (pathP _ (mx_series_lt compU)). have [[i ltiU] simUi] := rsim_regular_series irrG compUf lastUf. have{simUi} simUi: mx_rsim rG (subseries_repr i modUf). - by apply: mx_rsim_trans simUi _; exact: section_eqmx. + by apply: mx_rsim_trans simUi _; apply: section_eqmx. by rewrite (mx_rsim_abs_irr simUi) absUf; rewrite size_map in ltiU. Qed. @@ -5138,7 +5137,7 @@ Proof. by move=> x y; rewrite mxvalD mxvalN. Qed. Canonical mxval_additive := Additive mxval_sub. Lemma mxval_is_multiplicative : multiplicative mxval. -Proof. by split; [exact: mxvalM | exact: mxval1]. Qed. +Proof. by split; [apply: mxvalM | apply: mxval1]. Qed. Canonical mxval_rmorphism := AddRMorphism mxval_is_multiplicative. Lemma mxval_centg x : centgmx rG (mxval x). @@ -5196,7 +5195,7 @@ Lemma map_mxminpoly_groot : (map_poly gen pA).[groot] = 0. Proof. (* The [_ groot] prevents divergence of simpl. *) apply: mxval_inj; rewrite -horner_map [_ groot]/= mxval_groot mxval0. rewrite -(mx_root_minpoly A); congr ((_ : {poly _}).[A]). -by apply/polyP=> i; rewrite 3!coef_map; exact: genK. +by apply/polyP=> i; rewrite 3!coef_map; apply: genK. Qed. (* Plugging the extension morphism gen into the ext_repr construction *) @@ -5666,11 +5665,11 @@ Lemma sat_gen_form e f : GRing.rformula f -> Proof. have ExP := Exists_rowP; have set_val := set_nth_map_rVval. elim: f e => //. -- by move=> b e _; exact: (iffP satP). +- by move=> b e _; apply: (iffP satP). - rewrite /gen_form => t1 t2 e rt_t; set t := (_ - _)%T. have:= GRing.qf_evalP (gen_env e) (mxrank_form_qf 0 (gen_term t)). rewrite eval_mxrank mxrank_eq0 eval_gen_term // => tP. - by rewrite (sameP satP tP) /= subr_eq0 val_eqE; exact: eqP. + by rewrite (sameP satP tP) /= subr_eq0 val_eqE; apply: eqP. - move=> f1 IH1 f2 IH2 s /= /andP[/(IH1 s)f1P /(IH2 s)f2P]. by apply: (iffP satP) => [[/satP/f1P ? /satP/f2P] | [/f1P/satP ? /f2P/satP]]. - move=> f1 IH1 f2 IH2 s /= /andP[/(IH1 s)f1P /(IH2 s)f2P]. @@ -5785,7 +5784,7 @@ exists F => //; case=> [|n] rG irrG; first by case/mx_irrP: irrG. apply/idPn=> nabsG; pose cG := ('C(enveloping_algebra_mx rG))%MS. have{nabsG} [A]: exists2 A, (A \in cG)%MS & ~~ is_scalar_mx A. apply/has_non_scalar_mxP; rewrite ?scalar_mx_cent // ltnNge. - by apply: contra nabsG; exact: cent_mx_scalar_abs_irr. + by apply: contra nabsG; apply: cent_mx_scalar_abs_irr. rewrite {cG}memmx_cent_envelop -mxminpoly_linear_is_scalar -ltnNge => cGA. move/(non_linear_gen_reducible irrG cGA). set F' := gen_fieldType _ _; set rG' := @map_repr _ F' _ _ _ _ rG. @@ -5813,7 +5812,7 @@ have{sUV'} defV': V' = U'; last rewrite {V'}defV' in compV'. suffices{irrG'}: mx_irreducible rG' by case/mxsimpleP=> _ _ []. have ltiU': i < size U' by rewrite size_map. apply: mx_rsim_irr (mx_rsim_sym _ ) (mx_series_repr_irr compV' ltiU'). -apply: mx_rsim_trans (mx_rsim_map f' rsimVi) _; exact: map_regular_subseries. +by apply: mx_rsim_trans (mx_rsim_map f' rsimVi) _; apply: map_regular_subseries. Qed. Lemma group_closure_field_exists gT F : @@ -5824,17 +5823,17 @@ set n := #|{group gT}|. suffices: classically {Fs : fieldType & {rmorphism F -> Fs} & forall G : {group gT}, enum_rank G < n -> group_splitting_field Fs G}. - apply: classic_bind => [[Fs f splitFs]] _ -> //. - by exists Fs => // G; exact: splitFs. + by exists Fs => // G; apply: splitFs. elim: (n) => [|i IHi]; first by move=> _ -> //; exists F => //; exists id. apply: classic_bind IHi => [[F' f splitF']]. have [le_n_i _ -> // | lt_i_n] := leqP n i. - by exists F' => // G _; apply: splitF'; exact: leq_trans le_n_i. + by exists F' => // G _; apply: splitF'; apply: leq_trans le_n_i. have:= @group_splitting_field_exists _ (enum_val (Ordinal lt_i_n)) F'. apply: classic_bind => [[Fs f' splitFs]] _ -> //. exists Fs => [|G]; first exact: [rmorphism of (f' \o f)]. rewrite ltnS leq_eqVlt -{1}[i]/(val (Ordinal lt_i_n)) val_eqE. case/predU1P=> [defG | ltGi]; first by rewrite -[G]enum_rankK defG. -by apply: (extend_group_splitting_field f'); exact: splitF'. +by apply: (extend_group_splitting_field f'); apply: splitF'. Qed. Lemma group_closure_closed_field (F : closedFieldType) gT : @@ -5854,7 +5853,7 @@ have [a]: exists a, eigenvalue A a. by rewrite coefN Pd1 mulN1r /= subrr. case/negP; rewrite kermx_eq0 row_free_unit (mx_Schur irrG) ?subr_eq0 //. by rewrite -memmx_cent_envelop -raddfN linearD addmx_sub ?scalar_mx_cent. -by apply: contraNneq nscalA => ->; exact: scalar_mx_is_scalar. +by apply: contraNneq nscalA => ->; apply: scalar_mx_is_scalar. Qed. End BuildSplittingField. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 9071740..922a73c 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -1,17 +1,16 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg poly finalg zmodp cyclic vector ssrnum ssrint intdiv. -From mathcomp.solvable -Require Import sylow pgroup center frobenius. -From mathcomp.field -Require Import algnum algC. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg poly finset. +From mathcomp +Require Import fingroup morphism perm automorphism quotient finalg action. +From mathcomp +Require Import gproduct zmodp commutator cyclic center pgroup sylow frobenius. +From mathcomp +Require Import vector ssrnum ssrint intdiv algC algnum. +From mathcomp Require Import classfun character integral_char. Set Implicit Arguments. @@ -195,11 +194,11 @@ Qed. Lemma zchar_subseq S1 S2 A : subseq S1 S2 -> {subset 'Z[S1, A] <= 'Z[S2, A]}. -Proof. move=> sS12; exact: zchar_subset (mem_subseq sS12). Qed. +Proof. by move/mem_subseq; apply: zchar_subset. Qed. Lemma zchar_filter S A (p : pred 'CF(G)) : {subset 'Z[filter p S, A] <= 'Z[S, A]}. -Proof. by apply: zchar_subset=> f; rewrite mem_filter => /andP[]. Qed. +Proof. by apply: zchar_subset=> f; apply/mem_subseq/filter_subseq. Qed. End Zchar. @@ -297,7 +296,7 @@ Hypotheses (Inu : {in 'Z[S] &, isometry nu}) (oSS : pairwise_orthogonal S). Let freeS := orthogonal_free oSS. Let uniqS : uniq S := free_uniq freeS. -Let Z_S : {subset S <= 'Z[S]}. Proof. by move=> phi; exact: mem_zchar. Qed. +Let Z_S : {subset S <= 'Z[S]}. Proof. by move=> phi; apply: mem_zchar. Qed. Let notS0 : 0 \notin S. Proof. by case/andP: oSS. Qed. Let dotSS := proj2 (pairwise_orthogonalP oSS). @@ -311,7 +310,7 @@ have notSnu0: 0 \notin map nu S. by rewrite -cfnorm_eq0 Inu ?Z_S // cfnorm_eq0 => /eqP <-. apply/pairwise_orthogonalP; split; first by rewrite /= notSnu0 map_inj_in_uniq. move=>_ _ /mapP[phi Sphi ->] /mapP[psi Spsi ->]. -by rewrite (inj_in_eq inj_nu) // Inu ?Z_S //; exact: dotSS. +by rewrite (inj_in_eq inj_nu) // Inu ?Z_S //; apply: dotSS. Qed. Lemma cfproj_sum_orthogonal P z phi : @@ -410,7 +409,7 @@ Lemma cfnorm_orthonormal S : orthonormal S -> '[\sum_(xi <- S) xi] = (size S)%:R. Proof. exact: cfnorm_map_orthonormal. Qed. -Lemma zchar_orthonormalP S : +Lemma vchar_orthonormalP S : {subset S <= 'Z[irr G]} -> reflect (exists I : {set Iirr G}, exists b : Iirr G -> bool, perm_eq S [seq (-1) ^+ b i *: 'chi_i | i in I]) @@ -457,7 +456,7 @@ Lemma vchar_norm1P phi : Proof. move=> Zphi phiN1. have: orthonormal phi by rewrite /orthonormal/= phiN1 eqxx. -case/zchar_orthonormalP=> [xi /predU1P[->|] // | I [b def_phi]]. +case/vchar_orthonormalP=> [xi /predU1P[->|] // | I [b def_phi]]. have: phi \in (phi : seq _) := mem_head _ _. by rewrite (perm_eq_mem def_phi) => /mapP[i _ ->]; exists (b i), i. Qed. @@ -484,7 +483,7 @@ have orthS: orthonormal S. rewrite (leq_exp2r _ 1) // -ltnS -(@ltn_exp2r _ _ 2) //. apply: leq_ltn_trans lt_n_4; rewrite -leC_nat -def_n natrX. rewrite cfdot_sum_irr (bigD1 i) //= -normCK def_m addrC -subr_ge0 addrK. - by rewrite sumr_ge0 // => ? _; exact: mul_conjC_ge0. + by rewrite sumr_ge0 // => ? _; apply: mul_conjC_ge0. have <-: size S = n. by apply/eqP; rewrite -eqC_nat -def_n def_phi cfnorm_orthonormal. exists (in_tuple S); split=> // _ /mapP[i _ ->]. @@ -535,24 +534,14 @@ by rewrite linearZ scale_zchar ?Z_T // -defT map_f ?mem_nth. Qed. Lemma Zisometry_of_iso f : - pairwise_orthogonal S -> {in S, isometry f, to 'Z[irr G]} -> + free S -> {in S, isometry f, to 'Z[irr G]} -> {tau : {linear 'CF(L) -> 'CF(G)} | {in S, tau =1 f} & {in 'Z[S], isometry tau, to 'Z[irr G]}}. Proof. -move=> oS [If Zf]; have [/=/andP[S'0 uS] oSS] := pairwise_orthogonalP oS. -have injf: {in S &, injective f}. - move=> xi1 xi2 Sxi1 Sxi2 /=/(congr1 (cfdot (f xi1)))/eqP; rewrite !If //. - by apply: contraTeq => /oSS-> //; rewrite cfnorm_eq0 (memPn S'0). -have{injf} oSf: pairwise_orthogonal (map f S). - apply/pairwise_orthogonalP; split=> /=. - rewrite map_inj_in_uniq // uS (contra _ S'0) // => /mapP[chi Schi /eqP]. - by rewrite eq_sym -cfnorm_eq0 If // cfnorm_eq0 => /eqP <-. - move=> _ _ /mapP[xi1 Xxi1 ->] /mapP[xi2 Xxi2 ->]. - by rewrite If ?(inj_in_eq injf) // => /oSS->. -have{If} nSf: map cfnorm (map f S) = map cfnorm S. - by rewrite -map_comp; apply/eq_in_map=> xi Sxi; rewrite /= If. -have{Zf} ZSf: {subset map f S <= 'Z[irr G]} by move=> _ /mapP[xi /Zf Zfxi ->]. -by have [tau /eq_in_map] := Zisometry_of_cfnorm oS oSf nSf ZSf; exists tau. +move=> freeS [If Zf]; have [tau Dtau Itau] := isometry_of_free freeS If. +exists tau => //; split; first by apply: sub_in2 Itau; apply: zchar_span. +move=> _ /zchar_nth_expansion[a Za ->]; rewrite linear_sum rpred_sum // => i _. +by rewrite linearZ rpredZ_Cint ?Dtau ?Zf ?mem_nth. Qed. Lemma Zisometry_inj A nu : @@ -584,7 +573,7 @@ by rewrite cfAutZ_Cint // scale_zchar // mem_zchar ?SuS ?mem_nth. Qed. Lemma cfAut_vchar A psi : psi \in 'Z[irr G, A] -> psi^u \in 'Z[irr G, A]. -Proof. by apply: cfAut_zchar; exact: irr_aut_closed. Qed. +Proof. by apply: cfAut_zchar; apply: irr_aut_closed. Qed. Lemma sub_aut_zchar S A psi : {subset S <= 'Z[irr G]} -> psi \in 'Z[S, A] -> psi^u \in 'Z[S, A] -> @@ -797,11 +786,9 @@ Proof. by rewrite /dchi scale1r irr0. Qed. Lemma dirr_dchi i : dchi i \in dirr G. Proof. by apply/dirrP; exists i.1; exists i.2. Qed. -Lemma dIrrP (phi : 'CF(G)) : - reflect (exists i , phi = dchi i) (phi \in dirr G). +Lemma dIrrP phi : reflect (exists i, phi = dchi i) (phi \in dirr G). Proof. -by apply: (iffP idP)=> [/dirrP [b [i ->]]| [i ->]]; - [exists (b, i) | exact: dirr_dchi]. +by apply: (iffP idP)=> [/dirrP[b]|] [i ->]; [exists (b, i) | apply: dirr_dchi]. Qed. Lemma dchi_ndirrE (i : dIirr G) : dchi (ndirr i) = - dchi i. @@ -840,7 +827,7 @@ Qed. Lemma dirr_dIirrE J (f : J -> 'CF(G)) : (forall j, f j \in dirr G) -> forall j, dchi (dirr_dIirr f j) = f j. -Proof. by move=> dirrGf j; exact: (@dirr_dIirrPE _ _ xpredT). Qed. +Proof. by move=> dirrGf j; apply: (@dirr_dIirrPE _ _ xpredT). Qed. Definition dirr_constt (B : {set gT}) (phi: 'CF(B)) : {set (dIirr B)} := [set i | 0 < '[phi, dchi i]]. @@ -909,7 +896,7 @@ Proof. move=> PiZ; rewrite [X in X = _]cfun_sum_constt. *) move=> PiZ; rewrite {1}[phi]cfun_sum_constt. rewrite (reindex (to_dirr phi))=> [/= |]; last first. - by exists (@of_irr _)=> //; exact: of_irrK . + by exists (@of_irr _)=> //; apply: of_irrK . by apply: eq_big=> i; rewrite ?irr_constt_to_dirr // cfdot_todirrE. Qed. |