Library mathcomp.fingroup.gproduct

(* (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 choice fintype bigop finset fingroup morphism.
From mathcomp Require Import quotient action.

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_act 'J 'J 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.

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.

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.

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

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.

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.

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 → _ := uncurry 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.

Arguments mulgmP {gT H1 H2 G}.