Library mathcomp.solvable.center
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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.
+ +
+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].
+ +
+
+
++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.
+ +
+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.
+ +
+ +
+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 := subFinGroupType [group of setX H K / kerHK].
+Definition cprod_by := locked_with cprod_by_key cprod_by_def.
+ +
+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.
+ +
+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).
+ +
+
+
++ +
+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.
+ +
+ +
+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 := subFinGroupType [group of setX H K / kerHK].
+Definition cprod_by := locked_with cprod_by_key cprod_by_def.
+ +
+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.
+ +
+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 [finGroupType of 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 [finGroupType of 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.
+ +
+