(Joint Center)Library galgebra

(* (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.

(Joint Center)Finite Group as an algebra

(galg F gT) == the algebra generated by gT on F

Set Implicit Arguments.

Reserved Notation "g %:FG"
  (at level 2, F at level 1, 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 gTF}.

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 : f, GAlg (finfun f) =1 f.

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.
Lemma addrgC : commutative addrg.
Lemma addr0g : left_id g0 addrg.
Lemma addrNg : left_inverse g0 opprg addrg.

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}.

Lemma mulvgA : a b v, mulvg a (mulvg b v) = mulvg (a × b) v.

Lemma mulvg1 : v, mulvg 1 v = v.

Lemma mulvg_addr : a u v, mulvg a (u + v) = (mulvg a u) + (mulvg a v).

Lemma mulvg_addl : u a b, mulvg (a + b) u = (mulvg a u) + (mulvg b u).

Definition gAlgLmodMixin := LmodMixin mulvgA mulvg1 mulvg_addr mulvg_addl.
Canonical gAlgLmodType := Eval hnf in LmodType F galg gAlgLmodMixin.

Lemma sum_fgE : I r (P : pred I) (E : Igalg) i,
  (\sum_(k <- r | P k) E k) i = \sum_(k <- r | P k) E k i.

Lemma mulrgA : associative mulrg.

Lemma mulr1g : left_id g1 mulrg.

Lemma mulrg1 : right_id g1 mulrg.

Lemma mulrg_addl : left_distributive mulrg addrg.

Lemma mulrg_addr : right_distributive mulrg addrg.

Lemma nong0g1 : g1 != 0 :> galg.

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 : a x y, a *: (x × y) = (a *: x) × y.

Lemma mulg_mulvr : a x y, a *: (x × y) = x × (a *: y).

Canonical gAlgLalgType := Eval hnf in LalgType F galg mulg_mulvl.
Canonical gAlgAlgType := Eval hnf in AlgType F galg mulg_mulvr.

Lemma injGM : g h, (g × h)%g %:FG = (g %:FG) × (h %:FG).

Fact gAlg_iso_vect : Vector.axiom #|gT| galg.

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.

Definition gaspace : {aspace galg} := ASpace gspace_subproof.

End GroupAlgebraDef.

Notation " g %:FG " := (injG _ g).