+ +

Library mathcomp.fingroup.gproduct

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

+ Partial, semidirect, central, and direct products. + ++ Internal products, with A, B : {set gT}, are partial operations : + partial_product A B == A * B if A is a group normalised by the group B, + and the empty set otherwise. + A ><| B == A * B if this is a semi-direct product (i.e., if A + is normalised by B and intersects it trivially). + A \* B == A * B if this is a central product ( [A, B] = 1). + A \x B == A * B if this is a direct product. + [complements to K in G] == set of groups H s.t. K * H = G and K :&: H = 1. + [splits G, over K] == [complements to K in G] is not empty. + remgr A B x == the right remainder in B of x mod A, i.e., + some element of (A :* x) :&: B. + divgr A B x == the "division" in B of x by A: for all x, + x = divgr A B x * remgr A B x. + ++ External products : + pairg1, pair1g == the isomorphisms aT1 -> aT1 * aT2, aT2 -> aT1 * aT2. + (aT1 * aT2 has a direct product group structure.) + sdprod_by to == the semidirect product defined by to : groupAction H K. + This is a finGroupType; the actual semidirect product is + the total set [set: sdprod_by to] on that type. + sdpair[12] to == the isomorphisms injecting K and H into + sdprod_by to = sdpair1 to @* K ><| sdpair2 to @* H. + External central products (with identified centers) will be defined later + in file center.v. + ++ Morphisms on product groups: + pprodm nAB fJ fAB == the morphism extending fA and fB on A <*> B when + nAB : B \subset 'N(A), + fJ : {in A & B, morph_actj fA fB}, and + fAB : {in A :&: B, fA =1 fB}. + sdprodm defG fJ == the morphism extending fA and fB on G, given + defG : A ><| B = G and + fJ : {in A & B, morph_act 'J 'J fA fB}. + xsdprodm fHKact == the total morphism on sdprod_by to induced by + fH : {morphism H >-> rT}, fK : {morphism K >-> rT}, + with to : groupAction K H, + given fHKact : morph_act to 'J fH fK. + cprodm defG cAB fAB == the morphism extending fA and fB on G, when + defG : A \* B = G, + cAB : fB @* B \subset 'C(fB @* A), + and fAB : {in A :&: B, fA =1 fB}. + dprodm defG cAB == the morphism extending fA and fB on G, when + defG : A \x B = G and + cAB : fA @* B \subset 'C(fA @* A) + mulgm (x, y) == x * y; mulgm is an isomorphism from setX A B to G + iff A \x B = G . +

+ +
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section Defs.
+ +
+Variables gT : finGroupType.
+Implicit Types A B C : {set gT }.
+ +
+Definition partial_product A B :=
+  if A == 1 then B else if B == 1 then A else
+  if [&& group_set A , group_set B & B \subset 'N (A )] then A × B else set0.
+ +
+Definition semidirect_product A B :=
+  if A :&: B \subset 1%G then partial_product A B else set0.
+ +
+Definition central_product A B :=
+  if B \subset 'C (A ) then partial_product A B else set0.
+ +
+Definition direct_product A B :=
+  if A :&: B \subset 1%G then central_product A B else set0.
+ +
+Definition complements_to_in A B :=
+  [set K : {group gT } | A :&: K == 1 & A × K == B ].
+ +
+Definition splits_over B A := complements_to_in A B != set0.
+ +
+

+ +

+ Product remainder functions -- right variant only. +

+Definition remgr A B x := repr (A :* x :&: B).
+Definition divgr A B x := x × (remgr A B x )^-1.
+ +
+End Defs.
+ +
+Notation pprod := (partial_product _).
+Notation sdprod := (semidirect_product _).
+Notation cprod := (central_product _).
+Notation dprod := (direct_product _).
+ +
+Notation "G ><| H" := (sdprod G H)%g (at level 40, left associativity).
+Notation "G \* H" := (cprod G H)%g (at level 40, left associativity).
+Notation "G \x H" := (dprod G H)%g (at level 40, left associativity).
+ +
+Notation "[ 'complements' 'to' A 'in' B ]" := (complements_to_in A B)
+ (at level 0, format "[ 'complements' 'to' A 'in' B ]") : group_scope.
+ +
+Notation "[ 'splits' B , 'over' A ]" := (splits_over B A)
+ (at level 0, format "[ 'splits' B , 'over' A ]") : group_scope.
+ +
+

+ +

+ Prenex Implicits remgl divgl. +

+ +
+Section InternalProd.
+ +
+Variable gT : finGroupType.
+Implicit Types A B C : {set gT }.
+Implicit Types G H K L M : {group gT }.
+ +
+ +
+Lemma pprod1g : left_id 1 pprod.
+ +
+Lemma pprodg1 : right_id 1 pprod.
+ +
+CoInductive are_groups A B : Prop := AreGroups K H of A = K & B = H.
+ +
+Lemma group_not0 G : set0 ≠ G.
+ +
+Lemma mulg0 : right_zero (@set0 gT) mulg.
+ +
+Lemma mul0g : left_zero (@set0 gT) mulg.
+ +
+Lemma pprodP A B G :
+ pprod A B = G → [/\ are_groups A B , A × B = G & B \subset 'N (A )].
+ +
+Lemma pprodE K H : H \subset 'N (K ) → pprod K H = K × H.
+ +
+Lemma pprodEY K H : H \subset 'N (K ) → pprod K H = K <*> H.
+ +
+Lemma pprodW A B G : pprod A B = G → A × B = G.
+ +
+Lemma pprodWC A B G : pprod A B = G → B × A = G.
+ +
+Lemma pprodWY A B G : pprod A B = G → A <*> B = G.
+ +
+Lemma pprodJ A B x : pprod A B :^ x = pprod (A :^ x) (B :^ x).
+ +
+

+ +

+ Properties of the remainders +

+ +
+Lemma remgrMl K B x y : y \in K → remgr K B (y × x) = remgr K B x.
+ +
+Lemma remgrP K B x : (remgr K B x \in K :* x :&: B ) = (x \in K × B ).
+ +
+Lemma remgr1 K H x : x \in K → remgr K H x = 1.
+ +
+Lemma divgr_eq A B x : x = divgr A B x × remgr A B x.
+ +
+Lemma divgrMl K B x y : x \in K → divgr K B (x × y) = x × divgr K B y.
+ +
+Lemma divgr_id K H x : x \in K → divgr K H x = x.
+ +
+Lemma mem_remgr K B x : x \in K × B → remgr K B x \in B.
+ +
+Lemma mem_divgr K B x : x \in K × B → divgr K B x \in K.
+ +
+Section DisjointRem.
+ +
+Variables K H : {group gT }.
+ +
+Hypothesis tiKH : K :&: H = 1.
+ +
+Lemma remgr_id x : x \in H → remgr K H x = x.
+ +
+Lemma remgrMid x y : x \in K → y \in H → remgr K H (x × y) = y.
+ +
+Lemma divgrMid x y : x \in K → y \in H → divgr K H (x × y) = x.
+ +
+End DisjointRem.
+ +
+

+ +

+ Intersection of a centraliser with a disjoint product. +

+ +
+Lemma subcent_TImulg K H A :
+ K :&: H = 1 → A \subset 'N (K ) :&: 'N (H ) → 'C_K (A ) × 'C_H (A ) = 'C_(K × H )(A ).
+ +
+

+ +

+ Complements, and splitting. +

+ +
+Lemma complP H A B :
+  reflect (A :&: H = 1 ∧ A × H = B) (H \in [complements to A in B ]).
+ +
+Lemma splitsP B A :
+  reflect (∃ H, H \in [complements to A in B ]) [splits B , over A ].
+ +
+Lemma complgC H K G :
+  (H \in [complements to K in G ]) = (K \in [complements to H in G ]).
+ +
+Section NormalComplement.
+ +
+Variables K H G : {group gT }.
+ +
+Hypothesis complH_K : H \in [complements to K in G ].
+ +
+Lemma remgrM : K <| G → {in G &, {morph remgr K H : x y / x × y }}.
+ +
+Lemma divgrM : H \subset 'C (K ) → {in G &, {morph divgr K H : x y / x × y }}.
+ +
+End NormalComplement.
+ +
+

+ +

+ Semi-direct product +

+ +
+Lemma sdprod1g : left_id 1 sdprod.
+ +
+Lemma sdprodg1 : right_id 1 sdprod.
+ +
+Lemma sdprodP A B G :
+  A ><| B = G → [/\ are_groups A B , A × B = G , B \subset 'N (A ) & A :&: B = 1].
+ +
+Lemma sdprodE K H : H \subset 'N (K ) → K :&: H = 1 → K ><| H = K × H.
+ +
+Lemma sdprodEY K H : H \subset 'N (K ) → K :&: H = 1 → K ><| H = K <*> H.
+ +
+Lemma sdprodWpp A B G : A ><| B = G → pprod A B = G.
+ +
+Lemma sdprodW A B G : A ><| B = G → A × B = G.
+ +
+Lemma sdprodWC A B G : A ><| B = G → B × A = G.
+ +
+Lemma sdprodWY A B G : A ><| B = G → A <*> B = G.
+ +
+Lemma sdprodJ A B x : (A ><| B ) :^ x = A :^ x ><| B :^ x.
+ +
+Lemma sdprod_context G K H : K ><| H = G →
+  [/\ K <| G , H \subset G , K × H = G , H \subset 'N (K ) & K :&: H = 1].
+ +
+Lemma sdprod_compl G K H : K ><| H = G → H \in [complements to K in G ].
+ +
+Lemma sdprod_normal_complP G K H :
+  K <| G → reflect (K ><| H = G) (K \in [complements to H in G ]).
+ +
+Lemma sdprod_card G A B : A ><| B = G → (#|A | × #|B |)%N = #|G |.
+ +
+Lemma sdprod_isom G A B :
+    A ><| B = G →
+ {nAB : B \subset 'N (A ) | isom B (G / A) (restrm nAB (coset A))}.
+ +
+Lemma sdprod_isog G A B : A ><| B = G → B \isog G / A.
+ +
+Lemma sdprod_subr G A B M : A ><| B = G → M \subset B → A ><| M = A <*> M.
+ +
+Lemma index_sdprod G A B : A ><| B = G → #|B | = #|G : A |.
+ +
+Lemma index_sdprodr G A B M :
+  A ><| B = G → M \subset B → #|B : M | = #|G : A <*> M |.
+ +
+Lemma quotient_sdprodr_isom G A B M :
+    A ><| B = G → M <| B →
+  {f : {morphism B / M >-> coset_of (A <*> M)} |
+    isom (B / M) (G / (A <*> M )) f
+  & ∀ L, L \subset B → f @* (L / M ) = A <*> L / (A <*> M )}.
+ +
+Lemma quotient_sdprodr_isog G A B M :
+  A ><| B = G → M <| B → B / M \isog G / (A <*> M ).
+ +
+Lemma sdprod_modl A B G H :
+  A ><| B = G → A \subset H → A ><| (B :&: H ) = G :&: H.
+ +
+Lemma sdprod_modr A B G H :
+  A ><| B = G → B \subset H → (H :&: A ) ><| B = H :&: G.
+ +
+Lemma subcent_sdprod B C G A :
+  B ><| C = G → A \subset 'N (B ) :&: 'N (C ) → 'C_B (A ) ><| 'C_C (A ) = 'C_G (A ).
+ +
+Lemma sdprod_recl n G K H K1 :
+    #|G | ≤ n → K ><| H = G → K1 \proper K → H \subset 'N (K1 ) →
+  ∃ G1 : {group gT }, [/\ #|G1 | < n , G1 \subset G & K1 ><| H = G1 ].
+ +
+Lemma sdprod_recr n G K H H1 :
+    #|G | ≤ n → K ><| H = G → H1 \proper H →
+  ∃ G1 : {group gT }, [/\ #|G1 | < n , G1 \subset G & K ><| H1 = G1 ].
+ +
+Lemma mem_sdprod G A B x : A ><| B = G → x \in G →
+  ∃ y, ∃ z,
+    [/\ y \in A , z \in B , x = y × z &
+        {in A & B , ∀ u t, x = u × t → u = y ∧ t = z }].
+ +
+

+ +

+ Central product +

+ +
+Lemma cprod1g : left_id 1 cprod.
+ +
+Lemma cprodg1 : right_id 1 cprod.
+ +
+Lemma cprodP A B G :
+  A \* B = G → [/\ are_groups A B , A × B = G & B \subset 'C (A )].
+ +
+Lemma cprodE G H : H \subset 'C (G ) → G \* H = G × H.
+ +
+Lemma cprodEY G H : H \subset 'C (G ) → G \* H = G <*> H.
+ +
+Lemma cprodWpp A B G : A \* B = G → pprod A B = G.
+ +
+Lemma cprodW A B G : A \* B = G → A × B = G.
+ +
+Lemma cprodWC A B G : A \* B = G → B × A = G.
+ +
+Lemma cprodWY A B G : A \* B = G → A <*> B = G.
+ +
+Lemma cprodJ A B x : (A \* B ) :^ x = A :^ x \* B :^ x.
+ +
+Lemma cprod_normal2 A B G : A \* B = G → A <| G ∧ B <| G.
+ +
+Lemma bigcprodW I (r : seq I) P F G :
+  \big [cprod /1]_(i <- r | P i ) F i = G → \prod_(i <- r | P i ) F i = G.
+ +
+Lemma bigcprodWY I (r : seq I) P F G :
+  \big [cprod /1]_(i <- r | P i ) F i = G → << \bigcup_(i <- r | P i ) F i >> = G.
+ +
+Lemma triv_cprod A B : (A \* B == 1) = (A == 1) && (B == 1).
+ +
+Lemma cprod_ntriv A B : A != 1 → B != 1 →
+  A \* B =
+    if [&& group_set A , group_set B & B \subset 'C (A )] then A × B else set0.
+ +
+Lemma trivg0 : (@set0 gT == 1) = false.
+ +
+Lemma group0 : group_set (@set0 gT) = false.
+ +
+Lemma cprod0g A : set0 \* A = set0.
+ +
+Lemma cprodC : commutative cprod.
+ +
+Lemma cprodA : associative cprod.
+ +
+Canonical cprod_law := Monoid.Law cprodA cprod1g cprodg1.
+Canonical cprod_abelaw := Monoid.ComLaw cprodC.
+ +
+Lemma cprod_modl A B G H :
+  A \* B = G → A \subset H → A \* (B :&: H ) = G :&: H.
+ +
+Lemma cprod_modr A B G H :
+  A \* B = G → B \subset H → (H :&: A ) \* B = H :&: G.
+ +
+Lemma bigcprodYP (I : finType) (P : pred I) (H : I → {group gT }) :
+  reflect (∀ i j, P i → P j → i != j → H i \subset 'C (H j ))
+          (\big [cprod /1]_(i | P i ) H i == (\prod_(i | P i ) H i)%G).
+ +
+Lemma bigcprodEY I r (P : pred I) (H : I → {group gT }) G :
+    abelian G → (∀ i, P i → H i \subset G ) →
+  \big [cprod /1]_(i <- r | P i ) H i = (\prod_(i <- r | P i ) H i)%G.
+ +
+Lemma perm_bigcprod (I : eqType) r1 r2 (A : I → {set gT }) G x :
+    \big [cprod /1]_(i <- r1 ) A i = G → {in r1 , ∀ i, x i \in A i } →
+    perm_eq r1 r2 →
+  \prod_(i <- r1 ) x i = \prod_(i <- r2 ) x i.
+ +
+Lemma reindex_bigcprod (I J : finType) (h : J → I) P (A : I → {set gT }) G x :
+    {on SimplPred P , bijective h } → \big [cprod /1]_(i | P i ) A i = G →
+    {in SimplPred P , ∀ i, x i \in A i } →
+  \prod_(i | P i ) x i = \prod_(j | P (h j)) x (h j).
+ +
+

+ +

+ Direct product +

+ +
+Lemma dprod1g : left_id 1 dprod.
+ +
+Lemma dprodg1 : right_id 1 dprod.
+ +
+Lemma dprodP A B G :
+  A \x B = G → [/\ are_groups A B , A × B = G , B \subset 'C (A ) & A :&: B = 1].
+ +
+Lemma dprodE G H : H \subset 'C (G ) → G :&: H = 1 → G \x H = G × H.
+ +
+Lemma dprodEY G H : H \subset 'C (G ) → G :&: H = 1 → G \x H = G <*> H.
+ +
+Lemma dprodEcp A B : A :&: B = 1 → A \x B = A \* B.
+ +
+Lemma dprodEsd A B : B \subset 'C (A ) → A \x B = A ><| B.
+ +
+Lemma dprodWcp A B G : A \x B = G → A \* B = G.
+ +
+Lemma dprodWsd A B G : A \x B = G → A ><| B = G.
+ +
+Lemma dprodW A B G : A \x B = G → A × B = G.
+ +
+Lemma dprodWC A B G : A \x B = G → B × A = G.
+ +
+Lemma dprodWY A B G : A \x B = G → A <*> B = G.
+ +
+Lemma cprod_card_dprod G A B :
+  A \* B = G → #|A | × #|B | ≤ #|G | → A \x B = G.
+ +
+Lemma dprodJ A B x : (A \x B ) :^ x = A :^ x \x B :^ x.
+ +
+Lemma dprod_normal2 A B G : A \x B = G → A <| G ∧ B <| G.
+ +
+Lemma dprodYP K H : reflect (K \x H = K <*> H) (H \subset 'C (K ) :\: K ^#).
+ +
+Lemma dprodC : commutative dprod.
+ +
+Lemma dprodWsdC A B G : A \x B = G → B ><| A = G.
+ +
+Lemma dprodA : associative dprod.
+ +
+Canonical dprod_law := Monoid.Law dprodA dprod1g dprodg1.
+Canonical dprod_abelaw := Monoid.ComLaw dprodC.
+ +
+Lemma bigdprodWcp I (r : seq I) P F G :
+  \big [dprod /1]_(i <- r | P i ) F i = G → \big [cprod /1]_(i <- r | P i ) F i = G.
+ +
+Lemma bigdprodW I (r : seq I) P F G :
+  \big [dprod /1]_(i <- r | P i ) F i = G → \prod_(i <- r | P i ) F i = G.
+ +
+Lemma bigdprodWY I (r : seq I) P F G :
+  \big [dprod /1]_(i <- r | P i ) F i = G → << \bigcup_(i <- r | P i ) F i >> = G.
+ +
+Lemma bigdprodYP (I : finType) (P : pred I) (F : I → {group gT }) :
+  reflect (∀ i, P i →
+             (\prod_(j | P j && (j != i )) F j)%G \subset 'C (F i ) :\: (F i )^#)
+          (\big [dprod /1]_(i | P i ) F i == (\prod_(i | P i ) F i)%G).
+ +
+Lemma dprod_modl A B G H :
+  A \x B = G → A \subset H → A \x (B :&: H ) = G :&: H.
+ +
+Lemma dprod_modr A B G H :
+  A \x B = G → B \subset H → (H :&: A ) \x B = H :&: G.
+ +
+Lemma subcent_dprod B C G A :
+   B \x C = G → A \subset 'N (B ) :&: 'N (C ) → 'C_B (A ) \x 'C_C (A ) = 'C_G (A ).
+ +
+Lemma dprod_card A B G : A \x B = G → (#|A | × #|B |)%N = #|G |.
+ +
+Lemma bigdprod_card I r (P : pred I) E G :
+    \big [dprod /1]_(i <- r | P i ) E i = G →
+  (\prod_(i <- r | P i ) #|E i |)%N = #|G |.
+ +
+Lemma bigcprod_card_dprod I r (P : pred I) (A : I → {set gT }) G :
+    \big [cprod /1]_(i <- r | P i ) A i = G →
+    \prod_(i <- r | P i ) #|A i | ≤ #|G | →
+  \big [dprod /1]_(i <- r | P i ) A i = G.
+ +
+Lemma bigcprod_coprime_dprod (I : finType) (P : pred I) (A : I → {set gT }) G :
+    \big [cprod /1]_(i | P i ) A i = G →
+    (∀ i j, P i → P j → i != j → coprime #|A i | #|A j |) →
+  \big [dprod /1]_(i | P i ) A i = G.
+ +
+Lemma mem_dprod G A B x : A \x B = G → x \in G →
+  ∃ y, ∃ z,
+    [/\ y \in A , z \in B , x = y × z &
+        {in A & B , ∀ u t, x = u × t → u = y ∧ t = z }].
+ +
+Lemma mem_bigdprod (I : finType) (P : pred I) F G x :
+    \big [dprod /1]_(i | P i ) F i = G → x \in G →
+  ∃ c, [/\ ∀ i, P i → c i \in F i , x = \prod_(i | P i ) c i
+              & ∀ e, (∀ i, P i → e i \in F i ) →
+                          x = \prod_(i | P i ) e i →
+                ∀ i, P i → e i = c i ].
+ +
+End InternalProd.
+ +
+ +
+Section MorphimInternalProd.
+ +
+Variables (gT rT : finGroupType) (D : {group gT }) (f : {morphism D >-> rT }).
+ +
+Section OneProd.
+ +
+Variables G H K : {group gT }.
+Hypothesis sGD : G \subset D.
+ +
+Lemma morphim_pprod : pprod K H = G → pprod (f @* K) (f @* H) = f @* G.
+ +
+Lemma morphim_coprime_sdprod :
+  K ><| H = G → coprime #|K | #|H | → f @* K ><| f @* H = f @* G.
+ +
+Lemma injm_sdprod : 'injm f → K ><| H = G → f @* K ><| f @* H = f @* G.
+ +
+Lemma morphim_cprod : K \* H = G → f @* K \* f @* H = f @* G.
+ +
+Lemma injm_dprod : 'injm f → K \x H = G → f @* K \x f @* H = f @* G.
+ +
+Lemma morphim_coprime_dprod :
+  K \x H = G → coprime #|K | #|H | → f @* K \x f @* H = f @* G.
+ +
+End OneProd.
+ +
+Implicit Type G : {group gT }.
+ +
+Lemma morphim_bigcprod I r (P : pred I) (H : I → {group gT }) G :
+    G \subset D → \big [cprod /1]_(i <- r | P i ) H i = G →
+  \big [cprod /1]_(i <- r | P i ) f @* H i = f @* G.
+ +
+Lemma injm_bigdprod I r (P : pred I) (H : I → {group gT }) G :
+    G \subset D → 'injm f → \big [dprod /1]_(i <- r | P i ) H i = G →
+  \big [dprod /1]_(i <- r | P i ) f @* H i = f @* G.
+ +
+Lemma morphim_coprime_bigdprod (I : finType) P (H : I → {group gT }) G :
+    G \subset D → \big [dprod /1]_(i | P i ) H i = G →
+    (∀ i j, P i → P j → i != j → coprime #|H i | #|H j |) →
+  \big [dprod /1]_(i | P i ) f @* H i = f @* G.
+ +
+End MorphimInternalProd.
+ +
+Section QuotientInternalProd.
+ +
+Variables (gT : finGroupType) (G K H M : {group gT }).
+ +
+Hypothesis nMG: G \subset 'N (M ).
+ +
+Lemma quotient_pprod : pprod K H = G → pprod (K / M) (H / M) = G / M.
+ +
+Lemma quotient_coprime_sdprod :
+  K ><| H = G → coprime #|K | #|H | → (K / M ) ><| (H / M ) = G / M.
+ +
+Lemma quotient_cprod : K \* H = G → (K / M ) \* (H / M ) = G / M.
+ +
+Lemma quotient_coprime_dprod :
+  K \x H = G → coprime #|K | #|H | → (K / M ) \x (H / M ) = G / M.
+ +
+End QuotientInternalProd.
+ +
+Section ExternalDirProd.
+ +
+Variables gT1 gT2 : finGroupType.
+ +
+Definition extprod_mulg (x y : gT1 × gT2) := (x .1 × y .1 , x .2 × y .2 ).
+Definition extprod_invg (x : gT1 × gT2) := (x .1 ^-1 , x .2 ^-1 ).
+ +
+Lemma extprod_mul1g : left_id (1, 1) extprod_mulg.
+ +
+Lemma extprod_mulVg : left_inverse (1, 1) extprod_invg extprod_mulg.
+ +
+Lemma extprod_mulgA : associative extprod_mulg.
+ +
+Definition extprod_groupMixin :=
+  Eval hnf in FinGroup.Mixin extprod_mulgA extprod_mul1g extprod_mulVg.
+Canonical extprod_baseFinGroupType :=
+  Eval hnf in BaseFinGroupType (gT1 × gT2) extprod_groupMixin.
+Canonical prod_group := FinGroupType extprod_mulVg.
+ +
+Lemma group_setX (H1 : {group gT1 }) (H2 : {group gT2 }) : group_set (setX H1 H2).
+ +
+Canonical setX_group H1 H2 := Group (group_setX H1 H2).
+ +
+Definition pairg1 x : gT1 × gT2 := (x , 1).
+Definition pair1g x : gT1 × gT2 := (1, x ).
+ +
+Lemma pairg1_morphM : {morph pairg1 : x y / x × y }.
+ +
+Canonical pairg1_morphism := @Morphism _ _ setT _ (in2W pairg1_morphM).
+ +
+Lemma pair1g_morphM : {morph pair1g : x y / x × y }.
+ +
+Canonical pair1g_morphism := @Morphism _ _ setT _ (in2W pair1g_morphM).
+ +
+Lemma fst_morphM : {morph (@fst gT1 gT2 ) : x y / x × y }.
+ +
+Lemma snd_morphM : {morph (@snd gT1 gT2 ) : x y / x × y }.
+ +
+Canonical fst_morphism := @Morphism _ _ setT _ (in2W fst_morphM).
+ +
+Canonical snd_morphism := @Morphism _ _ setT _ (in2W snd_morphM).
+ +
+Lemma injm_pair1g : 'injm pair1g.
+ +
+Lemma injm_pairg1 : 'injm pairg1.
+ +
+Lemma morphim_pairg1 (H1 : {set gT1 }) : pairg1 @* H1 = setX H1 1.
+ +
+Lemma morphim_pair1g (H2 : {set gT2 }) : pair1g @* H2 = setX 1 H2.
+ +
+Lemma morphim_fstX (H1: {set gT1 }) (H2 : {group gT2 }) :
+  [morphism of fun x ⇒ x .1 ] @* setX H1 H2 = H1.
+ +
+Lemma morphim_sndX (H1: {group gT1 }) (H2 : {set gT2 }) :
+  [morphism of fun x ⇒ x .2 ] @* setX H1 H2 = H2.
+ +
+Lemma setX_prod (H1 : {set gT1 }) (H2 : {set gT2 }) :
+  setX H1 1 × setX 1 H2 = setX H1 H2.
+ +
+Lemma setX_dprod (H1 : {group gT1 }) (H2 : {group gT2 }) :
+  setX H1 1 \x setX 1 H2 = setX H1 H2.
+ +
+Lemma isog_setX1 (H1 : {group gT1 }) : isog H1 (setX H1 1).
+ +
+Lemma isog_set1X (H2 : {group gT2 }) : isog H2 (setX 1 H2).
+ +
+Lemma setX_gen (H1 : {set gT1 }) (H2 : {set gT2 }) :
+  1 \in H1 → 1 \in H2 → <<setX H1 H2 >> = setX <<H1 >> <<H2 >>.
+ +
+End ExternalDirProd.
+ +
+Section ExternalSDirProd.
+ +
+Variables (aT rT : finGroupType) (D : {group aT }) (R : {group rT }).
+ +
+

+ +

+ The pair (a, x) denotes the product sdpair2 a * sdpair1 x +

+ +
+Inductive sdprod_by (to : groupAction D R) : predArgType :=
+   SdPair (ax : aT × rT) of ax \in setX D R.
+ +
+Coercion pair_of_sd to (u : sdprod_by to) := let: SdPair ax _ := u in ax.
+ +
+Variable to : groupAction D R.
+ +
+Notation sdT := (sdprod_by to).
+Notation sdval := (@pair_of_sd to).
+ +
+Canonical sdprod_subType := Eval hnf in [subType for sdval ].
+Definition sdprod_eqMixin := Eval hnf in [eqMixin of sdT by <:].
+Canonical sdprod_eqType := Eval hnf in EqType sdT sdprod_eqMixin.
+Definition sdprod_choiceMixin := [choiceMixin of sdT by <:].
+Canonical sdprod_choiceType := ChoiceType sdT sdprod_choiceMixin.
+Definition sdprod_countMixin := [countMixin of sdT by <:].
+Canonical sdprod_countType := CountType sdT sdprod_countMixin.
+Canonical sdprod_subCountType := Eval hnf in [subCountType of sdT ].
+Definition sdprod_finMixin := [finMixin of sdT by <:].
+Canonical sdprod_finType := FinType sdT sdprod_finMixin.
+Canonical sdprod_subFinType := Eval hnf in [subFinType of sdT ].
+ +
+Definition sdprod_one := SdPair to (group1 _).
+ +
+Lemma sdprod_inv_proof (u : sdT) : (u .1 ^-1 , to u .2 ^-1 u .1 ^-1 ) \in setX D R.
+ +
+Definition sdprod_inv u := SdPair to (sdprod_inv_proof u).
+ +
+Lemma sdprod_mul_proof (u v : sdT) :
+  (u .1 × v .1 , to u .2 v .1 × v .2 ) \in setX D R.
+ +
+Definition sdprod_mul u v := SdPair to (sdprod_mul_proof u v).
+ +
+Lemma sdprod_mul1g : left_id sdprod_one sdprod_mul.
+ +
+Lemma sdprod_mulVg : left_inverse sdprod_one sdprod_inv sdprod_mul.
+ +
+Lemma sdprod_mulgA : associative sdprod_mul.
+ +
+Canonical sdprod_groupMixin :=
+  FinGroup.Mixin sdprod_mulgA sdprod_mul1g sdprod_mulVg.
+ +
+Canonical sdprod_baseFinGroupType :=
+  Eval hnf in BaseFinGroupType sdT sdprod_groupMixin.
+ +
+Canonical sdprod_groupType := FinGroupType sdprod_mulVg.
+ +
+Definition sdpair1 x := insubd sdprod_one (1, x ) : sdT.
+Definition sdpair2 a := insubd sdprod_one (a , 1) : sdT.
+ +
+Lemma sdpair1_morphM : {in R &, {morph sdpair1 : x y / x × y }}.
+ +
+Lemma sdpair2_morphM : {in D &, {morph sdpair2 : a b / a × b }}.
+ +
+Canonical sdpair1_morphism := Morphism sdpair1_morphM.
+ +
+Canonical sdpair2_morphism := Morphism sdpair2_morphM.
+ +
+Lemma injm_sdpair1 : 'injm sdpair1.
+ +
+Lemma injm_sdpair2 : 'injm sdpair2.
+ +
+Lemma sdpairE (u : sdT) : u = sdpair2 u .1 × sdpair1 u .2.
+ +
+Lemma sdpair_act : {in R & D ,
+  ∀ x a, sdpair1 (to x a) = sdpair1 x ^ sdpair2 a }.
+ +
+Lemma sdpair_setact (G : {set rT }) a : G \subset R → a \in D →
+  sdpair1 @* (to ^~ a @: G ) = (sdpair1 @* G ) :^ sdpair2 a.
+ +
+Lemma im_sdpair_norm : sdpair2 @* D \subset 'N (sdpair1 @* R ).
+ +
+Lemma im_sdpair_TI : (sdpair1 @* R ) :&: (sdpair2 @* D ) = 1.
+ +
+Lemma im_sdpair : (sdpair1 @* R ) × (sdpair2 @* D ) = setT.
+ +
+Lemma sdprod_sdpair : sdpair1 @* R ><| sdpair2 @* D = setT.
+ +
+Variables (A : {set aT }) (G : {set rT }).
+ +
+Lemma gacentEsd : 'C_(|to )(A ) = sdpair1 @*^-1 'C (sdpair2 @* A ).
+ +
+Hypotheses (sAD : A \subset D) (sGR : G \subset R).
+ +
+Lemma astabEsd : 'C (G | to ) = sdpair2 @*^-1 'C (sdpair1 @* G ).
+ +
+Lemma astabsEsd : 'N (G | to ) = sdpair2 @*^-1 'N (sdpair1 @* G ).
+ +
+Lemma actsEsd : [acts A , on G | to ] = (sdpair2 @* A \subset 'N (sdpair1 @* G )).
+ +
+End ExternalSDirProd.
+ +
+Section ProdMorph.
+ +
+Variables gT rT : finGroupType.
+Implicit Types A B : {set gT }.
+Implicit Types G H K : {group gT }.
+Implicit Types C D : {set rT }.
+Implicit Type L : {group rT }.
+ +
+Section defs.
+ +
+Variables (A B : {set gT }) (fA fB : gT → FinGroup.sort rT).
+ +
+Definition pprodm of B \subset 'N (A ) & {in A & B , morph_act 'J 'J fA fB }
+                  & {in A :&: B , fA =1 fB } :=
+  fun x ⇒ fA (divgr A B x) × fB (remgr A B x).
+ +
+End defs.
+ +
+Section Props.
+ +
+Variables H K : {group gT }.
+Variables (fH : {morphism H >-> rT }) (fK : {morphism K >-> rT }).
+Hypothesis nHK : K \subset 'N (H ).
+Hypothesis actf : {in H & K , morph_act 'J 'J fH fK }.
+Hypothesis eqfHK : {in H :&: K , fH =1 fK }.
+ +
+ +
+Lemma pprodmE x a : x \in H → a \in K → f (x × a) = fH x × fK a.
+ +
+Lemma pprodmEl : {in H , f =1 fH }.
+ +
+Lemma pprodmEr : {in K , f =1 fK }.
+ +
+Lemma pprodmM : {in H <*> K &, {morph f : x y / x × y }}.
+ +
+Canonical pprodm_morphism := Morphism pprodmM.
+ +
+Lemma morphim_pprodm A B :
+  A \subset H → B \subset K → f @* (A × B ) = fH @* A × fK @* B.
+ +
+Lemma morphim_pprodml A : A \subset H → f @* A = fH @* A.
+ +
+Lemma morphim_pprodmr B : B \subset K → f @* B = fK @* B.
+ +
+Lemma ker_pprodm : 'ker f = [set x × a ^-1 | x in H , a in K & fH x == fK a ].
+ +
+Lemma injm_pprodm :
+  'injm f = [&& 'injm fH , 'injm fK & fH @* H :&: fK @* K == fH @* K ].
+ +
+End Props.
+ +
+Section Sdprodm.
+ +
+Variables H K G : {group gT }.
+Variables (fH : {morphism H >-> rT }) (fK : {morphism K >-> rT }).
+Hypothesis eqHK_G : H ><| K = G.
+Hypothesis actf : {in H & K , morph_act 'J 'J fH fK }.
+ +
+Lemma sdprodm_norm : K \subset 'N (H ).
+ +
+Lemma sdprodm_sub : G \subset H <*> K.
+ +
+Lemma sdprodm_eqf : {in H :&: K , fH =1 fK }.
+ +
+Definition sdprodm :=
+  restrm sdprodm_sub (pprodm sdprodm_norm actf sdprodm_eqf).
+ +
+Canonical sdprodm_morphism := Eval hnf in [morphism of sdprodm ].
+ +
+Lemma sdprodmE a b : a \in H → b \in K → sdprodm (a × b) = fH a × fK b.
+ +
+Lemma sdprodmEl a : a \in H → sdprodm a = fH a.
+ +
+Lemma sdprodmEr b : b \in K → sdprodm b = fK b.
+ +
+Lemma morphim_sdprodm A B :
+  A \subset H → B \subset K → sdprodm @* (A × B ) = fH @* A × fK @* B.
+ +
+Lemma im_sdprodm : sdprodm @* G = fH @* H × fK @* K.
+ +
+Lemma morphim_sdprodml A : A \subset H → sdprodm @* A = fH @* A.
+ +
+Lemma morphim_sdprodmr B : B \subset K → sdprodm @* B = fK @* B.
+ +
+Lemma ker_sdprodm :
+  'ker sdprodm = [set a × b ^-1 | a in H , b in K & fH a == fK b ].
+ +
+Lemma injm_sdprodm :
+  'injm sdprodm = [&& 'injm fH , 'injm fK & fH @* H :&: fK @* K == 1].
+ +
+End Sdprodm.
+ +
+Section Cprodm.
+ +
+Variables H K G : {group gT }.
+Variables (fH : {morphism H >-> rT }) (fK : {morphism K >-> rT }).
+Hypothesis eqHK_G : H \* K = G.
+Hypothesis cfHK : fK @* K \subset 'C (fH @* H ).
+Hypothesis eqfHK : {in H :&: K , fH =1 fK }.
+ +
+Lemma cprodm_norm : K \subset 'N (H ).
+ +
+Lemma cprodm_sub : G \subset H <*> K.
+ +
+Lemma cprodm_actf : {in H & K , morph_act 'J 'J fH fK }.
+ +
+Definition cprodm := restrm cprodm_sub (pprodm cprodm_norm cprodm_actf eqfHK).
+ +
+Canonical cprodm_morphism := Eval hnf in [morphism of cprodm ].
+ +
+Lemma cprodmE a b : a \in H → b \in K → cprodm (a × b) = fH a × fK b.
+ +
+Lemma cprodmEl a : a \in H → cprodm a = fH a.
+ +
+Lemma cprodmEr b : b \in K → cprodm b = fK b.
+ +
+Lemma morphim_cprodm A B :
+  A \subset H → B \subset K → cprodm @* (A × B ) = fH @* A × fK @* B.
+ +
+Lemma im_cprodm : cprodm @* G = fH @* H × fK @* K.
+ +
+Lemma morphim_cprodml A : A \subset H → cprodm @* A = fH @* A.
+ +
+Lemma morphim_cprodmr B : B \subset K → cprodm @* B = fK @* B.
+ +
+Lemma ker_cprodm : 'ker cprodm = [set a × b ^-1 | a in H , b in K & fH a == fK b ].
+ +
+Lemma injm_cprodm :
+  'injm cprodm = [&& 'injm fH , 'injm fK & fH @* H :&: fK @* K == fH @* K ].
+ +
+End Cprodm.
+ +
+Section Dprodm.
+ +
+Variables G H K : {group gT }.
+Variables (fH : {morphism H >-> rT }) (fK : {morphism K >-> rT }).
+Hypothesis eqHK_G : H \x K = G.
+Hypothesis cfHK : fK @* K \subset 'C (fH @* H ).
+ +
+Lemma dprodm_cprod : H \* K = G.
+ +
+Lemma dprodm_eqf : {in H :&: K , fH =1 fK }.
+ +
+Definition dprodm := cprodm dprodm_cprod cfHK dprodm_eqf.
+ +
+Canonical dprodm_morphism := Eval hnf in [morphism of dprodm ].
+ +
+Lemma dprodmE a b : a \in H → b \in K → dprodm (a × b) = fH a × fK b.
+ +
+Lemma dprodmEl a : a \in H → dprodm a = fH a.
+ +
+Lemma dprodmEr b : b \in K → dprodm b = fK b.
+ +
+Lemma morphim_dprodm A B :
+  A \subset H → B \subset K → dprodm @* (A × B ) = fH @* A × fK @* B.
+ +
+Lemma im_dprodm : dprodm @* G = fH @* H × fK @* K.
+ +
+Lemma morphim_dprodml A : A \subset H → dprodm @* A = fH @* A.
+ +
+Lemma morphim_dprodmr B : B \subset K → dprodm @* B = fK @* B.
+ +
+Lemma ker_dprodm : 'ker dprodm = [set a × b ^-1 | a in H , b in K & fH a == fK b ].
+ +
+Lemma injm_dprodm :
+  'injm dprodm = [&& 'injm fH , 'injm fK & fH @* H :&: fK @* K == 1].
+ +
+End Dprodm.
+ +
+Lemma isog_dprod A B G C D L :
+  A \x B = G → C \x D = L → isog A C → isog B D → isog G L.
+ +
+End ProdMorph.
+ +
+Section ExtSdprodm.
+ +
+Variables gT aT rT : finGroupType.
+Variables (H : {group gT }) (K : {group aT }) (to : groupAction K H).
+Variables (fH : {morphism H >-> rT }) (fK : {morphism K >-> rT }).
+ +
+Hypothesis actf : {in H & K , morph_act to 'J fH fK }.
+ +
+Let DgH := sdpair1 to @* H.
+Let DgK := sdpair2 to @* K.
+ +
+Lemma xsdprodm_dom1 : DgH \subset 'dom fsH.
+ +
+Lemma xsdprodm_dom2 : DgK \subset 'dom fsK.
+ +
+Lemma im_sdprodm1 : gH @* DgH = fH @* H.
+ +
+Lemma im_sdprodm2 : gK @* DgK = fK @* K.
+ +
+Lemma xsdprodm_act : {in DgH & DgK , morph_act 'J 'J gH gK }.
+ +
+Definition xsdprodm := sdprodm (sdprod_sdpair to) xsdprodm_act.
+Canonical xsdprod_morphism := [morphism of xsdprodm ].
+ +
+Lemma im_xsdprodm : xsdprodm @* setT = fH @* H × fK @* K.
+ +
+Lemma injm_xsdprodm :
+  'injm xsdprodm = [&& 'injm fH , 'injm fK & fH @* H :&: fK @* K == 1].
+ +
+End ExtSdprodm.
+ +
+Section DirprodIsom.
+ +
+Variable gT : finGroupType.
+Implicit Types G H : {group gT }.
+ +
+Definition mulgm : gT × gT → _ := prod_curry mulg.
+ +
+Lemma imset_mulgm (A B : {set gT }) : mulgm @: setX A B = A × B.
+ +
+Lemma mulgmP H1 H2 G : reflect (H1 \x H2 = G) (misom (setX H1 H2) G mulgm).
+ +
+End DirprodIsom.
+ +
+