Library mathcomp.solvable.gseries
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ H <|<| G <=> H is subnormal in G, i.e., H <| ... <| G.
+ invariant_factor A H G <=> A normalises both H and G, and H <| G.
+ A.-invariant <=> the (invariant_factor A) relation, in the context
+ of the g_rel.-series notation.
+ g_rel.-series H s <=> H :: s is a sequence of groups whose projection
+ to sets satisfies relation g_rel pairwise; for
+ example H <|<| G iff G = last H s for some s such
+ that normal.-series H s.
+ stable_factor A H G == H <| G and A centralises G / H.
+ A.-stable == the stable_factor relation, in the scope of the
+ r.-series notation.
+ G.-central == the central_factor relation, in the scope of the
+ r.-series notation.
+ maximal M G == M is a maximal proper subgroup of G.
+ maximal_eq M G == (M == G) or (maximal M G).
+ maxnormal M G N == M is a maximal subgroup of G normalized by N.
+ minnormal M N == M is a minimal nontrivial group normalized by N.
+ simple G == G is a (nontrivial) simple group.
+ := minnormal G G
+ G.-chief == the chief_factor relation, in the scope of the
+ r.-series notation.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section GroupDefs.
+ +
+Variable gT : finGroupType.
+Implicit Types A B U V : {set gT}.
+ +
+ +
+Definition subnormal A B :=
+ (A \subset B) && (iter #|B| (fun N ⇒ generated (class_support A N)) B == A).
+ +
+Definition invariant_factor A B C :=
+ [&& A \subset 'N(B), A \subset 'N(C) & B <| C].
+ +
+Definition group_rel_of (r : rel {set gT}) := [rel H G : groupT | r H G].
+ +
+Definition stable_factor A V U :=
+ ([~: U, A] \subset V) && (V <| U). (* this orders allows and3P to be used *)
+ +
+Definition central_factor A V U :=
+ [&& [~: U, A] \subset V, V \subset U & U \subset A].
+ +
+Definition maximal A B := [max A of G | G \proper B].
+ +
+Definition maximal_eq A B := (A == B) || maximal A B.
+ +
+Definition maxnormal A B U := [max A of G | G \proper B & U \subset 'N(G)].
+ +
+Definition minnormal A B := [min A of G | G :!=: 1 & B \subset 'N(G)].
+ +
+Definition simple A := minnormal A A.
+ +
+Definition chief_factor A V U := maxnormal V U A && (U <| A).
+End GroupDefs.
+ +
+ +
+Notation "H <|<| G" := (subnormal H G)
+ (at level 70, no associativity) : group_scope.
+ +
+Notation "A .-invariant" := (invariant_factor A)
+ (at level 2, format "A .-invariant") : group_rel_scope.
+Notation "A .-stable" := (stable_factor A)
+ (at level 2, format "A .-stable") : group_rel_scope.
+Notation "A .-central" := (central_factor A)
+ (at level 2, format "A .-central") : group_rel_scope.
+Notation "G .-chief" := (chief_factor G)
+ (at level 2, format "G .-chief") : group_rel_scope.
+ +
+ +
+Notation "r .-series" := (path (rel_of_simpl_rel (group_rel_of r)))
+ (at level 2, format "r .-series") : group_scope.
+ +
+Section Subnormal.
+ +
+Variable gT : finGroupType.
+Implicit Types (A B C D : {set gT}) (G H K : {group gT}).
+ +
+Let setIgr H G := (G :&: H)%G.
+Let sub_setIgr G H : G \subset H → G = setIgr H G.
+ +
+Let path_setIgr H G s :
+ normal.-series H s → normal.-series (setIgr G H) (map (setIgr G) s).
+ +
+Lemma subnormalP H G :
+ reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G).
+ +
+Lemma subnormal_refl G : G <|<| G.
+ +
+Lemma subnormal_trans K H G : H <|<| K → K <|<| G → H <|<| G.
+ +
+Lemma normal_subnormal H G : H <| G → H <|<| G.
+ +
+Lemma setI_subnormal G H K : K \subset G → H <|<| G → H :&: K <|<| K.
+ +
+Lemma subnormal_sub G H : H <|<| G → H \subset G.
+ +
+Lemma invariant_subnormal A G H :
+ A \subset 'N(G) → A \subset 'N(H) → H <|<| G →
+ exists2 s, (A.-invariant).-series H s & last H s = G.
+ +
+Lemma subnormalEsupport G H :
+ H <|<| G → H :=: G ∨ <<class_support H G>> \proper G.
+ +
+Lemma subnormalEr G H : H <|<| G →
+ H :=: G ∨ (∃ K : {group gT}, [/\ H <|<| K, K <| G & K \proper G]).
+ +
+Lemma subnormalEl G H : H <|<| G →
+ H :=: G ∨ (∃ K : {group gT}, [/\ H <| K, K <|<| G & H \proper K]).
+ +
+End Subnormal.
+ +
+ +
+Section MorphSubNormal.
+ +
+Variable gT : finGroupType.
+Implicit Type G H K : {group gT}.
+ +
+Lemma morphim_subnormal (rT : finGroupType) G (f : {morphism G >-> rT}) H K :
+ H <|<| K → f @* H <|<| f @* K.
+ +
+Lemma quotient_subnormal H G K : G <|<| K → G / H <|<| K / H.
+ +
+End MorphSubNormal.
+ +
+Section MaxProps.
+ +
+Variable gT : finGroupType.
+Implicit Types G H M : {group gT}.
+ +
+Lemma maximal_eqP M G :
+ reflect (M \subset G ∧
+ ∀ H, M \subset H → H \subset G → H :=: M ∨ H :=: G)
+ (maximal_eq M G).
+ +
+Lemma maximal_exists H G :
+ H \subset G →
+ H :=: G ∨ (exists2 M : {group gT}, maximal M G & H \subset M).
+ +
+Lemma mulg_normal_maximal G M H :
+ M <| G → maximal M G → H \subset G → ~~ (H \subset M) → (M × H = G)%g.
+ +
+End MaxProps.
+ +
+Section MinProps.
+ +
+Variable gT : finGroupType.
+Implicit Types G H M : {group gT}.
+ +
+Lemma minnormal_exists G H : H :!=: 1 → G \subset 'N(H) →
+ {M : {group gT} | minnormal M G & M \subset H}.
+ +
+End MinProps.
+ +
+Section MorphPreMax.
+ +
+Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
+Variables (M G : {group rT}).
+Hypotheses (dM : M \subset f @* D) (dG : G \subset f @* D).
+ +
+Lemma morphpre_maximal : maximal (f @*^-1 M) (f @*^-1 G) = maximal M G.
+ +
+Lemma morphpre_maximal_eq : maximal_eq (f @*^-1 M) (f @*^-1 G) = maximal_eq M G.
+ +
+End MorphPreMax.
+ +
+Section InjmMax.
+ +
+Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
+Variables M G L : {group gT}.
+ +
+Hypothesis injf : 'injm f.
+Hypotheses (dM : M \subset D) (dG : G \subset D) (dL : L \subset D).
+ +
+Lemma injm_maximal : maximal (f @* M) (f @* G) = maximal M G.
+ +
+Lemma injm_maximal_eq : maximal_eq (f @* M) (f @* G) = maximal_eq M G.
+ +
+Lemma injm_maxnormal : maxnormal (f @* M) (f @* G) (f @* L) = maxnormal M G L.
+ +
+Lemma injm_minnormal : minnormal (f @* M) (f @* G) = minnormal M G.
+ +
+End InjmMax.
+ +
+Section QuoMax.
+ +
+Variables (gT : finGroupType) (K G H : {group gT}).
+ +
+Lemma cosetpre_maximal (Q R : {group coset_of K}) :
+ maximal (coset K @*^-1 Q) (coset K @*^-1 R) = maximal Q R.
+ +
+Lemma cosetpre_maximal_eq (Q R : {group coset_of K}) :
+ maximal_eq (coset K @*^-1 Q) (coset K @*^-1 R) = maximal_eq Q R.
+ +
+Lemma quotient_maximal :
+ K <| G → K <| H → maximal (G / K) (H / K) = maximal G H.
+ +
+Lemma quotient_maximal_eq :
+ K <| G → K <| H → maximal_eq (G / K) (H / K) = maximal_eq G H.
+ +
+Lemma maximalJ x : maximal (G :^ x) (H :^ x) = maximal G H.
+ +
+Lemma maximal_eqJ x : maximal_eq (G :^ x) (H :^ x) = maximal_eq G H.
+ +
+End QuoMax.
+ +
+Section MaxNormalProps.
+ +
+Variables (gT : finGroupType).
+Implicit Types (A B C : {set gT}) (G H K L M : {group gT}).
+ +
+Lemma maxnormal_normal A B : maxnormal A B B → A <| B.
+ +
+Lemma maxnormal_proper A B C : maxnormal A B C → A \proper B.
+ +
+Lemma maxnormal_sub A B C : maxnormal A B C → A \subset B.
+ +
+Lemma ex_maxnormal_ntrivg G : G :!=: 1→ {N : {group gT} | maxnormal N G G}.
+ +
+Lemma maxnormalM G H K :
+ maxnormal H G G → maxnormal K G G → H :<>: K → H × K = G.
+ +
+Lemma maxnormal_minnormal G L M :
+ G \subset 'N(M) → L \subset 'N(G) → maxnormal M G L →
+ minnormal (G / M) (L / M).
+ +
+Lemma minnormal_maxnormal G L M :
+ M <| G → L \subset 'N(M) → minnormal (G / M) (L / M) → maxnormal M G L.
+ +
+End MaxNormalProps.
+ +
+Section Simple.
+ +
+Implicit Types gT rT : finGroupType.
+ +
+Lemma simpleP gT (G : {group gT}) :
+ reflect (G :!=: 1 ∧ ∀ H : {group gT}, H <| G → H :=: 1 ∨ H :=: G)
+ (simple G).
+ +
+Lemma quotient_simple gT (G H : {group gT}) :
+ H <| G → simple (G / H) = maxnormal H G G.
+ +
+Lemma isog_simple gT rT (G : {group gT}) (M : {group rT}) :
+ G \isog M → simple G = simple M.
+ +
+Lemma simple_maxnormal gT (G : {group gT}) : simple G = maxnormal 1 G G.
+ +
+End Simple.
+ +
+Section Chiefs.
+ +
+Variable gT : finGroupType.
+Implicit Types G H U V : {group gT}.
+ +
+Lemma chief_factor_minnormal G V U :
+ chief_factor G V U → minnormal (U / V) (G / V).
+ +
+Lemma acts_irrQ G U V :
+ G \subset 'N(V) → V <| U →
+ acts_irreducibly G (U / V) 'Q = minnormal (U / V) (G / V).
+ +
+Lemma chief_series_exists H G :
+ H <| G → {s | (G.-chief).-series 1%G s & last 1%G s = H}.
+ +
+End Chiefs.
+ +
+Section Central.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Types H K : {group gT}.
+ +
+Lemma central_factor_central H K :
+ central_factor G H K → (K / H) \subset 'Z(G / H).
+ +
+Lemma central_central_factor H K :
+ (K / H) \subset 'Z(G / H) → H <| K → H <| G → central_factor G H K.
+ +
+End Central.
+
++Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section GroupDefs.
+ +
+Variable gT : finGroupType.
+Implicit Types A B U V : {set gT}.
+ +
+ +
+Definition subnormal A B :=
+ (A \subset B) && (iter #|B| (fun N ⇒ generated (class_support A N)) B == A).
+ +
+Definition invariant_factor A B C :=
+ [&& A \subset 'N(B), A \subset 'N(C) & B <| C].
+ +
+Definition group_rel_of (r : rel {set gT}) := [rel H G : groupT | r H G].
+ +
+Definition stable_factor A V U :=
+ ([~: U, A] \subset V) && (V <| U). (* this orders allows and3P to be used *)
+ +
+Definition central_factor A V U :=
+ [&& [~: U, A] \subset V, V \subset U & U \subset A].
+ +
+Definition maximal A B := [max A of G | G \proper B].
+ +
+Definition maximal_eq A B := (A == B) || maximal A B.
+ +
+Definition maxnormal A B U := [max A of G | G \proper B & U \subset 'N(G)].
+ +
+Definition minnormal A B := [min A of G | G :!=: 1 & B \subset 'N(G)].
+ +
+Definition simple A := minnormal A A.
+ +
+Definition chief_factor A V U := maxnormal V U A && (U <| A).
+End GroupDefs.
+ +
+ +
+Notation "H <|<| G" := (subnormal H G)
+ (at level 70, no associativity) : group_scope.
+ +
+Notation "A .-invariant" := (invariant_factor A)
+ (at level 2, format "A .-invariant") : group_rel_scope.
+Notation "A .-stable" := (stable_factor A)
+ (at level 2, format "A .-stable") : group_rel_scope.
+Notation "A .-central" := (central_factor A)
+ (at level 2, format "A .-central") : group_rel_scope.
+Notation "G .-chief" := (chief_factor G)
+ (at level 2, format "G .-chief") : group_rel_scope.
+ +
+ +
+Notation "r .-series" := (path (rel_of_simpl_rel (group_rel_of r)))
+ (at level 2, format "r .-series") : group_scope.
+ +
+Section Subnormal.
+ +
+Variable gT : finGroupType.
+Implicit Types (A B C D : {set gT}) (G H K : {group gT}).
+ +
+Let setIgr H G := (G :&: H)%G.
+Let sub_setIgr G H : G \subset H → G = setIgr H G.
+ +
+Let path_setIgr H G s :
+ normal.-series H s → normal.-series (setIgr G H) (map (setIgr G) s).
+ +
+Lemma subnormalP H G :
+ reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G).
+ +
+Lemma subnormal_refl G : G <|<| G.
+ +
+Lemma subnormal_trans K H G : H <|<| K → K <|<| G → H <|<| G.
+ +
+Lemma normal_subnormal H G : H <| G → H <|<| G.
+ +
+Lemma setI_subnormal G H K : K \subset G → H <|<| G → H :&: K <|<| K.
+ +
+Lemma subnormal_sub G H : H <|<| G → H \subset G.
+ +
+Lemma invariant_subnormal A G H :
+ A \subset 'N(G) → A \subset 'N(H) → H <|<| G →
+ exists2 s, (A.-invariant).-series H s & last H s = G.
+ +
+Lemma subnormalEsupport G H :
+ H <|<| G → H :=: G ∨ <<class_support H G>> \proper G.
+ +
+Lemma subnormalEr G H : H <|<| G →
+ H :=: G ∨ (∃ K : {group gT}, [/\ H <|<| K, K <| G & K \proper G]).
+ +
+Lemma subnormalEl G H : H <|<| G →
+ H :=: G ∨ (∃ K : {group gT}, [/\ H <| K, K <|<| G & H \proper K]).
+ +
+End Subnormal.
+ +
+ +
+Section MorphSubNormal.
+ +
+Variable gT : finGroupType.
+Implicit Type G H K : {group gT}.
+ +
+Lemma morphim_subnormal (rT : finGroupType) G (f : {morphism G >-> rT}) H K :
+ H <|<| K → f @* H <|<| f @* K.
+ +
+Lemma quotient_subnormal H G K : G <|<| K → G / H <|<| K / H.
+ +
+End MorphSubNormal.
+ +
+Section MaxProps.
+ +
+Variable gT : finGroupType.
+Implicit Types G H M : {group gT}.
+ +
+Lemma maximal_eqP M G :
+ reflect (M \subset G ∧
+ ∀ H, M \subset H → H \subset G → H :=: M ∨ H :=: G)
+ (maximal_eq M G).
+ +
+Lemma maximal_exists H G :
+ H \subset G →
+ H :=: G ∨ (exists2 M : {group gT}, maximal M G & H \subset M).
+ +
+Lemma mulg_normal_maximal G M H :
+ M <| G → maximal M G → H \subset G → ~~ (H \subset M) → (M × H = G)%g.
+ +
+End MaxProps.
+ +
+Section MinProps.
+ +
+Variable gT : finGroupType.
+Implicit Types G H M : {group gT}.
+ +
+Lemma minnormal_exists G H : H :!=: 1 → G \subset 'N(H) →
+ {M : {group gT} | minnormal M G & M \subset H}.
+ +
+End MinProps.
+ +
+Section MorphPreMax.
+ +
+Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
+Variables (M G : {group rT}).
+Hypotheses (dM : M \subset f @* D) (dG : G \subset f @* D).
+ +
+Lemma morphpre_maximal : maximal (f @*^-1 M) (f @*^-1 G) = maximal M G.
+ +
+Lemma morphpre_maximal_eq : maximal_eq (f @*^-1 M) (f @*^-1 G) = maximal_eq M G.
+ +
+End MorphPreMax.
+ +
+Section InjmMax.
+ +
+Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
+Variables M G L : {group gT}.
+ +
+Hypothesis injf : 'injm f.
+Hypotheses (dM : M \subset D) (dG : G \subset D) (dL : L \subset D).
+ +
+Lemma injm_maximal : maximal (f @* M) (f @* G) = maximal M G.
+ +
+Lemma injm_maximal_eq : maximal_eq (f @* M) (f @* G) = maximal_eq M G.
+ +
+Lemma injm_maxnormal : maxnormal (f @* M) (f @* G) (f @* L) = maxnormal M G L.
+ +
+Lemma injm_minnormal : minnormal (f @* M) (f @* G) = minnormal M G.
+ +
+End InjmMax.
+ +
+Section QuoMax.
+ +
+Variables (gT : finGroupType) (K G H : {group gT}).
+ +
+Lemma cosetpre_maximal (Q R : {group coset_of K}) :
+ maximal (coset K @*^-1 Q) (coset K @*^-1 R) = maximal Q R.
+ +
+Lemma cosetpre_maximal_eq (Q R : {group coset_of K}) :
+ maximal_eq (coset K @*^-1 Q) (coset K @*^-1 R) = maximal_eq Q R.
+ +
+Lemma quotient_maximal :
+ K <| G → K <| H → maximal (G / K) (H / K) = maximal G H.
+ +
+Lemma quotient_maximal_eq :
+ K <| G → K <| H → maximal_eq (G / K) (H / K) = maximal_eq G H.
+ +
+Lemma maximalJ x : maximal (G :^ x) (H :^ x) = maximal G H.
+ +
+Lemma maximal_eqJ x : maximal_eq (G :^ x) (H :^ x) = maximal_eq G H.
+ +
+End QuoMax.
+ +
+Section MaxNormalProps.
+ +
+Variables (gT : finGroupType).
+Implicit Types (A B C : {set gT}) (G H K L M : {group gT}).
+ +
+Lemma maxnormal_normal A B : maxnormal A B B → A <| B.
+ +
+Lemma maxnormal_proper A B C : maxnormal A B C → A \proper B.
+ +
+Lemma maxnormal_sub A B C : maxnormal A B C → A \subset B.
+ +
+Lemma ex_maxnormal_ntrivg G : G :!=: 1→ {N : {group gT} | maxnormal N G G}.
+ +
+Lemma maxnormalM G H K :
+ maxnormal H G G → maxnormal K G G → H :<>: K → H × K = G.
+ +
+Lemma maxnormal_minnormal G L M :
+ G \subset 'N(M) → L \subset 'N(G) → maxnormal M G L →
+ minnormal (G / M) (L / M).
+ +
+Lemma minnormal_maxnormal G L M :
+ M <| G → L \subset 'N(M) → minnormal (G / M) (L / M) → maxnormal M G L.
+ +
+End MaxNormalProps.
+ +
+Section Simple.
+ +
+Implicit Types gT rT : finGroupType.
+ +
+Lemma simpleP gT (G : {group gT}) :
+ reflect (G :!=: 1 ∧ ∀ H : {group gT}, H <| G → H :=: 1 ∨ H :=: G)
+ (simple G).
+ +
+Lemma quotient_simple gT (G H : {group gT}) :
+ H <| G → simple (G / H) = maxnormal H G G.
+ +
+Lemma isog_simple gT rT (G : {group gT}) (M : {group rT}) :
+ G \isog M → simple G = simple M.
+ +
+Lemma simple_maxnormal gT (G : {group gT}) : simple G = maxnormal 1 G G.
+ +
+End Simple.
+ +
+Section Chiefs.
+ +
+Variable gT : finGroupType.
+Implicit Types G H U V : {group gT}.
+ +
+Lemma chief_factor_minnormal G V U :
+ chief_factor G V U → minnormal (U / V) (G / V).
+ +
+Lemma acts_irrQ G U V :
+ G \subset 'N(V) → V <| U →
+ acts_irreducibly G (U / V) 'Q = minnormal (U / V) (G / V).
+ +
+Lemma chief_series_exists H G :
+ H <| G → {s | (G.-chief).-series 1%G s & last 1%G s = H}.
+ +
+End Chiefs.
+ +
+Section Central.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Types H K : {group gT}.
+ +
+Lemma central_factor_central H K :
+ central_factor G H K → (K / H) \subset 'Z(G / H).
+ +
+Lemma central_central_factor H K :
+ (K / H) \subset 'Z(G / H) → H <| K → H <| G → central_factor G H K.
+ +
+End Central.
+