Library center

 Definition of the center of a group and of external central products:      
           'Z(G) == the center of the group G, i.e., 'C_G(G).               
   cprod_by isoZ == the finGroupType for the central product of H and K     
                    with centers identified by the isomorphism gz on 'Z(H); 
                    here isoZ : isom 'Z(H) 'Z(K) gz. Note that the actual   
                    central product is [set: cprod_by isoZ].                
    cpairg1 isoZ == the isomorphism from H to cprod_by isoZ, isoZ as above. 
    cpair1g isoZ == the isomorphism from K to cprod_by isoZ, isoZ as above. 
      xcprod H K == the finGroupType for the external central product of H  
                    and K with identified centers, provided the dynamically 
                    tested condition 'Z(H) \isog 'Z(K) holds.               
      ncprod H n == the finGroupType for the central product of n copies of 
                    H with their centers identified; [set: ncprod H 0] is   
                    isomorphic to 'Z(H).                                    
  xcprodm cf eqf == the morphism induced on cprod_by isoZ, where as above   
                    isoZ : isom 'Z(H) 'Z(K) gz, by fH : {morphism H >-> rT} 
                    and fK : {morphism K >-> rT}, given both                
                    cf : fH @* H \subset 'C(fK @* K) and                    
                    eqf : {in 'Z(H), fH =1 fK \o gz}.                       
   Following Aschbacher, we only provide external central products with     
 identified centers, as these are well defined provided the local center    
 isomorphism group of one of the subgroups is full. Nevertheless the        
 entire construction could be carried out under the weaker assumption that  
 gz is an isomorphism between subgroups of 'Z(H) and 'Z(K), and even the    
 uniqueness theorem holds under the weaker assumption that gz map 'Z(H) to  
 a characteristic subgroup of 'Z(K) not isomorphic to any other subgroup of 
 'Z(K), a condition that holds for example when K is cyclic, as in the      
 structure theorem for p-groups of symplectic type.                         


Import GroupScope.

Section Defs.

Variable gT : finGroupType.

Definition center (A : {set gT}) := 'C_A(A).

Canonical Structure center_group (G : {group gT}) : {group gT} :=
  Eval hnf in [group of center G].

End Defs.

Notation "''Z' ( A )" := (center A) : group_scope.
Notation "''Z' ( H )" := (center_group H) : subgroup_scope.

Lemma morphim_center : GFunctor.pcontinuous center.

Canonical Structure center_igFun :=
  [igFun by fun _ _ => subsetIl _ _ & morphim_center].
Canonical Structure center_gFun := [gFun by morphim_center].
Canonical Structure center_pgFun := [pgFun by morphim_center].

Section Center.

Variables gT : finGroupType.
Implicit Type rT : finGroupType.
Implicit Types x y : gT.
Implicit Types A B : {set gT}.
Implicit Types G H K D : {group gT}.

Lemma subcentP : forall A B x,
  reflect (x \in A /\ centralises x B) (x \in 'C_A(B)).

Lemma subcent_sub : forall A B, 'C_A(B) \subset 'N_A(B).

Lemma subcent_norm : forall G B, 'N_G(B) \subset 'N('C_G(B)).

Lemma subcent_normal : forall G B, 'C_G(B) <| 'N_G(B).

Lemma subcent_char : forall G H K, H \char G -> K \char G -> 'C_H(K) \char G.

Lemma centerP : forall A x,
  reflect (x \in A /\ centralises x A) (x \in 'Z(A)).

Lemma center_sub : forall A, 'Z(A) \subset A.

Lemma center1 : 'Z(1) = [1 gT].

Lemma centerC : forall A, {in A, centralised 'Z(A)}.

Lemma center_normal : forall G, 'Z(G) <| G.

Lemma sub_center_normal : forall H G, H \subset 'Z(G) -> H <| G.

Lemma center_abelian : forall G, abelian 'Z(G).

Lemma center_char : forall G, 'Z(G) \char G.

Lemma center_idP : forall A, reflect ('Z(A) = A) (abelian A).

Lemma subcent1P : forall A x y,
  reflect (y \in A /\ commute x y) (y \in 'C_A[x]).

Lemma subcent1_id : forall x G, x \in G -> x \in 'C_G[x].

Lemma subcent1_sub : forall x G, 'C_G[x] \subset G.

Lemma subcent1C : forall x y G, x \in G -> y \in 'C_G[x] -> x \in 'C_G[y].

Lemma subcent1_cycle_sub : forall x G, x \in G -> <[x]> \subset 'C_G[x].

Lemma subcent1_cycle_norm : forall x G, 'C_G[x] \subset 'N(<[x]>).

Lemma subcent1_cycle_normal : forall x G, x \in G -> <[x]> <| 'C_G[x].

 Gorenstein. 1.3.4 
Lemma cyclic_center_factor_abelian : forall G, cyclic (G / 'Z(G)) -> abelian G.

Lemma cyclic_factor_abelian : forall H G,
  H \subset 'Z(G) -> cyclic (G / H) -> abelian G.

Section Injm.

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

Hypothesis injf : 'injm f.

Lemma injm_center : forall G, G \subset D -> f @* 'Z(G) = 'Z(f @* G).

End Injm.

End Center.

Implicit Arguments center_idP [gT A].

Lemma isog_center : forall (aT rT : finGroupType),
  forall (G : {group aT}) (H : {group rT}), G \isog H -> 'Z(G) \isog 'Z(H).

Section Product.

Variable gT : finGroupType.
Implicit Types G H K : {group gT}.
Implicit Types A B C : {set gT}.

Lemma center_prod : forall H K,
  K \subset 'C(H) -> 'Z(H) * 'Z(K) = 'Z(H * K).

Lemma center_cprod : forall A B G, A \* B = G -> 'Z(A) \* 'Z(B) = 'Z(G).

Lemma center_bigcprod : forall I r P (F : I -> {set gT}) G,
  \big[cprod/1]_(i <- r | P i) F i = G
  -> \big[cprod/1]_(i <- r | P i) 'Z(F i) = 'Z(G).

Lemma cprod_center_id : forall G, G \* 'Z(G) = G.

Lemma center_dprod : forall A B G, A \x B = G -> 'Z(A) \x 'Z(B) = 'Z(G).

Lemma center_bigdprod : forall I r P (F: I -> {set gT}) G,
  \big[dprod/1]_(i <- r | P i) F i = G
    -> \big[dprod/1]_(i <- r | P i) 'Z(F i) = 'Z(G).

Lemma Aut_cprod_full : forall G H K,
    H \* K = G -> 'Z(H) = 'Z(K) ->
    Aut_in (Aut H) 'Z(H) \isog Aut 'Z(H) ->
    Aut_in (Aut K) 'Z(K) \isog Aut 'Z(K) ->
  Aut_in (Aut G) 'Z(G) \isog Aut 'Z(G).

End Product.

Section CprodBy.

Variables gTH gTK : finGroupType.
Variables (H : {group gTH}) (K : {group gTK}) (gz : {morphism 'Z(H) >-> gTK}).

Definition ker_cprod_by of isom 'Z(H) 'Z(K) gz :=
  [set xy | let: (x, y) := xy in (x \in 'Z(H)) && (y == (gz x)^-1)].

Hypothesis isoZ : isom 'Z(H) 'Z(K) gz.

Let injgz : 'injm gz.
Let gzZ : gz @* 'Z(H) = 'Z(K).
Let gzZchar : gz @* 'Z(H) \char 'Z(K).
Let sgzZZ : gz @* 'Z(H) \subset 'Z(K) := char_sub gzZchar.
Let sgzZG : gz @* 'Z(H) \subset K := subset_trans sgzZZ sZK.

Lemma ker_cprod_by_is_group : group_set kerHK.
Canonical Structure ker_cprod_by_group := Group ker_cprod_by_is_group.

Lemma ker_cprod_by_central : kerHK \subset 'Z(setX H K).

Definition cprod_by := locked (subFinGroupType [group of setX H K / kerHK]).
Local Notation C := [set: FinGroup.arg_sort (FinGroup.base cprod_by)].

Definition in_cprod : gTH * gTK -> cprod_by.

Lemma in_cprodM : {in setX H K &, {morph in_cprod : u v / u * v}}.
Canonical Structure in_cprod_morphism := Morphism in_cprodM.

Lemma ker_in_cprod : 'ker in_cprod = kerHK.

Lemma cpairg1_dom : H \subset 'dom (in_cprod \o @pairg1 gTH gTK).

Lemma cpair1g_dom : K \subset 'dom (in_cprod \o @pair1g gTH gTK).

Definition cpairg1 := tag (restrmP _ cpairg1_dom).
Definition cpair1g := tag (restrmP _ cpair1g_dom).

Local Notation CH := (mfun cpairg1 @* gval H).
Local Notation CK := (mfun cpair1g @* gval K).

Lemma injm_cpairg1 : 'injm cpairg1.

Lemma injm_cpair1g : 'injm cpair1g.

Lemma im_cpair_cent : CK \subset 'C(CH).
Hint Resolve im_cpair_cent.

Lemma im_cpair : CH * CK = C.

Lemma im_cpair_cprod : CH \* CK = C.

Lemma eq_cpairZ : {in 'Z(H), cpairg1 =1 cpair1g \o gz}.

Lemma setI_im_cpair : CH :&: CK = 'Z(CH).

Lemma cpair1g_center : cpair1g @* 'Z(K) = 'Z(C).

 Uses gzZ. 
Lemma cpair_center_id : 'Z(CH) = 'Z(CK).

 Uses gzZ. 
Lemma cpairg1_center : cpairg1 @* 'Z(H) = 'Z(C).

Section ExtCprodm.

Variable rT : finGroupType.
Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
Hypothesis cfHK : fK @* K \subset 'C(fH @* H).
Hypothesis eq_fHK : {in 'Z(H), fH =1 fK \o gz}.


Lemma xcprodm_cent : gK @* CK \subset 'C(gH @* CH).

Lemma xcprodmI : {in CH :&: CK, gH =1 gK}.

Definition xcprodm := cprodm im_cpair_cprod xcprodm_cent xcprodmI.
Canonical Structure xcprod_morphism := [morphism of xcprodm].

Lemma xcprodmEl : {in H, forall x, xcprodm (cpairg1 x) = fH x}.

Lemma xcprodmEr : {in K, forall y, xcprodm (cpair1g y) = fK y}.

Lemma xcprodmE :
  {in H & K, forall x y, xcprodm (cpairg1 x * cpair1g y) = fH x * fK y}.

Lemma im_xcprodm : xcprodm @* C = fH @* H * fK @* K.

Lemma im_xcprodml : forall A, xcprodm @* (cpairg1 @* A) = fH @* A.

Lemma im_xcprodmr : forall A, xcprodm @* (cpair1g @* A) = fK @* A.

Lemma injm_xcprodm : 'injm xcprodm = 'injm fH && 'injm fK.

End ExtCprodm.

 Uses gzZchar. 
Lemma Aut_cprod_by_full :
    Aut_in (Aut H) 'Z(H) \isog Aut 'Z(H) ->
    Aut_in (Aut K) 'Z(K) \isog Aut 'Z(K) ->
  Aut_in (Aut C) 'Z(C) \isog Aut 'Z(C).

Section Isomorphism.

Let gzZ_lone : forall Y : {group gTK},
  Y \subset 'Z(K) -> gz @* 'Z(H) \isog Y -> gz @* 'Z(H) = Y.

Variables (rT : finGroupType) (GH GK G : {group rT}).
Hypotheses (defG : GH \* GK = G) (ziGHK : GH :&: GK = 'Z(GH)).
Hypothesis AutZHfull : Aut_in (Aut H) 'Z(H) \isog Aut 'Z(H).
Hypotheses (isoGH : GH \isog H) (isoGK : GK \isog K).

 Uses gzZ_lone 
Lemma cprod_by_uniq :
  exists f : {morphism G >-> cprod_by},
    [/\ isom G C f, f @* GH = CH & f @* GK = CK].

Lemma isog_cprod_by : G \isog C.

End Isomorphism.

End CprodBy.

Section ExtCprod.
Import finfun.

Variables gTH gTK : finGroupType.
Variables (H : {group gTH}) (K : {group gTK}).

Local Notation isob := ('Z(H) \isog 'Z(K)) (only parsing).

Lemma xcprod_subproof :
  {gz : {morphism 'Z(H) >-> gt_ isob} | isom 'Z(H) 'Z(G_ isob) gz}.

Definition xcprod := cprod_by (svalP xcprod_subproof).

Inductive xcprod_spec : finGroupType -> Prop :=
  XcprodSpec gz isoZ : xcprod_spec (@cprod_by gTH gTK H K gz isoZ).

Lemma xcprodP : 'Z(H) \isog 'Z(K) -> xcprod_spec xcprod.

Lemma isog_xcprod : forall (rT : finGroupType) (GH GK G : {group rT}),
    Aut_in (Aut H) 'Z(H) \isog Aut 'Z(H) ->
    GH \isog H -> GK \isog K -> GH \* GK = G -> 'Z(GH) = 'Z(GK) ->
  G \isog [set: xcprod].

End ExtCprod.

Section IterCprod.

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

Definition ncprod := locked (fix loop n : finGroupType :=
  if n is n'.+1 then xcprod G [set: loop n']
  else [finGroupType of subg_of 'Z(G)]).

Local Notation G_ n := [set: gsort (ncprod n)].

Lemma ncprod0 : G_ 0 \isog 'Z(G).

Lemma center_ncprod0 : 'Z(G_ 0) = G_ 0.

Lemma center_ncprod : forall n, 'Z(G_ n) \isog 'Z(G).

Lemma ncprodS : forall n, xcprod_spec G [set: ncprod n] (ncprod n.+1).

Lemma ncprod1 : G_ 1 \isog G.

Lemma Aut_ncprod_full : forall n,
    Aut_in (Aut G) 'Z(G) \isog Aut 'Z(G) ->
  Aut_in (Aut (G_ n)) 'Z(G_ n) \isog Aut 'Z(G_ n).

End IterCprod.