Library mathcomp.solvable.center
(* (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 div.
From mathcomp Require Import fintype bigop finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient action gproduct gfunctor.
From mathcomp Require Import cyclic.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import fintype bigop finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient action gproduct gfunctor.
From mathcomp Require Import cyclic.
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.
Set Implicit Arguments.
Import GroupScope.
Section Defs.
Variable gT : finGroupType.
Definition center (A : {set gT}) := 'C_A(A).
Canonical center_group (G : {group gT}) : {group gT} :=
Eval hnf in [group of center G].
End Defs.
Arguments center {gT} A%g.
Notation "''Z' ( A )" := (center A) : group_scope.
Notation "''Z' ( H )" := (center_group H) : Group_scope.
Lemma morphim_center : GFunctor.pcontinuous (@center).
Canonical center_igFun := [igFun by fun _ _ ⇒ subsetIl _ _ & morphim_center].
Canonical center_gFun := [gFun by morphim_center].
Canonical center_pgFun := [pgFun by morphim_center].
Section Center.
Variables gT : finGroupType.
Implicit Type rT : finGroupType.
Implicit Types (x y : gT) (A B : {set gT}) (G H K D : {group gT}).
Lemma subcentP A B x : reflect (x \in A ∧ centralises x B) (x \in 'C_A(B)).
Lemma subcent_sub A B : 'C_A(B) \subset 'N_A(B).
Lemma subcent_norm G B : 'N_G(B) \subset 'N('C_G(B)).
Lemma subcent_normal G B : 'C_G(B) <| 'N_G(B).
Lemma subcent_char G H K : H \char G → K \char G → 'C_H(K) \char G.
Lemma centerP A x : reflect (x \in A ∧ centralises x A) (x \in 'Z(A)).
Lemma center_sub A : 'Z(A) \subset A.
Lemma center1 : 'Z(1) = 1 :> {set gT}.
Lemma centerC A : {in A, centralised 'Z(A)}.
Lemma center_normal G : 'Z(G) <| G.
Lemma sub_center_normal H G : H \subset 'Z(G) → H <| G.
Lemma center_abelian G : abelian 'Z(G).
Lemma center_char G : 'Z(G) \char G.
Lemma center_idP A : reflect ('Z(A) = A) (abelian A).
Lemma center_class_formula G :
#|G| = #|'Z(G)| + \sum_(xG in [set x ^: G | x in G :\: 'C(G)]) #|xG|.
Lemma subcent1P A x y : reflect (y \in A ∧ commute x y) (y \in 'C_A[x]).
Lemma subcent1_id x G : x \in G → x \in 'C_G[x].
Lemma subcent1_sub x G : 'C_G[x] \subset G.
Lemma subcent1C x y G : x \in G → y \in 'C_G[x] → x \in 'C_G[y].
Lemma subcent1_cycle_sub x G : x \in G → <[x]> \subset 'C_G[x].
Lemma subcent1_cycle_norm x G : 'C_G[x] \subset 'N(<[x]>).
Lemma subcent1_cycle_normal x G : x \in G → <[x]> <| 'C_G[x].
Gorenstein. 1.3.4
Lemma cyclic_center_factor_abelian G : cyclic (G / 'Z(G)) → abelian G.
Lemma cyclic_factor_abelian 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 G : G \subset D → f @* 'Z(G) = 'Z(f @* G).
End Injm.
End Center.
Arguments center_idP {gT A}.
Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) :
G \isog H → 'Z(G) \isog 'Z(H).
Section Product.
Variable gT : finGroupType.
Implicit Types (A B C : {set gT}) (G H K : {group gT}).
Lemma center_prod H K : K \subset 'C(H) → 'Z(H) × 'Z(K) = 'Z(H × K).
Lemma center_cprod A B G : A \* B = G → 'Z(A) \* 'Z(B) = 'Z(G).
Lemma center_bigcprod 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 G : G \* 'Z(G) = G.
Lemma center_dprod A B G : A \x B = G → 'Z(A) \x 'Z(B) = 'Z(G).
Lemma center_bigdprod 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 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 kerHK := ker_cprod_by isoZ.
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 sZH := center_sub H.
Let sZK := center_sub K.
Let sgzZG : gz @* 'Z(H) \subset K := subset_trans sgzZZ sZK.
Lemma ker_cprod_by_is_group : group_set kerHK.
Canonical ker_cprod_by_group := Group ker_cprod_by_is_group.
Lemma ker_cprod_by_central : kerHK \subset 'Z(setX H K).
Fact cprod_by_key : unit.
Definition cprod_by_def : finGroupType := subg_of (setX H K / kerHK).
Definition cprod_by := locked_with cprod_by_key cprod_by_def.
Lemma cyclic_factor_abelian 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 G : G \subset D → f @* 'Z(G) = 'Z(f @* G).
End Injm.
End Center.
Arguments center_idP {gT A}.
Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) :
G \isog H → 'Z(G) \isog 'Z(H).
Section Product.
Variable gT : finGroupType.
Implicit Types (A B C : {set gT}) (G H K : {group gT}).
Lemma center_prod H K : K \subset 'C(H) → 'Z(H) × 'Z(K) = 'Z(H × K).
Lemma center_cprod A B G : A \* B = G → 'Z(A) \* 'Z(B) = 'Z(G).
Lemma center_bigcprod 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 G : G \* 'Z(G) = G.
Lemma center_dprod A B G : A \x B = G → 'Z(A) \x 'Z(B) = 'Z(G).
Lemma center_bigdprod 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 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 kerHK := ker_cprod_by isoZ.
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 sZH := center_sub H.
Let sZK := center_sub K.
Let sgzZG : gz @* 'Z(H) \subset K := subset_trans sgzZZ sZK.
Lemma ker_cprod_by_is_group : group_set kerHK.
Canonical ker_cprod_by_group := Group ker_cprod_by_is_group.
Lemma ker_cprod_by_central : kerHK \subset 'Z(setX H K).
Fact cprod_by_key : unit.
Definition cprod_by_def : finGroupType := subg_of (setX H K / kerHK).
Definition cprod_by := locked_with cprod_by_key cprod_by_def.
FIXME : Check if we need arg_sort instead of sort
Definition in_cprod : gTH × gTK → cprod_by :=
let: tt as k := cprod_by_key return _ → locked_with k cprod_by_def in
subg _ \o coset kerHK.
Lemma in_cprodM : {in setX H K &, {morph in_cprod : u v / u × v}}.
Canonical 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).
Lemma injm_cpairg1 : 'injm cpairg1.
Let injH := injm_cpairg1.
Lemma injm_cpair1g : 'injm cpair1g.
Let injK := injm_cpair1g.
Lemma im_cpair_cent : CK \subset 'C(CH).
Hint Resolve im_cpair_cent : core.
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.
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}.
Let gH := ifactm fH injm_cpairg1.
Let gK := ifactm fK injm_cpair1g.
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 xcprod_morphism := [morphism of xcprodm].
Lemma xcprodmEl : {in H, ∀ x, xcprodm (cpairg1 x) = fH x}.
Lemma xcprodmEr : {in K, ∀ y, xcprodm (cpair1g y) = fK y}.
Lemma xcprodmE :
{in H & K, ∀ x y, xcprodm (cpairg1 x × cpair1g y) = fH x × fK y}.
Lemma im_xcprodm : xcprodm @* C = fH @* H × fK @* K.
Lemma im_xcprodml A : xcprodm @* (cpairg1 @* A) = fH @* A.
Lemma im_xcprodmr A : xcprodm @* (cpair1g @* A) = fK @* A.
Lemma injm_xcprodm : 'injm xcprodm = 'injm fH && 'injm fK.
End ExtCprodm.
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}.
Let gH := ifactm fH injm_cpairg1.
Let gK := ifactm fK injm_cpair1g.
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 xcprod_morphism := [morphism of xcprodm].
Lemma xcprodmEl : {in H, ∀ x, xcprodm (cpairg1 x) = fH x}.
Lemma xcprodmEr : {in K, ∀ y, xcprodm (cpair1g y) = fK y}.
Lemma xcprodmE :
{in H & K, ∀ x y, xcprodm (cpairg1 x × cpair1g y) = fH x × fK y}.
Lemma im_xcprodm : xcprodm @* C = fH @* H × fK @* K.
Lemma im_xcprodml A : xcprodm @* (cpairg1 @* A) = fH @* A.
Lemma im_xcprodmr 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 (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).
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 (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 :
∃ 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}).
Let gt_ b := if b then gTK else gTH.
Let G_ b := if b as b' return {group gt_ b'} then K else H.
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 (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}).
Fixpoint ncprod_def n : finGroupType :=
if n is n'.+1 then xcprod G [set: ncprod_def n']
else subg_of 'Z(G).
Fact ncprod_key : unit.
Definition ncprod := locked_with ncprod_key ncprod_def.
Lemma ncprod0 : G_ 0 \isog 'Z(G).
Lemma center_ncprod0 : 'Z(G_ 0) = G_ 0.
Lemma center_ncprod n : 'Z(G_ n) \isog 'Z(G).
Lemma ncprodS n : xcprod_spec G [set: ncprod n] (ncprod n.+1).
Lemma ncprod1 : G_ 1 \isog G.
Lemma Aut_ncprod_full 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.
∃ 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}).
Let gt_ b := if b then gTK else gTH.
Let G_ b := if b as b' return {group gt_ b'} then K else H.
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 (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}).
Fixpoint ncprod_def n : finGroupType :=
if n is n'.+1 then xcprod G [set: ncprod_def n']
else subg_of 'Z(G).
Fact ncprod_key : unit.
Definition ncprod := locked_with ncprod_key ncprod_def.
Lemma ncprod0 : G_ 0 \isog 'Z(G).
Lemma center_ncprod0 : 'Z(G_ 0) = G_ 0.
Lemma center_ncprod n : 'Z(G_ n) \isog 'Z(G).
Lemma ncprodS n : xcprod_spec G [set: ncprod n] (ncprod n.+1).
Lemma ncprod1 : G_ 1 \isog G.
Lemma Aut_ncprod_full 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.