Library mathcomp.solvable.gseries
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import fintype bigop finset fingroup morphism.
From mathcomp Require Import automorphism quotient action commutator center.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import fintype bigop finset fingroup morphism.
From mathcomp Require Import automorphism quotient action commutator center.
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.