Library mathcomp.solvable.gseries
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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.
-