\import Algebra.Group
\import Algebra.Group.GSet
\import Algebra.Group.Representation.Irreducible
\import Algebra.Group.Representation
\import Algebra.Group.Representation.SubLRepres
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Module.PowerLModule
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Category.Functor
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set

-- | Action given as $$g \cdot \left( \sum \lambda_i x_i \right) := \sum \lambda_{g^{ -1 }(i)}x_i $$  for a basis of $x_i$'s
\func PermRepr {R : Ring} {G : Group} (X : GSet G) : LinRepres R G \cowith
  | LModule => PowerLModule X (RingLModule R)
  | ** g f j => f (inverse g ** j)
  | **-assoc => ext \lam _ => rewrite (inv **-assoc, G.inverse_*) idp
  | **-ldistr => idp
  | **_*c => ext \lam _ => idp
  | **_ide => ext \lam _ => rewrite (G.inverse_ide, **_ide) idp

{- | Here we prove that $span(1, 1, \ldots)$ is an invariant and non-trivial subspace in $\prod_X R$ as an $R$-module.
     For this proof to work one needs to know that there are at least two points in $X$.
     Also, without some decidability constraint for X this fact will not be true
     (one cannot prove that representation of $G = \mathbb{Z}$ over $R = \mathbb{Z}$ induced by action of
     $\mathbb{Z}$ on $\mathbb{R}$ by translations is reducible. That is because one cannot construct
     a non-constant function $\mathbb{R} \to \mathbb{Z}$ in constructive mathematics).
 -}
\class PermutationRepresReducible {R : Ring} {G : Group} (X : GSet G)
  (somepoint somepoint' : X)
  (different-points : somepoint' /= somepoint)
  (decideEq-somepoint : \Pi (x : X) -> Dec (x = somepoint))
{
  \func invSubRepr : SubLRepres R G (PermRepr X) \cowith
    | contains f => ∀ {x y} (f x = f y)
    | contains_zro => idp
    | contains_+ {f} {g} fp gp {x} {y} => pmap2 (+) fp gp
    | contains_negative {f} p {x} {y} => pmap negative p
    | contains_*c {r} {f} p {x} {y} => unfold $ pmap (r *c) p
    | contains_** {e} {f} p {x} {y} => p

  \func nonConstantVector : PermRepr X
    => \lam j => \case decideEq-somepoint j \with {
      | yes e => R.ide
      | no n => R.zro
    }

  -- | We prove that $span(1,1,\ldots)$ is neither zero submodule nor does it contain the whole space.
  \lemma SubRepr-non-trivial (it : invSubRepr.IsTrivial) :  = {R}  \elim it
    | byLeft zm => inv $ path \lam i => zm (\lam _ => ) i somepoint
    | byRight cs => cases (decideEq-somepoint somepoint', decideEq-somepoint somepoint, unfold nonConstantVector in cs nonConstantVector {somepoint'} {somepoint}) \with {
        | yes p, yes _, x => absurd (different-points p)
        | yes e, no n, r => inv r
        | no n, yes e, r => r
        | no _, no q, x => absurd (q idp)
      }

  \lemma Not-Irreducible (p : IsIrreducible {R} (PermRepr X)) :  = {R} 
    => SubRepr-non-trivial (p invSubRepr)
}