Library mathcomp.fingroup.gproduct

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype bigop finset fingroup morphism.
From mathcomp Require Import quotient action finfun.

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.

Definition remgr A B x := repr (A :* x :&: B).
Definition divgr A B x := x × (remgr A B x)^-1.

End Defs.

Arguments partial_product _ _%g _%g : clear implicits.
Arguments semidirect_product _ _%g _%g : clear implicits.
Arguments central_product _ _%g _%g : clear implicits.
Arguments complements_to_in _ _%g _%g.
Arguments splits_over _ _%g _%g.
Arguments remgr _ _%g _%g _%g.
Arguments divgr _ _%g _%g _%g.
Arguments direct_product : clear implicits.
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) : group_scope.
Notation "G \* H" := (cprod G H)%g
  (at level 40, left associativity) : group_scope.
Notation "G \x H" := (dprod G H)%g
  (at level 40, left associativity) : group_scope.

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.

Section InternalProd.

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

Local Notation pprod := (partial_product gT).
Local Notation sdprod := (semidirect_product gT) (only parsing).
Local Notation cprod := (central_product gT) (only parsing).
Local Notation dprod := (direct_product gT) (only parsing).

Lemma pprod1g : left_id 1 pprod.

Lemma pprodg1 : right_id 1 pprod.

Variant 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).

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.

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).

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.

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}].

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.


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).

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.


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].

Lemma comm_prodG I r (G : I → {group gT}) (P : {pred I}) :
  {in P &, ∀ i j, commute (G i) (G j)} →
  (\prod_(i <- r | P i) G i)%G = \prod_(i <- r | P i) G i :> {set gT}.

End InternalProd.

Arguments complP {gT H A B}.
Arguments splitsP {gT B A}.
Arguments sdprod_normal_complP {gT G K H}.
Arguments dprodYP {gT K H}.
Arguments bigdprodYP {gT I P F}.

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.


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 ExternalDirDepProd.

Variables (I : finType) (gT : I → finGroupType).
Notation gTn := {dffun ∀ i, gT i}.
Implicit Types (H : ∀ i, {group gT i}) (x y : {dffun ∀ i, gT i}).

Definition extnprod_mulg (x y : gTn) : gTn := [ffun i ⇒ (x i × y i)%g].
Definition extnprod_invg (x : gTn) : gTn := [ffun i ⇒ (x i)^-1%g].

Lemma extnprod_mul1g : left_id [ffun⇒ 1%g] extnprod_mulg.

Lemma extnprod_mulVg : left_inverse [ffun⇒ 1%g] extnprod_invg extnprod_mulg.

Lemma extnprod_mulgA : associative extnprod_mulg.


Lemma oneg_ffun i : (1 : gTn) i = 1.

Lemma mulg_ffun i (x y : gTn) : (x × y) i = x i × y i.

Lemma invg_ffun i (x : gTn) : x^-1 i = (x i)^-1.

Lemma prodg_ffun T (r : seq T) (F : T → gTn) (P : {pred T}) i :
  (\prod_(t <- r | P t) F t) i = \prod_(t <- r | P t) F t i.

Lemma group_setXn H : group_set (setXn H).

Canonical setXn_group H := Group (group_setXn H).

Definition dfung1 i (g : gT i) : gTn := finfun (dfwith (fun⇒ 1 : gT _) g).

Lemma dfung1_id i (g : gT i) : dfung1 g i = g.

Lemma dfung1_dflt i (g : gT i) j : i != j → dfung1 g j = 1.

Lemma dfung1_morphM i : {morph @dfung1 i : g h / g × h}.
Canonical dfung1_morphism i := @Morphism _ _ setT _ (in2W (@dfung1_morphM i)).

Lemma dffunM i : {morph (fun x ⇒ x i) : x y / x × y}.

Canonical dffun_morphism i := @Morphism _ _ setT _ (in2W (@dffunM i)).

Lemma injm_dfung1 i : 'injm (@dfung1 i).

Lemma group_set_dfwith H i (G : {group gT i}) j :
  group_set (dfwith (H : ∀ k, {set gT k}) (G : {set _}) j).

Canonical group_dfwith H i G j := Group (@group_set_dfwith H i G j).

Lemma group_dfwithE H i G j : @group_dfwith H i G j = dfwith H G j.

Fact set1gXn_key : unit.
Definition set1gXn {i} (H : {set gT i}) : {set {dffun ∀ i : I, gT i}} :=
  locked_with set1gXn_key (setXn (dfwith (fun i0 : I ⇒ [1 gT _]%g) H)).

Lemma set1gXnE {i} (H : {set gT i}) :
  set1gXn H = setXn (dfwith (fun i0 : I ⇒ [1 gT _]%g) H).

Lemma set1gXnP {i} (H : {set gT i}) x :
  reflect (exists2 h, h \in H & x = dfung1 h) (x \in set1gXn H).

Lemma morphim_dfung1 i (G : {set gT i}) : @dfung1 i @* G = set1gXn G.

Lemma morphim_dffunXn i H : dffun_morphism i @* setXn H = H i.

Lemma set1gXn_group_set {i} (H : {group gT i}) : group_set (set1gXn H).

Canonical groupXn1 {i} (H : {group gT i}) := Group (set1gXn_group_set H).

Lemma setXn_prod H : \prod_i set1gXn (H i) = setXn H.

Lemma set1gXn_commute (H : ∀ i, {group gT i}) i j :
  commute (set1gXn (H i)) (set1gXn (H j)).

Lemma setXn_dprod H : \big[dprod/1]_i set1gXn (H i) = setXn H.

Lemma isog_setXn i (G : {group gT i}) : G \isog set1gXn G.

Lemma setXn_gen H : (∀ i, 1 \in H i) →
  <<setXn H>> = setXn (fun i ⇒ <<H i>>).

End ExternalDirDepProd.

Lemma groupX0 (gT : 'I_0 → finGroupType) (G : ∀ i, {group gT i}) :
  setXn G = 1%g.

Section ExternalSDirProd.

Variables (aT rT : finGroupType) (D : {group aT}) (R : {group rT}).