\import Algebra.Group
\import Algebra.Group.GSet
\import Algebra.Group.Representation
\import Algebra.Group.Representation.InterwiningMap
\import Algebra.Group.Representation.LinRepresCat
\import Algebra.Group.Representation.SubLRepres
\import Algebra.Module
\import Algebra.Module.Instances
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Ring
\import Category
\import Data.Array
\import Equiv
\import Function \hiding (id, o)
\import Function.Meta
\import Logic
\import Meta \hiding (in)
\import Paths
\import Paths.Meta
\import Set.Fin

\class MaschkeLemma {R : CRing} {G : FinGroup} (cardInv : Monoid.Inv (R.natCoef G.card)) {E : LinRepres R G} {S : SubLRepres R G E} {
  \func mean_func {E W : LinRepres R G} (f : LinearMap E W) : InterwiningMap E W
    => cardInv.inv *c SumOverGroup f

  -- | If the subrepresentation splits as a submodule, then it splits as a subrepresentation.
  \lemma mean-func-preserve {f : LinearMap E (ILinRepres S)} (p : \Pi (s : ILinRepres S) -> f s. = s) (t : ILinRepres S)
    : mean_func f t. = t
    => pmap (_ *c) SumOverGroup-multiply *> inv *c-assoc *> pmap (*c _) (*-comm *> cardInv.inv-right) *> ide_*c
    \where {
      \func SumOverGroup-multiply : SumOverGroup f t. = R.natCoef G.card *c t
        => SumOverGroup_same-elements *> SumOverGroup.FinSumEqual-multiply t

      \lemma SumOverGroup_Sub : SumOverGroup f t. = AbMonoid.FinSum (\lam g => g ** f (inverse g ** t.))
        => SumOverGroup.FinSumRewrite (\lam g => SumOverGroup.adjust g f) t.

      \lemma SumOverGroup_same-elements : SumOverGroup f t. = AbMonoid.FinSum (\lam (_ : G) => t)
        => SumOverGroup_Sub *> AbMonoid.FinSum-ext (\lam g => SumOverGroup_subrepr-property g t)

      \lemma SumOverGroup_subrepr-property (g : G) (t : ILinRepres S) : g ** f (inverse g ** t.) = t
        => pmap (g **) (p (inverse g ** t)) *> inv **-assoc *> pmap (** t) inverse-right *> **_ide
    }
}

{- | It is a function that given a linear map $f : A \to B$ between two representations of a finite group $G$
produces an interwining linear map $f'$ via the following formula
 $f' a := \sum_{g : G} g f (g^{ -1} a)$
 -}
\func SumOverGroup {R : CRing} {G : FinGroup} {A B : LinRepres R G} (f : LinearMap A B) : InterwiningMap A B \cowith
  | LinearMap => int
  | func-** {a} {h} => rewrite (bring_h_out h a, inv $ ap-rearrange h a) idp
  \where {
    \func Ab : AbGroup
      => LinearMapAbGroup A B

    \func adjust (g : G) (f : LinearMap A B) : LinearMap A B \cowith
      | func a => g B.** f (inverse g A.** a)
      | func-+ => rewrite (A.**-ldistr, f.func-+, B.**-ldistr) idp
      | func-*c => rewrite (A.**_*c, f.func-*c, B.**_*c) idp

    \func int : LinearMap A B
      => Ab.FinSum (\lam (g : G) => adjust g f)

    \func group_prop (g h : G)(a : A) : adjust g f (h A.** a) = h B.** adjust (inverse h * g) f a
      => unfold (inv (rewrite (inv B.**-assoc, inv G.*-assoc, G.inverse-right, G.ide-left, G.inverse_*, G.inverse-isInv, A.**-assoc) idp))

    \func FinSum-equivariance (h : G) {x : G -> B} : h B.** B.FinSum x = B.FinSum (\lam z => h B.** x z)
      => \case B.FinSum_char x  \with {
        | inP p => rewrite (p., B.FinSum_char2 p., BigSum-equivariance) idp
      }
      \where {
        \func act_array (h : G)(e : Array B) : Array B => \lam i => h B.** e i

        \func BigSum-equivariance (e : Array B) : h B.** B.BigSum e = B.BigSum (act_array h e) \elim e
          | nil => rewrite B.**_zro idp
          | a :: l => rewrite (B.**-ldistr, BigSum-equivariance l) idp
      }

    \func FinSumRewrite (x : G -> Ab) (a : A)
      : (Ab.FinSum x) a = B.FinSum (\lam e => (x e) a)
      => \case Ab.FinSum_char x \with {
        | inP a1 => rewrite (a1., B.FinSum_char2 a1., BigSumRewrite) idp
      }
      \where {
        \func Ab_Helper {f g : Ab}{x : A} : (f + g) x = f x + g x => idp

        \func ap_BigSum_el_wise (e : Array Ab)(a : A) : Array B => \lam i => (e i) a

        \func BigSumRewrite (e : Array Ab)(a : A) : (Ab.BigSum e) a = B.BigSum (ap_BigSum_el_wise e a) \elim e
          | nil => idp
          | a1 :: l => rewrite (Ab_Helper, BigSumRewrite l a) idp
      }

    \lemma PermutationInvariance {E : AbMonoid}{A : FinSet}
                                 (x : A -> E)(p : A -> A)(permute : QEquiv p): E.FinSum x  = E.FinSum {A} (x Function.o p)
      => E.FinSum_Equiv {A}{A} permute

    \lemma rearrange (h : G) : int = Ab.FinSum (\lam (g : G) => adjust (inverse h * g) f)
      => PermutationInvariance (adjust __ f) (inverse h *) (Group.translate-is-Equiv (inverse h))

    \lemma ap-rearrange (h : G) (a : A)
      : int a = Ab.FinSum (\lam g => adjust (inverse h * g) f) a
      => path \lam i => rearrange h i a

    \func bring_h_out (h : G) (a : A)
      : int (h A.** a) = h B.** (Ab.FinSum (\lam g => adjust (inverse h * g) f)) a
      => inv $ rewrite (zero-2-step h a, FinSum-equivariance, step-4 h a, inv $ FinSumRewrite (adjust __ f) (h A.** a)) idp
      \where {
        \lemma zero-2-step (h : G)(a : A)
          : Ab.FinSum (\lam g => adjust (G.inverse h G.* g) f) a = B.FinSum (\lam g => adjust (G.inverse h G.* g) f a)
          => FinSumRewrite (\lam g => adjust (G.inverse h G.* g) f) a

        \lemma step-4 (h : G) (a : A)
          : B.FinSum (\lam g => h B.** adjust (inverse h * g) f a) =
            B.FinSum (\lam g => g B.** f (inverse g A.** (h A.** a)))
          => rewrite (AbMonoid.FinSum-ext helper) idp
          \where {
            \func helper {h : G}{a : A}(g : G) : h B.** adjust (inverse h * g) f a = g B.** f (inverse g A.** (h A.** a))
              => unfold $ rewrite (G.inverse_*, G.inverse-isInv, A.**-assoc, inv B.**-assoc, inv G.*-assoc, G.inverse-right, G.ide-left) idp
          }

      }
    \func FinSumEqual-multiply {E : LModule R} {A : FinSet} (e : E) : E.FinSum (\lam (_ : A) => e) = R.natCoef A.card *c e =>
      \case E.FinSum_char (\lam (_ : A) => e) \with {
        | inP a => rewrite (a., BigSumEqual A.card) idp
      }
      \where {
        \func BigSumEqual (n : Nat) : AddMonoid.BigSum (\new Array E n (\lam _ => e)) = R.natCoef n *c e \elim n
          |  => rewrite (R.natCoefZero, E.*c_zro-left) idp
          | suc n => rewrite (R.natCoefSuc n, E.*c-rdistr, inv $ BigSumEqual n, E.ide_*c, E.+-comm) idp
      }
  }