Library gseries

           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      
                            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 subgroup 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.                              


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 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).
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.
Notation sT := {set gT}.

Implicit Types A B C D : sT.
Implicit Type G H K : {group gT}.

Let sub_setIgr : forall G H, G \subset H -> G = setIgr H G.

Let path_setIgr : forall H G s,
   normal.-series H s -> normal.-series (setIgr G H) (map (setIgr G) s).

Lemma subnormalP : forall H G,
  reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G).

Lemma subnormal_refl : forall G, G <|<| G.

Lemma subnormal_trans : forall K H G, H <|<| K -> K <|<| G -> H <|<| G.

Lemma normal_subnormal : forall H G, H <| G -> H <|<| G.

Lemma setI_subnormal : forall G H K,
  K \subset G -> H <|<| G -> H :&: K <|<| K.

Lemma subnormal_sub : forall G H, H <|<| G -> H \subset G.

Lemma invariant_subnormal : forall 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 : forall G H,
  H <|<| G -> H :=: G \/ <<class_support H G>> \proper G.

Lemma subnormalEr : forall G H, H <|<| G ->
  H :=: G \/ (exists K : {group gT}, [/\ H <|<| K, K <| G & K \proper G]).

Lemma subnormalEl : forall G H, H <|<| G ->
  H :=: G \/ (exists 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 : forall (rT : finGroupType)
  G (f : {morphism G >-> rT}) H K, H <|<| K -> f @* H <|<| f @* K.

Lemma quotient_subnormal : forall 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 : forall M G,
  reflect (M \subset G /\
             forall H, M \subset H -> H \subset G -> H :=: M \/ H :=: G)
       (maximal_eq M G).

Lemma maximal_exists : forall H G,
    H \subset G ->
  H :=: G \/ (exists2 M : {group gT}, maximal M G & H \subset M).

Lemma mulg_normal_maximal : forall 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 : forall 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}).
Implicit Types Q R : {group rT}.

Lemma morphpre_maximal : forall Q R,
  Q \subset f @* D -> R \subset f @* D ->
  maximal (f @*^-1 Q) (f @*^-1 R) = maximal Q R.

Lemma morphpre_maximal_eq : forall Q R,
  Q \subset f @* D -> R \subset f @* D ->
  maximal_eq (f @*^-1 Q) (f @*^-1 R) = maximal_eq Q R.

End MorphPreMax.

Section InjmMax.

Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
Variables G H K : {group gT}.

Hypothesis injf : 'injm f.

Lemma injm_maximal :
  G \subset D -> H \subset D -> maximal (f @* G) (f @* H) = maximal G H.

Lemma injm_maximal_eq :
  G \subset D -> H \subset D -> maximal (f @* G) (f @* H) = maximal G H.

End InjmMax.

Section QuoMax.

Variables (gT : finGroupType) (K G H : {group gT}).

Lemma cosetpre_maximal : forall Q R : {group coset_of K},
  maximal (coset K @*^-1 Q) (coset K @*^-1 R) = maximal Q R.

Lemma cosetpre_maximal_eq : forall 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 : forall x, maximal (G :^ x) (H :^ x) = maximal G H.

Lemma maximal_eqJ : forall 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}.
Implicit Types G H K : {group gT}.

Lemma maxnormal_normal : forall A B, maxnormal A B B -> A <| B.

Lemma maxnormal_proper : forall A B C, maxnormal A B C -> A \proper B.

Lemma maxnormal_sub : forall A B C, maxnormal A B C -> A \subset B.

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

Lemma maxnormalM : forall G H K,
  maxnormal H G G -> maxnormal K G G -> H :<>: K -> H * K = G.

End MaxNormalProps.

Section Simple.

Implicit Types gT rT : finGroupType.

Lemma simpleP : forall gT (G : {group gT}),
  reflect (G :!=: 1 /\ forall H : {group gT}, H <| G -> H :=: 1 \/ H :=: G)
          (simple G).

Lemma quotient_simple : forall gT (G H : {group gT}),
  H <| G -> simple (G / H) = maxnormal H G G.

Lemma isog_simple : forall gT rT (G : {group gT}) (M : {group rT}),
  G \isog M -> simple G = simple M.

Lemma simple_maxnormal : forall gT (G : {group gT}),
   simple G = maxnormal 1 G G.

End Simple.

Section Chiefs.

Variable gT: finGroupType.

Lemma chief_factor_minnormal : forall G V U : {group gT},
  chief_factor G V U -> minnormal (U / V) (G / V).

Lemma acts_irrQ : forall G U V : {group gT},
    G \subset 'N(V) -> V <| U ->
  acts_irreducibly G (U / V) 'Q = minnormal (U / V) (G / V).

Lemma chief_series_exists : forall H G : {group gT},
  H <| G -> {s | (G.-chief).-series 1%G s & last 1%G s = H}.

End Chiefs.

Section Central.

Variable gT : finGroupType.
Variable G : {group gT}.
Implicit Type H K : {group gT}.

Lemma central_factor_central : forall H K,
  central_factor G H K -> (K / H) \subset 'Z(G / H).

Lemma central_central_factor : forall H K,
  (K / H) \subset 'Z(G / H) -> H <| K -> H <| G -> central_factor G H K.

End Central.