(Joint Center)Library amodule

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype fintype finfun finset ssralg.
Require Import bigop seq tuple choice ssrnat prime ssralg fingroup pgroup.
Require Import zmodp matrix vector falgebra galgebra.

(Joint Center)Module over an algebra

amoduleType A == type for finite dimension module structure.
v :* x == right product of the module (M :* A)%VS == the smallest vector space that contains {v :* x | v \in M & x \in A} (modv M A) == M is a module for A (modf f M A) == f is a module homomorphism on M for A

Set Implicit Arguments.
Open Local Scope ring_scope.

Delimit Scope amodule_scope with aMS.

Import GRing.Theory.

Module AModuleType.
Section ClassDef.

Variable R : ringType.
Variable V: vectType R.
Variable A: FalgType R.

Structure mixin_of (V : vectType R) : Type := Mixin {
  action: A'End(V);
  action_morph: x a b, action (a × b) x = action b (action a x);
  action_linear: x , linear (action^~ x);
  action1: x , action 1 x = x

Structure class_of (V : Type) : Type := Class {
  base : Vector.class_of R V;
   mixin : mixin_of (Vector.Pack _ base V)
Local Coercion base : class_of >-> Vector.class_of.

Implicit Type phA : phant A.

Structure type phA : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.

Definition class phA (cT : type phA):=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phA T cT c of phant_id (@class phA cT) c := @Pack phA T c T.

Definition pack phA V V0 (m0 : mixin_of (@Vector.Pack R _ V V0 V)) :=
  fun bT b & phant_id (@Vector.class _ (Phant R) bT) b
  fun m & phant_id m0 mPack phA (@Class V b m) V.

Definition eqType phA cT := Equality.Pack (@class phA cT) cT.
Definition choiceType phA cT := choice.Choice.Pack (@class phA cT) cT.
Definition zmodType phA cT := GRing.Zmodule.Pack (@class phA cT) cT.
Definition lmodType phA cT := GRing.Lmodule.Pack (Phant R) (@class phA cT) cT.
Definition vectType phA cT := Vector.Pack (Phant R) (@class phA cT) cT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Vector.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.

Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion lmodType : type>-> GRing.Lmodule.type.
Canonical Structure lmodType.
Coercion vectType : type >-> Vector.type.
Canonical Structure vectType.

Notation amoduleType A := (@type _ _ (Phant A)).
Notation AModuleType A m := (@pack _ _ (Phant A) _ _ m _ _ id _ id).
Notation AModuleMixin := Mixin.

End Exports.

End AModuleType.
Import AModuleType.Exports.

Section AModuleDef.
Variables (F : fieldType) (A: FalgType F) (M: amoduleType A).

Definition rmorph (a: A) := AModuleType.action (AModuleType.class M) a.
Definition rmul (a: M) (b: A) : M := rmorph b a.
Notation "a :* b" := (rmul a b): ring_scope.

Implicit Types x y: A.
Implicit Types v w: M.
Implicit Types c: F.

Lemma rmulD x: {morph (rmul^~ x): v1 v2 / v1 + v2}.

Lemma rmul_linear_proof : v, linear (rmul v).
Canonical Structure rmul_linear v := GRing.Linear (rmul_linear_proof v).

Lemma rmulA v x y: v :* (x × y) = (v :* x) :* y.

Lemma rmulZ : c v x, (c *: v) :* x = c *: (v :* x).

Lemma rmul0 : left_zero 0 rmul.

Lemma rmul1 : v , v :* 1 = v.

Lemma rmul_sum : I r P (f : IM) x,
  \sum_(i <- r | P i) f i :* x = (\sum_(i <- r | P i) f i) :* x.

Implicit Types vs: {vspace M}.
Implicit Types ws: {vspace A}.

Lemma size_eprodv : vs ws,
  size (allpairs rmul (vbasis vs) (vbasis ws)) == (\dim vs × \dim ws)%N.

Definition eprodv vs ws := span (Tuple (size_eprodv vs ws)).
Local Notation "A :* B" := (eprodv A B) : vspace_scope.

Lemma memv_eprod vs ws a b : a \in vsb \in wsa :* b \in (vs :* ws)%VS.

Lemma eprodvP : vs1 ws vs2,
  reflect ( a b, a \in vs1b \in wsa :* b \in vs2)
          (vs1 :* ws vs2)%VS.

Lemma eprod0v: left_zero 0%VS eprodv.

Lemma eprodv0 : vs, (vs :* 0 = 0)%VS.

Lemma eprodv1 : vs, (vs :* 1 = vs)%VS.

Lemma eprodvSl ws vs1 vs2 : (vs1 vs2vs1 :* ws vs2 :* ws)%VS.

Lemma eprodvSr vs ws1 ws2 : (ws1 ws2vs :* ws1 vs :* ws2)%VS.

Lemma eprodv_addl: left_distributive eprodv addv.

Lemma eprodv_sumr vs ws1 ws2 : (vs :* (ws1 + ws2) = vs :* ws1 + vs :* ws2)%VS.

Definition modv (vs: {vspace M}) (al: {aspace A}) :=
   (vs :* al vs)%VS.

Lemma mod0v : al, modv 0 al.

Lemma modv1 : vs, modv vs (aspace1 A).

Lemma modfv : al, modv fullv al.

Lemma memv_mod_mul : ms al m a,
  modv ms alm \in msa \in alm :* a \in ms.

Lemma modvD : ms1 ms2 al ,
  modv ms1 almodv ms2 almodv (ms1 + ms2) al.

Lemma modv_cap : ms1 ms2 al ,
  modv ms1 almodv ms2 almodv (ms1:&: ms2) al.

Definition irreducible ms al :=
  [/\ modv ms al, ms != 0%VS &
     ms1, modv ms1 al → (ms1 ms)%VSms != 0%VSms1 = ms].

Definition completely_reducible ms al :=
   ms1, modv ms1 al → (ms1 ms)%VS
    [/\ modv ms2 al, (ms1 :&: ms2 = 0)%VS & (ms1 + ms2)%VS = ms].

Lemma completely_reducible0 : al, completely_reducible 0 al.

End AModuleDef.

Notation "a :* b" := (rmul a b): ring_scope.
Notation "A :* B" := (eprodv A B) : vspace_scope.

Section HomMorphism.

Variable (K: fieldType) (A: FalgType K) (M1 M2: amoduleType A).

Implicit Types ms : {vspace M1}.
Implicit Types f : 'Hom(M1, M2).
Implicit Types al : {aspace A}.

Definition modf f ms al :=
       all (fun pf (p.1 :* p.2) == f p.1 :* p.2)
               (allpairs (fun x y(x,y)) (vbasis ms) (vbasis al)).

Lemma modfP : f ms al,
  reflect ( x v, v \in msx \in alf (v :* x) = f v :* x)
          (modf f ms al).

Lemma modf_zero : ms al, modf 0 ms al.

Lemma modf_add : f1 f2 ms al,
  modf f1 ms almodf f2 ms almodf (f1 + f2) ms al.

Lemma modf_scale : k f ms al, modf f ms almodf (k *: f) ms al.

Lemma modv_ker : f ms al,
  modv ms almodf f ms almodv (ms :&: lker f) al.

Lemma modv_img : f ms al,
  modv ms almodf f ms almodv (f @: ms) al.

End HomMorphism.

Section ModuleRepresentation.

Variable (F: fieldType) (gT: finGroupType)
         (G: {group gT}) (M: amoduleType (galg F gT)).
Hypothesis CG: ([char F]^'.-group G)%g.
Implicit Types ms : {vspace M}.

Let FG := gaspace F G.
Local Notation " g %:FG " := (injG _ g).

Lemma Maschke : ms, modv ms FGcompletely_reducible ms FG.

End ModuleRepresentation.

Export AModuleType.Exports.