Library mathcomp.fingroup.gproduct

(* (c) Copyright 2006-2015 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.

Implicit Arguments partial_product [].
Implicit Arguments semidirect_product [].
Implicit Arguments central_product [].
Implicit Arguments direct_product [].
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.

Implicit Arguments complP [gT H A B].
Implicit Arguments splitsP [gT A B].
Implicit Arguments sdprod_normal_complP [gT K H G].
Implicit Arguments dprodYP [gT K H].
Implicit 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}.

Notation Local f := (pprodm nHK actf eqfHK).

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.

Implicit Arguments mulgmP [gT H1 H2 G].