blob: 2b34dca3acd792246a3843ab0c08974866988d2f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
|
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq choice fintype finfun.
From mathcomp
Require Import bigop finset ssralg fingroup zmodp matrix vector falgebra.
(*****************************************************************************)
(* * Finite Group as an algebra *)
(* (galg F gT) == the algebra generated by gT on F *)
(*****************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Reserved Notation "g %:FG"
(at level 2, left associativity, format "g %:FG").
Open Local Scope ring_scope.
Import GRing.Theory.
Section GroupAlgebraDef.
Variables (F : fieldType) (gT : finGroupType).
Inductive galg : predArgType := GAlg of {ffun gT -> F}.
Definition galg_val A := let: GAlg f := A in f.
Canonical galg_subType := Eval hnf in [newType for galg_val].
Definition galg_eqMixin := Eval hnf in [eqMixin of galg by <:].
Canonical galg_eqType := Eval hnf in EqType galg galg_eqMixin.
Definition galg_choiceMixin := [choiceMixin of galg by <:].
Canonical galg_choiceType := Eval hnf in ChoiceType galg galg_choiceMixin.
Definition fun_of_galg A (i : gT) := galg_val A i.
Coercion fun_of_galg : galg >-> Funclass.
Lemma galgE : forall f, GAlg (finfun f) =1 f.
Proof. by move=> f i; rewrite /fun_of_galg ffunE. Qed.
Definition injG (g : gT) := GAlg ([ffun k => (k == g)%:R]).
Notation Local "g %:FG" := (injG g).
Implicit Types v: galg.
Definition g0 := GAlg 0.
Definition g1 := 1%g %:FG.
Definition opprg v := GAlg (-galg_val v).
Definition addrg v1 v2 := GAlg (galg_val v1 + galg_val v2).
Definition mulvg a v := GAlg ([ffun k => a * galg_val v k]).
Definition mulrg v1 v2 :=
GAlg ([ffun g => \sum_(k : gT) (v1 k) * (v2 ((k^-1) * g)%g)]).
Lemma addrgA : associative addrg.
Proof.
by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrA.
Qed.
Lemma addrgC : commutative addrg.
Proof.
by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrC.
Qed.
Lemma addr0g : left_id g0 addrg.
Proof.
by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE add0r.
Qed.
Lemma addrNg : left_inverse g0 opprg addrg.
Proof.
by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addNr.
Qed.
(* abelian group structure *)
Definition gAlgZmodMixin := ZmodMixin addrgA addrgC addr0g addrNg.
Canonical Structure gAlgZmodType :=
Eval hnf in ZmodType galg gAlgZmodMixin.
Lemma GAlg_morph : {morph GAlg: x y / x + y}.
Proof. by move=> f1 f2; apply/eqP. Qed.
Lemma mulvgA : forall a b v, mulvg a (mulvg b v) = mulvg (a * b) v.
Proof.
by move=> *; apply: val_inj; apply/ffunP=> g; rewrite !ffunE mulrA.
Qed.
Lemma mulvg1 : forall v, mulvg 1 v = v.
Proof. by move=> v; apply: val_inj; apply/ffunP=> g; rewrite ffunE mul1r. Qed.
Lemma mulvg_addr : forall a u v, mulvg a (u + v) = (mulvg a u) + (mulvg a v).
Proof.
by move=> *; apply: val_inj; apply/ffunP=> g; rewrite !ffunE mulrDr.
Qed.
Lemma mulvg_addl : forall u a b, mulvg (a + b) u = (mulvg a u) + (mulvg b u).
Proof.
by move=> *; apply: val_inj; apply/ffunP=> g; rewrite !ffunE mulrDl.
Qed.
Definition gAlgLmodMixin := LmodMixin mulvgA mulvg1 mulvg_addr mulvg_addl.
Canonical gAlgLmodType := Eval hnf in LmodType F galg gAlgLmodMixin.
Lemma sum_fgE : forall I r (P : pred I) (E : I -> galg) i,
(\sum_(k <- r | P k) E k) i = \sum_(k <- r | P k) E k i.
Proof.
move=> I r P E i.
by apply: (big_morph (fun A : galg => A i)) => [A B|]; rewrite galgE.
Qed.
Lemma mulrgA : associative mulrg.
Proof.
move=> x y z; apply: val_inj; apply/ffunP=> g; rewrite !ffunE; symmetry.
rewrite (eq_bigr (fun k => \sum_i x i * (y (i^-1 * k)%g * z (k^-1 * g)%g)))
=> [| *]; last by rewrite galgE big_distrl; apply: eq_bigr => *; rewrite mulrA.
rewrite exchange_big /=.
transitivity (\sum_j x j * \sum_i y (j^-1 * i)%g * z (i^-1 * g)%g).
by apply: eq_bigr => i _; rewrite big_distrr /=.
apply: eq_bigr => i _; rewrite galgE (reindex (fun j => (i * j)%g)); last first.
by exists [eta mulg i^-1] => /= j _; rewrite mulgA 1?mulgV 1?mulVg mul1g.
by congr (_ * _); apply: eq_bigr => *; rewrite mulgA mulVg mul1g invMg mulgA.
Qed.
Lemma mulr1g : left_id g1 mulrg.
Proof.
move=> x; apply: val_inj; apply/ffunP=> g.
rewrite ffunE (bigD1 1%g) //= galgE eqxx invg1.
by rewrite mul1g mul1r big1 1?addr0 // => i Hi; rewrite galgE (negbTE Hi) mul0r.
Qed.
Lemma mulrg1 : right_id g1 mulrg.
Proof.
move=> x; apply: val_inj; apply/ffunP=> g.
rewrite ffunE (bigD1 g) //= galgE mulVg eqxx mulr1.
by rewrite big1 1?addr0 // => i Hi; rewrite galgE -eq_mulVg1 (negbTE Hi) mulr0.
Qed.
Lemma mulrg_addl : left_distributive mulrg addrg.
Proof.
move=> x y z; apply: val_inj; apply/ffunP=> g; rewrite !ffunE -big_split /=.
by apply: eq_bigr => i _; rewrite galgE mulrDl.
Qed.
Lemma mulrg_addr : right_distributive mulrg addrg.
Proof.
move=> x y z; apply: val_inj; apply/ffunP=> g; rewrite !ffunE -big_split /=.
by apply: eq_bigr => i _; rewrite galgE mulrDr.
Qed.
Lemma nong0g1 : g1 != 0 :> galg.
Proof.
apply/eqP; case.
move/ffunP; move/(_ 1%g); rewrite !ffunE eqxx.
by move/eqP; rewrite oner_eq0.
Qed.
Definition gAlgRingMixin :=
RingMixin mulrgA mulr1g mulrg1 mulrg_addl mulrg_addr nong0g1.
Canonical gAlgRingType := Eval hnf in RingType galg gAlgRingMixin.
Implicit Types x y : galg.
Lemma mulg_mulvl : forall a x y, a *: (x * y) = (a *: x) * y.
Proof.
move=> a x y; apply: val_inj; apply/ffunP=> g.
rewrite !ffunE big_distrr /=.
by apply: eq_bigr => i _; rewrite mulrA galgE.
Qed.
Lemma mulg_mulvr : forall a x y, a *: (x * y) = x * (a *: y).
Proof.
move=> a x y; apply: val_inj; apply/ffunP=> g.
rewrite !ffunE big_distrr /=.
by apply: eq_bigr => i _; rewrite galgE mulrCA.
Qed.
Canonical gAlgLalgType := Eval hnf in LalgType F galg mulg_mulvl.
Canonical gAlgAlgType := Eval hnf in AlgType F galg mulg_mulvr.
Lemma injGM : forall g h, (g * h)%g %:FG = (g %:FG) * (h %:FG).
Proof.
move=> g h; apply: val_inj; apply/ffunP=> k.
rewrite !ffunE (bigD1 g) //= !galgE eqxx mul1r.
rewrite big1 1?addr0 => [| i Hi]; last by rewrite !galgE (negbTE Hi) mul0r.
by rewrite -(inj_eq (mulgI (g^-1)%g)) mulgA mulVg mul1g.
Qed.
Fact gAlg_iso_vect : Vector.axiom #|gT| galg.
Proof.
exists (fun x => \row_(i < #|gT|) x (enum_val i)) => [k x y | ].
by apply/rowP=> i; rewrite !mxE !galgE !ffunE.
exists (fun x : 'rV[F]_#|gT| => GAlg ([ffun k => (x 0 (enum_rank k))])) => x.
by apply: val_inj; apply/ffunP=> i; rewrite ffunE mxE enum_rankK.
by apply/rowP=> i; rewrite // !mxE galgE enum_valK.
Qed.
Definition galg_vectMixin := VectMixin gAlg_iso_vect.
Canonical galg_vectType := VectType F galg galg_vectMixin.
Canonical galg_unitRingType := FalgUnitRingType galg.
Canonical galg_unitAlgFType := [unitAlgType F of galg].
Canonical gAlgAlgFType := [FalgType F of galg].
Variable G : {group gT}.
Definition gvspace: {vspace galg} := (\sum_(g in G) <[g%:FG]>)%VS.
Fact gspace_subproof : has_algid gvspace && (gvspace * gvspace <= gvspace)%VS.
Proof.
apply/andP; split.
apply: has_algid1.
rewrite /gvspace (bigD1 (1)%g) //=.
apply: subv_trans (addvSl _ _).
by apply/vlineP; exists 1; rewrite scale1r.
apply/prodvP=> u v Hu Hv.
case/memv_sumP: Hu => u_ Hu ->; rewrite big_distrl /=.
apply: memv_suml=> i Hi.
case/memv_sumP: Hv => v_ Hv ->; rewrite big_distrr /=.
apply: memv_suml=> j Hj.
rewrite /gvspace (bigD1 (i*j)%g) /=; last by apply: groupM.
apply: subv_trans (addvSl _ _).
case/vlineP: (Hu _ Hi)=> k ->; case/vlineP: (Hv _ Hj)=> l ->.
apply/vlineP; exists (k * l).
by rewrite -scalerAl -scalerAr scalerA injGM.
Qed.
Definition gaspace : {aspace galg} := ASpace gspace_subproof.
End GroupAlgebraDef.
Notation " g %:FG " := (injG _ g).
|
