\import Algebra.Algebra
\import Algebra.Group.Category
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Monoid.PermSet
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Category
\import Algebra.Ring.RingHom
\import Algebra.Ring.MonoidRing
\import Algebra.Ring.Poly
\import Algebra.Semiring
\import Arith.Nat
\import Category
\import Data.Array
\import Data.Fin \hiding (Index)
\import Equiv
\import Function (isSurj)
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.LinearOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Set.Fin
\open MonoidSet \hiding (~)
\open Monoid(pow)

\func MPoly (J : \Set) (R : CRing) => MonoidAlgebra (PermSetMonoid J) R

\func mPolyHom {J : \Set} {R : CRing} : RingHom R (MPoly J R)
  => monoidRingHom

\func mPoly-map {J : \Set} {R S : CRing} (f : AddMonoidHom R S) (p : MPoly J R) : MPoly J S
  => monoidSet-map (\lam x => x) f p

\lemma mPoly-map-comp {J : \Set} {R E S : CRing} {f : AddMonoidHom R E} {g : AddMonoidHom E S} {p : MPoly J R}
  : mPoly-map (g AddMonoidCat.∘ f) p = mPoly-map g (mPoly-map f p) \elim p
  | in~ l => idp

\func mPoly-mapHom {J : \Set} {R S : CRing} (f : RingHom R S) : RingHom (MPoly J R) (MPoly J S) (mPoly-map f)
  => monoidSet-ringHom (MonoidCat.id _) f

\lemma mPoly-map_permSet-univ {I J : \Set} {R S : CRing} (f : RingHom R S) (g : I -> MPoly J R) {a : PermSet I}
  : mPoly-map f (permSet-univ {I} {MPoly J R} g a) = permSet-univ {I} {MPoly J S} (\lam i => mPoly-map f (g i)) a \elim a
  | in~ a => MonoidHom.func-BigProd {mPoly-mapHom f}

\func mPolyEval {J : \Set} {R : CRing} (f : J -> R) : RingHom (MPoly J R) R
  => evalMSRingHom (permSet-univ {J} {R} f)

\func mPolyMapEval {J : \Set} {R S : CRing} (f : AddMonoidHom R S) (p : MPoly J R) (a : J -> S) : S
  => mPolyEval a (mPoly-map f p)

\func mPolyMapEvalRingHom {J : \Set} {R S : CRing} (f : RingHom R S) (a : J -> S) : RingHom (MPoly J R) S
  => mPolyEval a RingCat.∘ mPoly-mapHom f

\func mVar {J : \Set} {R : CRing} (j : J) : MPoly J R
  => msMonomial  $ PermSet.inPS (j :: nil)

\lemma mVar_pow {J : \Set} {R : CRing} {j : J} {n : Nat} : pow (mVar j) n = msMonomial R.ide (pow (PermSet.inPS (j :: nil)) n)
  => msMonomial_pow *> pmap (msMonomial __ _) R.pow_ide

\func mConst {J : \Set} {R : CRing} (a : R) : MPoly J R
  => msMonomial a ide

\lemma msCoef_mVar=0 {J : DecSet} {R : CRing} {j : J} {n m : Nat} {p : MPoly J R} (q : n < m) : msCoef (pow (mVar j) m * p) (pow (PermSet.inPS (j :: nil)) n) =  \elim p
  | in~ l => rewrite mVar_pow $ pmap {Array (\Sigma R (PermSet J))} (\lam l => R.BigSum (map __. l)) {_} {nil} $ later $ rewrite ++_nil $
      keep-none \lam k => unfold MonoidSemiring.func $ cases (l k). \with {
        | in~ l => rewrite (permSet-pow,permSet-pow) \case PermSet.unext __ \with {
          | inP e => linarith (EPerm.EPerm_len e *> len_++)
        }
      }

\lemma msCoef_mMap {J : DecSet} {R E : CRing} {g : AddMonoidHom R E} {p : MPoly J R} {m : PermSet J} : msCoef (mPoly-map g p) m = g (msCoef p m)
  => msCoef_map (\lam p => p)

\lemma mPolyMapEval-var {J : \Set} {R S : CRing} (f : RingHom R S) (a : J -> S) (j : J) : mPolyMapEvalRingHom f a (mVar j) = a j
  => simplify $ pmap (`* _) f.func-ide *> ide-left

\lemma mPolyRingHom-unique {J : \Set} {R S : CRing} (f g : RingHom (MPoly J R) S) (p : \Pi (r : R) -> f (mConst r) = g (mConst r)) (q : \Pi (j : J) -> f (mVar j) = g (mVar j)) (x : MPoly J R) : f x = g x
  => monoidRingHom-unique p (\case \elim __ \with {
       | in~ l => pmap (\lam x => f (msMonomial  x)) (inv permSet-split) *> pmap f (inv msMonomial_BigProd_ide) *> f.func-BigProd {\lam j => msMonomial  (PermSet.inPS (l j :: nil))} *> pmap Monoid.BigProd (exts \lam j => q (l j)) *> inv (g.func-BigProd {\lam j => msMonomial  (PermSet.inPS (l j :: nil))}) *> pmap g (later idp *> msMonomial_BigProd_ide) *> pmap (\lam x => g (msMonomial  x)) permSet-split
     }) x

\func mLastCoef {J : \Set} {R : CRing} (p : MPoly J R) => monoidSet-coefs permSet-zro-dec p

\func MPoly_Empty {J : \Set} {R : CRing} (e : J -> Empty) : QEquiv {MPoly J R} {R} mLastCoef \cowith
  | ret a => in~ $ (a, in~ nil) :: nil
  | ret_f => \case \elim __ \with {
    | in~ l =>
      \have t j : (l j). =  => cases (l j). \with {
        | in~ nil => idp
        | in~ (j :: _) => absurd (e j)
      }
      \in unfold mLastCoef $ rewrite (keep-all t) $ inv $ fromClosure $ unique-sum (PermSet.inPS nil) t
  }
  | f_sec a => zro-right

\func MPoly_Fin-suc {n : Nat} {R : CRing} : QEquiv {MPoly (Fin (suc n)) R} {Poly (MPoly (Fin n) R)} \cowith
  | f (p : MPoly (Fin (suc n)) R) : Poly (MPoly (Fin n) R) \with {
    | in~ l => AddMonoid.BigSum (map m-func l)
    | ~-equiv l l' r => m-func-coh r
  }
  | ret (p : Poly (MPoly (Fin n) R)) : MPoly (Fin (suc n)) R \with {
    | pzero => 
    | padd p e => ret p * mVar fzero + monoidSet-map (permSet-map fsuc) (id R) e
    | peq => zro-right *> Ring.zro_*-left {MPoly (Fin (suc n)) R} {mVar fzero}
  }
  | ret_f => \case \elim __ \with {
    | in~ l => retHom.func-BigSum *> pmap AddMonoid.BigSum (exts \lam j => unfold $ unfold m-func $ cases (l j). \with {
      | in~ l' => ret-aux *> pmap (_ *) retHom.func-BigProd *>
                             later (pmap (_ *) {_} {msMonomial R.ide (PermSet.inPS l')} $ pmap Monoid.BigProd (exts \lam j => cases (l' j) \with {
                               |  => pmap (\lam x => inMS x) $ unfold MonoidSemiring.func $ rewrite ide-left idp
                               | suc j =>
                                 \let v => inMS ((R.ide, permSet-map fsuc (PermSet.inPS (j :: nil))) :: nil)
                                 \in unfold $ pmap (`+ v) (Ring.zro_*-left {_} {mVar fzero}) *> zro-left {_} {v}
                             }) *> msMonomial_BigProd_ide *> pmap (msMonomial _) permSet-split)
                               *> msMonomial-split
    }) *> msMonomial_BigSum-split
  }
  | f_sec (p : Poly (MPoly (Fin n) R)) : f (ret p) = p \with {
    | pzero => idp
    | padd p e => fHom.func-+ *> pmap (`+ _) (fHom.func-* *> pmap (`* _) (f_sec p)) *>
                  pmap2 (\lam x y => p * padd (padd  (inMS ((x,ide) :: nil)))  + y) (ide-left *> ide-left) (later \case \elim e \with {
                    | in~ l => pmap AddMonoid.BigSum (exts \lam j => cases (l j). \with {
                      | in~ l' => inv (pmap (_ *c) (polyHom.func-BigProd {map mVar l'})) *> pmap (padd pzero) (pmap (_ *) msMonomial_BigProd_ide *> pmap2 (\lam x y => inMS ((x,y) :: nil)) ide-right (ide-left *> permSet-split))
                    }) *> inv polyHom.func-BigSum *> pmap (padd pzero) msMonomial_BigSum-split
                  }) *> inv padd-expand
  }
  \where {
    \open MonoidSet

    \func var-func (j : Fin (suc n)) : Poly (MPoly (Fin n) R)
      |  => padd  
      | suc j => padd  (mVar j)

    \func f-monomial (x : PermSet (Fin (suc n))) : Poly (MPoly (Fin n) R)
      | in~ l => Monoid.BigProd (map var-func l)
      | ~-equiv l l' r => CMonoid.BigProd_EPerm (EPerm.EPerm_map var-func r)

    \lemma f-monomial_+ {x y : PermSet (Fin (suc n))} : f-monomial (x * y) = f-monomial x * f-monomial y \elim x, y
      | in~ l, in~ l' => pmap Monoid.BigProd (map_++ var-func) *> Monoid.BigProd_++

    \func m-func (s : \Sigma R (PermSet (Fin (suc n)))) => msMonomial s. ide *c f-monomial s.

    \func m-func-coh {l l' : Array (\Sigma R (PermSet (Fin (suc n))))} (e : l ~ l') : AddMonoid.BigSum (map m-func l) = AddMonoid.BigSum (map m-func l') \elim e
      | ~-perm e => AbMonoid.BigSum_EPerm (EPerm.EPerm_map m-func e)
      | ~-sym e => inv (m-func-coh e)
      | ~-zro {m} idp => pmap (`+ _) $ pmap (`*c _) (monoidSet-ext $ ~-pequiv (~-zro idp)) *> LModule.*c_zro-left
      | ~-+ m idp idp => pmap (`+ _) (pmap (`*c _) (later msMonomial_+) *> *c-rdistr) *> +-assoc

    \func fHom : RingHom (MPoly (Fin (suc n)) R) (PolyRing (MPoly (Fin n) R)) f \cowith
      | func-+ {x} {y} => \case \elim x, \elim y \with {
        | in~ l, in~ l' => pmap AddMonoid.BigSum (map_++ m-func) *> AddMonoid.BigSum_++
      }
      | func-ide => simplify
      | func-* {x} {y} => \case \elim x, \elim y \with {
        | in~ l, in~ l' => pairs.pairs-distr m-func \lam {a} {b} => pmap2 (*c) msMonomial_* f-monomial_+ *>
                            *c-assoc {_} {msMonomial a. ide} *> pmap (_ *c) *c-comm-right *> *c-comm-left
      }

    \lemma ret-aux {p : Poly (MPoly (Fin n) R)} {e : MPoly (Fin n) R}
      : ret (e *c p) = monoidSet-map (permSet-map fsuc) (id R) e * ret p \elim p
      | pzero => inv Ring.zro_*-right
      | padd p a => rewrite (ret-aux, func-* {monoidSet-ringHom (permSet-hom fsuc) (id R)}) (equation {CRing})

    \func retHom : RingHom (PolyRing (MPoly (Fin n) R)) (MPoly (Fin (suc n)) R) ret \cowith
      | func-zro => idp
      | func-+ {p q : Poly (MPoly (Fin n) R)} : ret (p + q) = ret p + ret q \elim p, q {
        | pzero, q => inv zro-left
        | padd p a, pzero => inv zro-right
        | padd p a, padd q b => rewrite func-+ $ rewrite (AddMonoidHom.func-+ {monoidSet-hom (permSet-map fsuc) (id R)}) (equation {Ring})
      }
      | func-ide => idp
      | func-* {p q : Poly (MPoly (Fin n) R)} : ret (p * q) = ret p * ret q \elim p {
        | pzero => inv Ring.zro_*-left
        | padd p e => func-+ *> rewrite (func-*,ret-aux) (equation {CRing})
      }

    \lemma ret_eval (p : Poly (MPoly (Fin n) R)) {a : R} (l : Array R n)
      : mPolyEval l (polyEval p (msMonomial a ide)) = mPolyEval (a :: l) (ret p) \elim p
      | pzero => idp
      | padd p e => func-+ *> pmap (`+ _) func-* *> pmap2 (_ * __ + __) simplify (pmap (evalMS e) (ext \lam m => \case \elim m \with { | in~ l => idp }) *> inv evalMS_map) *> pmap (`+ _) (pmap (`* _) (ret_eval p l) *> inv func-*) *> inv func-+

    \lemma f_eval (p : MPoly (Fin (suc n)) R) {a : R} (l : Array R n)
      : mPolyEval l (polyEval (f p) (msMonomial a ide)) = mPolyEval (a :: l) p
      => ret_eval (f p) l *> pmap (mPolyEval _) (MPoly_Fin-suc.ret_f p)

    \lemma f_polyMap {S : CRing} {p : MPoly (Fin (suc n)) R} {g : RingHom (MPoly (Fin n) R) (MPoly (Fin n) S)} (h : AddMonoidHom R S)
                     (g-var : \Pi (j : Fin n) -> g (mVar j) = mVar j) (g-const : \Pi (a : R) -> g (msMonomial a ide) = msMonomial (h a) ide)
      : polyMap g (f p) = f (mPoly-map h p) \elim p
      | in~ l => AddMonoidHom.func-BigSum {polyMapRingHom g} *> pmap AddMonoid.BigSum (exts \lam j => unfold $ unfold m-func $ unfold msMonomial $ polyMapRingHom.polyMap_*c *> pmap2 (*c) (g-const (l j).) (later $ cases (l j). \with {
        | in~ l' => MonoidHom.func-BigProd {polyMapRingHom g} *> pmap Monoid.BigProd (exts \lam j => cases (l' j) \with {
          |  => pmap2 (\lam x => padd (padd pzero x)) g.func-ide g.func-zro
          | suc j => pmap (padd pzero) (g-var j)
        })
      }))
  }

\lemma MPoly-surj {J : \Set} {R S : CRing} (f : AddMonoidHom R S) (fs : isSurj f) : isSurj (mPoly-map {J} f)
  => \case \elim __ \with {
       | in~ l => \case FinSet.finiteAC (\lam j => fs (l j).) \with {
         | inP g => inP (inMS \lam j => ((g j)., (l j).), pmap inMS $ exts \lam j => ext ((g j)., idp))
       }
  }

\func MPoly_Fin-suc' {n : Nat} {R : CRing} : QEquiv {MPoly (Fin (suc n)) R} {MPoly (Fin n) (PolyAlgebra R)} \cowith
  | f => fHom
  | ret => retHom
  | ret_f => mPolyRingHom-unique (retHom RingCat.∘ fHom) (RingCat.id _) (\lam r => simplify) \case \elim __ \with {
    |  => simplify $ monoidSet-ext $ ~-pequiv (~-perm $ later $ eperm-swap idp idp idp) *> ~-pequiv (~-zro idp)
    | suc j => simplify
  }
  | f_sec => mPolyRingHom-unique (fHom RingCat.∘ retHom) (RingCat.id _) (polyMapEval-unique (fHom ∘ retHom ∘ mPolyHom) mPolyHom (\lam r => simplify) (pmap fHom retHom_mConst *> fHom_mVar)) (\lam j => simplify)
  \where {
    \func fHom {R : CRing} : RingHom (MPoly (Fin (suc n)) R) (MPoly (Fin n) (PolyAlgebra R))
      => mPolyMapEvalRingHom (mPolyHom RingCat.∘ polyHom) $ later (mConst (padd  ) :: mkArray \lam j => mVar j)

    \func retHom {R : CRing} : RingHom (MPoly (Fin n) (PolyAlgebra R)) (MPoly (Fin (suc n)) R)
      => mPolyMapEvalRingHom (polyMapEvalRingHom mPolyHom (mVar ( : Fin (suc n)))) \lam j => mVar (fsuc j)

    \private \lemma retHom_mConst : retHom (mConst (padd  R.zro)) = mVar ( : Fin (suc n))
      => simplify $ monoidSet-ext $ ~-pequiv (~-perm $ later $ eperm-swap idp idp idp) *> ~-pequiv (~-zro idp)

    \private \lemma fHom_mVar : fHom (mVar ( : Fin (suc n))) = mConst (padd  R.zro)
      => mPolyMapEval-var (mPolyHom RingCat.∘ polyHom) (mConst (padd  ) :: mkArray \lam j => mVar j) 

    \lemma map-comm {R S : CRing} (f : RingHom R S) {p : MPoly (Fin n) (PolyAlgebra R)}
      : mPoly-map f (retHom p) = retHom (mPoly-map (polyMapRingHom f) p)
      => mPolyRingHom-unique (mPoly-mapHom f RingCat.∘ retHom) (retHom RingCat.∘ mPoly-mapHom {_} {PolyAlgebra R} {PolyAlgebra S} (polyMapRingHom f))
          (polyMapEval-unique (mPoly-mapHom f ∘ retHom ∘ mPolyHom) (retHom ∘ mPoly-mapHom {_} {PolyAlgebra R} {PolyAlgebra S} (polyMapRingHom f) ∘ mPolyHom {_} {PolyAlgebra R}) (\lam r => simplify) simplify) (\lam j => simplify) p

    \lemma eval-comm {R : CRing} {p : MPoly (Fin n) (PolyAlgebra R)} {a : R} {l : Array R n}
      : mPolyEval (a :: l) (retHom p) = mPolyEval l (mPoly-map (polyEvalRingHom a) p)
      => mPolyRingHom-unique (mPolyEval (a :: l) RingCat.∘ retHom) (mPolyEval l RingCat.∘ mPoly-mapHom {_} {PolyAlgebra R} (polyEvalRingHom a))
          (polyMapEval-unique (mPolyEval (a :: l) ∘ retHom ∘ mPolyHom) (mPolyEval l ∘ mPoly-mapHom {_} {PolyAlgebra R} (polyEvalRingHom a) ∘ mPolyHom {_} {PolyAlgebra R})
              (\lam r => simplify simplify) (simplify $ simplify $ inv ide-left)) (\lam j => simplify $ simplify $ inv ide-left) p

    \lemma mapEval-comm {R S : CRing} (f : RingHom R S) {p : MPoly (Fin (suc n)) R} {a : S} {l : Array (Poly R) n}
      : polyMapEval f (mPolyEval l (fHom p)) a = mPolyMapEval f p (a :: map (polyMapEval f __ a) l)
      => mPolyRingHom-unique (polyMapEvalRingHom f a ∘ mPolyEval l RingCat.∘ fHom) (mPolyMapEvalRingHom f _) (\lam r => simplify simplify) (\case \elim __ \with {
           |  => simplify $ simplify $ rewrite (f.func-ide,f.func-zro) simplify
           | suc j => simplify $ rewrite f.func-ide $ simplify $ pmap (polyMapEval f __ a) (pmap2 (+) peq ide_*c)
         }) p
  }

\func mdegree< {J : \Set} {R : CRing} (p : MPoly J R) (d : Nat) : \Prop \elim p
  | in~ (l : Array) => ∃ (l' : Array (\Sigma R (PermSetMonoid J))) (inMS~ l = inMS~ l') ∀ (s : l') (permSet-length s. < d)
  | ~-equiv l l' r => ext (TruncP.map __ \lam s => (s., inv (~-pequiv r) *> s., s.), TruncP.map __ \lam s => (s., ~-pequiv r *> s., s.))

\lemma mdegree<_map {J : \Set} {R E : CRing} {f : AddMonoidHom R E} {p : MPoly J R} {d : Nat} (pd : mdegree< p d) : mdegree< (mPoly-map f p) d \elim p, pd
  | in~ l, inP (l',p,q) => inP (map (\lam s => (f s., s.)) l', Transitive.Closure.toEquality (\lam l => inMS~ $ map (\lam s => later (f s., s.)) l) (\lam q => ~-pequiv $ MonoidSet.~_map f (\lam x => x) q) $ MonoidSet.toClosure (path \lam i => p i), q)

\lemma mdegree<-exists {J : \Set} {R : CRing} (p : MPoly J R) : ∃ (d : Nat) (mdegree< p d) \elim p
  | in~ l => inP (suc $ Big (∨)  $ map (\lam s => permSet-length s.) l, inP (l, idp, \lam j => suc_<=_< $ suc<=suc $ later $ NatSemiring.Big_<=_join1 {map (\lam s => permSet-length s.) l} j))

\lemma mdegree<0 {J : \Set} {R : CRing} {p : MPoly J R} (d : mdegree< p ) : p =  \elim p, d
  | in~ l, inP (nil, q, _) => path \lam i => q i
  | in~ l, inP (a :: l', _, q) => \case q 

\func decMdegree {J : DecSet} {R : CRing.Dec} (p : DecMonoidSet (PermSet J) R) : Nat \elim p
  | in~ s => Big (∨)  (map (\lam t => permSet-length t.) s.)
  | ~-equiv x y r => AbMonoid.BigSum_EPerm {Bounded.JoinSemilattice.toMonoid NatBSemilattice} $ EPerm.EPerm_map (\lam t => permSet-length t.) r

\func mdegree {J : DecSet} {R : CRing.Dec} (p : MPoly J R) : Nat
  => decMdegree (monoidSetDec-equiv.ret p)

\lemma mdegree_mdegree< {J : DecSet} {R : CRing.Dec} {p : MPoly J R} : mdegree< p (suc (mdegree p))
  => transport (mdegree< __ _) (monoidSetDec-equiv.f_ret p) $ unfold mdegree $ cases (monoidSetDec-equiv.ret p) \with {
    | in~ s => inP (_, idp, \lam j => NatBSemilattice.Big_<=_join1 {map (\lam t => permSet-length t.) s.} j <∘r id<suc)
  }