Library gproduct

  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 "quotient" 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 : fA @* A \subset fB @* B,   
                        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 @* A \subset fB @* B 
        mulgm (x, y) == x * y; mulgm is an isomorphism from setX A B to G   
                        iff A \x B = G .                                    


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 

 Deferring the left variant, as we don't need it for the moment
Definition remgl A B x := repr (A :&: x *: B).
Definition divgl A B x := (remgl A B x)^-1 * x.

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) (at level 40, left associativity).
Notation "G \* H" := (cprod G H) (at level 40, left associativity).
Notation "G \x H" := (dprod G H) (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 : {group gT}.

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

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 : forall G, set0 <> G.

Lemma mulg0 : right_zero (@set0 gT) mulg.

Lemma mul0g : left_zero (@set0 gT) mulg.

Lemma pprodP : forall A B G,
  pprod A B = G -> [/\ are_groups A B, A * B = G & B \subset 'N(A)].

Lemma pprodE : forall K H, H \subset 'N(K) -> pprod K H = K * H.

Lemma pprodEY : forall K H, H \subset 'N(K) -> pprod K H = K <*> H.

 Properties of the remainders 
 Outcommented left variant as not currently used -- GG
Lemma remgl_id : forall A G x y, y \in G -> remgl A G (x * y) = remgl A G x.
Proof. by move=> A G x y Gy; rewrite {1}/remgl lcosetM lcoset_id. Qed.

Lemma remglP : forall A G x, (remgl A G x \in A :&: x *: G) = (x \in A * G).
Proof.
move=> A G x; set y := remgl A G x; apply/idP/mulsgP=> [|[a g Aa Gg x_ag]].
  rewrite inE lcoset_sym mem_lcoset; case/andP=> Ay Gy'x.
  by exists y (y^-1 * x); rewrite ?mulKVg.
by apply: (mem_repr a); rewrite inE Aa lcoset_sym mem_lcoset x_ag mulKg.
Qed.

Lemma divgl_eq : forall A B x, x = remgl A B x * divgl A B x.
Proof. by move=> A B x; rewrite mulKVg. Qed.

Lemma divgl_id : forall A G x y,
  y \in G -> divgl A G (x * y) = divgl A G x * y.
Proof. by move=> A G x y Gy; rewrite /divgl remgl_id ?mulgA. Qed.

Lemma mem_remgl : forall A G x, x \in A * G -> remgl A G x \in A.
Proof. by move=> A G x; rewrite -remglP; case/setIP. Qed.

Lemma mem_divgl : forall A G x, x \in A * G -> divgl A G x \in G.
Proof.
by move=> A G x; rewrite -remglP inE lcoset_sym mem_lcoset; case/andP.
Qed.


Lemma remgrMl : forall K B x y, y \in K -> remgr K B (y * x) = remgr K B x.

Lemma remgrP : forall K B x, (remgr K B x \in K :* x :&: B) = (x \in K * B).

Lemma remgr1 : forall K H x, x \in K -> remgr K H x = 1.

Lemma divgr_eq : forall A B x, x = divgr A B x * remgr A B x.

Lemma divgrMl : forall K B x y,
  x \in K -> divgr K B (x * y) = x * divgr K B y.

Lemma divgr_id : forall K H x, x \in K -> divgr K H x = x.

Lemma mem_remgr : forall K B x, x \in K * B -> remgr K B x \in B.

Lemma mem_divgr : forall 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 : forall x, x \in H -> remgr K H x = x.

Lemma remgrMid : forall x y, x \in K -> y \in H -> remgr K H (x * y) = y.

Lemma divgrMid : forall 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 : forall 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 : forall H A B,
  reflect (A :&: H = 1 /\ A * H = B) (H \in [complements to A in B]).

Lemma splitsP : forall B A,
  reflect (exists H, H \in [complements to A in B]) [splits B, over A].

Lemma complgC : forall 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].
Hypothesis nKG : K <| G.

Lemma remgrM : {in G &, {morph remgr 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 : forall A B G,
  A ><| B = G -> [/\ are_groups A B, A * B = G, B \subset 'N(A) & A :&: B = 1].

Lemma sdprodE : forall K H, H \subset 'N(K) -> K :&: H = 1 -> K ><| H = K * H.

Lemma sdprodEY : forall K H,
  H \subset 'N(K) -> K :&: H = 1 -> K ><| H = K <*> H.

Lemma sdprod_context : forall G K H, K ><| H = G ->
  [/\ K <| G, H \subset G, K * H = G, H \subset 'N(K) & K :&: H = 1].

Lemma sdprod_compl : forall G K H, K ><| H = G -> H \in [complements to K in G].

Lemma sdprod_normal_complP : forall G K H,
  K <| G -> reflect (K ><| H = G) (K \in [complements to H in G]).

Lemma sdprod_card : forall G A B, A ><| B = G -> (#|A| * #|B|)%N = #|G|.

Lemma sdprod_modl : forall A B G H,
  A ><| B = G -> A \subset H -> A ><| (B :&: H) = G :&: H.

Lemma sdprod_modr : forall A B G H,
  A ><| B = G -> B \subset H -> (H :&: A) ><| B = H :&: G.

Lemma subcent_sdprod : forall 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 : forall n G K H K1,
  #|G| <= n -> K ><| H = G -> K1 \proper K -> H \subset 'N(K1) ->
  exists G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K1 ><| H = G1].

Lemma sdprod_recr : forall n G K H H1,
  #|G| <= n -> K ><| H = G -> H1 \proper H ->
  exists G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K ><| H1 = G1].

Lemma mem_sdprod : forall G A B x, A ><| B = G -> x \in G ->
  exists y, exists z,
    [/\ y \in A, z \in B, x = y * z &
        {in A & B, forall 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 : forall A B G,
  A \* B = G -> [/\ are_groups A B, A * B = G & B \subset 'C(A)].

Lemma cprodE : forall G H, H \subset 'C(G) -> G \* H = G * H.

Lemma cprodEY : forall G H, H \subset 'C(G) -> G \* H = G <*> H.

Lemma cprod_normal2 : forall K H G, K \* H = G -> K <| G /\ H <| G.

Lemma bigcprodE : forall 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 bigcprodEY : forall 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 cprodC : commutative cprod.

Lemma triv_cprod : forall A B, (A \* B == 1) = (A == 1) && (B == 1).

Lemma cprod_ntriv : forall 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 : forall A, set0 \* A = set0.

Lemma cprodA : associative cprod.

Canonical Structure cprod_law := Monoid.Law cprodA cprod1g cprodg1.
Canonical Structure cprod_abelaw := Monoid.ComLaw cprodC.

Lemma cprod_modl : forall A B G H,
  A \* B = G -> A \subset H -> A \* (B :&: H) = G :&: H.

Lemma cprod_modr : forall A B G H,
  A \* B = G -> B \subset H -> (H :&: A) \* B = H :&: G.

 Direct product 

Lemma dprod1g : left_id 1 dprod.

Lemma dprodg1 : right_id 1 dprod.

Lemma dprodP : forall A B G,
  A \x B = G -> [/\ are_groups A B, A * B = G, B \subset 'C(A) & A :&: B = 1].

Lemma dprodE : forall G H,
  H \subset 'C(G) -> G :&: H = 1 -> G \x H = G * H.

Lemma dprodEcprod : forall A B, A :&: B = 1 -> A \x B = A \* B.

Lemma dprodEsdprod : forall A B, B \subset 'C(A) -> A \x B = A ><| B.

Lemma dprodEY : forall G H,
  H \subset 'C(G) -> G :&: H = 1 -> G \x H = G <*> H.

Lemma dprod_normal2 : forall K H G, K \x H = G -> K <| G /\ H <| G.

Lemma dprodYP : forall K H,
  reflect (K \x H = K <*> H) (H \subset 'C(K) :\: K^#).

Lemma dprodC : commutative dprod.

Lemma dprodA : associative dprod.

Canonical Structure dprod_law := Monoid.Law dprodA dprod1g dprodg1.
Canonical Structure dprod_abelaw := Monoid.ComLaw dprodC.

Lemma bigdprodEcprod : forall 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 bigdprodE : forall 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 bigdprodEY : forall 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 : forall (I : finType) (P : pred I) (F : I -> {group gT}),
  reflect (forall 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 : forall A B G H,
  A \x B = G -> A \subset H -> A \x (B :&: H) = G :&: H.

Lemma dprod_modr : forall A B G H,
  A \x B = G -> B \subset H -> (H :&: A) \x B = H :&: G.

Lemma subcent_dprod : forall 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 : forall A B G, A \x B = G -> (#|A| * #|B|)%N = #|G|.

Lemma bigdprod_card : forall 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 mem_dprod : forall G A B x, A \x B = G -> x \in G ->
  exists y, exists z,
    [/\ y \in A, z \in B, x = y * z &
        {in A & B, forall u t, x = u * t -> u = y /\ t = z}].

Lemma mem_bigdprod : forall (I : finType) (P : pred I) F G x,
    \big[dprod/1]_(i | P i) F i = G -> x \in G ->
  exists c, [/\ forall i, P i -> c i \in F i, x = \prod_(i | P i) c i
              & forall e, (forall i, P i -> e i \in F i) ->
                          x = \prod_(i | P i) e i ->
                forall 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) (G K H D : {group gT}).

Variable f : {morphism D >-> rT}.
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 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 Structure extprod_baseFinGroupType :=
  Eval hnf in BaseFinGroupType (gT1 * gT2) extprod_groupMixin.
Canonical Structure prod_group := FinGroupType extprod_mulVg.

Lemma group_setX : forall (H1 : {group gT1}) (H2 : {group gT2}),
  group_set (setX H1 H2).

Canonical Structure 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 Structure pairg1_morphism :=
  @Morphism _ _ setT _ (in2W pairg1_morphM).

Lemma pair1g_morphM : {morph pair1g : x y / x * y}.

Canonical Structure 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 Structure fst_morphism :=
  @Morphism _ _ setT _ (in2W fst_morphM).

Canonical Structure snd_morphism :=
  @Morphism _ _ setT _ (in2W snd_morphM).

Lemma injm_pair1g : 'injm pair1g.

Lemma injm_pairg1 : 'injm pairg1.

Lemma morphim_pairg1 : forall (H1 : {set gT1}), pairg1 @* H1 = setX H1 1.

Lemma morphim_pair1g : forall (H2 : {set gT2}), pair1g @* H2 = setX 1 H2.

Lemma morphim_fstX : forall (H1: {set gT1}) (H2 : {group gT2}),
  [morphism of fun x => x.1] @* setX H1 H2 = H1.

Lemma morphim_sndX : forall (H1: {group gT1}) (H2 : {set gT2}),
  [morphism of fun x => x.2] @* setX H1 H2 = H2.

Lemma setX_prod : forall (H1 : {set gT1}) (H2 : {set gT2}),
  setX H1 1 * setX 1 H2 = setX H1 H2.

Lemma setX_dprod : forall (H1 : {group gT1}) (H2 : {group gT2}),
  setX H1 1 \x setX 1 H2 = setX H1 H2.

Lemma isog_setX1 : forall (H1 : {group gT1}), isog H1 (setX H1 1).

Lemma isog_set1X : forall (H2 : {group gT2}), isog H2 (setX 1 H2).

Lemma setX_gen : forall (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 Structure sdprod_subType :=
  Eval hnf in [subType for sdval by @sdprod_by_rect to].
Definition sdprod_eqMixin := Eval hnf in [eqMixin of sdT by <:].
Canonical Structure sdprod_eqType := Eval hnf in EqType sdT sdprod_eqMixin.
Definition sdprod_choiceMixin := [choiceMixin of sdT by <:].
Canonical Structure sdprod_choiceType := ChoiceType sdT sdprod_choiceMixin.
Definition sdprod_countMixin := [countMixin of sdT by <:].
Canonical Structure sdprod_countType := CountType sdT sdprod_countMixin.
Canonical Structure sdprod_subCountType := Eval hnf in [subCountType of sdT].
Definition sdprod_finMixin := [finMixin of sdT by <:].
Canonical Structure sdprod_finType := FinType sdT sdprod_finMixin.
Canonical Structure sdprod_subFinType := Eval hnf in [subFinType of sdT].

Definition sdprod_one := SdPair to (group1 _).

Lemma sdprod_inv_proof : forall 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 : forall 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 Structure sdprod_groupMixin :=
  FinGroup.Mixin sdprod_mulgA sdprod_mul1g sdprod_mulVg.

Canonical Structure sdprod_baseFinGroupType :=
  Eval hnf in BaseFinGroupType sdT sdprod_groupMixin.

Canonical Structure 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 Structure sdpair1_morphism := Morphism sdpair1_morphM.

Canonical Structure sdpair2_morphism := Morphism sdpair2_morphM.

Lemma injm_sdpair1 : 'injm sdpair1.

Lemma injm_sdpair2 : 'injm sdpair2.

Lemma sdpairE : forall u : sdT, u = sdpair2 u.1 * sdpair1 u.2.

Lemma sdpair_act : {in R & D,
  forall x a, sdpair1 (to x a) = sdpair1 x ^ sdpair2 a}.

Lemma sdpair_setact : forall (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 : forall 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 Structure pprodm_morphism := Morphism pprodmM.

Lemma morphim_pprodm : forall A B,
  A \subset H -> B \subset K -> f @* (A * B) = fH @* A * fK @* B.

Lemma morphim_pprodml : forall A, A \subset H -> f @* A = fH @* A.

Lemma morphim_pprodmr : forall B, B \subset K -> f @* B = fK @* B.

Lemma ker_pprodm : 'ker f = [set x * a^-1 | x <- H, a <- 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 Structure sdprodm_morphism := Eval hnf in [morphism of sdprodm].

Lemma sdprodmE : forall a b,
  a \in H -> b \in K -> sdprodm (a * b) = fH a * fK b.

Lemma sdprodmEl : forall a, a \in H -> sdprodm a = fH a.

Lemma sdprodmEr : forall b, b \in K -> sdprodm b = fK b.

Lemma morphim_sdprodm : forall 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 : forall A, A \subset H -> sdprodm @* A = fH @* A.

Lemma morphim_sdprodmr : forall B, B \subset K -> sdprodm @* B = fK @* B.

Lemma ker_sdprodm :
  'ker sdprodm = [set a * b^-1 | a <- H, b <- 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 Structure cprodm_morphism := Eval hnf in [morphism of cprodm].

Lemma cprodmE : forall a b, a \in H -> b \in K -> cprodm (a * b) = fH a * fK b.

Lemma cprodmEl : forall a, a \in H -> cprodm a = fH a.

Lemma cprodmEr : forall b, b \in K -> cprodm b = fK b.

Lemma morphim_cprodm : forall 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 : forall A, A \subset H -> cprodm @* A = fH @* A.

Lemma morphim_cprodmr : forall B, B \subset K -> cprodm @* B = fK @* B.

Lemma ker_cprodm : 'ker cprodm = [set a * b^-1 | a <- H, b <- 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 Structure dprodm_morphism := Eval hnf in [morphism of dprodm].

Lemma dprodmE : forall a b, a \in H -> b \in K -> dprodm (a * b) = fH a * fK b.

Lemma dprodmEl : forall a, a \in H -> dprodm a = fH a.

Lemma dprodmEr : forall b, b \in K -> dprodm b = fK b.

Lemma morphim_dprodm : forall 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 : forall A, A \subset H -> dprodm @* A = fH @* A.

Lemma morphim_dprodmr : forall B, B \subset K -> dprodm @* B = fK @* B.

Lemma ker_dprodm : 'ker dprodm = [set a * b^-1 | a <- H, b <- K, fH a == fK b].

Lemma injm_dprodm :
  'injm dprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].

End Dprodm.

Lemma isog_dprod : forall 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}.

Local Notation fsH := (fH \o invm (injm_sdpair1 to)).
Local Notation fsK := (fK \o invm (injm_sdpair2 to)).

Lemma xsdprodm_dom1 : DgH \subset 'dom fsH.
Local Notation gH := (restrm xsdprodm_dom1 fsH).

Lemma xsdprodm_dom2 : DgK \subset 'dom fsK.
Local Notation gK := (restrm xsdprodm_dom2 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 Structure 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 : forall A B : {set gT}, mulgm @: setX A B = A * B.

Lemma mulgmP : forall H1 H2 G,
  reflect (H1 \x H2 = G) (misom (setX H1 H2) G mulgm).

End DirprodIsom.

Implicit Arguments mulgmP [gT H1 H2 G].