# 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.
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.
Declare Scope group_rel_scope.
Import GroupScope.
Section GroupDefs.
Variable gT : finGroupType.
Implicit Types A B U V : {set gT}.
Local Notation groupT := (group_of 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.
Arguments subnormal {gT} A%g B%g.
Arguments invariant_factor {gT} A%g B%g C%g.
Arguments stable_factor {gT} A%g V%g U%g.
Arguments central_factor {gT} A%g V%g U%g.
Arguments maximal {gT} A%g B%g.
Arguments maximal_eq {gT} A%g B%g.
Arguments maxnormal {gT} A%g B%g U%g.
Arguments minnormal {gT} A%g B%g.
Arguments simple {gT} A%g.
Arguments chief_factor {gT} A%g V%g U%g.
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.
Arguments group_rel_of {gT} r%group_rel_scope _%G _%G : extra scopes.
Notation "r .-series" := (path (rel_of_simpl (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.
Arguments subnormalP {gT H G}.
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.