(Joint Center)Library MathComp.gseries

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path fintype bigop.
Require Import finset fingroup morphism automorphism quotient action.
Require Import 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}.

Notation Local groupT := (group_of (Phant gT)).

Definition subnormal A B :=
  (A \subset B) && (iter #|B| (fun Ngenerated (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 HG = setIgr H G.

Let path_setIgr H G s :
   normal.-series H snormal.-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 <|<| KK <|<| GH <|<| G.

Lemma normal_subnormal H G : H <| GH <|<| G.

Lemma setI_subnormal G H K : K \subset GH <|<| GH :&: K <|<| K.

Lemma subnormal_sub G H : H <|<| GH \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 <|<| GH :=: 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.

Implicit Arguments subnormalP [gT G H].

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 <|<| Kf @* H <|<| f @* K.

Lemma quotient_subnormal H G K : G <|<| KG / 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 HH \subset GH :=: 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 <| Gmaximal M GH \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 <| GK <| Hmaximal (G / K) (H / K) = maximal G H.

Lemma quotient_maximal_eq :
  K <| GK <| Hmaximal_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 BA <| B.

Lemma maxnormal_proper A B C : maxnormal A B CA \proper B.

Lemma maxnormal_sub A B C : maxnormal A B CA \subset B.

Lemma ex_maxnormal_ntrivg G : G :!=: 1-> {N : {group gT} | maxnormal N G G}.

Lemma maxnormalM G H K :
  maxnormal H G Gmaxnormal K G GH :<>: KH × 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 <| GL \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 <| GH :=: 1 H :=: G)
          (simple G).

Lemma quotient_simple gT (G H : {group gT}) :
  H <| Gsimple (G / H) = maxnormal H G G.

Lemma isog_simple gT rT (G : {group gT}) (M : {group rT}) :
  G \isog Msimple 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 Uminnormal (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 <| KH <| Gcentral_factor G H K.

End Central.