diff options
Diffstat (limited to 'mathcomp/attic/galgebra.v')
| -rw-r--r-- | mathcomp/attic/galgebra.v | 227 |
1 files changed, 227 insertions, 0 deletions
diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v new file mode 100644 index 0000000..411fb6a --- /dev/null +++ b/mathcomp/attic/galgebra.v @@ -0,0 +1,227 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun. +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 exact: 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). |