\import Algebra.Group
\import Algebra.Group.Sub
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Sub
\import Algebra.Pointed
\import Equiv
\import Function
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Algebra.Monoid
\import Set.Category

\class GroupAction (G : Group) \extends BaseSet {
  | \infixl  ** : G -> E -> E -- priority should be bigger than that of "+" in LModule (=7)
  | **-assoc {m n : G} {e : E} : m ** (n ** e) = (m * n) ** e
  | id-action {e : E} : ide ** e = e

  \func Stabilizer (s : E) : SubGroup G \cowith
    | contains m => m ** s = s
    | contains_* {m n : G} (p : m ** s = s) (q : n ** s = s)  =>
      (m * n) ** s  ==< inv **-assoc >==
      m ** (n ** s) ==< pmap (\lam x => m ** x) q >==
      m ** s  ==< p >==
      s `qed

    | contains_ide => id-action

    | contains_inverse {m : G} (p : m ** s = s) =>
      inverse m ** s ==< pmap (\lam x => inverse m ** x) (inv p) >==
      inverse m ** (m ** s) ==< **-assoc >==
      (inverse m * m) ** s ==< pmap (\lam x => x ** s) inverse-left >==
      ide ** s ==< id-action >==
      s `qed

  \func choosePoint (e : E) => ActionBySubgroup (Stabilizer e)
}

\class TransitiveGroupAction \extends GroupAction {
  | trans : \Pi (v v' : E) -> ∃ (g : G) (g ** v = v')
}
\func ActionBySubgroup {G : Group} (H : SubGroup G) : GroupAction G \cowith
  | E => H.Cosets
  | ** (g : G) (e : H.Cosets) : H.Cosets \with {
    | g, in~ a => in~ (g * a)
    | g, ~-equiv x y r => in~ (g * x) ==< H.invariant-right-multiplication (H.equivalence-to-1 r) >==
    in~ (g * x * (inverse x * y)) ==< pmap in~ (trivialRelation g x y ) >== in~ (g * y) `qed
    }
  | **-assoc {m n : G} {e : H.Cosets} : m ** (n ** e) = (m * n) ** e => \case \elim e \with{
    | in~ a =>  m ** (n ** in~ a) ==< pmap (m **) {n ** in~ a} {in~ (n * a)} idp >==
    m ** in~ (n * a) ==< idp >==
    in~ (m * (n * a)) ==< pmap in~ (inv *-assoc) >==
    in~ ((m * n) * a) ==< idp >==
    (m * n) ** in~ a `qed
  }
  | id-action {e : H.Cosets} : ide ** e = e => \case \elim e \with{
    | in~ a => ide ** in~ a ==< idp >==
    in~ (ide * a) ==< pmap in~ ide-left >==
    in~ a `qed
  }
  \where \func trivialRelation (g x y : G) : g * x * (inverse x * y) = g * y =>
    g * x * (inverse x * y)   ==< *-assoc >==
    g * (x * (inverse x * y)) ==< pmap (g *) (inv *-assoc) >==
    g * ((x * inverse x) * y) ==< pmap (\lam z => g *( z * y)) inverse-right >==
    g * (ide * y)             ==< pmap (g *) ide-left >==
    g * y `qed


\instance TransitiveActionBySubgroup {G : Group} (H : SubGroup G) : TransitiveGroupAction G
   | GroupAction => ActionBySubgroup H
   | trans (v v' : H.Cosets) : ∃ (g : G) (g ActionBySubgroup.** v = v') => \case \elim v, \elim v'\with{
      | in~ a, in~ a1 => inP(a1 * inverse a ,
                              in~ (a1 * inverse a * a) ==< pmap in~ *-assoc >==
                              in~ (a1 * (inverse a * a)) ==< pmap (\lam z => in~ (a1 * z)) inverse-left >==
                              in~ (a1 * ide) ==< pmap in~ ide-right >==
                              in~ a1 `qed
                           )
   }

-- action by conjugating its own elements
\func conjAction (G : Group) : GroupAction G \cowith
  | E => G
  | ** (g : G)  => conjugate g
  | **-assoc {m : G} {n : G} {e : G} : conjugate m (conjugate n e) = conjugate (m * n) e =>
  conjugate m (conjugate n e) ==< pmap (conjugate m) idp >==
  conjugate m (n * e * inverse n ) ==< idp >==
  m * (n * e * inverse n ) * inverse m ==< lemma-par >==
  (m * n) * e * (inverse n * inverse m) ==< pmap ((m * n * e) *) (inv G.inverse_*) >==
  (m * n) * e * (inverse (m * n)) ==< idp >==
  conjugate (m * n) e `qed
  | id-action {e : G} : conjugate ide e = e => conjugate-via-id e
  \where \lemma lemma-par {a b c d e : G} : a * (b * c * d) * e = (a * b) * c * (d * e) => equation