Library fingroup
Require Import ssreflect.
Require Import ssrbool.
Require Import ssrfun.
Require Import eqtype.
Require Import seq.
Require Import fintype.
Require Import ssrnat.
Require Import general.
Require Import finfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Opaque fgraph_of_fun.
Section FiniteGroup.
Structure finGroupType: Type := FinGroupType {
element :> finType;
unit: element;
inv: element -> element;
mul: element -> element -> element;
unitlP: forall x, mul unit x = x;
invlP: forall x, mul (inv x) x = unit;
mulP: forall x y z, mul x (mul y z) = mul (mul x y) z
}.
Variable G:finGroupType.
Lemma invrP: forall x:G, mul x (inv x) = unit G.
Proof. by move=>x; rewrite -(unitlP (mul x (inv x))) -{1}(invlP (inv x))
mulP -(mulP (inv (inv x)) _ _) invlP -mulP unitlP invlP. Qed.
Lemma unitrP: forall x:G, mul x (unit G) = x.
Proof. move=>x. by rewrite -(invlP x) mulP invrP unitlP. Qed.
Lemma inv_unit: inv (unit G) = (unit G).
Proof.
have H: mul (unit G) (inv (unit _)) = (unit _) by apply invrP.
by rewrite unitlP in H.
Qed.
Lemma inv_inv: forall x:G, inv (inv x) = x.
Proof.
move=>x.
have H: (mul (inv (inv x)) (inv x) = (unit _)).
by rewrite invlP.
have K: (mul (mul (inv (inv x)) (inv x)) x = mul (unit _) x).
by rewrite H.
by rewrite -mulP invlP unitlP unitrP in K.
Qed.
Notation "'mul'":=(mul).
Notation "'inv'":=(inv).
Lemma inv_mul: forall x y:G, inv (mul x y) = mul (inv y) (inv x).
Proof.
move=>x y.
have H: (mul (mul x y) (inv (mul x y))) = mul (mul x y) (mul (inv y) (inv x)).
by rewrite invrP -mulP [mul y _]mulP invrP unitlP invrP.
rewrite invrP in H.
rewrite -(unitrP (inv (mul x y))) H.
by rewrite [mul x y]lock mulP -!lock invlP unitlP.
Qed.
Lemma cancelr: forall x y:G, mul x y = x -> y = (unit G).
Proof. by move=>x y H; rewrite -(unitlP y) -(invlP x) -mulP H invlP. Qed.
Lemma cancell: forall x y:G, mul y x = x -> y = (unit G).
Proof. by move=>x y H; rewrite -(unitrP y) -(invrP x) mulP H invrP. Qed.
Definition commutative := forall x y:G, mul x y == mul y x.
Notation "'mul'":=(mul (f:=G)).
Notation "'inv'":=(inv (f:=G)).
Definition order(m:nat) (x:G):= (iter m (mul x) (unit G) = (unit G)).
Definition sum_seq(l:seq G) := foldr (fun x y=>mul x y) (unit G) l.
Lemma sum_seq_cat: forall (l1 l2:seq G),
sum_seq (cat l1 l2) = mul (sum_seq l1) (sum_seq l2).
Proof.
elim=>//=[l2|x xs IH l2]; first by rewrite unitlP. by rewrite -mulP -IH.
Qed.
Lemma sum_seq_flatten: forall l,
sum_seq (flatten l) = sum_seq (maps sum_seq l).
Proof. elim=>//=[x xs IH]; by rewrite -IH sum_seq_cat. Qed.
Definition generators(gens:pred G) :=
forall g:G, {l:seq G | (all (fun x=> gens x || gens (inv x)) l) /\ g = (sum_seq l)}.
End FiniteGroup.
Implicit Arguments mul [].
Implicit Arguments inv [].
Notation "'mul'":=(mul _).
Notation "'inv'":=(inv _).
Section GroupAction.
Variable G:finGroupType.
Variable S:Type.
Structure groupAction: Type := GroupAction {
action :> S -> G -> S;
act_unitP: forall x, action x (unit G) = x;
act_mulP: forall x g g', action (action x g) g' = action x (mul g g')
}.
Variable act: groupAction.
Definition free := forall x g, act x g = x -> g == (unit G).
Lemma act_free_eq: free -> forall x g g', act x g = act x g' -> g == g'.
Proof.
move=>F x g g' E.
have H:(mul g (inv g') = unit _).
have K:(act (act x g) (inv g') = act (act x g') (inv g')) by rewrite E; congruence.
rewrite !act_mulP invrP act_unitP in K.
rewrite /free in F.
exact (eqP (F x (mul g (inv g')) K)).
have K:(mul (mul g (inv g')) g' = mul (unit _) g') by congruence.
rewrite -mulP invlP unitlP unitrP in K.
rewrite K.
by apply/eqP.
Qed.
Definition transitive := forall x y, exists g, y = act x g.
End GroupAction.
Section CyclicGroup.
Variable m:nat.
Variable m_positive: 0 < m.
Definition inv_modulo: ordinal m -> ordinal m.
move=>[i im].
by apply: (Ordinal (mod_lt (m-i) m_positive)).
Defined.
Definition mul_modulo: ordinal m -> ordinal m -> ordinal m :=
fun x y => Ordinal (mod_lt (x + y) m_positive).
Definition cyclicgroup : finGroupType.
apply (@FinGroupType (ordinal_finType m) (Ordinal m_positive)
(fun x => Ordinal (mod_lt (m - x) m_positive))
(fun x y => Ordinal (mod_lt (x + y) m_positive))).
move=>[x xm].
apply/eqP; rewrite eqE /=.
by rewrite add0n mod_small // eq_refl.
move=>[x xm].
apply/eqP; rewrite eqE /=.
by rewrite addnC -mod_add (subnK (ltnW xm)) -{1}(mul1n m) mod0 eq_refl.
move=>[x xm] [y ym] [z zm].
apply/eqP; rewrite eqE /=.
by rewrite -mod_add [mod _ _ +z]addnC -mod_add [z+_]addnC addnA eq_refl.
Defined.
Lemma order_cyclicgroup: forall x:cyclicgroup, order m x.
move=>x; rewrite /order.
have H: forall n, (iter n (mul x) (unit cyclicgroup)) == Ordinal (mod_lt (n*x) m_positive).
elim=>/=[|n IH].
by rewrite eqE /= (mod_small).
by rewrite eqE (eqP IH) /= -mod_add eq_refl.
rewrite (eqP (H m)).
by apply/eqP; rewrite eqE /= mulnC mod0 eq_refl.
Qed.
Lemma comm_cyclicgroup: commutative cyclicgroup.
Proof. by move=>[x xm] [y ym]; rewrite eqE /= addnC eq_refl. Qed.
Construction of Generators:
Variable mgt1: (1 < m).
Definition one_cyclicgroup: cyclicgroup := Ordinal mgt1.
The generators of the cylic group
Definition gens_cyclicgroup := [:: one_cyclicgroup].
Lemma size_gens_cyclicgroup : size gens_cyclicgroup = 1.
Proof. done. Qed.
Lemma gen_cyclicgroup: generators (gens_cyclicgroup).
Proof.
move=>[i im].
exists (seqn i one_cyclicgroup); split.
by clear im; elim: i.
apply/eqP; rewrite eqE /=; apply/eqP.
elim: i im =>//=[n IH im].
rewrite -IH.
by rewrite add1n (@eq_mod (S n) m m_positive 0 (S n) im) //.
by apply: ltnW.
Qed.
End CyclicGroup.
Section TuplesGroup.
Variable d : nat.
Variable G : finGroupType.
Definition tuplegroup : finGroupType.
apply (@FinGroupType (finFun (ordinal_finType d) G)
(fgraph_of_fun (fun i => unit G))
(fun x => fgraph_of_fun (fun i => inv (x i)))
(fun x y => fgraph_of_fun (fun i => mul (x i) (y i)))).
move=>x. by apply/eqP; apply: eq_finfun=>i; rewrite !fgraph_fun_eq unitlP.
move=>x. apply/eqP; apply: eq_finfun=>i. by rewrite !fgraph_fun_eq invlP.
move=>x y z. apply/eqP; apply: eq_finfun=>i. by rewrite !fgraph_fun_eq mulP.
Defined.
Lemma order_tuplegroup: forall m,
(forall x:G, order m x) -> forall t:tuplegroup, order m t.
Proof.
move=>m H t; rewrite /order.
have K: forall n i, (iter n (mul t) (unit tuplegroup)) i == iter n (mul (t i)) (unit G).
elim=>/=[i|n IH i].
by rewrite fgraph_fun_eq eq_refl.
by move: (IH i); rewrite !fgraph_fun_eq=>K; rewrite (eqP K) eq_refl.
apply/eqP; apply: eq_finfun=>i.
by rewrite (eqP (K m i)) (H (t i)) /= fgraph_fun_eq.
Qed.
Lemma comm_tuplegroup: commutative G -> commutative tuplegroup.
Proof. by move=>c x y; apply: eq_finfun=>i;
rewrite /= !fgraph_fun_eq (eqP (c _ _)). Qed.
Construction of Generators:
Variable gens_G : seq G.
Variable generators_G : generators gens_G.
Definition unit_vector (i: ordinal d) (g:G) : tuplegroup
:= fgraph_of_fun (fun j=> if i == j then g else unit G).
Each vector can be written as a sum of unit vectors, i.e. vectors that
have at most one entry different from the unit element
Lemma sum_unit_vector: forall g:tuplegroup,
g = sum_seq (maps (fun i => unit_vector i (g i)) (enum (ordinal_finType d))).
Proof.
have H: forall (g:tuplegroup) (l:seq (ordinal_eqType d)) x,
((count (pred1 x) l) <= 1) ->
sum_seq (maps (fun i => unit_vector i (g i)) l) x = if l x then g x else unit _.
move=>h l y.
elim: l=>//=[_|z zs IH H].
by rewrite !fgraph_fun_eq /=.
case U: (y == z).
rewrite -(eqP U) eq_refl -(addn0 1) leq_add2l in H.
rewrite !fgraph_fun_eq /= /predU1 -(eqP U) eq_refl orTb IH.
case V: (zs y).
by rewrite -(has_pred1 y) has_count in V; move: (leq_trans V H).
by rewrite unitrP.
by apply: (leq_trans H _).
rewrite fgraph_fun_eq IH /predU1.
case V: (mem zs y).
rewrite orbT /unit_vector fgraph_fun_eq eq_sym.
have W: mul (if y == z then fun_of_fgraph h z else unit G) (h y) = h y
by rewrite U unitlP.
by exact W.
rewrite orbF /unit_vector !fgraph_fun_eq /= unitrP.
rewrite eq_sym in U.
have W: (z == y) = false ->
(if z == y then fun_of_fgraph h z else unit G)
= (if z == y then fun_of_fgraph h y else unit G)
by move=>[->].
by apply: W.
by apply: (leq_trans _ H); apply: leq_addl.
move=>g; apply/eqP; apply: eq_finfun=>x.
by rewrite H ?mem_enum // FinType.enumP.
Qed.
Each unit vector can be written as a sum of unit vectors, which may only
contain generators of
G as entries.
Lemma unit_vector_gen: forall i g,
unit_vector i g = sum_seq (maps (unit_vector i) (proj1_sig (generators_G g))).
Proof.
move=>i g.
move: (proj2_sig (generators_G g))=>[_ H].
rewrite {1}H.
elim: (proj1_sig (generators_G g))=>//=[|x xs IH].
apply/eqP; apply: eq_finfun=>x; rewrite !fgraph_fun_eq /=.
by case: ifP.
rewrite -IH.
apply/eqP; apply: eq_finfun=>y; rewrite /unit_vector !fgraph_fun_eq /=.
by case: ifP=>U; rewrite U ?unitrP.
Qed.
The generators of the tuple group are the vectors that contain
at most one non-unit entry, which moreover can be assumed to come
from the generators of
G.
Definition gens_tuplegroup : seq tuplegroup :=
flatten (maps (fun i=> maps (fun g => unit_vector i g) gens_G) (enum (ordinal_finType d))).
Lemma mem_gens_tuplegroup: forall t,
gens_tuplegroup t =
has (fun i => has (fun g => t == unit_vector i g) gens_G) (enum (ordinal_finType d)).
Proof.
move=>t.
rewrite /gens_tuplegroup.
elim: (enum (ordinal_finType d))=>//=[y ys <-].
rewrite mem_cat /predU; congr (_ || _).
elim: gens_G=>//=[z zs <-].
by rewrite /predU1; congr (_ || _); rewrite eq_sym.
Qed.
Lemma size_gens_tuplegroup: size gens_tuplegroup = d * (size gens_G).
Proof.
have H: d = size (enum (ordinal_finType d)) by rewrite -cardA card_ordinal.
rewrite /gens_tuplegroup {4}H.
elim: (enum _)=>//=[x xs K].
rewrite mulSn -K.
rewrite size_cat size_maps; congr (_ + _).
Qed.
Lemma generators_tuplegroup: generators (gens_tuplegroup).
Proof.
move=>g.
exists (flatten (maps (fun i=> maps (fun g => unit_vector i g) (proj1_sig (generators_G (g i)))) (enum (ordinal_finType d)))).
split.
apply/allP=>h.
elim: (enum (ordinal_finType d)) =>//[i s IH /=H].
rewrite mem_cat /predU in H.
move/orP:H=>[H1|H2].
clear IH.
move: (proj2_sig (generators_G (g i))) => [K _].
elim: (proj1_sig (generators_G (g i))) H1 K =>//=[x y IH L K].
move/orP:L=>[L1|L2].
move/andP: K=>[K1 K2].
rewrite -(eqP L1) !mem_gens_tuplegroup.
move/orP: K1=>[K1|K1].
apply/orP; left.
apply/hasP; exists i; first by rewrite mem_enum.
apply/hasP. by exists x.
apply/orP; right.
apply/hasP; exists i; first by rewrite mem_enum.
apply/hasP. exists (inv x)=>//.
apply: eq_finfun=>z; rewrite /unit_vector !fgraph_fun_eq /=.
by symmetry; case: ifP=>U; rewrite U ?inv_unit.
by rewrite IH=>//; move/andP: K=>[_ K].
move/orP: (IH H2)=>[K1|K2]; clear IH H2.
by apply/orP; left=>//.
by apply/orP; right=>//.
rewrite sum_seq_flatten -maps_comp /comp {1}(sum_unit_vector g).
by congr sum_seq; apply: eq_maps=>i; rewrite unit_vector_gen.
Qed.
End TuplesGroup.
Section WreathProduct.
Variable G H : finGroupType.
Variable ordG ordH : nat.
Variable orderG : forall g:G, order ordG g.
Variable orderH : forall h:H, order ordH h.
Definition carrier_wp : finType := {G * (finFun G H) :as finType}.
Definition unit_wp : carrier_wp := (unit G, fgraph_of_fun (fun i:G => unit H)).
Definition inv_wp : carrier_wp -> carrier_wp :=
(fun x => (inv x.1,
fgraph_of_fun (fun i=>inv (x.2 (mul x.1 i))))).
Definition mul_wp: carrier_wp -> carrier_wp -> carrier_wp :=
(fun x y => (mul x.1 y.1,
fgraph_of_fun (fun i=> mul (x.2 i)
(y.2 (mul (inv x.1) i))))).
The Wreath Product of
G and H
Definition wp : finGroupType.
apply (@FinGroupType carrier_wp unit_wp inv_wp mul_wp).
move=>[x1 x2].
apply/pair_eqP; apply/andP; split.
by rewrite /= unitlP eq_refl.
apply: eq_finfun=>i. by rewrite /= !fgraph_fun_eq /= inv_unit !unitlP.
move=>[x1 x2].
apply/pair_eqP; apply/andP; split=>/=.
by rewrite invlP eq_refl.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
by rewrite inv_inv invlP.
move=>[x1 x2] [y1 y2] [z1 z2].
apply/pair_eqP; apply/andP; split=>/=.
by rewrite mulP eq_refl.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
by rewrite inv_mul -!mulP.
Defined.
Lemma order_wp: (commutative H) -> forall d:wp, order (ordG * ordH) d.
Proof.
move=>commH [x1 x2].
set x:wp:= (x1, x2).
set times:=fun (G:finGroupType) k x => iter k (mul x) (unit G).
have times_add: forall D k l x, times D (k+l) x = mul (times D k x) (times D l x).
move=>D.
elim=>/=[l z|k IH l z].
by rewrite add0n unitlP.
by rewrite IH -!mulP.
set sum:= fun k i => iter_n k (fun n z => mul (x2 (mul (inv (times _ n x1)) i)) z) (unit _).
have Hsum: forall k i, sum (S k) i = mul (x2 i) (sum k (mul (inv x1) i)).
elim=>[i|k IH i].
by rewrite /= inv_unit unitlP !unitrP.
move:(IH i)=>/= ->.
rewrite !mulP.
by rewrite (eqP (commH _ (x2 i))) inv_mul.
have K: forall k, times _ k x = (times _ k x1, fgraph_of_fun (fun i=>sum k i)).
elim=>/=[|k IH].
by apply/pair_eqP; apply/andP; split=>//=.
apply/pair_eqP; apply/andP; split=>//=.
by rewrite IH /=; apply/eqP.
rewrite IH.
apply: eq_finfun=>i; rewrite /= !fgraph_fun_eq /=.
by rewrite -Hsum.
have L: forall k, times _ (k*ordG) x =
(times _ (k*ordG) x1, fgraph_of_fun (fun i=>times _ k (sum ordG i))).
elim=>/=[|k IH].
by apply/pair_eqP; apply/andP; split=>//=.
rewrite !times_add IH.
apply/pair_eqP; apply/andP; split.
apply/eqP=>/=.
by rewrite K/=.
rewrite K/=.
apply: eq_finfun=>i; rewrite /= !fgraph_fun_eq /=.
by rewrite {2}/times orderG inv_unit unitlP.
have M: forall k, times _ (k*ordG) x1 = unit _.
elim=>[|k IH].
by rewrite mul0n.
by rewrite /= times_add IH /times orderG unitrP.
move: (L ordH); clear K L.
rewrite /times /order mulnC => [->].
apply/pair_eqP; apply/andP; split=>/=.
by apply/eqP; rewrite mulnC -{2}(M ordH).
by apply: eq_finfun=>i; rewrite /= !fgraph_fun_eq /=; apply: orderH.
Qed.
Construction of Generators for the Wreath Product
Variable gensG : seq G.
Variable gensH : seq H.
Variable generatorsG: generators gensG.
Variable generatorsH: generators gensH.
Definition mkunitG(g:G): wp :=
(g, fgraph_of_fun (fun i=>unit _)).
Definition mkunitH(g:G)(h:H): wp :=
(unit G, fgraph_of_fun (fun i=>if i== g then h else (unit H))).
We show that the list gens_wp is a set of generators
for the wreath product of G and H.
Definition gens_wp: seq wp :=
cat (maps mkunitG gensG) (maps (mkunitH (unit G)) gensH).
Lemma mem_gens_wp: forall x,
gens_wp x = (has (fun g => x == mkunitG g) gensG)
|| (has (fun h => x == mkunitH (unit G) h) gensH).
Proof.
move=>x; rewrite /gens_wp mem_cat /predU; congr (_||_).
by elim: gensG=>//=[y ys <-]; rewrite eq_sym.
by elim: gensH=>//=[y ys <-]; rewrite eq_sym.
Qed.
Lemma inv_mkunitG: forall g, inv (mkunitG g) = mkunitG (inv g).
Proof.
move=>g.
apply/pair_eqP; apply/andP; split=>//=.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
by rewrite inv_unit.
Qed.
Lemma inv_mkunitH_unit: forall h,
inv (mkunitH (unit G) h) = mkunitH (unit G) (inv h).
Proof.
move=>h.
apply/pair_eqP; apply/andP; split=>//=.
by apply/eqP; rewrite inv_unit.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
rewrite unitlP.
case U: (i== unit G)=>//.
by rewrite inv_unit.
Qed.
Lemma mkunitG_unit: mkunitG (unit G) = unit wp.
Proof. done. Qed.
Lemma mkunitG_mul: forall (g1 g2:G),
mkunitG (mul g1 g2) = mul (mkunitG g1) (mkunitG g2).
Proof.
move=>g1 g2.
apply/pair_eqP; apply/andP; split=>//=.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
by rewrite unitrP.
Qed.
Lemma mkunitH_mul: forall (g:G) (h1 h2:H),
mkunitH g (mul h1 h2) = mul (mkunitH g h1) (mkunitH g h2).
Proof.
move=>g h1 h2.
apply/pair_eqP; apply/andP; split=>//=.
by apply/eqP; rewrite unitrP.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
rewrite inv_unit unitlP.
case: (i == g)=>//; by rewrite unitrP.
Qed.
Lemma mkunitH_unit: mkunitH (unit G) (unit H) = unit wp.
Proof.
apply/pair_eqP; apply/andP; split=>//=.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
by case: (i == unit G).
Qed.
Lemma mkunitH_genH: forall (g:G) (h:H),
{l: seq H |
all (fun x=> gensH x || gensH (inv x)) l /\ (mkunitH g h) = sum_seq (maps (mkunitH g) l)}.
Proof.
move=>g h.
move:(generatorsH h)=>[l [K1 K2]].
exists l.
rewrite K1 K2 /sum_seq foldr_maps; split=>//; clear K1 K2.
elim: l=>/=[|x l IH].
apply/pair_eqP; apply/andP; split=>//=.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
by case: (i == g).
by rewrite -IH mkunitH_mul.
Qed.
Lemma mkunitH_g_unit: forall (g:G) (h:H),
mkunitH g h = mul (mkunitG g) (mul (mkunitH (unit G) h) (mkunitG (inv g))).
move=>g h.
apply/pair_eqP; apply/andP; split=>//=.
by apply/eqP; rewrite unitlP invrP.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
case U: (i == g).
by rewrite unitlP (eqP U) invlP eq_refl unitrP.
rewrite unitlP.
case V: (mul (inv g) i == unit G)=>//.
by rewrite -(unitrP g) -(eqP V) mulP invrP unitlP eq_refl in U.
by rewrite unitrP.
Qed.
Lemma all_maps: forall (d1 d2:eqType) (a:pred d2) f (l:seq d1),
all a (maps f l) = all (fun x=>a (f x)) l.
Proof.
move=>d1 d2 a f.
elim=>//=[x xs IH].
by rewrite IH.
Qed.
Lemma mkunitG_gen: forall (g:G) ,
{l: seq wp |
all (fun x=> gens_wp x || gens_wp (inv x)) l /\ (mkunitG g) = sum_seq l}.
Proof.
move=>g.
move:(generatorsG g)=>[gs [K1 K2]].
exists (maps mkunitG gs).
split=>/=.
rewrite all_maps.
apply/allP=>i K.
move/orP: (allP K1 i K)=>[E1|E2].
apply/orP; left.
rewrite mem_gens_wp; apply/orP; left.
by apply/hasP; exists i; rewrite ?eq_refl.
apply/orP; right.
rewrite mem_gens_wp; apply/orP; left.
by apply/hasP; exists (inv i); rewrite ?inv_mkunitG ?eq_refl.
rewrite /sum_seq foldr_maps.
rewrite /sum_seq in K2.
have UG: forall x0 l,
mkunitG (foldr (fun x y => mul x y) x0 l)
= foldr (fun x y => (mul (mkunitG x) y)) (mkunitG x0) l.
move=>x0; elim=>//=[l ls IH]; by rewrite -IH mkunitG_mul.
by rewrite {1}K2 UG mkunitG_unit.
Qed.
Lemma mkunitH_gen: forall (g:G) (h:H),
{l: seq wp |
all (fun x=> gens_wp x || gens_wp (inv x)) l /\ (mkunitH g h) = sum_seq l}.
Proof.
move=>g h.
move:(mkunitH_genH (unit G) h)=>[hs [K1 K2]].
move:(generatorsG (inv g))=>[igs [L1 L2]].
move:(generatorsG g)=>[gs [M1 M2]].
exists (cat (maps mkunitG gs) (cat (maps (mkunitH (unit G)) hs) (maps mkunitG igs))).
rewrite !all_cat !all_maps.
split=>/=.
apply/andP; split.
apply/allP=>i K.
move/orP: (allP M1 i K)=>[E1|E2].
apply/orP; left.
rewrite mem_gens_wp; apply/orP; left.
by apply/hasP; exists i; rewrite ?eq_refl.
apply/orP; right.
rewrite mem_gens_wp; apply/orP; left.
by apply/hasP; exists (inv i); rewrite ?inv_mkunitG ?eq_refl.
apply/andP; split.
apply/allP=>i K.
move/orP: (allP K1 i K)=>[E1|E2].
apply/orP; left.
rewrite mem_gens_wp; apply/orP; right.
by apply/hasP; exists i; rewrite ?eq_refl.
apply/orP; right.
rewrite mem_gens_wp; apply/orP; right.
by apply/hasP; exists (inv i); rewrite ?inv_mkunitH_unit ?eq_refl.
apply/allP=>i K.
move/orP: (allP L1 i K)=>[E1|E2].
apply/orP; left.
rewrite mem_gens_wp; apply/orP; left.
by apply/hasP; exists i; rewrite ?eq_refl.
apply/orP; right.
rewrite mem_gens_wp; apply/orP; left.
by apply/hasP; exists (inv i); rewrite ?inv_mkunitG ?eq_refl.
rewrite /sum_seq !foldr_cat !foldr_maps.
rewrite /sum_seq in K2 L2 M2.
have UG: forall x0 l,
mkunitG (foldr (fun x y => mul x y) x0 l)
= foldr (fun x y => (mul (mkunitG x) y)) (mkunitG x0) l.
move=>x0; elim=>//=[l ls IH]; by rewrite -IH mkunitG_mul.
have L2': mkunitG (inv g) = mkunitG (foldr (fun x y : G => mul x y) (unit G) igs)
by rewrite L2.
rewrite UG mkunitG_unit in L2'.
rewrite foldr_maps in K2.
rewrite -L2'.
have UH: forall x,
mul (foldr (fun x (z : wp) => mul (mkunitH (unit G) x) z) (unit wp) hs) x
= (foldr (fun (x : H) (z : wp) => mul (mkunitH (unit G) x) z) x hs).
move=>x.
clear K1 K2 L1 L2 M1 M2 L2'.
elim: hs=>/=[|h' hs IH].
by rewrite -{2}(unitlP x).
rewrite -IH.
have UH1:
mul (mul (mkunitH (unit G) h') (foldr (fun (x0 : H) z => mul (mkunitH (unit G) x0) z) (unit_wp) hs)) x
= mul (mkunitH (unit G) h') (mul (foldr (fun (x0 : H) z => mul (mkunitH (unit G) x0) z) (unit_wp) hs) x).
by rewrite mulP.
apply: UH1.
have K2':
mul (mkunitH (unit G) h) (mkunitG (inv g))
= mul (foldr (fun (x : H) (z : wp) => mul (mkunitH (unit G) x) z) (unit wp) hs) (mkunitG (inv g))
by rewrite K2.
rewrite UH in K2'.
rewrite -K2'.
have UL: forall x,
mul (mkunitG (foldr (fun x y : G => mul x y) (unit G) gs)) x
= foldr (fun x y => mul (mkunitG x) y) x gs.
move=>x.
clear K1 K2 L1 L2 M1 M2 L2'.
elim: gs=>/=[|i' gs' IH].
by rewrite mkunitG_unit -{2}(unitlP x).
rewrite -IH mkunitG_mul.
have UL':
mul (mul (mkunitG i')(mkunitG (foldr (fun x0 y : G => mul x0 y) (unit G) gs'))) x
= mul (mkunitG i')(mul (mkunitG (foldr (fun x0 y : G => mul x0 y) (unit G) gs')) x).
by rewrite mulP.
by apply: UL'.
rewrite -UL -M2.
apply: mkunitH_g_unit.
Qed.
Lemma gen_x: forall x:wp, x = mul (sum_seq (maps (fun g=>mkunitH g (x.2 g)) (enum G))) (mkunitG x.1).
Proof.
move=>[x1 x2].
have K: forall (l:seq G) (g:G),
(forall x, count (pred1 x) l <= 1) ->
(sum_seq (maps (fun g=>mkunitH g (x2 g)) l)).2 g
= if (l g) then x2 g else (unit H).
elim=>//=[g _|g ls IH i C].
by rewrite !fgraph_fun_eq /=.
rewrite !fgraph_fun_eq /=.
case U: (i == g).
rewrite /predU1 eq_sym U orTb inv_unit !unitlP.
rewrite (IH i); clear IH.
move: (C i); rewrite U;clear C=>C.
case V: (ls i).
rewrite -(has_pred1 i) in V.
rewrite has_count in V.
rewrite -add1n leq_add2l in C.
by move: (leq_trans V C).
by rewrite (eqP U) unitrP.
move=>x.
move: (C x).
case: (x == g).
rewrite -{1}add1n leq_add2l => D.
by apply: (leq_trans D _).
by rewrite add0n.
rewrite inv_unit !unitlP.
rewrite /predU1 eq_sym U orFb.
rewrite -(IH i)=>//.
move=>x.
move: (C x).
case: (x == g).
rewrite -{1}add1n leq_add2l => D.
by apply: (leq_trans D _).
by rewrite add0n.
apply/pair_eqP; apply/andP; split=>//=.
elim: (enum G)=>/=[|g gs IH].
by apply/eqP; rewrite unitlP.
by rewrite unitlP.
apply: eq_finfun=>i; rewrite !fgraph_fun_eq /=.
rewrite unitrP K.
by rewrite mem_enum.
by move=>x; rewrite FinType.enumP.
Qed.
Lemma all_flatten: forall (d:eqType) (a:pred d) l,
all a (flatten l) = all (all a) l.
Proof.
move=>d a l.
rewrite /flatten.
elim:l=>//=[x xs IH].
by rewrite -IH all_cat.
Qed.
The number of generators for the wreath product is the sum of the number
of generators of
G and H.
Lemma size_gens_wp: size gens_wp = (size gensG) + (size gensH).
Proof. by rewrite /gens_wp size_cat !size_maps. Qed.
The list
gens_wp forms a set of generators of the wreath product.
Theorem generators_wp: generators gens_wp.
Proof.
move=>x.
exists (cat (flatten (maps (fun g=>proj1_sig (mkunitH_gen g (x.2 g))) (enum G)))
(proj1_sig (mkunitG_gen x.1))).
rewrite all_cat.
split=>/=.
apply/andP; split.
rewrite all_flatten.
rewrite all_maps.
apply/allP=>g _.
move: (proj2_sig (mkunitH_gen g (x.2 g)))=>[K1 K2].
apply: K1.
move: (proj2_sig (mkunitG_gen x.1))=>[K1 K2].
apply: K1.
rewrite (@sum_seq_cat wp).
rewrite (@sum_seq_flatten wp).
rewrite -maps_comp /comp /=.
have U: (maps (fun x0 : G => sum_seq (G:=wp) (proj1_sig (mkunitH_gen x0 (x.2 x0)))) (enum G))
= maps (fun g:G => mkunitH g (x.2 g)) (enum G).
apply: eq_maps=>g.
move: (proj2_sig (mkunitH_gen g (x.2 g)))=>[K1 K2].
by rewrite -K2.
move: (proj2_sig (mkunitG_gen (x.1)))=>[_ V].
have W: (mul_wp (sum_seq
(maps
(fun x0 : G =>
sum_seq (G:=wp) (proj1_sig (mkunitH_gen x0 (x.2 x0))))
(enum G))) (sum_seq (G:=wp) (proj1_sig (mkunitG_gen x.1))))
= (mul (sum_seq (maps (fun g : G => mkunitH g (x.2 g)) (enum G))) (mkunitG x.1)).
by rewrite U -V.
rewrite -gen_x in W.
by rewrite -{1}W.
Qed.
End WreathProduct.
Opaque cyclicgroup tuplegroup.