\import Algebra.Field
\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Group.SubGroup
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Ideal
\import Algebra.Ring.MPoly
\import Algebra.Ring.Poly()
\import Algebra.Semiring
\import Arith.Int
\import Arith.Nat
\import Category
\import Data.Array
\import Function (IsInj, IsSurj)
\import Function.Meta
\import Logic.Unique
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta

\lemma *-addMonoidHom-left {R : PseudoSemiring} {a : R} : AddMonoidHom R R (a *) \cowith
  | func-zro => zro_*-right
  | func-+ => ldistr

\lemma *-addMonoidHom-right {R : PseudoSemiring} {a : R} : AddMonoidHom R R (* a) \cowith
  | func-zro => zro_*-left
  | func-+ => rdistr

\record SemiringHom \extends AddMonoidHom, MonoidHom {
  \override Dom : Semiring
  \override Cod : Semiring

  \lemma func-natCoef {n : Nat} : func (natCoef n) = natCoef n \elim n
    |  => rewrite (natCoefZero,natCoefZero) func-zro
    | suc n => rewrite (natCoefSuc,natCoefSuc) $ func-+ *> pmap2 (+) func-natCoef func-ide
}

\lemma *-addGroupHom-left {R : PseudoRing} {a : R} : AddGroupHom R R (a *) \cowith
  | func-+ => ldistr

\lemma *-addGroupHom-right {R : PseudoRing} {a : R} : AddGroupHom R R (* a) \cowith
  | func-+ => rdistr

\record PseudoRingHom \extends AddGroupHom, SemigroupHom {
  \override Dom : PseudoRing
  \override Cod : PseudoRing
} \where {
  \lemma func-Ideal_closure {R S : CRing} (f : PseudoRingHom R S) {J : \Set} {g : J -> R} {x : R} (gx : Ideal.closure g x) : Ideal.closure (\lam j => f (g j)) (f x) \elim gx
    | inP (l,p) => inP (map (\lam s => (f s., s.)) l, pmap f p *> f.func-BigSum *> pmap S.BigSum (exts \lam j => f.func-*))

  \lemma func-Ideal_sclosure {R S : CRing} (f : PseudoRingHom R S) {U : R -> \Prop} {x : R} (Ux : Ideal.sclosure U x) : Ideal.sclosure (SetIm f U) (f x) \elim Ux
    | inP (l,p) => inP (map (\lam s => later (f s., (f s.., SetIm-con s..))) l, pmap f p *> f.func-BigSum *> pmap S.BigSum (exts \lam j => f.func-*))

  \lemma func-Ideal_lclosure {R S : CRing} (f : PseudoRingHom R S) {l : Array R} {x : R} (lx : Ideal.lclosure l x) : Ideal.lclosure (\lam j => f (l j)) (f x)
    => func-Ideal_closure f {_} {l} lx

  \func func-Ideal {R S : CRing} (f : PseudoRingHom R S) (I : Ideal S) : Ideal R \cowith
    | contains x => I (f x)
    | contains_zro => transportInv I f.func-zro I.contains_zro
    | contains_+ Ifx Ify => transportInv I f.func-+ $ I.contains_+ Ifx Ify
    | ideal-left Ifa => transportInv I f.func-* $ I.ideal-left Ifa
}

\record RingHom \extends PseudoRingHom, SemiringHom {
  \override Dom : Ring
  \override Cod : Ring

  \protected \func Kernel : TIdeal Dom \cowith
    | SubAddGroup => KernelAddGroup \this
    | ideal-left A0 => rewrite (func-*, A0, zro_*-right) idp
    | ideal-right A0 => rewrite (func-*, A0, zro_*-left) idp
} \where {
    \func equals {R S : Ring} {f g : RingHom R S} (p : \Pi (x : R) -> f x = g x) : f = g
      => exts p

    \func id {R : Ring} : RingHom R R \cowith
      | func x => x
      | func-ide => idp
      | func-+ => idp
      | func-* => idp

    \func \fixl  compose \alias \infixl  ∘ {R S T : Ring} (g : RingHom S T) (f : RingHom R S) : RingHom R T \cowith
      | func x => g (f x)
      | func-ide => pmap g f.func-ide *> g.func-ide
      | func-+ => pmap g f.func-+ *> g.func-+
      | func-* => pmap g f.func-* *> g.func-*

  \lemma contr-isTerm {R S : Ring} (c : Contr S) : Contr (RingHom R S) \cowith
      | center => \new RingHom {
        | func _ => c.center
        | func-+ => c.contraction _
        | func-ide => c.contraction _
        | func-* => c.contraction _
      }
      | contraction f => exts \lam e => c.contraction _

    \lemma field-isInj {K : Field} {R : NonZeroRing} {f : RingHom K R} : IsInj f
      => f.injective \lam p => K.#0-tight \lam a#0 => R.inv-nonZero (f.func-Inv a#0) p

    \type isAlgebraGenerated {R E : CRing} (f : RingHom R E) (l : Array E) : \Prop
      => \Pi (x : E) -> ∃ (p : MPoly (Fin l.len) R) (x = mPolyEval l (mPoly-map f p))

    \type isFiniteAlgebra {R E : CRing} (f : RingHom R E) : \Prop
      => ∃ (l : Array E) (isAlgebraGenerated f l)

    \open Algebra.Ring.Poly

    \lemma isAlgebraGenerated-comp {R E S : CRing} {f : RingHom R E} {g : RingHom E S} {a : E} {l : Array S}
                                   (fg : \Pi (x : E) -> ∃ (p : Poly R) (polyMapEval f p a = x)) (gg : isAlgebraGenerated g l) : isAlgebraGenerated (g ∘ f) (g a :: l)
      => \lam x =>
          \have | (inP (p,pq)) => gg x
                | (inP ((s : MPoly (Fin l.len) (PolyAlgebra R)),sq)) => MPoly-surj {Fin l.len} (polyMapEvalRingHom f a) fg p
          \in inP (MPoly_Fin-suc'.retHom s, pq *> rewrite (inv sq, MPoly_Fin-suc'.map-comm) (pmap (mPolyEval l)
              (inv mPoly-map-comp *> pmap (mPoly-map __ s) (exts \lam p => unfold (inv polyEval_polyMap) *> pmap (polyEval __ _) (polyMap-comp f g)) *> mPoly-map-comp {_} {PolyAlgebra R} {PolyAlgebra S}) *> inv MPoly_Fin-suc'.eval-comm))

    \lemma isAlgebraGenerated-poly {R E : CRing} {f : RingHom R E} {a : E}
                                   (fg : \Pi (x : E) -> ∃ (p : Poly R) (polyMapEval f p a = x)) : isAlgebraGenerated f (a :: nil)
      => isAlgebraGenerated-comp {R} {E} {E} {f} {RingHom.id} {a} {nil} fg \lam x => inP (mConst x, simplify)

  \func KernelC {R : CRing} {S : Ring} (f : RingHom R S) : Ideal R \cowith
    | TIdeal => f.Kernel
}

\func natMap {R : Semiring} : SemiringHom NatSemiring R \cowith
  | func => natCoef
  | func-+ {n m : Nat} : R.natCoef (n + m) = natCoef n + natCoef m \elim m {
    |  => inv (pmap (natCoef n +) natCoefZero *> zro-right)
    | suc m => natCoefSuc (n + m) *> pmap (+ ide) func-+ *> +-assoc *> pmap (natCoef n +) (inv (natCoefSuc m))
  }
  | func-zro => natCoefZero
  | func-ide => natCoefSuc  *> pmap (+ ide) natCoefZero *> zro-left
  | func-* {n m : Nat} : R.natCoef (n * m) = natCoef n * natCoef m \elim m {
    |  => natCoefZero *> inv (pmap (natCoef n *) natCoefZero *> zro_*-right)
    | suc m => func-+ *> pmap (+ natCoef n) func-* *> inv (pmap (natCoef n *) (natCoefSuc m) *> ldistr *> pmap (natCoef n * natCoef m +) ide-right)
  }

\lemma natComm {R : Semiring} (n : Nat) (x : R) : natMap n * x = x * natMap n \elim n
  |  => pmap (* x) natCoefZero *> zro_*-left *> inv (pmap (x *) natCoefZero *> zro_*-right)
  | suc n => pmap (* x) (natCoefSuc n) *> rdistr *> pmap (natCoef n * x +) ide-left *> pmap (+ x) (natComm n x) *> inv (pmap (x *) (natCoefSuc n) *> ldistr *> pmap (x * natCoef n +) ide-right)

\func intMap {R : Ring} : RingHom IntRing R \cowith
  | func => intCoef
  | func-+ {x y : Int} : R.intCoef (x + y) = intCoef x + intCoef y \elim x, y {
    | pos n, pos m => natMap.func-+
    | pos n, neg (suc _ \as m) => intCoef_diff n m
    | neg (suc _ \as n), pos m => intCoef_diff m n *> +-comm
    | neg (suc _ \as n), neg (suc _ \as m) => pmap negative natMap.func-+ *> negative_+ *> +-comm
  }
  | func-ide => natMap.func-ide
  | func-* {x y : Int} : R.intCoef (x * y) = intCoef x * intCoef y \elim x, y {
    | pos n, pos m => natMap.func-*
    | pos n, neg (suc _ \as m) => intCoef_neg _ *> pmap negative natMap.func-* *> inv R.negative_*-right
    | neg (suc _ \as n), pos m => intCoef_neg _ *> pmap negative natMap.func-* *> inv R.negative_*-left
    | neg (suc _ \as n), neg m => natMap.func-* *> inv (pmap (negative (natCoef n) *) (intCoef_neg m) *> R.negative_*)
  }
  \where {
    \open AddGroup(negative_zro,negative_+)
    \open Ring

    \lemma intCoef_diff {R : Ring} (n m : Nat) : R.intCoef (n Nat.- m) = intCoef n - intCoef m \elim n, m
      | ,  => inv (pmap (natCoef  + negative __) natCoefZero *> pmap (natCoef  +) negative_zro *> zro-right)
      | , suc _ \as m => inv (pmap (__ - natCoef m) natCoefZero *> zro-left)
      | suc _ \as n,  => inv (pmap (natCoef n + negative __) natCoefZero *> pmap (natCoef n +) negative_zro *> zro-right)
      | suc n, suc m => intCoef_diff n m *>
      pmap (natCoef n +) (inv (pmap (ide +) negative_+ *> inv +-assoc *> pmap (- natCoef m) negative-right *> zro-left)) *>
      inv (pmap2 (__ + negative __) (natCoefSuc n) (natCoefSuc m) *> +-assoc)
  }

\lemma intComm {R : Ring} (n : Int) (x : R) : intMap n * x = x * intMap n \elim n
  | pos n => natComm n x
  | neg n => rewrite Ring.intCoef_neg (Ring.negative_*-left *> pmap negative (natComm n x) *> inv Ring.negative_*-right)