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/fingroup | |
| parent | f180c539a00fd83d8b3b5fd2d5710eb16e971e2e (diff) | |
Updating files + reorganizing everything
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/Make | 2 | ||||
| -rw-r--r-- | mathcomp/fingroup/action.v | 167 | ||||
| -rw-r--r-- | mathcomp/fingroup/all_fingroup.v (renamed from mathcomp/fingroup/all.v) | 0 | ||||
| -rw-r--r-- | mathcomp/fingroup/automorphism.v | 64 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 350 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 55 | ||||
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 117 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 43 | ||||
| -rw-r--r-- | mathcomp/fingroup/presentation.v | 17 | ||||
| -rw-r--r-- | mathcomp/fingroup/quotient.v | 75 |
10 files changed, 438 insertions, 452 deletions
diff --git a/mathcomp/fingroup/Make b/mathcomp/fingroup/Make index ece5714..90d7618 100644 --- a/mathcomp/fingroup/Make +++ b/mathcomp/fingroup/Make @@ -1,5 +1,5 @@ action.v -all.v +all_fingroup.v automorphism.v fingroup.v gproduct.v diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 3e92be4..685bc18 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -1,10 +1,9 @@ (* (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 fintype bigop finset. -Require Import fingroup morphism perm automorphism quotient. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat div seq fintype. +From mathcomp +Require Import bigop finset fingroup morphism perm automorphism quotient. (******************************************************************************) (* Group action: orbits, stabilisers, transitivity. *) @@ -23,20 +22,20 @@ Require Import fingroup morphism perm automorphism quotient. (* groupAction D R == the structure for group actions of D on R. This *) (* is a telescope on action D rT. *) (* gact_range to == the range R of to : groupAction D R. *) -(* GroupAction toAut == construct a groupAction for action to from *) +(* GroupAction toAut == constructs a groupAction for action to from *) (* toAut : actm to @* D \subset Aut R (actm to is *) (* the morphism to {perm rT} associated to 'to'). *) (* orbit to A x == the orbit of x under the action of A via to. *) (* orbit_transversal to A S == a transversal of the partition orbit to A @: S *) (* of S, provided A acts on S via to. *) -(* amove to A x y == the set of a in A whose action send x to y. *) +(* amove to A x y == the set of a in A whose action sends x to y. *) (* 'C_A[x | to] == the stabiliser of x : rT in A :&: D. *) -(* 'C_A(S | to) == the point-wise stabiliser of S : {set rT} in D :&: A. *) +(* 'C_A(S | to) == the pointwise stabiliser of S : {set rT} in D :&: A. *) (* 'N_A(S | to) == the global stabiliser of S : {set rT} in D :&: A. *) (* 'Fix_(S | to)[a] == the set of fixpoints of a in S. *) (* 'Fix_(S | to)(A) == the set of fixpoints of A in S. *) (* In the first three _A can be omitted and defaults to the domain D of to; *) -(* In the last two S can be omitted and defaults to [set: T], so 'Fix_to[a] *) +(* in the last two S can be omitted and defaults to [set: T], so 'Fix_to[a] *) (* is the set of all fixpoints of a. *) (* The domain restriction ensures that stabilisers have a canonical group *) (* structure, but note that 'Fix sets are generally not groups. Indeed, we *) @@ -44,7 +43,7 @@ Require Import fingroup morphism perm automorphism quotient. (* 'C_(G | to)(A) == the centraliser in R :&: G of the group action of *) (* D :&: A via to *) (* 'C_(G | to)[a] == the centraliser in R :&: G of a \in D, via to. *) -(* These sets are groups when G is. G can be omitted: 'C(|to)(A) is the *) +(* These sets are groups when G is; G can be omitted: 'C(|to)(A) is the *) (* centraliser in R of the action of D :&: A via to. *) (* [acts A, on S | to] == A \subset D acts on the set S via to. *) (* {acts A, on S | to} == A acts on the set S (Prop statement). *) @@ -66,13 +65,13 @@ Require Import fingroup morphism perm automorphism quotient. (* 'P == natural action of a permutation group via aperm. *) (* 'J == internal group action (conjugation) via conjg (_ ^ _). *) (* 'R == regular group action (right translation) via mulg (_ * _). *) -(* (but, to limit ambiguity, _ * _ is NOT a canonical action) *) +(* (However, to limit ambiguity, _ * _ is NOT a canonical action.) *) (* to^* == the action induced by to on {set rT} via to^* (== setact to). *) (* 'Js == the internal action on subsets via _ :^ _, equivalent to 'J^*. *) (* 'Rs == the regular action on subsets via rcoset, equivalent to 'R^*. *) (* 'JG == the conjugation action on {group rT} via (_ :^ _)%G. *) (* to / H == the action induced by to on coset_of H via qact to H, and *) -(* restricted to qact_dom to H == 'N(rcosets H 'N(H) | to^* ). *) +(* restricted to (qact_dom to H) == 'N(rcosets H 'N(H) | to^* ). *) (* 'Q == the action induced to cosets by conjugation; the domain is *) (* qact_dom 'J H, which is provably equal to 'N(H). *) (* to %% A == the action of coset_of A via modact to A, with domain D / A *) @@ -90,7 +89,7 @@ Require Import fingroup morphism perm automorphism quotient. (* be the actual morphism object (e.g., coset_morphism H), not *) (* the underlying function (e.g., coset H). *) (* The explicit application of an action to is usually written (to%act x a), *) -(* where the %act omitted if to is an abstract action or a set action to0^*. *) +(* but %act can be omitted if to is an abstract action or a set action to0^*. *) (* Note that this form will simplify and expose the acting function. *) (* There is a %gact scope for group actions; the notations above are *) (* recognised in %gact when they denote canonical group actions. *) @@ -100,7 +99,7 @@ Require Import fingroup morphism perm automorphism quotient. (* the identity function. If to is a group action with range R *) (* then actm to a is canonically a morphism on R. *) (* We also define here the restriction operation on permutations (the domain *) -(* of this operations is a stabiliser), and local automorphpism groups: *) +(* of this operations is a stabiliser), and local automorphism groups: *) (* restr_perm S p == if p acts on S, the permutation with support in S that *) (* coincides with p on S; else the identity. Note that *) (* restr_perm is a permutation group morphism that maps *) @@ -305,12 +304,12 @@ Lemma mem_setact S a x : x \in S -> to x a \in to^* S a. Proof. exact: mem_imset. Qed. Lemma card_setact S a : #|to^* S a| = #|S|. -Proof. by apply: card_imset; exact: act_inj. Qed. +Proof. by apply: card_imset; apply: act_inj. Qed. Lemma setact_is_action : is_action D to^*. Proof. split=> [a R S eqRS | a b Da Db S]; last first. - rewrite /setact /= -imset_comp; apply: eq_imset => x; exact: actMin. + by rewrite /setact /= -imset_comp; apply: eq_imset => x; apply: actMin. apply/setP=> x; apply/idP/idP=> /(mem_setact a). by rewrite eqRS => /imsetP[y Sy /act_inj->]. by rewrite -eqRS => /imsetP[y Sy /act_inj->]. @@ -335,13 +334,13 @@ by rewrite inE xfix. Qed. Lemma afixS A B : A \subset B -> 'Fix_to(B) \subset 'Fix_to(A). -Proof. by move=> sAB; apply/subsetP=> u; rewrite !inE; exact: subset_trans. Qed. +Proof. by move=> sAB; apply/subsetP=> u; rewrite !inE; apply: subset_trans. Qed. Lemma afixU A B : 'Fix_to(A :|: B) = 'Fix_to(A) :&: 'Fix_to(B). Proof. by apply/setP=> x; rewrite !inE subUset. Qed. Lemma afix1P a x : reflect (to x a = x) (x \in 'Fix_to[a]). -Proof. by rewrite inE sub1set inE; exact: eqP. Qed. +Proof. by rewrite inE sub1set inE; apply: eqP. Qed. Lemma astabIdom S : 'C_D(S | to) = 'C(S | to). Proof. by rewrite setIA setIid. Qed. @@ -423,7 +422,7 @@ Lemma astabCin A S : A \subset D -> (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)). Proof. move=> sAD; apply/subsetP/subsetP=> [sAC x xS | sSF a aA]. - by apply/afixP=> a aA; exact: astab_act (sAC _ aA) xS. + by apply/afixP=> a aA; apply: astab_act (sAC _ aA) xS. rewrite !inE (subsetP sAD _ aA); apply/subsetP=> x xS. by move/afixP/(_ _ aA): (sSF _ xS); rewrite inE => ->. Qed. @@ -463,7 +462,7 @@ Qed. Lemma subset_faithful A B S : B \subset A -> [faithful A, on S | to] -> [faithful B, on S | to]. -Proof. by move=> sAB; apply: subset_trans; exact: setSI. Qed. +Proof. by move=> sAB; apply: subset_trans; apply: setSI. Qed. Section Reindex. @@ -478,7 +477,7 @@ Qed. Lemma reindex_acts A a F : [acts A, on S | to] -> a \in A -> \big[op/idx]_(i in S) F i = \big[op/idx]_(i in S) F (to i a). -Proof. by move=> nSA /(subsetP nSA); exact: reindex_astabs. Qed. +Proof. by move=> nSA /(subsetP nSA); apply: reindex_astabs. Qed. End Reindex. @@ -521,7 +520,7 @@ Proof. by move=> a Da /= x; rewrite -{2}(invgK a) actKin ?groupV. Qed. Lemma setactVin S a : a \in D -> to^* S a^-1 = to^~ a @^-1: S. Proof. -by move=> Da; apply: can2_imset_pre; [exact: actKVin | exact: actKin]. +by move=> Da; apply: can2_imset_pre; [apply: actKVin | apply: actKin]. Qed. Lemma actXin x a i : a \in D -> to x (a ^+ i) = iter i (to^~ a) x. @@ -539,10 +538,10 @@ Proof. by rewrite -{2}(setD1K (group1 G)) afixU afix1 setTI. Qed. Lemma orbit_refl G x : x \in orbit to G x. Proof. by rewrite -{1}[x]act1 mem_orbit. Qed. -Local Notation orbit_rel A := (fun x y => y \in orbit to A x). +Local Notation orbit_rel A := (fun x y => x \in orbit to A y). Lemma contra_orbit G x y : x \notin orbit to G y -> x != y. -Proof. by apply: contraNneq => ->; exact: orbit_refl. Qed. +Proof. by apply: contraNneq => ->; apply: orbit_refl. Qed. Lemma orbit_in_sym G : G \subset D -> symmetric (orbit_rel G). Proof. @@ -552,31 +551,31 @@ Qed. Lemma orbit_in_trans G : G \subset D -> transitive (orbit_rel G). Proof. -move=> sGD _ x _ /imsetP[a Ga ->] /imsetP[b Gb ->]. +move=> sGD _ _ z /imsetP[a Ga ->] /imsetP[b Gb ->]. by rewrite -actMin ?mem_orbit ?groupM // (subsetP sGD). Qed. -Lemma orbit_in_transl G x y : - G \subset D -> y \in orbit to G x -> orbit to G y = orbit to G x. +Lemma orbit_in_eqP G x y : + G \subset D -> reflect (orbit to G x = orbit to G y) (x \in orbit to G y). Proof. -move=> sGD Gxy; apply/setP=> z. -by apply/idP/idP; apply: orbit_in_trans; rewrite // orbit_in_sym. +move=> sGD; apply: (iffP idP) => [yGx|<-]; last exact: orbit_refl. +by apply/setP=> z; apply/idP/idP=> /orbit_in_trans-> //; rewrite orbit_in_sym. Qed. -Lemma orbit_in_transr G x y z : +Lemma orbit_in_transl G x y z : G \subset D -> y \in orbit to G x -> (y \in orbit to G z) = (x \in orbit to G z). Proof. -by move=> sGD Gxy; rewrite !(orbit_in_sym _ z) ?(orbit_in_transl _ Gxy). +by move=> sGD Gxy; rewrite !(orbit_in_sym sGD _ z) (orbit_in_eqP y x sGD Gxy). Qed. Lemma orbit_act_in x a G : G \subset D -> a \in G -> orbit to G (to x a) = orbit to G x. -Proof. by move=> sGD /mem_orbit/orbit_in_transl->. Qed. +Proof. by move=> sGD /mem_orbit/orbit_in_eqP->. Qed. Lemma orbit_actr_in x a G y : G \subset D -> a \in G -> (to y a \in orbit to G x) = (y \in orbit to G x). -Proof. by move=> sGD /mem_orbit/orbit_in_transr->. Qed. +Proof. by move=> sGD /mem_orbit/orbit_in_transl->. Qed. Lemma orbit_inv_in A x y : A \subset D -> (y \in orbit to A^-1 x) = (x \in orbit to A y). @@ -630,7 +629,7 @@ Lemma orbit_partition G S : Proof. move=> actsGS; have sGD := acts_dom actsGS. have eqiG: {in S & &, equivalence_rel [rel x y | y \in orbit to G x]}. - by move=> x y z * /=; rewrite orbit_refl; split=> // /orbit_in_transl->. + by move=> x y z * /=; rewrite orbit_refl; split=> // /orbit_in_eqP->. congr (partition _ _): (equivalence_partitionP eqiG). apply: eq_in_imset => x Sx; apply/setP=> y. by rewrite inE /= andb_idl // => /acts_in_orbit->. @@ -718,7 +717,7 @@ Lemma acts_sub_orbit G S x : [acts G, on S | to] -> (orbit to G x \subset S) = (x \in S). Proof. move/acts_act=> GactS. -apply/subsetP/idP=> [| Sx y]; first by apply; exact: orbit_refl. +apply/subsetP/idP=> [| Sx y]; first by apply; apply: orbit_refl. by case/orbitP=> a Ga <-{y}; rewrite GactS. Qed. @@ -738,7 +737,7 @@ by rewrite /= (afixP Cx) // memJ_norm // groupV (subsetP (normsGI _ _) _ nAa). Qed. Lemma atrans_orbit G x : [transitive G, on orbit to G x | to]. -Proof. by apply: mem_imset; exact: orbit_refl. Qed. +Proof. by apply: mem_imset; apply: orbit_refl. Qed. Section OrbitStabilizer. @@ -757,7 +756,7 @@ Lemma amove_orbit : amove to G x @: orbit to G x = rcosets 'C_G[x | to] G. Proof. apply/setP => Ha; apply/imsetP/rcosetsP=> [[y] | [a Ga ->]]. by case/imsetP=> b Gb -> ->{Ha y}; exists b => //; rewrite amove_act. -by rewrite -amove_act //; exists (to x a); first exact: mem_orbit. +by rewrite -amove_act //; exists (to x a); first apply: mem_orbit. Qed. Lemma amoveK : @@ -842,7 +841,7 @@ Qed. Lemma atransPin G S : G \subset D -> [transitive G, on S | to] -> forall x, x \in S -> orbit to G x = S. -Proof. by move=> sGD /imsetP[y _ ->] x; exact: orbit_in_transl. Qed. +Proof. by move=> sGD /imsetP[y _ ->] x; apply/orbit_in_eqP. Qed. Lemma atransP2in G S : G \subset D -> [transitive G, on S | to] -> @@ -869,7 +868,7 @@ apply: (iffP idP) => [trH | defG]. rewrite -(mulgK b a) mem_mulg ?groupV // !inE groupM //= sub1set inE. by rewrite actMin -?xab. apply/imsetP; exists x => //; apply/setP=> y; rewrite -(atransPin sGD trG Sx). -apply/imsetP/imsetP=> [] [a]; last by exists a; first exact: (subsetP sHG). +apply/imsetP/imsetP=> [] [a]; last by exists a; first apply: (subsetP sHG). rewrite -defG => /imset2P[c b /setIP[_ cxc] Hb ->] ->. exists b; rewrite ?actMin ?(astab_dom cxc) ?(subsetP sHD) //. by rewrite (astab_act cxc) ?inE. @@ -879,9 +878,10 @@ End PartialAction. Arguments Scope orbit_transversal [_ group_scope _ action_scope group_scope group_scope]. +Implicit Arguments orbit_in_eqP [aT D rT to G x y]. Implicit Arguments orbit1P [aT D rT to G x]. Implicit Arguments contra_orbit [aT D rT x y]. -Prenex Implicits orbit1P. +Prenex Implicits orbit_in_eqP orbit1P. Notation "''C' ( S | to )" := (astab_group to S) : Group_scope. Notation "''C_' A ( S | to )" := (setI_group A 'C(S | to)) : Group_scope. @@ -922,33 +922,31 @@ Proof. by rewrite !actM actK. Qed. Lemma actCJV a b x : to (to x a) b = to (to x (b ^ a^-1)) a. Proof. by rewrite (actCJ _ a) conjgKV. Qed. -Lemma orbit_sym G x y : (y \in orbit to G x) = (x \in orbit to G y). -Proof. by apply: orbit_in_sym; exact: subsetT. Qed. +Lemma orbit_sym G x y : (x \in orbit to G y) = (y \in orbit to G x). +Proof. exact/orbit_in_sym/subsetT. Qed. Lemma orbit_trans G x y z : - y \in orbit to G x -> z \in orbit to G y -> z \in orbit to G x. -Proof. by apply: orbit_in_trans; exact: subsetT. Qed. + x \in orbit to G y -> y \in orbit to G z -> x \in orbit to G z. +Proof. exact/orbit_in_trans/subsetT. Qed. -Lemma orbit_transl G x y : y \in orbit to G x -> orbit to G y = orbit to G x. -Proof. -move=> Gxy; apply/setP=> z; apply/idP/idP; apply: orbit_trans => //. -by rewrite orbit_sym. -Qed. +Lemma orbit_eqP G x y : + reflect (orbit to G x = orbit to G y) (x \in orbit to G y). +Proof. exact/orbit_in_eqP/subsetT. Qed. -Lemma orbit_transr G x y z : +Lemma orbit_transl G x y z : y \in orbit to G x -> (y \in orbit to G z) = (x \in orbit to G z). -Proof. by move=> Gxy; rewrite orbit_sym (orbit_transl Gxy) orbit_sym. Qed. +Proof. exact/orbit_in_transl/subsetT. Qed. Lemma orbit_act G a x: a \in G -> orbit to G (to x a) = orbit to G x. -Proof. by move/mem_orbit/orbit_transl; exact. Qed. +Proof. exact/orbit_act_in/subsetT. Qed. Lemma orbit_actr G a x y : a \in G -> (to y a \in orbit to G x) = (y \in orbit to G x). -Proof. by move/mem_orbit/orbit_transr; exact. Qed. +Proof. by move/mem_orbit/orbit_transl; apply. Qed. Lemma orbit_eq_mem G x y : (orbit to G x == orbit to G y) = (x \in orbit to G y). -Proof. by apply/eqP/idP=> [<-|]; [exact: orbit_refl | exact: orbit_transl]. Qed. +Proof. exact: sameP eqP (orbit_eqP G x y). Qed. Lemma orbit_inv A x y : (y \in orbit to A^-1 x) = (x \in orbit to A y). Proof. by rewrite orbit_inv_in ?subsetT. Qed. @@ -971,7 +969,7 @@ by rewrite !inE; apply/subsetP=> x Sx; rewrite inE cSa. Qed. Lemma astab1P x a : reflect (to x a = x) (a \in 'C[x | to]). -Proof. by rewrite !inE sub1set inE; exact: eqP. Qed. +Proof. by rewrite !inE sub1set inE; apply: eqP. Qed. Lemma sub_astab1 A x : (A \subset 'C[x | to]) = (x \in 'Fix_to(A)). Proof. by rewrite sub_astab1_in ?subsetT. Qed. @@ -1031,7 +1029,7 @@ Proof. by rewrite -astab_setact /setact imset_set1. Qed. Lemma atransP G S : [transitive G, on S | to] -> forall x, x \in S -> orbit to G x = S. -Proof. by case/imsetP=> x _ -> y; exact: orbit_transl. Qed. +Proof. by case/imsetP=> x _ -> y; apply/orbit_eqP. Qed. Lemma atransP2 G S : [transitive G, on S | to] -> {in S &, forall x y, exists2 a, a \in G & y = to x a}. @@ -1066,13 +1064,13 @@ rewrite (cardD1 X) {X}X_Gx mem_imset // ltnS leqn0 => /eqP GtrS. apply/imsetP; exists x => //; apply/eqP. rewrite eqEsubset acts_sub_orbit // Sx andbT. apply/subsetP=> y Sy; have:= card0_eq GtrS (orbit to G y). -rewrite !inE /= mem_imset // andbT => /eqP <-; exact: orbit_refl. +by rewrite !inE /= mem_imset // andbT => /eqP <-; apply: orbit_refl. Qed. Lemma atrans_dvd G S : [transitive G, on S | to] -> #|S| %| #|G|. -Proof. by case/imsetP=> x _ ->; exact: dvdn_orbit. Qed. +Proof. by case/imsetP=> x _ ->; apply: dvdn_orbit. Qed. -(* Aschbacher 5.2 *) +(* This is Aschbacher (5.2) *) Lemma acts_fix_norm A B : A \subset 'N(B) -> [acts A, on 'Fix_to(B) | to]. Proof. move=> nAB; have:= acts_subnorm_fix to B; rewrite !setTI. @@ -1084,8 +1082,8 @@ Lemma faithfulP A S : [faithful A, on S | to]. Proof. apply: (iffP subsetP) => [Cto1 a Aa Ca | Cto1 a]. - apply/set1P; rewrite Cto1 // inE Aa; exact/astabP. -case/setIP=> Aa /astabP Ca; apply/set1P; exact: Cto1. + by apply/set1P; rewrite Cto1 // inE Aa; apply/astabP. +by case/setIP=> Aa /astabP Ca; apply/set1P; apply: Cto1. Qed. (* This is the first part of Aschbacher (5.7) *) @@ -1100,13 +1098,13 @@ case/(atransP2 transG Su) => y Gy ->{uy}. by apply/astab1P; rewrite astab1_act (bigcapP cSx). Qed. -(* Aschbacher 5.20 *) +(* This is Aschbacher (5.20) *) Theorem subgroup_transitiveP G H S x : x \in S -> H \subset G -> [transitive G, on S | to] -> reflect ('C_G[x | to] * H = G) [transitive H, on S | to]. -Proof. by move=> Sx sHG; exact: subgroup_transitivePin (subsetT G). Qed. +Proof. by move=> Sx sHG; apply: subgroup_transitivePin (subsetT G). Qed. -(* Aschbacher 5.21 *) +(* This is Aschbacher (5.21) *) Lemma trans_subnorm_fixP x G H S : let C := 'C_G[x | to] in let T := 'Fix_(S | to)(H) in [transitive G, on S | to] -> x \in S -> H \subset C -> @@ -1139,12 +1137,13 @@ Qed. End TotalActions. Implicit Arguments astabP [aT rT to S a]. +Implicit Arguments orbit_eqP [aT rT to G x y]. Implicit Arguments astab1P [aT rT to x a]. Implicit Arguments astabsP [aT rT to S a]. Implicit Arguments atransP [aT rT to G S]. Implicit Arguments actsP [aT rT to A S]. Implicit Arguments faithfulP [aT rT to A S]. -Prenex Implicits astabP astab1P astabsP atransP actsP faithfulP. +Prenex Implicits astabP orbit_eqP astab1P astabsP atransP actsP faithfulP. Section Restrict. @@ -1158,7 +1157,7 @@ Variable sAD : A \subset D. Lemma ract_is_action : is_action A (ract sAD). Proof. rewrite /ract; case: to => f [injf fM]. -split=> // x; exact: (sub_in2 (subsetP sAD)). +by split=> // x; apply: (sub_in2 (subsetP sAD)). Qed. Canonical raction := Action ract_is_action. @@ -1334,14 +1333,14 @@ Qed. Lemma qactEcond x a : x \in 'N(H) -> - quotient_action (coset H x) a = - (if a \in qact_dom then coset H (to x a) else coset H x). + quotient_action (coset H x) a + = coset H (if a \in qact_dom then to x a else x). Proof. move=> Nx; apply: val_inj; rewrite val_subact //= qact_subdomE. have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE mem_imset. case nNa: (a \in _); rewrite // -(astabs_act _ nNa). rewrite !val_coset ?(acts_act acts_qact_dom nNa) //=. -case/rcosetsP=> y Ny defHy; rewrite defHy; apply: rcoset_transl. +case/rcosetsP=> y Ny defHy; rewrite defHy; apply: rcoset_eqP. by rewrite rcoset_sym -defHy (mem_imset (_^~_)) ?rcoset_refl. Qed. @@ -1712,7 +1711,7 @@ Qed. Lemma restr_perm_Aut : restr_perm H @* Aut G \subset Aut H. Proof. -by apply/subsetP=> a'; case/morphimP=> a _ AutGa ->{a'}; exact: Aut_restr_perm. +by apply/subsetP=> a'; case/morphimP=> a _ AutGa ->{a'}; apply: Aut_restr_perm. Qed. Lemma Aut_in_isog : Aut_in (Aut G) H \isog restr_perm H @* Aut G. @@ -1730,11 +1729,11 @@ Proof. rewrite (isog_transl _ Aut_in_isog) /=; set rG := _ @* _. apply: (iffP idP) => [iso_rG h injh hH| AutHinG]. have: aut injh hH \in rG; last case/morphimP=> g nHg AutGg def_g. - suffices ->: rG = Aut H by exact: Aut_aut. + suffices ->: rG = Aut H by apply: Aut_aut. by apply/eqP; rewrite eqEcard restr_perm_Aut /= (card_isog iso_rG). exists (autm_morphism AutGg); rewrite injm_autm im_autm; split=> // x Hx. by rewrite -(autE injh hH Hx) def_g actpermE actbyE. -suffices ->: rG = Aut H by exact: isog_refl. +suffices ->: rG = Aut H by apply: isog_refl. apply/eqP; rewrite eqEsubset restr_perm_Aut /=. apply/subsetP=> h AutHh; have hH := im_autm AutHh. have [g [injg gG eq_gh]] := AutHinG _ (injm_autm AutHh) hH. @@ -1881,7 +1880,7 @@ Variable to : groupAction D R. Lemma actperm_Aut : is_groupAction R to. Proof. by case: to. Qed. Lemma im_actperm_Aut : actperm to @* D \subset Aut R. -Proof. by apply/subsetP=> _ /morphimP[a _ Da ->]; exact: actperm_Aut. Qed. +Proof. by apply/subsetP=> _ /morphimP[a _ Da ->]; apply: actperm_Aut. Qed. Lemma gact_out x a : a \in D -> x \notin R -> to x a = x. Proof. by move=> Da Rx; rewrite -actpermE (out_Aut _ Rx) ?actperm_Aut. Qed. @@ -1893,7 +1892,7 @@ by rewrite Aut_morphic ?actperm_Aut. Qed. Lemma actmM a : {in R &, {morph actm to a : x y / x * y}}. -Proof. rewrite /actm; case: ifP => //; exact: gactM. Qed. +Proof. by rewrite /actm; case: ifP => //; apply: gactM. Qed. Canonical act_morphism a := Morphism (actmM a). @@ -2155,7 +2154,7 @@ rewrite eqEcard (card_preimset _ (act_inj _ _)) leqnn andbT. apply/subsetP=> x Nx; rewrite inE; move/(astabs_act (H :* x)): HDa. rewrite mem_rcosets mulSGid ?normG // Nx => /rcosetsP[y Ny defHy]. suffices: to x a \in H :* y by apply: subsetP; rewrite mul_subG ?sub1set ?normG. -by rewrite -defHy; apply: mem_imset; exact: rcoset_refl. +by rewrite -defHy; apply: mem_imset; apply: rcoset_refl. Qed. Lemma qact_is_groupAction : is_groupAction (R / H) (to / H). @@ -2177,8 +2176,8 @@ Proof. move=> sHR; apply/setP=> a; apply/idP/idP=> nHa; have Da := astabs_dom nHa. rewrite !inE Da; apply/subsetP=> x Hx; rewrite inE -(rcoset1 H). have /rcosetsP[y Ny defHy]: to^~ a @: H \in rcosets H 'N(H). - by rewrite (astabs_act _ nHa) -{1}(mulg1 H) -rcosetE mem_imset ?group1. - by rewrite (@rcoset_transl _ H 1 y) -defHy -1?(gact1 Da) mem_setact. + by rewrite (astabs_act _ nHa); apply/rcosetsP; exists 1; rewrite ?mulg1. + by rewrite (rcoset_eqP (_ : 1 \in H :* y)) -defHy -1?(gact1 Da) mem_setact. rewrite !inE Da; apply/subsetP=> Hx; rewrite inE => /rcosetsP[x Nx ->{Hx}]. apply/imsetP; exists (to x a). case Rx: (x \in R); last by rewrite gact_out ?Rx. @@ -2201,14 +2200,14 @@ Variable H : {group aT}. Lemma modact_is_groupAction : is_groupAction 'C_(|to)(H) (to %% H). Proof. -move=> Ha /morphimP[a Na Da ->]; have NDa: a \in 'N_D(H) by exact/setIP. +move=> Ha /morphimP[a Na Da ->]; have NDa: a \in 'N_D(H) by apply/setIP. rewrite inE; apply/andP; split. apply/subsetP=> x; rewrite 2!inE andbC actpermE /= modactEcond //. by apply: contraR; case: ifP => // E Rx; rewrite gact_out. apply/morphicP=> x y /setIP[Rx cHx] /setIP[Ry cHy]. rewrite /= !actpermE /= !modactE ?gactM //. suffices: x * y \in 'C_(|to)(H) by case/setIP. -rewrite groupM //; exact/setIP. +by rewrite groupM //; apply/setIP. Qed. Canonical mod_groupAction := GroupAction modact_is_groupAction. @@ -2367,7 +2366,7 @@ Proof. have [[_ defD2] [injh _]] := (isomP iso_f, isomP iso_h). move=> sSR1; rewrite (morphimEsub _ sSR1). apply: (morph_astabs (gact_stable to1) (injmP injh)) => // u x. -by move/(subsetP sSR1); exact: hfJ. +by move/(subsetP sSR1); apply: hfJ. Qed. Lemma morph_gastab S : S \subset R1 -> f @* 'C(S | to1) = 'C(h @* S | to2). @@ -2375,7 +2374,7 @@ Proof. have [[_ defD2] [injh _]] := (isomP iso_f, isomP iso_h). move=> sSR1; rewrite (morphimEsub _ sSR1). apply: (morph_astab (gact_stable to1) (injmP injh)) => // u x. -by move/(subsetP sSR1); exact: hfJ. +by move/(subsetP sSR1); apply: hfJ. Qed. Lemma morph_gacent A : A \subset D1 -> h @* 'C_(|to1)(A) = 'C_(|to2)(f @* A). @@ -2653,10 +2652,10 @@ Lemma index_cent1 x : #|G : 'C_G[x]| = #|x ^: G|. Proof. by rewrite -astab1J -card_orbit. Qed. Lemma classes_partition : partition (classes G) G. -Proof. by apply: orbit_partition; apply/actsP=> x Gx y; exact: groupJr. Qed. +Proof. by apply: orbit_partition; apply/actsP=> x Gx y; apply: groupJr. Qed. Lemma sum_card_class : \sum_(C in classes G) #|C| = #|G|. -Proof. by apply: acts_sum_card_orbit; apply/actsP=> x Gx y; exact: groupJr. Qed. +Proof. by apply: acts_sum_card_orbit; apply/actsP=> x Gx y; apply: groupJr. Qed. Lemma class_formula : \sum_(C in classes G) #|G : 'C_G[repr C]| = #|G|. Proof. @@ -2668,7 +2667,7 @@ Qed. Lemma abelian_classP : reflect {in G, forall x, x ^: G = [set x]} (abelian G). Proof. rewrite /abelian -astabJ astabC. -by apply: (iffP subsetP) => cGG x Gx; apply/orbit1P; exact: cGG. +by apply: (iffP subsetP) => cGG x Gx; apply/orbit1P; apply: cGG. Qed. Lemma card_classes_abelian : abelian G = (#|classes G| == #|G|). diff --git a/mathcomp/fingroup/all.v b/mathcomp/fingroup/all_fingroup.v index 903da3c..903da3c 100644 --- a/mathcomp/fingroup/all.v +++ b/mathcomp/fingroup/all_fingroup.v diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index 8c9b0b9..c13a343 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -1,9 +1,8 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat. -From mathcomp.discrete -Require Import fintype finset. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat fintype finset. +From mathcomp Require Import fingroup perm morphism. (******************************************************************************) @@ -13,7 +12,7 @@ Require Import fingroup perm morphism. (* are permutations of type {perm gT} contained in Aut G : {set {perm gT}}. *) (* This lets us use the finGroupType of {perm gT}. Note also that while *) (* morphisms on G are undefined outside G, automorphisms have their support *) -(* in G, i.e., they are the identity ouside G. *) +(* in G, i.e., they are the identity outside G. *) (* Definitions: *) (* Aut G (or [Aut G]) == the automorphism group of G. *) (* [Aut G]%G == the group structure for Aut G. *) @@ -55,7 +54,7 @@ Lemma Aut_morphic A a : a \in Aut A -> morphic A a. Proof. by case/setIdP. Qed. Lemma out_Aut A a x : a \in Aut A -> x \notin A -> a x = x. -Proof. by case/setIdP=> Aa _; exact: out_perm. Qed. +Proof. by case/setIdP=> Aa _; apply: out_perm. Qed. Lemma eq_Aut A : {in Aut A &, forall a b, {in A, a =1 b} -> a = b}. Proof. @@ -91,7 +90,7 @@ Notation f := (autm AutGa). Notation fE := (autmE AutGa). Lemma injm_autm : 'injm f. -Proof. apply/injmP; apply: in2W; exact: perm_inj. Qed. +Proof. by apply/injmP; apply: in2W; apply: perm_inj. Qed. Lemma ker_autm : 'ker f = 1. Proof. by move/trivgP: injm_autm. Qed. @@ -102,7 +101,7 @@ by have:= AutGa; rewrite inE => /andP[/perm_closed <-]; rewrite permKV. Qed. Lemma Aut_closed x : x \in G -> a x \in G. -Proof. by move=> Gx; rewrite -im_autm; exact: mem_morphim. Qed. +Proof. by move=> Gx; rewrite -im_autm; apply: mem_morphim. Qed. End AutGroup. @@ -165,13 +164,13 @@ Lemma morphim_fixP A : A \subset G -> reflect (f @* A = A) (f @* A \subset A). Proof. rewrite /morphim => sAG; have:= eqEcard (f @: A) A. rewrite (setIidPr sAG) card_in_imset ?leqnn ?andbT => [<-|]; first exact: eqP. -move/injmP: injf; apply: sub_in2; exact/subsetP. +by move/injmP: injf; apply: sub_in2; apply/subsetP. Qed. Hypothesis Gf : f @* G = G. Lemma aut_closed : f @: G \subset G. -Proof. by rewrite -morphimEdom; exact/morphim_fixP. Qed. +Proof. by rewrite -morphimEdom; apply/morphim_fixP. Qed. Definition aut := perm_in (injmP injf) aut_closed. @@ -187,7 +186,7 @@ Proof. by rewrite inE morphic_aut perm_in_on. Qed. Lemma imset_autE A : A \subset G -> aut @: A = f @* A. Proof. move=> sAG; rewrite /morphim (setIidPr sAG). -apply: eq_in_imset; apply: sub_in1 autE; exact/subsetP. +by apply: eq_in_imset; apply: sub_in1 autE; apply/subsetP. Qed. Lemma preim_autE A : A \subset G -> aut @^-1: A = f @*^-1 A. @@ -259,7 +258,7 @@ Let domG := subsetP sGD. Lemma im_Aut_isom : Aut_isom injf sGD @* Aut G = Aut (f @* G). Proof. apply/eqP; rewrite eqEcard; apply/andP; split. - by apply/subsetP=> _ /morphimP[a _ AutGa ->]; exact: Aut_Aut_isom. + by apply/subsetP=> _ /morphimP[a _ AutGa ->]; apply: Aut_Aut_isom. have inj_isom' := injm_Aut_isom (injm_invm injf) (morphimS _ sGD). rewrite card_injm ?injm_Aut_isom // -(card_injm inj_isom') ?subset_leq_card //. apply/subsetP=> a /morphimP[a' _ AutfGa' def_a]. @@ -267,7 +266,7 @@ by rewrite -(morphim_invm injf sGD) def_a Aut_Aut_isom. Qed. Lemma Aut_isomP : isom (Aut G) (Aut (f @* G)) (Aut_isom injf sGD). -Proof. by apply/isomP; split; [exact: injm_Aut_isom | exact: im_Aut_isom]. Qed. +Proof. by apply/isomP; split; [apply: injm_Aut_isom | apply: im_Aut_isom]. Qed. Lemma injm_Aut : Aut (f @* G) \isog Aut G. Proof. by rewrite isog_sym (isom_isog _ _ Aut_isomP). Qed. @@ -294,7 +293,7 @@ Proof. by []. Qed. Variable G : {group gT}. Lemma injm_conj x : 'injm (conjgm G x). -Proof. by apply/injmP; apply: in2W; exact: conjg_inj. Qed. +Proof. by apply/injmP; apply: in2W; apply: conjg_inj. Qed. Lemma conj_isom x : isom G (G :^ x) (conjgm G x). Proof. by apply/isomP; rewrite morphim_conj setIid injm_conj. Qed. @@ -303,7 +302,7 @@ Lemma conj_isog x : G \isog G :^ x. Proof. exact: isom_isog (conj_isom x). Qed. Lemma norm_conjg_im x : x \in 'N(G) -> conjgm G x @* G = G. -Proof. by rewrite morphimEdom; exact: normP. Qed. +Proof. by rewrite morphimEdom; apply: normP. Qed. Lemma norm_conj_isom x : x \in 'N(G) -> isom G G (conjgm G x). Proof. by move/norm_conjg_im/restr_isom_to/(_ (conj_isom x))->. Qed. @@ -314,7 +313,7 @@ Lemma norm_conj_autE : {in 'N(G) & G, forall x y, conj_aut x y = y ^ x}. Proof. by move=> x y nGx Gy; rewrite /= autE //= subgK. Qed. Lemma conj_autE : {in G &, forall x y, conj_aut x y = y ^ x}. -Proof. by apply: sub_in11 norm_conj_autE => //; exact: subsetP (normG G). Qed. +Proof. by apply: sub_in11 norm_conj_autE => //; apply: subsetP (normG G). Qed. Lemma conj_aut_morphM : {in 'N(G) &, {morph conj_aut : x y / x * y}}. Proof. @@ -336,7 +335,7 @@ by rewrite perm1 norm_conj_autE // conjgE -cGx ?mulKg. Qed. Lemma Aut_conj_aut A : conj_aut @* A \subset Aut G. -Proof. by apply/subsetP=> _ /imsetP[x _ ->]; exact: Aut_aut. Qed. +Proof. by apply/subsetP=> _ /imsetP[x _ ->]; apply: Aut_aut. Qed. End ConjugationMorphism. @@ -359,17 +358,13 @@ Definition characteristic A B := Infix "\char" := characteristic. Lemma charP H G : - reflect [/\ H \subset G - & forall f : {morphism G >-> gT}, - 'injm f -> f @* G = G -> f @* H = H] - (H \char G). + let fixH (f : {morphism G >-> gT}) := 'injm f -> f @* G = G -> f @* H = H in + reflect [/\ H \subset G & forall f, fixH f] (H \char G). Proof. -apply: (iffP andP) => [] [sHG chHG]; split=> //. - move=> f injf Gf; apply/morphim_fixP=> //. - by have:= forallP chHG (aut injf Gf); rewrite Aut_aut imset_autE. -apply/forall_inP=> f Af; have injf := injm_autm Af. -move/(morphim_fixP injf _ sHG): (chHG _ injf (im_autm Af)). -by rewrite /morphim (setIidPr _). +do [apply: (iffP andP) => -[sHG chHG]; split] => // [f injf Gf|]. + by apply/morphim_fixP; rewrite // -imset_autE ?(forall_inP chHG) ?Aut_aut. +apply/forall_inP=> f Af; rewrite -(autmE Af) -morphimEsub //. +by rewrite chHG ?injm_autm ?im_autm. Qed. (* Characteristic subgroup properties : composition, relational properties *) @@ -385,13 +380,13 @@ Proof. case/charP=> sKH chKH; case/charP=> sHG chHG. apply/charP; split=> [|f injf Gf]; first exact: subset_trans sHG. rewrite -{1}(setIidPr sKH) -(morphim_restrm sHG) chKH //. - rewrite ker_restrm; move/trivgP: injf => ->; exact: subsetIr. + by rewrite ker_restrm; move/trivgP: injf => ->; apply: subsetIr. by rewrite morphim_restrm setIid chHG. Qed. Lemma char_norms H G : H \char G -> 'N(G) \subset 'N(H). Proof. -case/charP=> sHG chHG; apply/normsP=> x /normP Nx. +case/charP=> sHG chHG; apply/normsP=> x /normP-Nx. have:= chHG [morphism of conjgm G x] => /=. by rewrite !morphimEsub //=; apply; rewrite // injm_conj. Qed. @@ -400,7 +395,7 @@ Lemma char_sub A B : A \char B -> A \subset B. Proof. by case/andP. Qed. Lemma char_norm_trans H G A : H \char G -> A \subset 'N(G) -> A \subset 'N(H). -Proof. by move/char_norms=> nHnG nGA; exact: subset_trans nHnG. Qed. +Proof. by move/char_norms=> nHnG nGA; apply: subset_trans nHnG. Qed. Lemma char_normal_trans H G K : K \char H -> H <| G -> K <| G. Proof. @@ -418,10 +413,10 @@ Lemma charI G H K : H \char G -> K \char G -> H :&: K \char G. Proof. case/charP=> sHG chHG; case/charP=> _ chKG. apply/charP; split=> [|f injf Gf]; first by rewrite subIset // sHG. -rewrite morphimGI ?(chHG, chKG) //; exact: subset_trans (sub1G H). +by rewrite morphimGI ?(chHG, chKG) //; apply: subset_trans (sub1G H). Qed. -Lemma charMgen G H K : H \char G -> K \char G -> H <*> K \char G. +Lemma charY G H K : H \char G -> K \char G -> H <*> K \char G. Proof. case/charP=> sHG chHG; case/charP=> sKG chKG. apply/charP; split=> [|f injf Gf]; first by rewrite gen_subG subUset sHG. @@ -430,7 +425,7 @@ Qed. Lemma charM G H K : H \char G -> K \char G -> H * K \char G. Proof. -move=> chHG chKG; rewrite -norm_joinEl ?charMgen //. +move=> chHG chKG; rewrite -norm_joinEl ?charY //. exact: subset_trans (char_sub chHG) (char_norm chKG). Qed. @@ -440,7 +435,7 @@ Lemma lone_subgroup_char G H : Proof. move=> sHG Huniq; apply/charP; split=> // f injf Gf; apply/eqP. have{injf} injf: {in H &, injective f}. - by move/injmP: injf; apply: sub_in2; exact/subsetP. + by move/injmP: injf; apply: sub_in2; apply/subsetP. have fH: f @* H = f @: H by rewrite /morphim (setIidPr sHG). rewrite eqEcard {2}fH card_in_imset ?{}Huniq //=. by rewrite -{3}Gf morphimS. @@ -453,6 +448,7 @@ End Characteristicity. Arguments Scope characteristic [_ group_scope group_scope]. Notation "H \char G" := (characteristic H G) : group_scope. +Hint Resolve char_refl. Section InjmChar. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 9044cd0..40d25ba 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1,9 +1,9 @@ (* (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 choice fintype div path bigop prime finset. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq choice fintype. +From mathcomp +Require Import div path bigop prime finset. (******************************************************************************) (* This file defines the main interface for finite groups : *) @@ -27,7 +27,7 @@ Require Import choice fintype div path bigop prime finset. (* from proofs of the group axioms. *) (* [baseFinGroupType of T] == a clone of an existing baseFinGroupType *) (* structure on T, for T (the existing structure *) -(* might be for som delta-expansion of T). *) +(* might be for some delta-expansion of T). *) (* [finGroupType of T] == a clone of an existing finGroupType structure on *) (* T, for the canonical baseFinGroupType structure *) (* of T (the existing structure might be for the *) @@ -60,7 +60,9 @@ Require Import choice fintype div path bigop prime finset. (* x^-1 == the group inverse of x. *) (* x ^- n == the inverse of x ^+ n (notation for (x ^+ n)^-1). *) (* 1 == the unit element. *) -(* x ^ y == the conjugate of x by y. *) +(* x ^ y == the conjugate of x by y (i.e., y^-1 * (x * y)). *) +(* [~ x, y] == the commutator of x and y (i.e., x^-1 * x ^ y). *) +(* [~ x1, ..., xn] == the commutator of x1, ..., xn (associating left). *) (* \prod_(i ...) x i == the product of the x i (order-sensitive). *) (* commute x y <-> x and y commute. *) (* centralises x A <-> x centralises A. *) @@ -68,17 +70,19 @@ Require Import choice fintype div path bigop prime finset. (* 'C_G[x] == the set of elements of G that commute with x. *) (* <[x]> == the cyclic subgroup generated by the element x. *) (* #[x] == the order of the element x, i.e., #|<[x]>|. *) -(* [~ x1, ..., xn] == the commutator of x1, ..., xn. *) (* Operations on subsets/subgroups of a finite group: *) (* H * G == {xy | x \in H, y \in G}. *) (* 1 or [1] or [1 gT] == the unit group. *) (* [set: gT]%G == the group of all x : gT (in Group_scope). *) +(* group_set G == G contains 1 and is closed under binary product; *) +(* this is the characteristic property of the *) +(* {group gT} subtype of {set gT}. *) (* [subg G] == the subtype, set, or group of all x \in G: this *) (* notation is defined simultaneously in %type, %g *) (* and %G scopes, and G must denote a {group gT} *) (* structure (G is in the %G scope). *) (* subg, sgval == the projection into and injection from [subg G]. *) -(* H^# == the set H minus the unit element *) +(* H^# == the set H minus the unit element. *) (* repr H == some element of H if 1 \notin H != set0, else 1. *) (* (repr is defined over sets of a baseFinGroupType, *) (* so it can be used, e.g., to pick right cosets.) *) @@ -92,20 +96,23 @@ Require Import choice fintype div path bigop prime finset. (* classes G == the set of all conjugate classes of G. *) (* G :^: H == {G :^ x | x \in H}. *) (* class_support G H == {x ^ y | x \in G, y \in H}. *) -(* [~: H1, ..., Hn] == commutator subgroup of H1, ..., Hn. *) -(*{in G, centralised H} <-> G centralises H. *) +(* commg_set G H == {[~ x, y] | x \in G, y \in H}; NOT the commutator! *) +(* <<H>> == the subgroup generated by the set H. *) +(* [~: G, H] == the commmutator subgroup of G and H, i.e., *) +(* <<commg_set G H>>>. *) +(* [~: H1, ..., Hn] == commutator subgroup of H1, ..., Hn (left assoc.). *) +(* H <*> G == the subgroup generated by sets H and G (H join G). *) +(* (H * G)%G == the join of G H : {group gT} (convertible, but not *) +(* identical to (G <*> H)%G). *) +(* (\prod_(i ...) H i)%G == the group generated by the H i. *) +(* {in G, centralised H} <-> G centralises H. *) (* {in G, normalised H} <-> G normalises H. *) (* <-> forall x, x \in G -> H :^ x = H. *) (* 'N(H) == the normaliser of H. *) (* 'N_G(H) == the normaliser of H in G. *) -(* H <| G <=> H is normal in G. *) +(* H <| G <=> H is a normal subgroup of G. *) (* 'C(H) == the centraliser of H. *) (* 'C_G(H) == the centraliser of H in G. *) -(* <<H>> == the subgroup generated by the set H. *) -(* H <*> G == the subgroup generated by sets H and G (H join G). *) -(* (H * G)%G == the join of G H : {group gT} (convertible, but not *) -(* identical to (G <*> H)%G). *) -(* (\prod_(i ...) H i)%G == the group generated by the H i. *) (* gcore H G == the largest subgroup of H normalised by G. *) (* If H is a subgroup of G, this is the largest *) (* normal subgroup of G contained in H). *) @@ -142,7 +149,7 @@ Delimit Scope group_scope with g. Delimit Scope Group_scope with G. (* This module can be imported to open the scope for group element *) -(* operations locally to a file, without exporing the Open to *) +(* operations locally to a file, without exporting the Open to *) (* clients of that file (as Open would do). *) Module GroupScope. Open Scope group_scope. @@ -412,7 +419,7 @@ Lemma invMg x y : (x * y)^-1 = y^-1 * x^-1. Proof. by case: T x y => ? []. Qed. Lemma invg_inj : @injective T T invg. Proof. exact: can_inj invgK. Qed. Lemma eq_invg_sym x y : (x^-1 == y) = (x == y^-1). -Proof. by exact: (inv_eq invgK). Qed. +Proof. by apply: (inv_eq invgK). Qed. Lemma invg1 : 1^-1 = 1 :> T. Proof. by apply: invg_inj; rewrite -{1}[1^-1]mul1g invMg invgK mul1g. Qed. @@ -467,11 +474,11 @@ Proof. by move=> cxy cxz; rewrite /commute -mulgA -cxz !mulgA cxy. Qed. Lemma commuteX x y n : commute x y -> commute x (y ^+ n). Proof. -move=> cxy; elim: n => [|n]; [exact: commute1 | rewrite expgS; exact: commuteM]. +by move=> cxy; case: n; [apply: commute1 | elim=> // n; apply: commuteM]. Qed. Lemma commuteX2 x y m n : commute x y -> commute (x ^+ m) (y ^+ n). -Proof. by move=> cxy; exact/commuteX/commute_sym/commuteX. Qed. +Proof. by move=> cxy; apply/commuteX/commute_sym/commuteX. Qed. Lemma expgVn x n : x^-1 ^+ n = x ^- n. Proof. by elim: n => [|n IHn]; rewrite ?invg1 // expgSr expgS invMg IHn. Qed. @@ -507,7 +514,7 @@ Lemma mulKVg : rev_left_loop invg mulgT. Proof. by move=> x y; rewrite mulgA mulgV mul1g. Qed. Lemma mulgI : right_injective mulgT. -Proof. move=> x; exact: can_inj (mulKg x). Qed. +Proof. by move=> x; apply: can_inj (mulKg x). Qed. Lemma mulgK : right_loop invg mulgT. Proof. by move=> x y; rewrite -mulgA mulgV mulg1. Qed. @@ -516,7 +523,7 @@ Lemma mulgKV : rev_right_loop invg mulgT. Proof. by move=> x y; rewrite -mulgA mulVg mulg1. Qed. Lemma mulIg : left_injective mulgT. -Proof. move=> x; exact: can_inj (mulgK x). Qed. +Proof. by move=> x; apply: can_inj (mulgK x). Qed. Lemma eq_invg_mul x y : (x^-1 == y :> T) = (x * y == 1 :> T). Proof. by rewrite -(inj_eq (@mulgI x)) mulgV eq_sym. Qed. @@ -566,7 +573,7 @@ Lemma conjgKV : @rev_right_loop T T invg conjg. Proof. by move=> y x; rewrite -conjgM mulVg conjg1. Qed. Lemma conjg_inj : @left_injective T T T conjg. -Proof. move=> y; exact: can_inj (conjgK y). Qed. +Proof. by move=> y; apply: can_inj (conjgK y). Qed. Lemma conjg_eq1 x y : (x ^ y == 1) = (x == 1). Proof. by rewrite -(inj_eq (@conjg_inj y) x) conj1g. Qed. @@ -595,10 +602,10 @@ Lemma invg_comm x y : [~ x, y]^-1 = [~ y, x]. Proof. by rewrite commgEr conjVg invMg invgK. Qed. Lemma commgP x y : reflect (commute x y) ([~ x, y] == 1 :> T). -Proof. by rewrite [[~ x, y]]mulgA -invMg -eq_mulVg1 eq_sym; exact: eqP. Qed. +Proof. by rewrite [[~ x, y]]mulgA -invMg -eq_mulVg1 eq_sym; apply: eqP. Qed. Lemma conjg_fixP x y : reflect (x ^ y = x) ([~ x, y] == 1 :> T). -Proof. by rewrite -eq_mulVg1 eq_sym; exact: eqP. Qed. +Proof. by rewrite -eq_mulVg1 eq_sym; apply: eqP. Qed. Lemma commg1_sym x y : ([~ x, y] == 1 :> T) = ([~ y, x] == 1 :> T). Proof. by rewrite -invg_comm (inv_eq invgK) invg1. Qed. @@ -610,13 +617,13 @@ Lemma comm1g x : [~ 1, x] = 1. Proof. by rewrite -invg_comm commg1 invg1. Qed. Lemma commgg x : [~ x, x] = 1. -Proof. by exact/eqP/commgP. Qed. +Proof. exact/eqP/commgP. Qed. Lemma commgXg x n : [~ x, x ^+ n] = 1. Proof. exact/eqP/commgP/commuteX. Qed. Lemma commgVg x : [~ x, x^-1] = 1. -Proof. by exact/eqP/commgP/commuteV. Qed. +Proof. exact/eqP/commgP/commuteV. Qed. Lemma commgXVg x n : [~ x, x ^- n] = 1. Proof. exact/eqP/commgP/commuteV/commuteX. Qed. @@ -654,7 +661,7 @@ by rewrite /repr; case: ifP => // _; case: pickP => // A0; rewrite [x \in A]A0. Qed. Lemma card_mem_repr A : #|A| > 0 -> repr A \in A. -Proof. by rewrite lt0n => /existsP[x]; exact: mem_repr. Qed. +Proof. by rewrite lt0n => /existsP[x]; apply: mem_repr. Qed. Lemma repr_set1 x : repr [set x] = x. Proof. by apply/set1P/card_mem_repr; rewrite cards1. Qed. @@ -818,8 +825,8 @@ Notation "#| B : A |" := (indexg B A) : group_scope. (* No notation for lcoset and rcoset, which are to be used mostly *) (* in curried form; x *: B and A :* 1 denote singleton products, *) -(* so thus we can use mulgA, mulg1, etc, on, say, A :* 1 * B :* x. *) -(* No notation for the set commutator generator set set_commg. *) +(* so we can use mulgA, mulg1, etc, on, say, A :* 1 * B :* x. *) +(* No notation for the set commutator generator set commg_set. *) Notation "''N' ( A )" := (normaliser A) : group_scope. Notation "''N_' G ( A )" := (G%g :&: 'N(A)) : group_scope. @@ -856,24 +863,20 @@ Lemma prodsgP (I : finType) (P : pred I) (A : I -> {set gT}) x : (x \in \prod_(i | P i) A i). Proof. rewrite -big_filter filter_index_enum; set r := enum P. -pose inA c i := c i \in A i; set RHS := x \in _. -suffices IHr: reflect (exists2 c, all (inA c) r & x = \prod_(i <- r) c i) RHS. - apply: (iffP IHr) => [][c inAc ->]. - rewrite -[r]filter_index_enum big_filter; exists c => // i Pi. - by apply: (allP inAc); rewrite mem_enum. - rewrite -big_filter filter_index_enum; exists c => //; apply/allP=> i. - rewrite mem_enum; exact: inAc. -have: uniq r by [rewrite enum_uniq]; rewrite {}/RHS. -elim: {P}r x => /= [x _|i r IHr x /andP[r'i Ur]]. - by rewrite unlock; apply: (iffP set1P) => [-> | [] //]; exists (fun _ => 1). +pose inA c := all (fun i => c i \in A i); set piAx := x \in _. +suffices IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx. + apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_filter]. + by move=> i Pi; rewrite (allP inAc) ?mem_enum. + by apply/allP=> i; rewrite mem_enum => /inAc. +have: uniq r by rewrite enum_uniq. +elim: {P}r x @piAx => /= [x _ | i r IHr x /andP[r'i /IHr{IHr}IHr]]. + by rewrite unlock; apply: (iffP set1P) => [-> | [] //]; exists (fun=> x). rewrite big_cons; apply: (iffP idP) => [|[c /andP[Aci Ac] ->]]; last first. by rewrite big_cons mem_mulg //; apply/IHr=> //; exists c. -case/mulsgP=> y _ Ai_y /IHr[//| c Ac ->] ->{x}. -exists [eta c with i |-> y] => /=. - rewrite /inA /= eqxx Ai_y; apply/allP=> j rj. - by case: eqP rj r'i => [-> -> // | _ rj _]; exact: (allP Ac). -rewrite big_cons eqxx !big_seq; congr (_ * _). -by apply: eq_bigr => j rj; case: eqP rj r'i => // -> ->. +case/mulsgP=> c_i _ Ac_i /IHr[c /allP-inAcr ->] ->{x}. +exists [eta c with i |-> c_i]; rewrite /= ?big_cons eqxx ?Ac_i. + by apply/allP=> j rj; rewrite /= ifN ?(memPn r'i) ?inAcr. +by congr (_ * _); apply: eq_big_seq => j rj; rewrite ifN ?(memPn r'i). Qed. Lemma mem_prodg (I : finType) (P : pred I) (A : I -> {set gT}) c : @@ -925,7 +928,7 @@ Lemma memV_invg x A : (x^-1 \in A^-1) = (x \in A). Proof. by rewrite inE invgK. Qed. Lemma card_invg A : #|A^-1| = #|A|. -Proof. by apply: card_preimset; exact: invg_inj. Qed. +Proof. exact/card_preimset/invg_inj. Qed. (* Product with singletons. *) @@ -938,7 +941,7 @@ Lemma mulg_set1 x y : [set x] :* y = [set x * y]. Proof. by rewrite [_ * _]imset2_set1l imset_set1. Qed. Lemma invg_set1 x : [set x]^-1 = [set x^-1]. -Proof. by apply/setP=> y; rewrite !inE inv_eq //; exact: invgK. Qed. +Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed. End BaseSetMulProp. @@ -964,7 +967,7 @@ Lemma mem_lcoset A x y : (y \in x *: A) = (x^-1 * y \in A). Proof. by rewrite -lcosetE [_ x](can_imset_pre _ (mulKg _)) inE. Qed. Lemma lcosetP A x y : reflect (exists2 a, a \in A & y = x * a) (y \in x *: A). -Proof. rewrite -lcosetE; exact: imsetP. Qed. +Proof. by rewrite -lcosetE; apply: imsetP. Qed. Lemma lcosetsP A B C : reflect (exists2 x, x \in B & C = x *: A) (C \in lcosets A B). @@ -983,7 +986,7 @@ Lemma lcosetKV : rev_left_loop invg (fun x A => x *: A). Proof. by move=> x A; rewrite -lcosetM mulgV mul1g. Qed. Lemma lcoset_inj : right_injective (fun x A => x *: A). -Proof. by move=> x; exact: can_inj (lcosetK x). Qed. +Proof. by move=> x; apply: can_inj (lcosetK x). Qed. Lemma lcosetS x A B : (x *: A \subset x *: B) = (A \subset B). Proof. @@ -1009,7 +1012,7 @@ Lemma mem_rcoset A x y : (y \in A :* x) = (y * x^-1 \in A). Proof. by rewrite -rcosetE [_ x](can_imset_pre A (mulgK _)) inE. Qed. Lemma rcosetP A x y : reflect (exists2 a, a \in A & y = a * x) (y \in A :* x). -Proof. by rewrite -rcosetE; exact: imsetP. Qed. +Proof. by rewrite -rcosetE; apply: imsetP. Qed. Lemma rcosetsP A B C : reflect (exists2 x, x \in B & C = A :* x) (C \in rcosets A B). @@ -1028,7 +1031,7 @@ Lemma rcosetKV : rev_right_loop invg (fun A x => A :* x). Proof. by move=> x A; rewrite -rcosetM mulVg mulg1. Qed. Lemma rcoset_inj : left_injective (fun A x => A :* x). -Proof. by move=> x; exact: can_inj (rcosetK x). Qed. +Proof. by move=> x; apply: can_inj (rcosetK x). Qed. Lemma rcosetS x A B : (A :* x \subset B :* x) = (A \subset B). Proof. @@ -1042,14 +1045,11 @@ Proof. by rewrite -(rcosetS x^-1) rcosetK. Qed. Lemma sub_rcosetV x A B : (A \subset B :* x^-1) = (A :* x \subset B). Proof. by rewrite sub_rcoset invgK. Qed. -(* Inverse map lcosets to rcosets *) - -Lemma lcosets_invg A B : lcosets A^-1 B^-1 = invg @^-1: rcosets A B. +(* Inverse maps lcosets to rcosets *) +Lemma invg_lcosets A B : (lcosets A B)^-1 = rcosets A^-1 B^-1. Proof. -apply/setP=> C; rewrite inE. -apply/imsetP/imsetP=> [] [a]; rewrite -memV_invg ?invgK => Aa; - try move/(canRL invgK); move->; exists a^-1; - by rewrite // lcosetE rcosetE invMg invg_set1 ?invgK. +rewrite /A^-1/= - -[RHS]imset_comp -imset_comp. +by apply: eq_imset => x /=; rewrite lcosetE rcosetE invMg invg_set1. Qed. (* Conjugates. *) @@ -1082,7 +1082,7 @@ Lemma conjsgKV : @rev_right_loop _ gT invg conjugate. Proof. by move=> x A; rewrite -conjsgM mulVg conjsg1. Qed. Lemma conjsg_inj : @left_injective _ gT _ conjugate. -Proof. by move=> x; exact: can_inj (conjsgK x). Qed. +Proof. by move=> x; apply: can_inj (conjsgK x). Qed. Lemma cardJg A x : #|A :^ x| = #|A|. Proof. by rewrite (card_imset _ (conjg_inj x)). Qed. @@ -1232,7 +1232,7 @@ Lemma group_setP A : Proof. apply: (iffP andP) => [] [A1 AM]; split=> {A1}//. by move=> x y Ax Ay; apply: (subsetP AM); rewrite mem_mulg. -apply/subsetP=> _ /mulsgP[x y Ax Ay ->]; exact: AM. +by apply/subsetP=> _ /mulsgP[x y Ax Ay ->]; apply: AM. Qed. Structure group_type : Type := Group { @@ -1402,14 +1402,14 @@ Definition cardG_gt0_reduced : 0 < card (@mem gT (predPredType gT) G) Lemma indexg_gt0 A : 0 < #|G : A|. Proof. rewrite lt0n; apply/existsP; exists A. -rewrite -{2}[A]mulg1 -rcosetE; exact: mem_imset. +by rewrite -{2}[A]mulg1 -rcosetE; apply: mem_imset. Qed. Lemma trivgP : reflect (G :=: 1) (G \subset [1]). -Proof. by rewrite subG1; exact: eqP. Qed. +Proof. by rewrite subG1; apply: eqP. Qed. Lemma trivGP : reflect (G = 1%G) (G \subset [1]). -Proof. by rewrite subG1; exact: eqP. Qed. +Proof. by rewrite subG1; apply: eqP. Qed. Lemma proper1G : ([1] \proper G) = (G :!=: 1). Proof. by rewrite properEneq sub1G andbT eq_sym. Qed. @@ -1481,12 +1481,12 @@ Lemma groupVl x : x^-1 \in G -> x \in G. Proof. by move/groupVr; rewrite invgK. Qed. Lemma groupV x : (x^-1 \in G) = (x \in G). -Proof. by apply/idP/idP; [exact: groupVl | exact: groupVr]. Qed. +Proof. by apply/idP/idP; [apply: groupVl | apply: groupVr]. Qed. Lemma groupMl x y : x \in G -> (x * y \in G) = (y \in G). Proof. -move=> Gx; apply/idP/idP=> Gy; last exact: groupM. -rewrite -(mulKg x y); exact: groupM (groupVr _) _. +move=> Gx; apply/idP/idP=> [Gxy|]; last exact: groupM. +by rewrite -(mulKg x y) groupM ?groupVr. Qed. Lemma groupMr x y : x \in G -> (y * x \in G) = (y \in G). @@ -1505,7 +1505,7 @@ Proof. by move=> Gx Gy; rewrite !in_group. Qed. Lemma group_prod I r (P : pred I) F : (forall i, P i -> F i \in G) -> \prod_(i <- r | P i) F i \in G. -Proof. by move=> G_P; elim/big_ind: _ => //; exact: groupM. Qed. +Proof. by move=> G_P; elim/big_ind: _ => //; apply: groupM. Qed. (* Inverse is an anti-morphism. *) @@ -1549,20 +1549,20 @@ Proof. by rewrite mem_lcoset mulVg group1. Qed. Lemma lcoset_sym x y : (x \in y *: G) = (y \in x *: G). Proof. by rewrite !mem_lcoset -groupV invMg invgK. Qed. -Lemma lcoset_transl x y : x \in y *: G -> x *: G = y *: G. +Lemma lcoset_eqP {x y} : reflect (x *: G = y *: G) (x \in y *: G). Proof. -move=> Gyx; apply/setP=> u; rewrite !mem_lcoset in Gyx *. -by rewrite -{2}(mulKVg x u) mulgA (groupMl _ Gyx). +suffices <-: (x *: G == y *: G) = (x \in y *: G) by apply: eqP. +by rewrite eqEsubset !mulSG !sub1set lcoset_sym andbb. Qed. -Lemma lcoset_transr x y z : x \in y *: G -> (x \in z *: G) = (y \in z *: G). -Proof. by move=> Gyx; rewrite -2!(lcoset_sym z) (lcoset_transl Gyx). Qed. +Lemma lcoset_transl x y z : x \in y *: G -> (x \in z *: G) = (y \in z *: G). +Proof. by move=> Gyx; rewrite -2!(lcoset_sym z) (lcoset_eqP Gyx). Qed. Lemma lcoset_trans x y z : x \in y *: G -> y \in z *: G -> x \in z *: G. -Proof. by move/lcoset_transr->. Qed. +Proof. by move/lcoset_transl->. Qed. Lemma lcoset_id x : x \in G -> x *: G = G. -Proof. rewrite -{-2}(mul1g G); exact: lcoset_transl. Qed. +Proof. by move=> Gx; rewrite (lcoset_eqP (_ : x \in 1 *: G)) mul1g. Qed. (* Right cosets, with an elimination form for repr. *) @@ -1572,20 +1572,20 @@ Proof. by rewrite mem_rcoset mulgV group1. Qed. Lemma rcoset_sym x y : (x \in G :* y) = (y \in G :* x). Proof. by rewrite -!memV_lcosetV lcoset_sym. Qed. -Lemma rcoset_transl x y : x \in G :* y -> G :* x = G :* y. +Lemma rcoset_eqP {x y} : reflect (G :* x = G :* y) (x \in G :* y). Proof. -move=> Gyx; apply: invg_inj; rewrite !invg_rcoset. -by apply: lcoset_transl; rewrite memV_lcosetV. +suffices <-: (G :* x == G :* y) = (x \in G :* y) by apply: eqP. +by rewrite eqEsubset !mulGS !sub1set rcoset_sym andbb. Qed. -Lemma rcoset_transr x y z : x \in G :* y -> (x \in G :* z) = (y \in G :* z). -Proof. by move=> Gyx; rewrite -2!(rcoset_sym z) (rcoset_transl Gyx). Qed. +Lemma rcoset_transl x y z : x \in G :* y -> (x \in G :* z) = (y \in G :* z). +Proof. by move=> Gyx; rewrite -2!(rcoset_sym z) (rcoset_eqP Gyx). Qed. -Lemma rcoset_trans x y z : y \in G :* x -> z \in G :* y -> z \in G :* x. +Lemma rcoset_trans x y z : x \in G :* y -> y \in G :* z -> x \in G :* z. Proof. by move/rcoset_transl->. Qed. Lemma rcoset_id x : x \in G -> G :* x = G. -Proof. by rewrite -{-2}(mulg1 G); exact: rcoset_transl. Qed. +Proof. by move=> Gx; rewrite (rcoset_eqP (_ : x \in G :* 1)) mulg1. Qed. (* Elimination form. *) @@ -1603,22 +1603,20 @@ by rewrite -[repr _](mulgKV x); split; rewrite -mem_rcoset mem_repr_rcoset. Qed. Lemma rcoset_repr x : G :* (repr (G :* x)) = G :* x. -Proof. by apply: rcoset_transl; exact: mem_repr (rcoset_refl x). Qed. +Proof. exact/rcoset_eqP/mem_repr_rcoset. Qed. (* Coset spaces. *) -Lemma mem_lcosets A x : (x *: G \in lcosets G A) = (x \in A * G). +Lemma mem_rcosets A x : (G :* x \in rcosets G A) = (x \in G * A). Proof. -apply/imsetP/mulsgP=> [[a Aa eqxaG] | [a g Aa Gg ->{x}]]. - exists a (a^-1 * x); rewrite ?mulKVg //. - by rewrite -mem_lcoset -lcosetE -eqxaG lcoset_refl. -by exists a; rewrite // lcosetM lcosetE lcoset_id. +apply/rcosetsP/mulsgP=> [[a Aa /rcoset_eqP/rcosetP[g]] | ]; first by exists g a. +by case=> g a Gg Aa ->{x}; exists a; rewrite // rcosetM rcoset_id. Qed. -Lemma mem_rcosets A x : (G :* x \in rcosets G A) = (x \in G * A). +Lemma mem_lcosets A x : (x *: G \in lcosets G A) = (x \in A * G). Proof. -rewrite -memV_invg invMg invGid -mem_lcosets. -by rewrite -{4}invGid lcosets_invg inE invg_lcoset invgK. +rewrite -[LHS]memV_invg invg_lcoset invg_lcosets. +by rewrite -[RHS]memV_invg invMg invGid mem_rcosets. Qed. (* Conjugates. *) @@ -1650,17 +1648,19 @@ Lemma classGidr x : {in G, normalised (x ^: G)}. Proof. by move=> y Gy /=; rewrite -class_rcoset rcoset_id. Qed. Lemma class_refl x : x \in x ^: G. -Proof. by apply/imsetP; exists (1 : gT); rewrite ?conjg1. Qed. +Proof. by apply/imsetP; exists 1; rewrite ?conjg1. Qed. Hint Resolve class_refl. -Lemma class_transr x y : x \in y ^: G -> x ^: G = y ^: G. -Proof. by case/imsetP=> z Gz ->; rewrite classGidl. Qed. +Lemma class_eqP x y : reflect (x ^: G = y ^: G) (x \in y ^: G). +Proof. +by apply: (iffP idP) => [/imsetP[z Gz ->] | <-]; rewrite ?class_refl ?classGidl. +Qed. Lemma class_sym x y : (x \in y ^: G) = (y \in x ^: G). -Proof. by apply/idP/idP=> /class_transr->. Qed. +Proof. by apply/idP/idP=> /class_eqP->. Qed. Lemma class_transl x y z : x \in y ^: G -> (x \in z ^: G) = (y \in z ^: G). -Proof. by rewrite -!(class_sym z) => /class_transr->. Qed. +Proof. by rewrite -!(class_sym z) => /class_eqP->. Qed. Lemma class_trans x y z : x \in y ^: G -> y \in z ^: G -> x \in z ^: G. Proof. by move/class_transl->. Qed. @@ -1668,7 +1668,7 @@ Proof. by move/class_transl->. Qed. Lemma repr_class x : {y | y \in G & repr (x ^: G) = x ^ y}. Proof. set z := repr _; have: #|[set y in G | z == x ^ y]| > 0. - have: z \in x ^: G by exact: (mem_repr x). + have: z \in x ^: G by apply: (mem_repr x). by case/imsetP=> y Gy ->; rewrite (cardD1 y) inE Gy eqxx. by move/card_mem_repr; move: (repr _) => y /setIdP[Gy /eqP]; exists y. Qed. @@ -1693,7 +1693,7 @@ by have [y Gy ->] := repr_class x; rewrite classGidl ?groupJ. Qed. Lemma mem_repr_classes xG : xG \in classes G -> repr xG \in xG. -Proof. by case/repr_classesP=> _ {2}->; exact: class_refl. Qed. +Proof. by case/repr_classesP=> _ {2}->; apply: class_refl. Qed. Lemma classes_gt0 : 0 < #|classes G|. Proof. by rewrite (cardsD1 1) classes1. Qed. @@ -1703,7 +1703,7 @@ Proof. rewrite (cardsD1 1) classes1 ltnS lt0n cards_eq0. apply/set0Pn/trivgPn=> [[xG /setD1P[nt_xG]] | [x Gx ntx]]. by case/imsetP=> x Gx def_xG; rewrite def_xG classG_eq1 in nt_xG; exists x. -by exists (x ^: G); rewrite !inE classG_eq1 ntx; exact: mem_imset. +by exists (x ^: G); rewrite !inE classG_eq1 ntx; apply: mem_imset. Qed. Lemma mem_class_support A x : x \in A -> x \in class_support A G. @@ -1722,7 +1722,7 @@ Qed. Lemma class_support_subG A : A \subset G -> class_support A G \subset G. Proof. -by move=> sAG; rewrite class_supportEr; apply/bigcupsP=> x Gx; exact: conj_subG. +by move=> sAG; rewrite class_supportEr; apply/bigcupsP=> x Gx; apply: conj_subG. Qed. Lemma sub_class_support A : A \subset class_support A G. @@ -1768,12 +1768,12 @@ Definition subg_one := Subg group1. Definition subg_inv u := Subg (groupVr (subgP u)). Definition subg_mul u v := Subg (groupM (subgP u) (subgP v)). Lemma subg_oneP : left_id subg_one subg_mul. -Proof. move=> u; apply: val_inj; exact: mul1g. Qed. +Proof. by move=> u; apply: val_inj; apply: mul1g. Qed. Lemma subg_invP : left_inverse subg_one subg_inv subg_mul. -Proof. move=> u; apply: val_inj; exact: mulVg. Qed. +Proof. by move=> u; apply: val_inj; apply: mulVg. Qed. Lemma subg_mulP : associative subg_mul. -Proof. move=> u v w; apply: val_inj; exact: mulgA. Qed. +Proof. by move=> u v w; apply: val_inj; apply: mulgA. Qed. Definition subFinGroupMixin := FinGroup.Mixin subg_mulP subg_oneP subg_invP. Canonical subBaseFinGroupType := @@ -1788,7 +1788,7 @@ Definition subg : gT -> subg_of := insubd (1 : subg_of). Lemma subgK x : x \in G -> val (subg x) = x. Proof. by move=> Gx; rewrite insubdK. Qed. Lemma sgvalK : cancel sgval subg. -Proof. case=> x Gx; apply: val_inj; exact: subgK. Qed. +Proof. by case=> x Gx; apply: val_inj; apply: subgK. Qed. Lemma subg_default x : (x \in G) = false -> val (subg x) = 1. Proof. by move=> Gx; rewrite val_insubd Gx. Qed. Lemma subgM : {in G &, {morph subg : x y / x * y}}. @@ -1811,22 +1811,20 @@ Lemma mulGSid G H : H \subset G -> G * H = G. Proof. exact: mulGSgid (group1 H). Qed. Lemma mulGidPl G H : reflect (G * H = G) (H \subset G). -Proof. by apply: (iffP idP) => [|<-]; [exact: mulGSid | exact: mulG_subr]. Qed. +Proof. by apply: (iffP idP) => [|<-]; [apply: mulGSid | apply: mulG_subr]. Qed. Lemma mulGidPr G H : reflect (G * H = H) (G \subset H). -Proof. by apply: (iffP idP) => [|<-]; [exact: mulSGid | exact: mulG_subl]. Qed. +Proof. by apply: (iffP idP) => [|<-]; [apply: mulSGid | apply: mulG_subl]. Qed. Lemma comm_group_setP G H : reflect (commute G H) (group_set (G * H)). Proof. rewrite /group_set (subsetP (mulG_subl _ _)) ?group1 // andbC. have <-: #|G * H| <= #|H * G| by rewrite -invMG card_invg. -rewrite -mulgA mulGS mulgA mulSG -eqEcard eq_sym; exact: eqP. +by rewrite -mulgA mulGS mulgA mulSG -eqEcard eq_sym; apply: eqP. Qed. Lemma card_lcosets G H : #|lcosets H G| = #|G : H|. -Proof. -by rewrite -[#|G : H|](card_preimset _ invg_inj) -lcosets_invg !invGid. -Qed. +Proof. by rewrite -card_invg invg_lcosets !invGid. Qed. (* Group Modularity equations *) @@ -1861,11 +1859,14 @@ Bind Scope group_scope with subg_of. Implicit Arguments trivgP [gT G]. Implicit Arguments trivGP [gT G]. +Implicit Arguments lcoset_eqP [gT G x y]. +Implicit Arguments rcoset_eqP [gT G x y]. Implicit Arguments mulGidPl [gT G H]. Implicit Arguments mulGidPr [gT G H]. Implicit Arguments comm_group_setP [gT G H]. +Implicit Arguments class_eqP [gT G x y]. Implicit Arguments repr_classesP [gT G xG]. -Prenex Implicits trivgP trivGP comm_group_setP. +Prenex Implicits trivgP trivGP lcoset_eqP rcoset_eqP comm_group_setP class_eqP. Section GroupInter. @@ -1887,8 +1888,7 @@ Variables (I : finType) (P : pred I) (F : I -> {group gT}). Lemma group_set_bigcap : group_set (\bigcap_(i | P i) F i). Proof. -elim/big_rec: _ => [|i G _ gG]; first exact: groupP. -exact: group_setI (Group gG). +by elim/big_rec: _ => [|i G _ gG]; rewrite -1?(insubdK 1%G gG) groupP. Qed. Canonical bigcap_group := group group_set_bigcap. @@ -1901,6 +1901,10 @@ Canonical commutator_group A B : {group _} := Eval hnf in [group of [~: A, B]]. Canonical joing_group A B : {group _} := Eval hnf in [group of A <*> B]. Canonical cycle_group x : {group _} := Eval hnf in [group of <[x]>]. +Definition joinG G H := joing_group G H. + +Definition subgroups A := [set G : {group gT} | G \subset A]. + Lemma order_gt0 (x : gT) : 0 < #[x]. Proof. exact: cardG_gt0. Qed. @@ -1908,13 +1912,9 @@ End GroupInter. Hint Resolve order_gt0. -Definition joinG (gT : finGroupType) (G H : {group gT}) := joing_group G H. - -Definition subgroups (gT : finGroupType) (G : {set gT}) := - [set H : {group gT} | H \subset G]. - Arguments Scope generated_group [_ group_scope]. Arguments Scope joing_group [_ group_scope group_scope]. +Arguments Scope subgroups [_ group_scope]. Notation "G :&: H" := (setI_group G H) : Group_scope. Notation "<< A >>" := (generated_group A) : Group_scope. @@ -1923,7 +1923,7 @@ Notation "[ ~: A1 , A2 , .. , An ]" := (commutator_group .. (commutator_group A1 A2) .. An) : Group_scope. Notation "A <*> B" := (joing_group A B) : Group_scope. Notation "G * H" := (joinG G H) : Group_scope. -Prenex Implicits joinG. +Prenex Implicits joinG subgroups. Notation "\prod_ ( i <- r | P ) F" := (\big[joinG/1%G]_(i <- r | P%B) F%G) : Group_scope. @@ -1960,8 +1960,7 @@ Proof. rewrite -[#|G|]sum1_card (partition_big_imset (rcoset H)) /=. rewrite mulnC -sum_nat_const; apply: eq_bigr => _ /rcosetsP[x Gx ->]. rewrite -(card_rcoset _ x) -sum1_card; apply: eq_bigl => y. -rewrite rcosetE eqEcard mulGS !card_rcoset leqnn andbT. -by rewrite group_modr sub1set // inE. +by rewrite rcosetE (sameP eqP rcoset_eqP) group_modr (sub1set, inE). Qed. Lemma divgI G H : #|G| %/ #|G :&: H| = #|G : H|. @@ -1995,10 +1994,10 @@ Lemma divg_indexS G H : H \subset G -> #|G| %/ #|G : H| = #|H|. Proof. by move/Lagrange <-; rewrite mulnK. Qed. Lemma coprimeSg G H p : H \subset G -> coprime #|G| p -> coprime #|H| p. -Proof. by move=> sHG; exact: coprime_dvdl (cardSg sHG). Qed. +Proof. by move=> sHG; apply: coprime_dvdl (cardSg sHG). Qed. Lemma coprimegS G H p : H \subset G -> coprime p #|G| -> coprime p #|H|. -Proof. by move=> sHG; exact: coprime_dvdr (cardSg sHG). Qed. +Proof. by move=> sHG; apply: coprime_dvdr (cardSg sHG). Qed. Lemma indexJg G H x : #|G :^ x : H :^ x| = #|G : H|. Proof. by rewrite -!divgI -conjIg !cardJg. Qed. @@ -2051,26 +2050,23 @@ Proof. by rewrite -divgS ?sub1G // cards1 divn1. Qed. Lemma indexMg G A : #|G * A : G| = #|A : G|. Proof. -congr #|(_ : {set _})|; apply/eqP; rewrite eqEsubset andbC imsetS ?mulG_subr //. -by apply/subsetP=> _ /imsetP[x GAx ->]; rewrite rcosetE mem_rcosets. +apply/eq_card/setP/eqP; rewrite eqEsubset andbC imsetS ?mulG_subr //. +by apply/subsetP=> _ /rcosetsP[x GAx ->]; rewrite mem_rcosets. Qed. Lemma rcosets_partition_mul G H : partition (rcosets H G) (H * G). Proof. -have eqiR: {in H * G & &, equivalence_rel [rel x y | y \in rcoset H x]}. - by move=> *; rewrite /= !rcosetE rcoset_refl; split=> // /rcoset_transl->. -congr (partition _ _): (equivalence_partitionP eqiR); apply/setP=> Hx. -apply/imsetP/idP=> [[x HGx defHx] | /rcosetsP[x Gx ->]]. - suffices ->: Hx = H :* x by rewrite mem_rcosets. - apply/setP=> y; rewrite defHx inE /= rcosetE andb_idl //. - by apply: subsetP y; rewrite mulGS sub1set. -exists (1 * x); rewrite ?mem_mulg // mul1g. -apply/setP=> y; rewrite inE /= rcosetE andb_idl //. -by apply: subsetP y; rewrite mulgS ?sub1set. +set HG := H * G; have sGHG: {subset G <= HG} by apply/subsetP/mulG_subr. +have defHx x: x \in HG -> [set y in HG | rcoset H x == rcoset H y] = H :* x. + move=> HGx; apply/setP=> y; rewrite inE !rcosetE (sameP eqP rcoset_eqP). + by rewrite rcoset_sym; apply/andb_idl/subsetP; rewrite mulGS sub1set. +have:= preim_partitionP (rcoset H) HG; congr (partition _ _); apply/setP=> Hx. +apply/imsetP/idP=> [[x HGx ->] | ]; first by rewrite defHx // mem_rcosets. +by case/rcosetsP=> x /sGHG-HGx ->; exists x; rewrite ?defHx. Qed. Lemma rcosets_partition G H : H \subset G -> partition (rcosets H G) G. -Proof. by move/mulSGid=> {2}<-; exact: rcosets_partition_mul. Qed. +Proof. by move=> sHG; have:= rcosets_partition_mul G H; rewrite mulSGid. Qed. Lemma LagrangeMl G H : (#|G| * #|H : G|)%N = #|G * H|. Proof. @@ -2111,9 +2107,9 @@ Qed. Lemma prime_TIg G H : prime #|G| -> ~~ (G \subset H) -> G :&: H = 1. Proof. -case/primeP=> _; move/(_ _ (cardSg (subsetIl G H))). -rewrite (sameP setIidPl eqP) eqEcard subsetIl -ltnNge ltn_neqAle -trivg_card1. -by case/predU1P=> ->. +case/primeP=> _ /(_ _ (cardSg (subsetIl G H))). +rewrite (sameP setIidPl eqP) eqEcard subsetIl => /pred2P[/card1_trivg|] //= ->. +by case/negP. Qed. Lemma prime_meetG G H : prime #|G| -> G :&: H != 1 -> G \subset H. @@ -2145,7 +2141,7 @@ Lemma subset_gen A : A \subset <<A>>. Proof. exact/bigcapsP. Qed. Lemma sub_gen A B : A \subset B -> A \subset <<B>>. -Proof. by move/subset_trans=> -> //; exact: subset_gen. Qed. +Proof. by move/subset_trans=> -> //; apply: subset_gen. Qed. Lemma mem_gen x A : x \in A -> x \in <<A>>. Proof. exact: subsetP (subset_gen A) x. Qed. @@ -2163,10 +2159,10 @@ Lemma genGid G : <<G>> = G. Proof. by apply/eqP; rewrite eqEsubset gen_subG subset_gen andbT. Qed. Lemma genGidG G : <<G>>%G = G. -Proof. by apply: val_inj; exact: genGid. Qed. +Proof. by apply: val_inj; apply: genGid. Qed. Lemma gen_set_id A : group_set A -> <<A>> = A. -Proof. by move=> gA; exact: (genGid (group gA)). Qed. +Proof. by move=> gA; apply: (genGid (group gA)). Qed. Lemma genS A B : A \subset B -> <<A>> \subset <<B>>. Proof. by move=> sAB; rewrite gen_subG sub_gen. Qed. @@ -2279,19 +2275,19 @@ by rewrite joingE (setUidPl sHG) genGid. Qed. Lemma joing_idPr A G : reflect (A <*> G = G) (A \subset G). -Proof. by rewrite joingC; exact: joing_idPl. Qed. +Proof. by rewrite joingC; apply: joing_idPl. Qed. Lemma joing_subP A B G : reflect (A \subset G /\ B \subset G) (A <*> B \subset G). -Proof. by rewrite join_subG; exact: andP. Qed. +Proof. by rewrite join_subG; apply: andP. Qed. Lemma joing_sub A B C : A <*> B = C -> A \subset C /\ B \subset C. -Proof. by move <-; exact/joing_subP. Qed. +Proof. by move <-; apply/joing_subP. Qed. Lemma genDU A B C : A \subset C -> <<C :\: A>> = <<B>> -> <<A :|: B>> = <<C>>. Proof. move=> sAC; rewrite -joingE -joing_idr => <- {B}; rewrite joing_idr. -by congr <<_>>; rewrite setDE setUIr setUCr setIT; exact/setUidPr. +by congr <<_>>; rewrite setDE setUIr setUCr setIT; apply/setUidPr. Qed. Lemma joingA : associative joingT. @@ -2314,7 +2310,7 @@ Lemma mulG_subG G H K : (G * H \subset K) = (G \subset K) && (H \subset K). Proof. by rewrite -gen_subG genM_join join_subG. Qed. Lemma mulGsubP K H G : reflect (K \subset G /\ H \subset G) (K * H \subset G). -Proof. by rewrite mulG_subG; exact: andP. Qed. +Proof. by rewrite mulG_subG; apply: andP. Qed. Lemma mulG_sub K H A : K * H = A -> K \subset A /\ H \subset A. Proof. by move <-; rewrite mulG_subl mulG_subr. Qed. @@ -2326,20 +2322,20 @@ Qed. Lemma comm_joingE G H : commute G H -> G <*> H = G * H. Proof. -by move/comm_group_setP=> gGH; rewrite -genM_join; exact: (genGid (group gGH)). +by move/comm_group_setP=> gGH; rewrite -genM_join; apply: (genGid (group gGH)). Qed. Lemma joinGC : commutative joinGT. -Proof. by move=> G H; apply: val_inj; exact: joingC. Qed. +Proof. by move=> G H; apply: val_inj; apply: joingC. Qed. Lemma joinGA : associative joinGT. -Proof. by move=> G H K; apply: val_inj; exact: joingA. Qed. +Proof. by move=> G H K; apply: val_inj; apply: joingA. Qed. Lemma join1G : left_id 1%G joinGT. -Proof. by move=> G; apply: val_inj; exact: joing1G. Qed. +Proof. by move=> G; apply: val_inj; apply: joing1G. Qed. Lemma joinG1 : right_id 1%G joinGT. -Proof. by move=> G; apply: val_inj; exact: joingG1. Qed. +Proof. by move=> G; apply: val_inj; apply: joingG1. Qed. Canonical joinG_law := Monoid.Law joinGA join1G joinG1. Canonical joinG_abelaw := Monoid.ComLaw joinGC. @@ -2373,12 +2369,12 @@ Proof. by move=> sAB sCD; rewrite genS ?imset2S. Qed. Lemma der1_subG G : [~: G, G] \subset G. Proof. -by rewrite gen_subG; apply/subsetP=> _ /imset2P[x y Gx Gy ->]; exact: groupR. +by rewrite gen_subG; apply/subsetP=> _ /imset2P[x y Gx Gy ->]; apply: groupR. Qed. Lemma comm_subG A B G : A \subset G -> B \subset G -> [~: A, B] \subset G. Proof. -by move=> sAG sBG; apply: subset_trans (der1_subG G); exact: commgSS. +by move=> sAG sBG; apply: subset_trans (der1_subG G); apply: commgSS. Qed. Lemma commGC A B : [~: A, B] = [~: B, A]. @@ -2468,7 +2464,7 @@ Qed. Lemma cycleP x y : reflect (exists i, y = x ^+ i) (y \in <[x]>). Proof. -by apply: (iffP idP) => [/cyclePmin[i _]|[i ->]]; [exists i | exact: mem_cycle]. +by apply: (iffP idP) => [/cyclePmin[i _]|[i ->]]; [exists i | apply: mem_cycle]. Qed. Lemma expg_order x : x ^+ #[x] = 1. @@ -2497,7 +2493,7 @@ Lemma invg2id x : #[x] = 2 -> x^-1 = x. Proof. by move=> ox; rewrite invg_expg ox. Qed. Lemma cycleX x i : <[x ^+ i]> \subset <[x]>. -Proof. rewrite cycle_subG; exact: mem_cycle. Qed. +Proof. by rewrite cycle_subG; apply: mem_cycle. Qed. Lemma cycleV x : <[x^-1]> = <[x]>. Proof. @@ -2524,7 +2520,7 @@ Implicit Type G H K : {group gT}. Lemma normP x A : reflect (A :^ x = A) (x \in 'N(A)). Proof. -suffices ->: (x \in 'N(A)) = (A :^ x == A) by exact: eqP. +suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP. by rewrite eqEcard cardJg leqnn andbT inE. Qed. Implicit Arguments normP [x A]. @@ -2540,7 +2536,7 @@ Canonical normaliser_group A := group (group_set_normaliser A). Lemma normsP A B : reflect {in A, normalised B} (A \subset 'N(B)). Proof. apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //. -by apply/normP; exact: nBA. +by apply/normP; apply: nBA. Qed. Implicit Arguments normsP [A B]. @@ -2560,13 +2556,13 @@ Lemma normCs A : 'N(~: A) = 'N(A). Proof. by apply/setP=> x; rewrite -groupV !inE conjCg setCS sub_conjg. Qed. Lemma normG G : G \subset 'N(G). -Proof. by apply/normsP; exact: conjGid. Qed. +Proof. by apply/normsP; apply: conjGid. Qed. Lemma normT : 'N([set: gT]) = [set: gT]. Proof. by apply/eqP; rewrite -subTset normG. Qed. Lemma normsG A G : A \subset G -> A \subset 'N(G). -Proof. move=> sAG; exact: subset_trans (normG G). Qed. +Proof. by move=> sAG; apply: subset_trans (normG G). Qed. Lemma normC A B : A \subset 'N(B) -> commute A B. Proof. @@ -2580,7 +2576,7 @@ Lemma norm_joinEl G H : G \subset 'N(H) -> G <*> H = G * H. Proof. by move/normC/comm_joingE. Qed. Lemma norm_joinEr G H : H \subset 'N(G) -> G <*> H = G * H. -Proof. by move/normC=> cHG; exact: comm_joingE. Qed. +Proof. by move/normC=> cHG; apply: comm_joingE. Qed. Lemma norm_rlcoset G x : x \in 'N(G) -> G :* x = x *: G. Proof. by rewrite -sub1set => /normC. Qed. @@ -2604,7 +2600,7 @@ Lemma norm_gen A : 'N(A) \subset 'N(<<A>>). Proof. by apply/normsP=> x Nx; rewrite -genJ (normP Nx). Qed. Lemma class_norm x G : G \subset 'N(x ^: G). -Proof. by apply/normsP=> y; exact: classGidr. Qed. +Proof. by apply/normsP=> y; apply: classGidr. Qed. Lemma class_normal x G : x \in G -> x ^: G <| G. Proof. by move=> Gx; rewrite /normal class_norm class_subG. Qed. @@ -2616,7 +2612,7 @@ by case/imsetP=> y Gy ->; rewrite memJ_norm ?(subsetP nAG). Qed. Lemma class_support_norm A G : G \subset 'N(class_support A G). -Proof. by apply/normsP; exact: class_supportGidr. Qed. +Proof. by apply/normsP; apply: class_supportGidr. Qed. Lemma class_support_sub_norm A B G : A \subset G -> B \subset 'N(G) -> class_support A B \subset G. @@ -2756,7 +2752,7 @@ Proof. by move=> nAG; rewrite /normal subsetIl normsI ?normG. Qed. Lemma normalGI G H A : H \subset G -> A <| G -> H :&: A <| H. Proof. -by move=> sHG /andP[_ nAG]; exact: norm_normalI (subset_trans sHG nAG). +by move=> sHG /andP[_ nAG]; apply: norm_normalI (subset_trans sHG nAG). Qed. Lemma normal_subnorm G H : (H <| 'N_G(H)) = (H \subset G). @@ -2860,16 +2856,16 @@ by apply/subsetP=> _ /imsetP[y Ay ->]; rewrite /conjg -cAx ?mulKg. Qed. Lemma cents_norm A B : A \subset 'C(B) -> A \subset 'N(B). -Proof. by move=> cAB; exact: subset_trans (cent_sub B). Qed. +Proof. by move=> cAB; apply: subset_trans (cent_sub B). Qed. Lemma centC A B : A \subset 'C(B) -> commute A B. -Proof. by move=> cAB; exact: normC (cents_norm cAB). Qed. +Proof. by move=> cAB; apply: normC (cents_norm cAB). Qed. Lemma cent_joinEl G H : G \subset 'C(H) -> G <*> H = G * H. -Proof. by move=> cGH; exact: norm_joinEl (cents_norm cGH). Qed. +Proof. by move=> cGH; apply: norm_joinEl (cents_norm cGH). Qed. Lemma cent_joinEr G H : H \subset 'C(G) -> G <*> H = G * H. -Proof. by move=> cGH; exact: norm_joinEr (cents_norm cGH). Qed. +Proof. by move=> cGH; apply: norm_joinEr (cents_norm cGH). Qed. Lemma centJ A x : 'C(A :^ x) = 'C(A) :^ x. Proof. @@ -2882,7 +2878,7 @@ Lemma cent_norm A : 'N(A) \subset 'N('C(A)). Proof. by apply/normsP=> x nCx; rewrite -centJ (normP nCx). Qed. Lemma norms_cent A B : A \subset 'N(B) -> A \subset 'N('C(B)). -Proof. move=> nBA; exact: subset_trans nBA (cent_norm B). Qed. +Proof. by move=> nBA; apply: subset_trans nBA (cent_norm B). Qed. Lemma cent_normal A : 'C(A) <| 'N(A). Proof. by rewrite /(_ <| _) cent_sub cent_norm. Qed. @@ -2891,11 +2887,11 @@ Lemma centS A B : B \subset A -> 'C(A) \subset 'C(B). Proof. by move=> sAB; rewrite centsC (subset_trans sAB) 1?centsC. Qed. Lemma centsS A B C : A \subset B -> C \subset 'C(B) -> C \subset 'C(A). -Proof. by move=> sAB cCB; exact: subset_trans cCB (centS sAB). Qed. +Proof. by move=> sAB cCB; apply: subset_trans cCB (centS sAB). Qed. Lemma centSS A B C D : A \subset C -> B \subset D -> C \subset 'C(D) -> A \subset 'C(B). -Proof. move=> sAC sBD cCD; exact: subset_trans (centsS sBD cCD). Qed. +Proof. by move=> sAC sBD cCD; apply: subset_trans (centsS sBD cCD). Qed. Lemma centI A B : 'C(A) <*> 'C(B) \subset 'C(A :&: B). Proof. by rewrite gen_subG subUset !centS ?(subsetIl, subsetIr). Qed. @@ -2916,7 +2912,7 @@ Lemma sub_cent1 A x : (A \subset 'C[x]) = (x \in 'C(A)). Proof. by rewrite -cent_cycle centsC cycle_subG. Qed. Lemma cents_cycle x y : commute x y -> <[x]> \subset 'C(<[y]>). -Proof. move=> cxy; rewrite cent_cycle cycle_subG; exact/cent1P. Qed. +Proof. by move=> cxy; rewrite cent_cycle cycle_subG; apply/cent1P. Qed. Lemma cycle_abelian x : abelian <[x]>. Proof. exact: cents_cycle. Qed. @@ -2939,7 +2935,7 @@ Lemma commG1P A B : reflect ([~: A, B] = 1) (A \subset 'C(B)). Proof. apply: (iffP (centsP A B)) => [cAB | cAB1 x Ax y By]. apply/trivgP; rewrite gen_subG; apply/subsetP=> _ /imset2P[x y Ax Ay ->]. - by rewrite inE; apply/commgP; exact: cAB. + by rewrite inE; apply/commgP; apply: cAB. by apply/commgP; rewrite -in_set1 -[[set 1]]cAB1 mem_commg. Qed. @@ -2948,7 +2944,7 @@ Lemma abelianE A : abelian A = (A \subset 'C(A)). Proof. by []. Qed. Lemma abelian1 : abelian [1 gT]. Proof. exact: sub1G. Qed. Lemma abelianS A B : A \subset B -> abelian B -> abelian A. -Proof. by move=> sAB; exact: centSS. Qed. +Proof. by move=> sAB; apply: centSS. Qed. Lemma abelianJ A x : abelian (A :^ x) = abelian A. Proof. by rewrite /abelian centJ conjSg. Qed. @@ -2976,7 +2972,7 @@ Lemma sub_abelian_cent : C \subset A -> A \subset 'C(C). Proof. by move=> sCA; rewrite centsC (subset_trans sCA). Qed. Lemma sub_abelian_cent2 : B \subset A -> C \subset A -> B \subset 'C(C). -Proof. by move=> sBA; move/sub_abelian_cent; exact: subset_trans. Qed. +Proof. by move=> sBA; move/sub_abelian_cent; apply: subset_trans. Qed. Lemma sub_abelian_norm : C \subset A -> A \subset 'N(C). Proof. by move=> sCA; rewrite cents_norm ?sub_abelian_cent. Qed. @@ -3048,7 +3044,7 @@ Lemma mingroupP : Proof. apply: (iffP minsetP); rewrite /= groupP genGidG /= => [] [-> minG]. by split=> // H gPH sGH; apply: minG; rewrite // groupP genGidG. -split=> // A; case/andP=> gA gPA; rewrite -(gen_set_id gA); exact: minG. +by split=> // A; case/andP=> gA gPA; rewrite -(gen_set_id gA); apply: minG. Qed. Lemma maxgroupP : @@ -3056,7 +3052,7 @@ Lemma maxgroupP : Proof. apply: (iffP maxsetP); rewrite /= groupP genGidG /= => [] [-> maxG]. by split=> // H gPH sGH; apply: maxG; rewrite // groupP genGidG. -split=> // A; case/andP=> gA gPA; rewrite -(gen_set_id gA); exact: maxG. +by split=> // A; case/andP=> gA gPA; rewrite -(gen_set_id gA); apply: maxG. Qed. Lemma maxgroupp : maxgroup G -> gP G. Proof. by case/maxgroupP. Qed. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 2706df6..39f19cc 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -1,10 +1,9 @@ (* (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 bigop finset. -Require Import fingroup morphism quotient action. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import bigop finset fingroup morphism quotient action. (******************************************************************************) (* Partial, semidirect, central, and direct products. *) @@ -19,7 +18,7 @@ Require Import fingroup morphism quotient action. (* [splits G, over K] == [complements to K in G] is not empty. *) (* remgr A B x == the right remainder in B of x mod A, i.e., *) (* some element of (A :* x) :&: B. *) -(* divgr A B x == the "quotient" in B of x by A: for all x, *) +(* divgr A B x == the "division" in B of x by A: for all x, *) (* x = divgr A B x * remgr A B x. *) (* ++ External products : *) (* pairg1, pair1g == the isomorphisms aT1 -> aT1 * aT2, aT2 -> aT1 * aT2. *) @@ -179,7 +178,7 @@ Proof. by case/pprodP=> [[K H -> ->] <- /norm_joinEr]. Qed. Lemma pprodJ A B x : pprod A B :^ x = pprod (A :^ x) (B :^ x). Proof. rewrite /pprod !conjsg_eq1 !group_setJ normJ conjSg -conjsMg. -by do 3?case: ifP => // _; exact: conj0g. +by do 3?case: ifP => // _; apply: conj0g. Qed. (* Properties of the remainders *) @@ -223,7 +222,7 @@ Lemma remgr_id x : x \in H -> remgr K H x = x. Proof. move=> Hx; apply/eqP; rewrite eq_mulgV1 (sameP eqP set1gP) -tiKH inE. rewrite -mem_rcoset groupMr ?groupV // -in_setI remgrP. -by apply: subsetP Hx; exact: mulG_subr. +by apply: subsetP Hx; apply: mulG_subr. Qed. Lemma remgrMid x y : x \in K -> y \in H -> remgr K H (x * y) = y. @@ -326,7 +325,7 @@ Proof. by move/sdprodWpp/pprodWY. Qed. Lemma sdprodJ A B x : (A ><| B) :^ x = A :^ x ><| B :^ x. Proof. rewrite /sdprod -conjIg sub_conjg conjs1g -pprodJ. -by case: ifP => _ //; exact: imset0. +by case: ifP => _ //; apply: imset0. Qed. Lemma sdprod_context G K H : K ><| H = G -> @@ -337,7 +336,7 @@ by rewrite /normal mulG_subl mulG_subr mulG_subG normG. Qed. Lemma sdprod_compl G K H : K ><| H = G -> H \in [complements to K in G]. -Proof. by case/sdprodP=> _ mulKH _ tiKH; exact/complP. Qed. +Proof. by case/sdprodP=> _ mulKH _ tiKH; apply/complP. Qed. Lemma sdprod_normal_complP G K H : K <| G -> reflect (K ><| H = G) (K \in [complements to H in G]). @@ -504,7 +503,7 @@ Proof. by move/cprodWpp/pprodWY. Qed. Lemma cprodJ A B x : (A \* B) :^ x = A :^ x \* B :^ x. Proof. -by rewrite /cprod centJ conjSg -pprodJ; case: ifP => _ //; exact: imset0. +by rewrite /cprod centJ conjSg -pprodJ; case: ifP => _ //; apply: imset0. Qed. Lemma cprod_normal2 A B G : A \* B = G -> A <| G /\ B <| G. @@ -587,7 +586,7 @@ Qed. Lemma cprod_modr A B G H : A \* B = G -> B \subset H -> (H :&: A) \* B = H :&: G. -Proof. by rewrite -!(cprodC B) !(setIC H); exact: cprod_modl. Qed. +Proof. by rewrite -!(cprodC B) !(setIC H); apply: cprod_modl. Qed. Lemma bigcprodYP (I : finType) (P : pred I) (H : I -> {group gT}) : reflect (forall i j, P i -> P j -> i != j -> H i \subset 'C(H j)) @@ -692,12 +691,12 @@ Proof. by move/dprodWsd/sdprodWY. Qed. Lemma cprod_card_dprod G A B : A \* B = G -> #|A| * #|B| <= #|G| -> A \x B = G. -Proof. by case/cprodP=> [[K H -> ->] <- cKH] /cardMg_TI; exact: dprodE. Qed. +Proof. by case/cprodP=> [[K H -> ->] <- cKH] /cardMg_TI; apply: dprodE. Qed. Lemma dprodJ A B x : (A \x B) :^ x = A :^ x \x B :^ x. Proof. rewrite /dprod -conjIg sub_conjg conjs1g -cprodJ. -by case: ifP => _ //; exact: imset0. +by case: ifP => _ //; apply: imset0. Qed. Lemma dprod_normal2 A B G : A \x B = G -> A <| G /\ B <| G. @@ -754,11 +753,11 @@ Qed. Lemma bigdprodW I (r : seq I) P F G : \big[dprod/1]_(i <- r | P i) F i = G -> \prod_(i <- r | P i) F i = G. -Proof. by move/bigdprodWcp; exact: bigcprodW. Qed. +Proof. by move/bigdprodWcp; apply: bigcprodW. Qed. Lemma bigdprodWY I (r : seq I) P F G : \big[dprod/1]_(i <- r | P i) F i = G -> << \bigcup_(i <- r | P i) F i >> = G. -Proof. by move/bigdprodWcp; exact: bigcprodWY. Qed. +Proof. by move/bigdprodWcp; apply: bigcprodWY. Qed. Lemma bigdprodYP (I : finType) (P : pred I) (F : I -> {group gT}) : reflect (forall i, P i -> @@ -787,13 +786,13 @@ Qed. Lemma dprod_modr A B G H : A \x B = G -> B \subset H -> (H :&: A) \x B = H :&: G. -Proof. by rewrite -!(dprodC B) !(setIC H); exact: dprod_modl. Qed. +Proof. by rewrite -!(dprodC B) !(setIC H); apply: dprod_modl. Qed. Lemma subcent_dprod B C G A : B \x C = G -> A \subset 'N(B) :&: 'N(C) -> 'C_B(A) \x 'C_C(A) = 'C_G(A). Proof. move=> defG; have [_ _ cBC _] := dprodP defG; move: defG. -by rewrite !dprodEsd 1?(centSS _ _ cBC) ?subsetIl //; exact: subcent_sdprod. +by rewrite !dprodEsd 1?(centSS _ _ cBC) ?subsetIl //; apply: subcent_sdprod. Qed. Lemma dprod_card A B G : A \x B = G -> (#|A| * #|B|)%N = #|G|. @@ -895,7 +894,7 @@ Lemma morphim_coprime_sdprod : K ><| H = G -> coprime #|K| #|H| -> f @* K ><| f @* H = f @* G. Proof. rewrite /sdprod => defG coHK; move: defG. -by rewrite !coprime_TIg ?coprime_morph // !subxx; exact: morphim_pprod. +by rewrite !coprime_TIg ?coprime_morph // !subxx; apply: morphim_pprod. Qed. Lemma injm_sdprod : 'injm f -> K ><| H = G -> f @* K ><| f @* H = f @* G. @@ -920,7 +919,7 @@ Lemma morphim_coprime_dprod : K \x H = G -> coprime #|K| #|H| -> f @* K \x f @* H = f @* G. Proof. rewrite /dprod => defG coHK; move: defG. -by rewrite !coprime_TIg ?coprime_morph // !subxx; exact: morphim_cprod. +by rewrite !coprime_TIg ?coprime_morph // !subxx; apply: morphim_cprod. Qed. End OneProd. @@ -990,13 +989,13 @@ Definition extprod_mulg (x y : gT1 * gT2) := (x.1 * y.1, x.2 * y.2). Definition extprod_invg (x : gT1 * gT2) := (x.1^-1, x.2^-1). Lemma extprod_mul1g : left_id (1, 1) extprod_mulg. -Proof. case=> x1 x2; congr (_, _); exact: mul1g. Qed. +Proof. by case=> x1 x2; congr (_, _); apply: mul1g. Qed. Lemma extprod_mulVg : left_inverse (1, 1) extprod_invg extprod_mulg. -Proof. by move=> x; congr (_, _); exact: mulVg. Qed. +Proof. by move=> x; congr (_, _); apply: mulVg. Qed. Lemma extprod_mulgA : associative extprod_mulg. -Proof. by move=> x y z; congr (_, _); exact: mulgA. Qed. +Proof. by move=> x y z; congr (_, _); apply: mulgA. Qed. Definition extprod_groupMixin := Eval hnf in FinGroup.Mixin extprod_mulgA extprod_mul1g extprod_mulVg. @@ -1037,10 +1036,10 @@ Canonical fst_morphism := @Morphism _ _ setT _ (in2W fst_morphM). Canonical snd_morphism := @Morphism _ _ setT _ (in2W snd_morphM). Lemma injm_pair1g : 'injm pair1g. -Proof. by apply/subsetP=> x /morphpreP[_ /set1P[->]]; exact: set11. Qed. +Proof. by apply/subsetP=> x /morphpreP[_ /set1P[->]]; apply: set11. Qed. Lemma injm_pairg1 : 'injm pairg1. -Proof. by apply/subsetP=> x /morphpreP[_ /set1P[->]]; exact: set11. Qed. +Proof. by apply/subsetP=> x /morphpreP[_ /set1P[->]]; apply: set11. Qed. Lemma morphim_pairg1 (H1 : {set gT1}) : pairg1 @* H1 = setX H1 1. Proof. by rewrite -imset2_pair imset2_set1r morphimEsub ?subsetT. Qed. @@ -1453,7 +1452,7 @@ Lemma morphim_sdprodm A B : A \subset H -> B \subset K -> sdprodm @* (A * B) = fH @* A * fK @* B. Proof. move=> sAH sBK; rewrite morphim_restrm /= (setIidPr _) ?morphim_pprodm //. -case/sdprodP: eqHK_G => _ <- _ _; exact: mulgSS. +by case/sdprodP: eqHK_G => _ <- _ _; apply: mulgSS. Qed. Lemma im_sdprodm : sdprodm @* G = fH @* H * fK @* K. @@ -1523,7 +1522,7 @@ Lemma morphim_cprodm A B : A \subset H -> B \subset K -> cprodm @* (A * B) = fH @* A * fK @* B. Proof. move=> sAH sBK; rewrite morphim_restrm /= (setIidPr _) ?morphim_pprodm //. -case/cprodP: eqHK_G => _ <- _; exact: mulgSS. +by case/cprodP: eqHK_G => _ <- _; apply: mulgSS. Qed. Lemma im_cprodm : cprodm @* G = fH @* H * fK @* K. @@ -1690,7 +1689,7 @@ apply: (iffP misomP) => [[pM /isomP[injf /= <-]] | ]. have sH1H: setX H1 1 \subset setX H1 H2 by rewrite setXS ?sub1G. have sH2H: setX 1 H2 \subset setX H1 H2 by rewrite setXS ?sub1G. rewrite morphim1 injm_cent ?injmI //= subsetI => /andP[_]. - by rewrite !morphimEsub //= !imset_mulgm mulg1 mul1g; exact: dprodE. + by rewrite !morphimEsub //= !imset_mulgm mulg1 mul1g; apply: dprodE. case/dprodP=> _ defG cH12 trH12. have fM: morphic (setX H1 H2) mulgm. apply/morphicP=> [[x1 x2] [y1 y2] /setXP[_ Hx2] /setXP[Hy1 _]]. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 9649644..0c0ba5b 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -1,10 +1,9 @@ (* (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 choice fintype finfun bigop finset. -Require Import fingroup. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq choice fintype finfun. +From mathcomp +Require Import bigop finset fingroup. (******************************************************************************) (* This file contains the definitions of: *) @@ -19,50 +18,50 @@ Require Import fingroup. (* idm D == the identity morphism with domain D, or more precisely *) (* the identity function, but with a canonical *) (* {morphism G -> gT} structure. *) -(* trivm D == the trivial morphism with domain D *) +(* trivm D == the trivial morphism with domain D. *) (* If f has a {morphism D >-> rT} structure *) -(* 'dom f == D *) -(* f @* A == the image of A by f, where f is defined *) +(* 'dom f == D, the domain of f. *) +(* f @* A == the image of A by f, where f is defined. *) (* := f @: (D :&: A) *) -(* f @*^-1 R == the pre-image of R by f, where f is defined *) +(* f @*^-1 R == the pre-image of R by f, where f is defined. *) (* := D :&: f @^-1: R *) -(* 'ker f == the kernel of f *) -(* := f @^-1: 1 *) -(* 'ker_G f == the kernel of f restricted to G *) +(* 'ker f == the kernel of f. *) +(* := f @*^-1 1 *) +(* 'ker_G f == the kernel of f restricted to G. *) (* := G :&: 'ker f (this is a pure notation) *) -(* 'injm f <=> f injective on D *) +(* 'injm f <=> f injective on D. *) (* <-> ker f \subset 1 (this is a pure notation) *) (* invm injf == the inverse morphism of f, with domain f @* D, when f *) -(* is injective (injf : 'injm f) *) +(* is injective (injf : 'injm f). *) (* restrm f sDom == the restriction of f to a subset A of D, given *) (* (sDom : A \subset D); restrm f sDom is transparently *) (* identical to f; the restrmP and domP lemmas provide *) (* opaque restrictions. *) (* invm f infj == the inverse morphism for an injective f, with domain *) -(* f @* D, given (injf : 'injm f) *) +(* f @* D, given (injf : 'injm f). *) (* *) -(* G \isog H <=> G and H are isomorphic as groups *) -(* H \homg G <=> H is a homomorphic image of G *) -(* isom G H f <=> f maps G isomorphically to H, provided D contains G *) -(* <-> f @: G^# == H^# *) +(* G \isog H <=> G and H are isomorphic as groups. *) +(* H \homg G <=> H is a homomorphic image of G. *) +(* isom G H f <=> f maps G isomorphically to H, provided D contains G. *) +(* := f @: G^# == H^# *) (* *) (* If, moreover, g : {morphism G >-> gT} with G : {group aT}, *) (* factm sKer sDom == the (natural) factor morphism mapping f @* G to g @* G *) -(* given sDom : G \subset D, sKer : 'ker f \subset 'ker g *) +(* with sDom : G \subset D, sKer : 'ker f \subset 'ker g. *) (* ifactm injf g == the (natural) factor morphism mapping f @* G to g @* G *) (* when f is injective (injf : 'injm f); here g must *) -(* be an actual morphism structure, not its function *) +(* denote an actual morphism structure, not its function *) (* projection. *) (* *) (* If g has a {morphism G >-> aT} structure for any G : {group gT}, then *) -(* f \o g has a canonical {morphism g @*^-1 D >-> rT} structure *) +(* f \o g has a canonical {morphism g @*^-1 D >-> rT} structure. *) (* *) (* Finally, for an arbitrary function f : aT -> rT *) (* morphic D f <=> f preserves group multiplication in D, i.e., *) -(* f (x * y) = (f x) * (f y) for all x, y in D *) +(* f (x * y) = (f x) * (f y) for all x, y in D. *) (* morphm fM == a function identical to f, but with a canonical *) -(* {morphism D >-> rT} structure, given fM : morphic D f *) -(* misom D C f <=> f maps D isomorphically to C *) +(* {morphism D >-> rT} structure, given fM : morphic D f. *) +(* misom D C f <=> f is a morphism that maps D isomorphically to C. *) (* := morphic D f && isom D C f *) (******************************************************************************) @@ -83,10 +82,10 @@ Structure morphism (D : {set aT}) : Type := Morphism { _ : {in D &, {morph mfun : x y / x * y}} }. -(* We give the most 'lightweight' possible specification to define morphisms:*) -(* local congruence with the group law of aT. We then provide the properties *) -(* for the 'textbook' notion of morphism, when the required structures are *) -(* available (e.g. its domain is a group). *) +(* We give the 'lightest' possible specification to define morphisms: local *) +(* congruence, in D, with the group law of aT. We then provide the properties *) +(* for the 'textbook' notion of morphism, when the required structures are *) +(* available (e.g. its domain is a group). *) Definition morphism_for D of phant rT := morphism D. @@ -106,7 +105,7 @@ by exists z; first apply/setIP. Qed. Lemma morphpreP : reflect (x \in D /\ f x \in R) (x \in D :&: f @^-1: R). -Proof. rewrite !inE; exact: andP. Qed. +Proof. by rewrite !inE; apply: andP. Qed. End MorphismStructure. @@ -122,7 +121,7 @@ Implicit Arguments morphimP [aT rT D A f y]. Implicit Arguments morphpreP [aT rT D R f x]. Prenex Implicits morphimP morphpreP. -(* domain, image, preimage, kernel, using phantom types to infer the domain *) +(* Domain, image, preimage, kernel, using phantom types to infer the domain. *) Section MorphismOps1. @@ -206,7 +205,7 @@ Qed. Lemma morphR : {in D &, {morph f : x y / [~ x, y]}}. Proof. by move=> * /=; rewrite morphM ?(groupV, groupJ) // morphJ ?morphV. Qed. -(* morphic image,preimage properties w.r.t. set-theoretic operations *) +(* Morphic image, preimage properties w.r.t. set-theoretic operations. *) Lemma morphimE A : f @* A = f @: (D :&: A). Proof. by []. Qed. Lemma morphpreE R : f @*^-1 R = D :&: f @^-1: R. Proof. by []. Qed. @@ -237,7 +236,7 @@ Lemma mem_morphim A x : x \in D -> x \in A -> f x \in f @* A. Proof. by move=> Dx Ax; apply/morphimP; exists x. Qed. Lemma mem_morphpre R x : x \in D -> f x \in R -> x \in f @*^-1 R. -Proof. by move=> Dx Rfx; exact/morphpreP. Qed. +Proof. by move=> Dx Rfx; apply/morphpreP. Qed. Lemma morphimS A B : A \subset B -> f @* A \subset f @* B. Proof. by move=> sAB; rewrite imsetS ?setIS. Qed. @@ -270,7 +269,7 @@ Lemma morphim_eq0 A : A \subset D -> (f @* A == set0) = (A == set0). Proof. by rewrite imset_eq0 => /setIidPr->. Qed. Lemma morphim_set1 x : x \in D -> f @* [set x] = [set f x]. -Proof. by rewrite /morphim -sub1set => /setIidPr->; exact: imset_set1. Qed. +Proof. by rewrite /morphim -sub1set => /setIidPr->; apply: imset_set1. Qed. Lemma morphim1 : f @* 1 = 1. Proof. by rewrite morphim_set1 ?morph1. Qed. @@ -373,13 +372,13 @@ Proof. by apply/setP=> x; rewrite !inE; case: (x \in D). Qed. (* kernel, domain properties *) Lemma kerP x : x \in D -> reflect (f x = 1) (x \in 'ker f). -Proof. move=> Dx; rewrite 2!inE Dx; exact: set1P. Qed. +Proof. by move=> Dx; rewrite 2!inE Dx; apply: set1P. Qed. Lemma dom_ker : {subset 'ker f <= D}. Proof. by move=> x /morphpreP[]. Qed. Lemma mker x : x \in 'ker f -> f x = 1. -Proof. by move=> Kx; apply/kerP=> //; exact: dom_ker. Qed. +Proof. by move=> Kx; apply/kerP=> //; apply: dom_ker. Qed. Lemma mkerl x y : x \in 'ker f -> y \in D -> f (x * y) = f y. Proof. by move=> Kx Dy; rewrite morphM // ?(dom_ker, mker Kx, mul1g). Qed. @@ -391,12 +390,12 @@ Lemma rcoset_kerP x y : x \in D -> y \in D -> reflect (f x = f y) (x \in 'ker f :* y). Proof. move=> Dx Dy; rewrite mem_rcoset !inE groupM ?morphM ?groupV //=. -rewrite morphV // -eq_mulgV1; exact: eqP. +by rewrite morphV // -eq_mulgV1; apply: eqP. Qed. Lemma ker_rcoset x y : x \in D -> y \in D -> f x = f y -> exists2 z, z \in 'ker f & x = z * y. -Proof. move=> Dx Dy eqfxy; apply/rcosetP; exact/rcoset_kerP. Qed. +Proof. by move=> Dx Dy eqfxy; apply/rcosetP; apply/rcoset_kerP. Qed. Lemma ker_norm : D \subset 'N('ker f). Proof. @@ -513,7 +512,7 @@ Lemma sub_morphim_pre A R : A \subset D -> (f @* A \subset R) = (A \subset f @*^-1 R). Proof. move=> sAD; rewrite -morphpreSK (morphimS, morphimK) //. -apply/idP/idP; first by apply: subset_trans; exact: mulG_subr. +apply/idP/idP; first by apply: subset_trans; apply: mulG_subr. by move/(mulgS ('ker f)); rewrite -morphpreMl ?(sub1G, mul1g). Qed. @@ -625,7 +624,7 @@ Qed. Lemma morphim_norms A B : A \subset 'N(B) -> f @* A \subset 'N(f @* B). Proof. -by move=> nBA; apply: subset_trans (morphim_norm B); exact: morphimS. +by move=> nBA; apply: subset_trans (morphim_norm B); apply: morphimS. Qed. Lemma morphim_subnorm A B : f @* 'N_A(B) \subset 'N_(f @* A)(f @* B). @@ -639,7 +638,7 @@ Proof. by move=> Dx; rewrite -(morphim_set1 Dx) morphim_norm. Qed. Lemma morphim_cent1s A x : x \in D -> A \subset 'C[x] -> f @* A \subset 'C[f x]. Proof. -by move=> Dx cAx; apply: subset_trans (morphim_cent1 Dx); exact: morphimS. +by move=> Dx cAx; apply: subset_trans (morphim_cent1 Dx); apply: morphimS. Qed. Lemma morphim_subcent1 A x : x \in D -> f @* 'C_A[x] \subset 'C_(f @* A)[f x]. @@ -648,12 +647,12 @@ Proof. by move=> Dx; rewrite -(morphim_set1 Dx) morphim_subnorm. Qed. Lemma morphim_cent A : f @* 'C(A) \subset 'C(f @* A). Proof. apply/bigcapsP=> fx; case/morphimP=> x Dx Ax ->{fx}. -by apply: subset_trans (morphim_cent1 Dx); apply: morphimS; exact: bigcap_inf. +by apply: subset_trans (morphim_cent1 Dx); apply: morphimS; apply: bigcap_inf. Qed. Lemma morphim_cents A B : A \subset 'C(B) -> f @* A \subset 'C(f @* B). Proof. -by move=> cBA; apply: subset_trans (morphim_cent B); exact: morphimS. +by move=> cBA; apply: subset_trans (morphim_cent B); apply: morphimS. Qed. Lemma morphim_subcent A B : f @* 'C_A(B) \subset 'C_(f @* A)(f @* B). @@ -670,7 +669,7 @@ Qed. Lemma morphpre_norms R S : R \subset 'N(S) -> f @*^-1 R \subset 'N(f @*^-1 S). Proof. -by move=> nSR; apply: subset_trans (morphpre_norm S); exact: morphpreS. +by move=> nSR; apply: subset_trans (morphpre_norm S); apply: morphpreS. Qed. Lemma morphpre_normal R S : @@ -728,7 +727,7 @@ Proof. by move=> sRfD; move/morphim_cents; rewrite morphpreK. Qed. Lemma morphpre_subcent R A : 'C_(f @*^-1 R)(A) \subset f @*^-1 'C_R(f @* A). Proof. -by rewrite -morphpreIdom -setIA setICA morphpreI setIS //; exact: morphpre_cent. +by rewrite -morphpreIdom -setIA setICA morphpreI setIS //; apply: morphpre_cent. Qed. (* local injectivity properties *) @@ -892,7 +891,7 @@ Lemma injm_idm G : 'injm (idm G). Proof. by apply/injmP=> x y _ _. Qed. Lemma ker_idm G : 'ker (idm G) = 1. -Proof. by apply/trivgP; exact: injm_idm. Qed. +Proof. by apply/trivgP; apply: injm_idm. Qed. Lemma morphim_idm A B : B \subset A -> idm A @* B = B. Proof. @@ -1194,7 +1193,7 @@ Proof. by rewrite ker_ifactm => /trivgP->; rewrite morphim1. Qed. End InjFactm. -(* Reflected (boolean) form of morphism and isomorphism properties *) +(* Reflected (boolean) form of morphism and isomorphism properties. *) Section ReflectProp. @@ -1204,7 +1203,7 @@ Section Defs. Variables (A : {set aT}) (B : {set rT}). -(* morphic is the morphM property of morphisms seen through morphicP *) +(* morphic is the morphM property of morphisms seen through morphicP. *) Definition morphic (f : aT -> rT) := [forall u in [predX A & A], f (u.1 * u.2) == f u.1 * f u.2]. @@ -1240,14 +1239,14 @@ Lemma misom_isog f : misom f -> isog. Proof. case/andP=> fM iso_f; apply/existsP; exists (finfun f). apply/andP; split; last by rewrite /misom /isom !(eq_imset _ (ffunE f)). -apply/forallP=> u; rewrite !ffunE; exact: forallP fM u. +by apply/forallP=> u; rewrite !ffunE; apply: forallP fM u. Qed. Lemma isom_isog (D : {group aT}) (f : {morphism D >-> rT}) : A \subset D -> isom f -> isog. Proof. move=> sAD isof; apply: (@misom_isog f); rewrite /misom isof andbT. -apply/morphicP; exact: (sub_in2 (subsetP sAD) (morphM f)). +by apply/morphicP; apply: (sub_in2 (subsetP sAD) (morphM f)). Qed. Lemma isog_isom : isog -> {f : {morphism A >-> rT} | isom f}. @@ -1313,7 +1312,7 @@ by rewrite subDset setUC subsetU ?sAG. Qed. Lemma sub_isog (A : {set aT}) : A \subset G -> 'injm f -> isog A (f @* A). -Proof. by move=> sAG injf; apply: (isom_isog f sAG); exact: sub_isom. Qed. +Proof. by move=> sAG injf; apply: (isom_isog f sAG); apply: sub_isom. Qed. Lemma restr_isom_to (A : {set aT}) (C R : {group rT}) (sAG : A \subset G) : f @* A = C -> isom G R f -> isom A C (restrm sAG f). @@ -1349,7 +1348,7 @@ Proof. exact: sub_isom (im_idm G) (injm_idm G). Qed. Lemma isog_refl : G \isog G. Proof. exact: isom_isog idm_isom. Qed. Lemma card_isog : G \isog H -> #|G| = #|H|. -Proof. case/isogP=> f injf <-; apply: isom_card (f) _; exact/isomP. Qed. +Proof. by case/isogP=> f injf <-; apply: isom_card (f) _; apply/isomP. Qed. Lemma isog_abelian : G \isog H -> abelian G = abelian H. Proof. by case/isogP=> f injf <-; rewrite injm_abelian. Qed. @@ -1358,7 +1357,7 @@ Lemma trivial_isog : G :=: 1 -> H :=: 1 -> G \isog H. Proof. move=> -> ->; apply/isogP. exists [morphism of @trivm gT hT 1]; rewrite /= ?morphim1 //. -rewrite ker_trivm; exact: subxx. +by rewrite ker_trivm; apply: subxx. Qed. Lemma isog_eq1 : G \isog H -> (G :==: 1) = (H :==: 1). @@ -1393,7 +1392,7 @@ Variables gT hT kT : finGroupType. Variables (G : {group gT}) (H : {group hT}) (K : {group kT}). Lemma isog_sym : (G \isog H) = (H \isog G). -Proof. apply/idP/idP; exact: isog_symr. Qed. +Proof. by apply/idP/idP; apply: isog_symr. Qed. Lemma isog_transl : G \isog H -> (G \isog K) = (H \isog K). Proof. @@ -1467,14 +1466,14 @@ Qed. Lemma eq_homgl gT aT rT (G : {group gT}) (H : {group aT}) (K : {group rT}) : G \isog H -> homg G K = homg H K. Proof. -by rewrite isogEhom => /andP[homGH homHG]; apply/idP/idP; exact: homg_trans. +by rewrite isogEhom => /andP[homGH homHG]; apply/idP/idP; apply: homg_trans. Qed. Lemma eq_homgr gT rT aT (G : {group gT}) (H : {group rT}) (K : {group aT}) : G \isog H -> homg K G = homg K H. Proof. rewrite isogEhom => /andP[homGH homHG]. -by apply/idP/idP=> homK; exact: homg_trans homK _. +by apply/idP/idP=> homK; apply: homg_trans homK _. Qed. End Homg. @@ -1495,10 +1494,10 @@ Canonical sgval_morphism := Morphism (@sgvalM _ G). Canonical subg_morphism := Morphism (@subgM _ G). Lemma injm_sgval : 'injm sgval. -Proof. apply/injmP; apply: in2W; exact: subg_inj. Qed. +Proof. by apply/injmP; apply: in2W; apply: subg_inj. Qed. Lemma injm_subg : 'injm (subg G). -Proof. apply/injmP; exact: can_in_inj (@subgK _ _). Qed. +Proof. by apply/injmP; apply: can_in_inj (@subgK _ _). Qed. Hint Resolve injm_sgval injm_subg. Lemma ker_sgval : 'ker sgval = 1. Proof. exact/trivgP. Qed. @@ -1511,7 +1510,7 @@ by apply/subsetP=> u _; rewrite -(sgvalK u) mem_imset ?subgP. Qed. Lemma sgval_sub A : sgval @* A \subset G. -Proof. apply/subsetP=> x; case/imsetP=> u _ ->; exact: subgP. Qed. +Proof. by apply/subsetP=> x; case/imsetP=> u _ ->; apply: subgP. Qed. Lemma sgvalmK A : subg G @* (sgval @* A) = A. Proof. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 3719835..664129b 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -1,10 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import path choice fintype tuple finfun bigop finset binomial. -Require Import fingroup. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq path choice fintype. +From mathcomp +Require Import tuple finfun bigop finset binomial fingroup. (******************************************************************************) (* This file contains the definition and properties associated to the group *) @@ -15,14 +14,14 @@ Require Import fingroup. (* 'S_n == the set of all permutations of 'I_n, i.e., of {0,.., n-1} *) (* perm_on A u == u is a permutation with support A, i.e., u only displaces *) (* elements of A (u x != x implies x \in A). *) -(* tperm x y == the transposition of x, y *) -(* aperm x s == the image of x under the action of the permutation s *) +(* tperm x y == the transposition of x, y. *) +(* aperm x s == the image of x under the action of the permutation s. *) (* := s x *) (* pcycle s x == the set of all elements that are in the same cycle of the *) -(* permutation s as x, i.e., {x, s x, (s ^+ 2) x, ...} *) -(* pcycles s == the set of all the cycles of the permutation s *) -(* (s : bool) == s is an odd permutation (the coercion is called odd_perm) *) -(* dpair u == u is a pair (x, y) of distinct objects (i.e., x != y) *) +(* permutation s as x, i.e., {x, s x, (s ^+ 2) x, ...}. *) +(* pcycles s == the set of all the cycles of the permutation s. *) +(* (s : bool) == s is an odd permutation (the coercion is called odd_perm). *) +(* dpair u == u is a pair (x, y) of distinct objects (i.e., x != y). *) (* lift_perm i j s == the permutation obtained by lifting s : 'S_n.-1 over *) (* (i |-> j), that maps i to j and lift i k to lift j (s k). *) (* Canonical structures are defined allowing permutations to be an eqType, *) @@ -117,7 +116,7 @@ Variable T : finType. Implicit Types (x y : T) (s t : {perm T}) (S : {set T}). Lemma permP s t : s =1 t <-> s = t. -Proof. by split=> [| -> //]; rewrite unlock => eq_sv; exact/val_inj/ffunP. Qed. +Proof. by split=> [| -> //]; rewrite unlock => eq_sv; apply/val_inj/ffunP. Qed. Lemma pvalE s : pval s = s :> (T -> T). Proof. by rewrite [@fun_of_perm]unlock. Qed. @@ -126,7 +125,7 @@ Lemma permE f f_inj : @perm T f f_inj =1 f. Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed. Lemma perm_inj s : injective s. -Proof. by rewrite -!pvalE; exact: (injectiveP _ (valP s)). Qed. +Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed. Implicit Arguments perm_inj []. Hint Resolve perm_inj. @@ -204,7 +203,7 @@ by have [-> /tH | /sH] := eqVneq (s x) x. Qed. Lemma out_perm S u x : perm_on S u -> x \notin S -> u x = x. -Proof. by move=> uS; exact: contraNeq (subsetP uS x). Qed. +Proof. by move=> uS; apply: contraNeq (subsetP uS x). Qed. Lemma im_perm_on u S : perm_on S u -> u @: S = S. Proof. @@ -265,11 +264,11 @@ pose fA s : ffA := [ffun u => s (val u)]. rewrite -!sum1dep_card -sum1_card (reindex_onto fA pfT) => [|f]. apply: eq_bigl => p; rewrite andbC; apply/idP/and3P=> [onA | []]; first split. - apply/eqP; suffices fTAp: fT (fA p) = pval p. - by apply/permP=> x; rewrite -!pvalE insubdK fTAp //; exact: (valP p). + by apply/permP=> x; rewrite -!pvalE insubdK fTAp //; apply: (valP p). apply/ffunP=> x; rewrite ffunE pvalE. by case: insubP => [u _ <- | /out_perm->] //=; rewrite ffunE. - by apply/forallP=> [[x Ax]]; rewrite ffunE /= perm_closed. - - by apply/injectiveP=> u v; rewrite !ffunE => /perm_inj; exact: val_inj. + - by apply/injectiveP=> u v; rewrite !ffunE => /perm_inj; apply: val_inj. move/eqP=> <- _ _; apply/subsetP=> x; rewrite !inE -pvalE val_insubd fun_if. by rewrite if_arg ffunE; case: insubP; rewrite // pvalE perm1 if_same eqxx. case/andP=> /forallP-onA /injectiveP-f_inj. @@ -393,7 +392,7 @@ have lt_xf a b u n : n < xf a b u -> ~~ pred2 a b ((u ^+ n.+1) a). by rewrite permX iterSr nth_traject // (leq_trans lt_n). pose t a b u := tperm a b * u. have tC a b u : t a b u = t b a u by rewrite /t tpermC. -have tK a b: involutive (t a b) by move=> u; exact: tpermKg. +have tK a b: involutive (t a b) by move=> u; apply: tpermKg. have tXC a b u n: n <= xf a b u -> (t a b u ^+ n.+1) b = (u ^+ n.+1) a. elim: n => [|n IHn] lt_n_f; first by rewrite permM tpermR. rewrite !(expgSr _ n.+1) !permM {}IHn 1?ltnW //; congr (u _). @@ -408,7 +407,7 @@ have eq_xf a b u: pred2 a b ((u ^+ (xf a b u).+1) a). have xfC a b u: xf b a (t a b u) = xf a b u. without loss lt_a: a b u / xf b a (t a b u) < xf a b u. move=> IHab; set m := xf b a _; set n := xf a b u. - by case: (ltngtP m n) => // ltx; [exact: IHab | rewrite -[m]IHab tC tK]. + by case: (ltngtP m n) => // ltx; [apply: IHab | rewrite -[m]IHab tC tK]. by move/lt_xf: (lt_a); rewrite -(tXC a b) 1?ltnW //= orbC [_ || _]eq_xf. pose ts := t x y s; rewrite /= -[_ * s]/ts. pose dp u := #|pcycles u :\ pcycle u y :\ pcycle u x|. @@ -428,8 +427,8 @@ rewrite -/(dp s) !addnA !eq_pcycle_mem andbT; congr (_ + _); last first. by rewrite /aperm exp_id mem_pcycle. by rewrite /aperm -exp_id mem_pcycle. elim: n => // n IHn; rewrite !expgSr !permM {}IHn tpermD //. - apply: contraNneq sxz => ->; exact: mem_pcycle. - apply: contraNneq syz => ->; exact: mem_pcycle. + by apply: contraNneq sxz => ->; apply: mem_pcycle. + by apply: contraNneq syz => ->; apply: mem_pcycle. case: eqP {dp} => [<- | ne_xy]; first by rewrite /t tperm1 mul1g pcycle_id. suff ->: (x \in pcycle (t x y s) y) = (x \notin pcycle s y) by case: (x \in _). without loss xf_x: s x y ne_xy / (s ^+ (xf x y s).+1) x = x. @@ -556,13 +555,13 @@ congr (_ (+) _); last first. congr (_ (+) _); transitivity (tperm (lift j t.1) (lift j t.2)); last first. by rewrite odd_tperm (inj_eq (@lift_inj _ _)). congr odd_perm; apply/permP=> k; case: (unliftP j k) => [k'|] ->. - rewrite lift_perm_lift inj_tperm //; exact: lift_inj. + by rewrite lift_perm_lift inj_tperm //; apply: lift_inj. by rewrite lift_perm_id tpermD // eq_sym neq_lift. suff{i j s} odd_lift0 (k : 'I_n.+1): lift_perm ord0 k 1 = odd k :> bool. rewrite -!odd_lift0 -{2}invg1 -lift_permV odd_permV -odd_permM. by rewrite lift_permM mulg1. elim: {k}(k : nat) {1 3}k (erefl (k : nat)) => [|m IHm] k def_k. - rewrite (_ : k = ord0) ?lift_perm1 ?odd_perm1 //; exact: val_inj. + by rewrite (_ : k = ord0) ?lift_perm1 ?odd_perm1 //; apply: val_inj. have le_mn: m < n.+1 by [rewrite -def_k ltnW]; pose j := Ordinal le_mn. rewrite -(mulg1 1)%g -(lift_permM _ j) odd_permM {}IHm // addbC. rewrite (_ : _ 1 = tperm j k); first by rewrite odd_tperm neq_ltn def_k leqnn. diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v index 8f6ddb3..13dd99a 100644 --- a/mathcomp/fingroup/presentation.v +++ b/mathcomp/fingroup/presentation.v @@ -1,9 +1,8 @@ (* (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 fintype finset. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq fintype finset. +From mathcomp Require Import fingroup morphism. (******************************************************************************) @@ -187,7 +186,7 @@ Implicit Types gT rT : finGroupType. Import Presentation. Lemma isoGrp_hom gT (G : {group gT}) p : G \isog Grp p -> G \homg Grp p. -Proof. by move <-; exact: homg_refl. Qed. +Proof. by move <-; apply: homg_refl. Qed. Lemma isoGrpP gT (G : {group gT}) p rT (H : {group rT}) : G \isog Grp p -> reflect (#|H| = #|G| /\ H \homg Grp p) (H \isog G). @@ -216,7 +215,7 @@ have and_relE xT x1 x2 r: @and_rel xT x1 x2 r = (x1 == x2) && r :> bool. by case: r => //=; rewrite andbT. have rsatG e f: all (mem G) e -> rel e f NoRel -> rel (map h e) f NoRel. move=> Ge; have: NoRel -> NoRel by []; move: NoRel {2 4}NoRel. - elim: f => [x1 x2 | f1 IH1 f2 IH2] r hr IHr; last by apply: IH1; exact: IH2. + elim: f => [x1 x2 | f1 IH1 f2 IH2] r hr IHr; last by apply: IH1; apply: IH2. by rewrite !and_relE !evalG //; case/andP; move/eqP->; rewrite eqxx. set s := env1; set vT := gT : finType in s *. set s' := env1; set vT' := rT : finType in s' *. @@ -239,19 +238,19 @@ Qed. Lemma eq_homGrp gT rT (G : {group gT}) (H : {group rT}) p : G \isog H -> (G \homg Grp p) = (H \homg Grp p). Proof. -by rewrite isogEhom => /andP[homGH homHG]; apply/idP/idP; exact: homGrp_trans. +by rewrite isogEhom => /andP[homGH homHG]; apply/idP/idP; apply: homGrp_trans. Qed. Lemma isoGrp_trans gT rT (G : {group gT}) (H : {group rT}) p : G \isog H -> H \isog Grp p -> G \isog Grp p. -Proof. by move=> isoGH isoHp kT K; rewrite -isoHp; exact: eq_homgr. Qed. +Proof. by move=> isoGH isoHp kT K; rewrite -isoHp; apply: eq_homgr. Qed. Lemma intro_isoGrp gT (G : {group gT}) p : G \homg Grp p -> (forall rT (H : {group rT}), H \homg Grp p -> H \homg G) -> G \isog Grp p. Proof. move=> homGp freeG rT H. -by apply/idP/idP=> [homHp|]; [exact: homGrp_trans homGp | exact: freeG]. +by apply/idP/idP=> [homHp|]; [apply: homGrp_trans homGp | apply: freeG]. Qed. End PresentationTheory. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 1983e59..aa5bc0a 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -1,20 +1,19 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype prime finset. -Require Import fingroup morphism automorphism. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq div choice. +From mathcomp +Require Import fintype prime finset fingroup morphism automorphism. (******************************************************************************) (* This file contains the definitions of: *) -(* coset_of H == the (sub)type of bilateral cosets of H (see below) *) -(* coset H == the canonical projection into coset_of H *) +(* coset_of H == the (sub)type of bilateral cosets of H (see below). *) +(* coset H == the canonical projection into coset_of H. *) (* A / H == the quotient of A by H, that is, the morphic image *) (* of A by coset H. We do not require H <| A, so in a *) (* textbook A / H would be written 'N_A(H) * H / H. *) (* quotm f (nHG : H <| G) == the quotient morphism induced by f, *) -(* mapping G / H onto f @* G / f @* H *) +(* mapping G / H onto f @* G / f @* H. *) (* qisom f (eqHG : H = G) == the identity isomorphism between *) (* [set: coset_of G] and [set: coset_of H]. *) (* We also prove the three isomorphism theorems, and counting lemmas for *) @@ -32,13 +31,13 @@ Section Cosets. Variables (gT : finGroupType) (Q A : {set gT}). (******************************************************************************) -(* Cosets are right cosets of elements in the normaliser *) +(* Cosets are right cosets of elements in the normaliser. *) (* We let cosets coerce to GroupSet.sort, so they inherit the group subset *) (* base group structure. Later we will define a proper group structure on *) (* cosets, which will then hide the inherited structure once coset_of unifies *) (* with FinGroup.sort; the coercion to GroupSet.sort will no longer be used. *) (* Note that for Hx Hy : coset_of H, Hx * Hy : {set gT} can mean either *) -(* set_of_coset (mulg Hx Hy) OR mulg (set_of_coset Hx) (set_of_coset Hy) *) +(* set_of_coset (mulg Hx Hy) OR mulg (set_of_coset Hx) (set_of_coset Hy). *) (* However, since the two terms are actually convertible, we can live with *) (* this ambiguity. *) (* We take great care that neither the type coset_of H, nor its Canonical *) @@ -46,12 +45,12 @@ Variables (gT : finGroupType) (Q A : {set gT}). (* group structure of H. Otherwise, rewriting would be extremely awkward *) (* because all our equalities are stated at the set level. *) (* The trick we use is to interpret coset_of A, when A is any set, as the *) -(* type of cosets of the group <A> generated by A, in the group A <*> N(A) *) +(* type of cosets of the group <<A>> generated by A, in the group A <*> N(A) *) (* generated by A and its normaliser. This coincides with the type of *) (* bilateral cosets of A when A is a group. We restrict the domain of coset A *) (* to 'N(A), so that we get almost all the same conversion equalities as if *) (* we had forced A to be a group in the first place; the only exception, that *) -(* 1 : coset_of A : set _ = <<A>> rather than A, is covered by genGid. *) +(* 1 : coset_of A : {set gT} = <<A>> rather than A, can be handled by genGid. *) (******************************************************************************) Notation H := <<A>>. @@ -120,7 +119,7 @@ Canonical coset_baseGroupType := Eval hnf in BaseFinGroupType coset_of coset_of_groupMixin. Canonical coset_groupType := FinGroupType coset_invP. -(* Projection of the initial group type over the cosets groupType *) +(* Projection of the initial group type over the cosets groupType. *) Definition coset x : coset_of := insubd (1 : coset_of) (H :* x). @@ -152,19 +151,19 @@ Lemma coset_mem y xbar : y \in xbar -> coset y = xbar. Proof. case: xbar => /= Hx NHx Hxy; apply: val_inj=> /=. case/rcosetsP: NHx (NHx) Hxy => x Nx -> NHx Hxy. -by rewrite val_insubd /= (rcoset_transl Hxy) NHx. +by rewrite val_insubd /= (rcoset_eqP Hxy) NHx. Qed. (* coset is an inverse to repr *) Lemma mem_repr_coset xbar : repr xbar \in xbar. -Proof. case: xbar => /= _ /rcosetsP[x _ ->]; exact: mem_repr_rcoset. Qed. +Proof. by case: xbar => /= _ /rcosetsP[x _ ->]; apply: mem_repr_rcoset. Qed. Lemma repr_coset1 : repr (1 : coset_of) = 1. Proof. exact: repr_group. Qed. Lemma coset_reprK : cancel (fun xbar => repr xbar) coset. -Proof. by move=> xbar; exact: coset_mem (mem_repr_coset xbar). Qed. +Proof. by move=> xbar; apply: coset_mem (mem_repr_coset xbar). Qed. (* cosetP is slightly stronger than using repr because we only *) (* guarantee repr xbar \in 'N(A) when A is a group. *) @@ -178,7 +177,7 @@ by exists x; last rewrite (coset_mem xbar_x). Qed. Lemma coset_id x : x \in A -> coset x = 1. -Proof. by move=> Ax; apply: coset_mem; exact: mem_gen. Qed. +Proof. by move=> Ax; apply: coset_mem; apply: mem_gen. Qed. Lemma im_coset : coset @* 'N(A) = setT. Proof. @@ -293,7 +292,7 @@ Lemma im_quotient : 'N(H) / H = setT. Proof. exact: im_coset. Qed. Lemma quotientT : setT / H = setT. -Proof. by rewrite -im_quotient; exact: morphimT. Qed. +Proof. by rewrite -im_quotient; apply: morphimT. Qed. (* Variant of morphimIdom. *) Lemma quotientInorm A : 'N_A(H) / H = A / H. @@ -359,18 +358,18 @@ Qed. Lemma rcoset_kercosetP x y : x \in 'N(H) -> y \in 'N(H) -> reflect (coset H x = coset H y) (x \in H :* y). -Proof. rewrite -{6}ker_coset; exact: rcoset_kerP. Qed. +Proof. by rewrite -{6}ker_coset; apply: rcoset_kerP. Qed. Lemma kercoset_rcoset x y : x \in 'N(H) -> y \in 'N(H) -> coset H x = coset H y -> exists2 z, z \in H & x = z * y. -Proof. by move=> Nx Ny eqfxy; rewrite -ker_coset; exact: ker_rcoset. Qed. +Proof. by move=> Nx Ny eqfxy; rewrite -ker_coset; apply: ker_rcoset. Qed. Lemma quotientGI G A : H \subset G -> (G :&: A) / H = G / H :&: A / H. -Proof. by rewrite -{1}ker_coset; exact: morphimGI. Qed. +Proof. by rewrite -{1}ker_coset; apply: morphimGI. Qed. Lemma quotientIG A G : H \subset G -> (A :&: G) / H = A / H :&: G / H. -Proof. by rewrite -{1}ker_coset; exact: morphimIG. Qed. +Proof. by rewrite -{1}ker_coset; apply: morphimIG. Qed. Lemma quotientD A B : A / H :\: B / H \subset (A :\: B) / H. Proof. exact: morphimD. Qed. @@ -379,16 +378,16 @@ Lemma quotientD1 A : (A / H)^# \subset A^# / H. Proof. exact: morphimD1. Qed. Lemma quotientDG A G : H \subset G -> (A :\: G) / H = A / H :\: G / H. -Proof. by rewrite -{1}ker_coset; exact: morphimDG. Qed. +Proof. by rewrite -{1}ker_coset; apply: morphimDG. Qed. Lemma quotientK A : A \subset 'N(H) -> coset H @*^-1 (A / H) = H * A. -Proof. by rewrite -{8}ker_coset; exact: morphimK. Qed. +Proof. by rewrite -{8}ker_coset; apply: morphimK. Qed. Lemma quotientYK G : G \subset 'N(H) -> coset H @*^-1 (G / H) = H <*> G. Proof. by move=> nHG; rewrite quotientK ?norm_joinEr. Qed. Lemma quotientGK G : H <| G -> coset H @*^-1 (G / H) = G. -Proof. by case/andP; rewrite -{1}ker_coset; exact: morphimGK. Qed. +Proof. by case/andP; rewrite -{1}ker_coset; apply: morphimGK. Qed. Lemma quotient_class x A : x \in 'N(H) -> A \subset 'N(H) -> x ^: A / H = coset H x ^: (A / H). @@ -400,7 +399,7 @@ Proof. exact: classes_morphim. Qed. Lemma cosetpre_set1 x : x \in 'N(H) -> coset H @*^-1 [set coset H x] = H :* x. -Proof. by rewrite -{9}ker_coset; exact: morphpre_set1. Qed. +Proof. by rewrite -{9}ker_coset; apply: morphpre_set1. Qed. Lemma cosetpre_set1_coset xbar : coset H @*^-1 [set xbar] = xbar. Proof. by case: (cosetP xbar) => x Nx ->; rewrite cosetpre_set1 ?val_coset. Qed. @@ -416,14 +415,14 @@ Lemma quotientS1 G : G \subset H -> G / H = 1. Proof. by move=> sGH; apply/trivgP; rewrite -trivg_quotient quotientS. Qed. Lemma sub_cosetpre M : H \subset coset H @*^-1 M. -Proof. by rewrite -{1}ker_coset; exact: ker_sub_pre. Qed. +Proof. by rewrite -{1}ker_coset; apply: ker_sub_pre. Qed. Lemma quotient_proper G K : H <| G -> H <| K -> (G / H \proper K / H) = (G \proper K). Proof. by move=> nHG nHK; rewrite -cosetpre_proper ?quotientGK. Qed. Lemma normal_cosetpre M : H <| coset H @*^-1 M. -Proof. rewrite -{1}ker_coset; exact: ker_normal_pre. Qed. +Proof. by rewrite -{1}ker_coset; apply: ker_normal_pre. Qed. Lemma cosetpreSK C D : (coset H @*^-1 C \subset coset H @*^-1 D) = (C \subset D). @@ -447,15 +446,15 @@ Proof. by move=> nHA; rewrite morphimSK ?ker_coset. Qed. Lemma quotientSGK A G : A \subset 'N(H) -> H \subset G -> (A / H \subset G / H) = (A \subset G). -Proof. by rewrite -{2}ker_coset; exact: morphimSGK. Qed. +Proof. by rewrite -{2}ker_coset; apply: morphimSGK. Qed. Lemma quotient_injG : {in [pred G : {group gT} | H <| G] &, injective (fun G => G / H)}. -Proof. by rewrite /normal -{1}ker_coset; exact: morphim_injG. Qed. +Proof. by rewrite /normal -{1}ker_coset; apply: morphim_injG. Qed. Lemma quotient_inj G1 G2 : H <| G1 -> H <| G2 -> G1 / H = G2 / H -> G1 :=: G2. -Proof. by rewrite /normal -{1 3}ker_coset; exact: morphim_inj. Qed. +Proof. by rewrite /normal -{1 3}ker_coset; apply: morphim_inj. Qed. Lemma quotient_neq1 A : H <| A -> (A / H != 1) = (H \proper A). Proof. @@ -494,7 +493,7 @@ Qed. Lemma quotient_cent1s A x : A \subset 'C[x] -> A / H \subset 'C[coset H x]. Proof. -by move=> sAC; exact: subset_trans (quotientS sAC) (quotient_cent1 x). +by move=> sAC; apply: subset_trans (quotientS sAC) (quotient_cent1 x). Qed. Lemma quotient_subcent1 A x : 'C_A[x] / H \subset 'C_(A / H)[coset H x]. @@ -515,7 +514,7 @@ Proof. exact: morphim_subcent. Qed. Lemma norm_quotient_pre A C : A \subset 'N(H) -> A / H \subset 'N(C) -> A \subset 'N(coset H @*^-1 C). Proof. -by move/sub_quotient_pre=> -> /subset_trans-> //; exact: morphpre_norm. +by move/sub_quotient_pre=> -> /subset_trans-> //; apply: morphpre_norm. Qed. Lemma cosetpre_normal C D : (coset H @*^-1 C <| coset H @*^-1 D) = (C <| D). @@ -638,7 +637,7 @@ Lemma quotient1_isom : isom A (A / 1) (coset 1). Proof. by apply: sub_isom coset1_injm; rewrite ?norms1. Qed. Lemma quotient1_isog : isog A (A / 1). -Proof. apply: isom_isog quotient1_isom; exact: norms1. Qed. +Proof. by apply: isom_isog quotient1_isom; apply: norms1. Qed. End Quotient1. @@ -805,10 +804,10 @@ exact: first_isom_loc. Qed. Lemma second_isog : H / (K :&: H) \isog H / K. -Proof. by rewrite setIC -{1 3}(ker_coset K); exact: first_isog_loc. Qed. +Proof. by rewrite setIC -{1 3}(ker_coset K); apply: first_isog_loc. Qed. Lemma weak_second_isog : H / (K :&: H) \isog H * K / K. -Proof. by rewrite quotientMidr; exact: second_isog. Qed. +Proof. by rewrite quotientMidr; apply: second_isog. Qed. End SecondIsomorphism. @@ -859,7 +858,7 @@ case/charP; rewrite quotientSGK // => sKG /= chKG. apply/charP; split=> // f injf Gf; apply/morphim_fixP => //. rewrite -(quotientSGK _ sHK); last by rewrite -morphimIim Gf subIset ?nHG. have{chHG} Hf: f @* H = H by case/charP: chHG => _; apply. -set q := quotm_morphism f nsHG; have{injf}: 'injm q by exact: injm_quotm. +set q := quotm_morphism f nsHG; have{injf}: 'injm q by apply: injm_quotm. have: q @* _ = _ := morphim_quotm _ _ _; move: q; rewrite Hf => q im_q injq. by rewrite -im_q chKG // im_q Gf. Qed. @@ -954,7 +953,7 @@ Proof. exact: dvdn_morphim. Qed. Lemma index_quotient_ker : K \subset G -> G \subset 'N(H) -> (#|G / H : K / H| * #|G :&: H : K|)%N = #|G : K|. -Proof. by rewrite -{5}(ker_coset H); exact: index_morphim_ker. Qed. +Proof. by rewrite -{5}(ker_coset H); apply: index_morphim_ker. Qed. Lemma index_quotient : G :&: K \subset 'N(H) -> #|G / H : K / H| %| #|G : K|. Proof. exact: index_morphim. Qed. |