\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Sub
\import Algebra.Pointed
\import Data.Bool
\import Equiv
\import Function
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Order.PartialOrder
\import Set
\import Set.Category
\open Group


\class SubGroup \extends SubMonoid {
  \override S : Group
  | contains_inverse {x : S} : contains x -> contains (inverse x)

  \func struct : Group \cowith
    | Monoid => SubMonoid.struct
    | inverse x => (inverse x., contains_inverse x.)
    | inverse-left => ext inverse-left
    | inverse-right => ext inverse-right

  \func equivalence : Equivalence S \cowith
    | ~ x y => contains (inverse x * y)
    | ~-reflexive => transportInv contains inverse-left contains_ide
    | ~-symmetric c => transport contains (inverse_* *> pmap (_ *) inverse-isInv) (contains_inverse c)
    | ~-transitive {x} {y} c1 c2 => rewriteEq (inverse-right {S} {y}, ide-left) in contains_* c1 c2

  \func Cosets => Quotient (equivalence.~)

  \lemma contains->equiv {x : S} (p : contains x) :  equivalence.~ x =>
    transport (\lam x => contains x) (x ==< inv ide-left >== ide * x ==< pmap (\lam z => z * x) (inv inverse_ide)) p

  \lemma equiv->contains {x : S}(p :  equivalence.~ x) : contains x =>
    transport contains helper p
    \where
      \func helper {x : S} : inverse ide * x = x
        => inverse ide * x ==<  pmap (\lam z => z * x) inverse_ide >==
            ide * x        ==<  ide-left >==
            x `qed

  \lemma invariant-right-multiplication {x y : S} (p :  equivalence.~ y)
    : in~{S} {equivalence.~} x = in~ {S} {equivalence.~} (x * y)
    => ~-pequiv (transport contains *-assoc contains-x^-1*x*y)
    \where{
      \func helper : inverse x * x * y = y =>
        inverse x * x * y  ==< pmap (\lam z => z * y) inverse-left >==
        ide * y ==< ide-left >==
        y `qed

      \func contains-x^-1*x*y : contains (inverse x * x * y) => transport contains (inv helper) (equiv->contains p)
    }

  \lemma equivalence-to-1 {x y : S} (p : x equivalence.~ y) :  equivalence.~ inverse x * y =>
    contains->equiv p
--  \lemma equivalence-reverse {x y : S} (p : 1 equivalence.~ inverse x * y) : x equivalence.~ y

} \where {
  \func cStruct {G : CGroup} (S : SubGroup G) : CGroup \cowith
    | Group => S.struct
    | *-comm => ext *-comm
}

\class DecSubGroup \extends SubGroup, DecSubMonoid {
  \override S : Group
}

\func anotherSubgroupDefinition{G : Group} (X : SubSet G)
                               (p : \Pi (x y : G) -> X.contains x -> X.contains y -> X.contains (inverse x * y))
                               (q : X.contains ide) : SubGroup G {| contains => X.contains | contains_ide => q} \cowith
  | contains_* {x y : G} (r : X.contains x) (r' : X.contains y) : X.contains (x * y) => transport (\lam z => X.contains (z * y)) G.inverse-isInv (contains_*' r r')
  | contains_inverse {g : G} (xi : X.contains g) : X.contains (inverse g) => inv g xi
  \where {
    \func helper (g : G) (r : X.contains g) : X.contains (inverse g * G.ide) => p g ide r q

    \func inv (g : G) (r : X.contains g) : X.contains (inverse g) => transport X.contains G.ide-right (helper g r)

    \func contains_*' {x y : G} (r : X.contains x) (r' : X.contains y) : X.contains (inverse (inverse x) * y) => p (inverse x) y (inv x r) r'
  }



\instance SubGroupPreorder {G : Group} : Preorder (SubGroup G)
  | <= (H K : SubGroup G) => \Pi (g : G) -> H.contains g -> K.contains g
  | <=-refl {H : SubGroup G} => \lam (g : G) (p : H.contains g) => p
  | <=-transitive {H K N : SubGroup G}
                  (p : \Pi (g : G) -> H.contains g -> K.contains g)
                  (q : \Pi (g : G) -> K.contains g -> N.contains g)
  => \lam (g : G) (r : H.contains g) => q g (p g r)

\func kernelEquivProp {G : Group} (N : NormalSubGroup G) (a : G) (p : N.contains a) : N.quotient.ide = in~ a =>
  N.quotient.ide ==< idp >==
  in~ ide ==< inv (~-pequiv help-condition) >==
  in~ a `qed
  \where
    \func help-condition : a N.equivalence.~  => N.equivalence.~-symmetric {} {a} (N.contains->equiv p)

\class NormalSubGroup \extends SubGroup {
  | isNormal (g : S) {h : S} : contains h -> contains (conjugate g h)

  \lemma isNormal' (g : S) {h : S} (c : contains h) : contains ((inverse g) * h * g)
    => simplify in isNormal (inverse g) c

  \func quotient : Group Cosets \cowith
    | ide => in~ 
    | * (x y : Cosets) : Cosets \with {
      | in~ g, in~ g' => in~ (g Group.* g')
      | in~ g, ~-equiv x y r =>  ~-pequiv $ rewriteEq (inverse_*, inverse-left {S} {g}, ide-left) r
      | ~-equiv x y r, in~ g =>  ~-pequiv $ rewriteEq inverse_* $ transport contains equation (isNormal' g r)
    }
    | ide-left {x} => cases x \with {
      | in~ a => pmap in~ ide-left
    }
    | ide-right {x} => cases x \with {
      | in~ a => pmap in~ ide-right
    }
    | *-assoc {x} {y} {z} => cases (x,y,z) \with {
      | in~ x, in~ y, in~ z => pmap in~ *-assoc
    }
    | inverse (x : Cosets) : Cosets \with {
      | in~ g => in~ (Group.inverse g)
      | ~-equiv x y r => ~-pequiv $ rewrite inverse-isInv $ rewriteEq (inverse_*, inverse-isInv) in
                                    contains_inverse (rewriteEq (inverse-right {S} {x}, ide-left) in isNormal x r)
    }
    | inverse-left {x} => cases x \with {
      | in~ a => pmap in~ inverse-left
    }
    | inverse-right {x} => cases x \with {
      | in~ a => pmap in~ inverse-right
    }

  \func quotient-proj-setwise : SetHom S quotient \cowith
    | func s => in~ s

  \func criterionForKernel (a : S) (p : contains a) : quotient.ide = in~ a => rewrite (inv (~-pequiv help-condition)) idp
    \where
      \func help-condition : a equivalence.~  => equivalence.~-symmetric {} {a} (contains->equiv p)

  {- | probably it can be re-done with Quotient.in-surj function -}
  \func quotIsSurj : isSurj quotient-proj-setwise =>
    \lam (z : quotient) => \case \elim z \with{
      | in~ a => inP (a, quotient-proj-setwise a ==< idp >== in~ a `qed)
    }
}

\class SubAddGroup \extends SubAddMonoid {
  \override S : AddGroup
  | contains_negative {x : S} : contains x -> contains (negative x)

  \lemma contains_- {x y : S} : contains x -> contains y -> contains (x - y)
    => \lam cx cy => contains_+ cx (contains_negative cy)

  \func struct : AddGroup \cowith
    | AddMonoid => SubAddMonoid.struct
    | negative x => (negative x., contains_negative x.)
    | negative-left => ext negative-left
    | negative-right => ext negative-right
} \where {
  \func abStruct {A : AbGroup} (S : SubAddGroup A) : AbGroup \cowith
    | AddGroup => S.struct
    | +-comm => ext +-comm

  \func max {A : AddGroup} : SubAddGroup \cowith
    | SubAddMonoid => SubAddMonoid.max {A}
    | contains_negative _ => ()
}

\class FinSubGroup \extends DecSubGroup {
  \override S : FinGroup

  \func struct : FinGroup \cowith
    | Group => SubGroup.struct
    | FinSet => DecSubSet.isFin S \this
}