\import Algebra.Field
\import Algebra.Group
\import Algebra.Group.GroupHom
\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.Ring.Sub
\import Algebra.Semiring
\import Arith.Int
\import Arith.Nat
\import Category
\import Function (IsInj, IsSurj)
\import Function.Meta
\import Logic.Unique
\import Logic
\import Logic.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 RingHom \extends SemiringHom, AddGroupHom {
  \override Dom : Ring
  \override Cod : Ring

  \protected \func Kernel : TIdeal Dom \cowith
    | SubAddGroup => AddGroupHom.Kernel
    | ideal-left A0 => rewrite (func-*, A0, zro_*-right) idp
    | ideal-right A0 => rewrite (func-*, A0, zro_*-left) idp

  \protected \func Image : SubRing Cod \cowith
    | SubRing => ringHomImage _

  \protected \func image : RingHom (SubRing.IRing {Image}) Cod \cowith
    | func x => x.
    | func-+ => idp
    | func-ide => idp
    | func-* => idp
    \where {
      \lemma isInj : IsInj image => \lam p => ext p

      \lemma isSurj (s : IsSurj func) : IsSurj image
        => \lam y => \case s y \with {
        | inP (x, p) => inP ((func x, inP (x, idp)), p)
      }
    }
} \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 => 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 ImageC {R : Ring} {S : CRing} (f : RingHom R S) : CSubRing S \cowith
    | SubRing => ringHomImage f
}

\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)