- -

Library mathcomp.fingroup.gproduct

- -

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

- -

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

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

- -

- Product remainder functions -- right variant only. -

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

- -

- Prenex Implicits remgl divgl. -

- -
-Section InternalProd.
- -
-Variable gT : finGroupType.
-Implicit Types A B C : {set gT }.
-Implicit Types G H K L M : {group gT }.
- -
- -
-Lemma pprod1g : left_id 1 pprod.
- -
-Lemma pprodg1 : right_id 1 pprod.
- -
-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.
- -
- -
-Section MorphimInternalProd.
- -
-Variables (gT rT : finGroupType) (D : {group gT }) (f : {morphism D >-> rT }).
- -
-Section OneProd.
- -
-Variables G H K : {group gT }.
-Hypothesis sGD : G \subset D.
- -
-Lemma morphim_pprod : pprod K H = G → pprod (f @* K) (f @* H) = f @* G.
- -
-Lemma morphim_coprime_sdprod :
-  K ><| H = G → coprime #|K | #|H | → f @* K ><| f @* H = f @* G.
- -
-Lemma injm_sdprod : 'injm f → K ><| H = G → f @* K ><| f @* H = f @* G.
- -
-Lemma morphim_cprod : K \* H = G → f @* K \* f @* H = f @* G.
- -
-Lemma injm_dprod : 'injm f → K \x H = G → f @* K \x f @* H = f @* G.
- -
-Lemma morphim_coprime_dprod :
-  K \x H = G → coprime #|K | #|H | → f @* K \x f @* H = f @* G.
- -
-End OneProd.
- -
-Implicit Type G : {group gT }.
- -
-Lemma morphim_bigcprod I r (P : pred I) (H : I → {group gT }) G :
-    G \subset D → \big [cprod /1]_(i <- r | P i ) H i = G →
-  \big [cprod /1]_(i <- r | P i ) f @* H i = f @* G.
- -
-Lemma injm_bigdprod I r (P : pred I) (H : I → {group gT }) G :
-    G \subset D → 'injm f → \big [dprod /1]_(i <- r | P i ) H i = G →
-  \big [dprod /1]_(i <- r | P i ) f @* H i = f @* G.
- -
-Lemma morphim_coprime_bigdprod (I : finType) P (H : I → {group gT }) G :
-    G \subset D → \big [dprod /1]_(i | P i ) H i = G →
-    (∀ i j, P i → P j → i != j → coprime #|H i | #|H j |) →
-  \big [dprod /1]_(i | P i ) f @* H i = f @* G.
- -
-End MorphimInternalProd.
- -
-Section QuotientInternalProd.
- -
-Variables (gT : finGroupType) (G K H M : {group gT }).
- -
-Hypothesis nMG: G \subset 'N (M ).
- -
-Lemma quotient_pprod : pprod K H = G → pprod (K / M) (H / M) = G / M.
- -
-Lemma quotient_coprime_sdprod :
-  K ><| H = G → coprime #|K | #|H | → (K / M ) ><| (H / M ) = G / M.
- -
-Lemma quotient_cprod : K \* H = G → (K / M ) \* (H / M ) = G / M.
- -
-Lemma quotient_coprime_dprod :
-  K \x H = G → coprime #|K | #|H | → (K / M ) \x (H / M ) = G / M.
- -
-End QuotientInternalProd.
- -
-Section ExternalDirProd.
- -
-Variables gT1 gT2 : finGroupType.
- -
-Definition extprod_mulg (x y : gT1 × gT2) := (x .1 × y .1 , x .2 × y .2 ).
-Definition extprod_invg (x : gT1 × gT2) := (x .1 ^-1 , x .2 ^-1 ).
- -
-Lemma extprod_mul1g : left_id (1, 1) extprod_mulg.
- -
-Lemma extprod_mulVg : left_inverse (1, 1) extprod_invg extprod_mulg.
- -
-Lemma extprod_mulgA : associative extprod_mulg.
- -
-Definition extprod_groupMixin :=
-  Eval hnf in FinGroup.Mixin extprod_mulgA extprod_mul1g extprod_mulVg.
-Canonical extprod_baseFinGroupType :=
-  Eval hnf in BaseFinGroupType (gT1 × gT2) extprod_groupMixin.
-Canonical prod_group := FinGroupType extprod_mulVg.
- -
-Lemma group_setX (H1 : {group gT1 }) (H2 : {group gT2 }) : group_set (setX H1 H2).
- -
-Canonical setX_group H1 H2 := Group (group_setX H1 H2).
- -
-Definition pairg1 x : gT1 × gT2 := (x , 1).
-Definition pair1g x : gT1 × gT2 := (1, x ).
- -
-Lemma pairg1_morphM : {morph pairg1 : x y / x × y }.
- -
-Canonical pairg1_morphism := @Morphism _ _ setT _ (in2W pairg1_morphM).
- -
-Lemma pair1g_morphM : {morph pair1g : x y / x × y }.
- -
-Canonical pair1g_morphism := @Morphism _ _ setT _ (in2W pair1g_morphM).
- -
-Lemma fst_morphM : {morph (@fst gT1 gT2 ) : x y / x × y }.
- -
-Lemma snd_morphM : {morph (@snd gT1 gT2 ) : x y / x × y }.
- -
-Canonical fst_morphism := @Morphism _ _ setT _ (in2W fst_morphM).
- -
-Canonical snd_morphism := @Morphism _ _ setT _ (in2W snd_morphM).
- -
-Lemma injm_pair1g : 'injm pair1g.
- -
-Lemma injm_pairg1 : 'injm pairg1.
- -
-Lemma morphim_pairg1 (H1 : {set gT1 }) : pairg1 @* H1 = setX H1 1.
- -
-Lemma morphim_pair1g (H2 : {set gT2 }) : pair1g @* H2 = setX 1 H2.
- -
-Lemma morphim_fstX (H1: {set gT1 }) (H2 : {group gT2 }) :
-  [morphism of fun x ⇒ x .1 ] @* setX H1 H2 = H1.
- -
-Lemma morphim_sndX (H1: {group gT1 }) (H2 : {set gT2 }) :
-  [morphism of fun x ⇒ x .2 ] @* setX H1 H2 = H2.
- -
-Lemma setX_prod (H1 : {set gT1 }) (H2 : {set gT2 }) :
-  setX H1 1 × setX 1 H2 = setX H1 H2.
- -
-Lemma setX_dprod (H1 : {group gT1 }) (H2 : {group gT2 }) :
-  setX H1 1 \x setX 1 H2 = setX H1 H2.
- -
-Lemma isog_setX1 (H1 : {group gT1 }) : isog H1 (setX H1 1).
- -
-Lemma isog_set1X (H2 : {group gT2 }) : isog H2 (setX 1 H2).
- -
-Lemma setX_gen (H1 : {set gT1 }) (H2 : {set gT2 }) :
-  1 \in H1 → 1 \in H2 → <<setX H1 H2 >> = setX <<H1 >> <<H2 >>.
- -
-End ExternalDirProd.
- -
-Section ExternalSDirProd.
- -
-Variables (aT rT : finGroupType) (D : {group aT }) (R : {group rT }).
- -
-

- -

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

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