Library mathcomp.solvable.center
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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 : 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).
- -
-
-
-- -
-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 : 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 [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.
- -
-