\import Algebra.Field
\import Algebra.Group
\import Algebra.LatticeColimit
\import Algebra.Linear.Matrix
\import Algebra.Linear.Matrix.CharPoly
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Monoid.PermSet
\import Algebra.Monoid.SubMonoid
\import Algebra.Pointed
\import Algebra.Pointed.PointedHom
\import Algebra.Pointed.SubPointed
\import Algebra.Ring
\import Algebra.Ring.MonoidRing(evalMS,evalMS_map2,monoidSet-ringHom,msMonomial)
\import Algebra.Ring.RingCat
\import Algebra.Ring.RingHom
\import Algebra.Ring.Factor(FactorRing,factorHom,factor-lift)
\import Algebra.Ring.Ideal
\import Algebra.Ring.MPoly
\import Algebra.Ring.Poly
\import Algebra.Ring.SubRing
\import Algebra.Semiring
\import Arith.Nat
\import Category.Functor
\import Data.Array
\import Equiv
\import Function (IsInj, IsSurj)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Logic.TFAE
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set.SetCategory
\import Set.Fin
\open Monoid
\open RingHom (id, ∘)

\func polyImage {R : Ring} {E : CRing} (f : RingHom R E) (a : E) : SubRing E
  => ImageRing (polyMapEvalRingHom f a)

\lemma polyImage-closed {R : Ring} {E : CRing} (f : RingHom R E) (a : E) (x : IRing (polyImage f a)) : polyImage f a (a * x.) \elim x
  | (x, inP (p,q)) => inP $ unfold (padd p , unfold $ rewrite (q,f.func-zro) (zro-right *> *-comm))

\lemma polyImage-ext {R : Ring} {E : CRing} (f : RingHom R E) (a : E) (b : R) : polyImage f a (f b)
  => inP (padd pzero b, simplify)

\lemma polyImage-element {R : Ring} {E : CRing} {f : RingHom R E} {a : E} : polyImage f a a
  => rewrite ide-right in polyImage-closed f a 

\lemma polyImage-pow {R : Ring} {E : CRing} (f : RingHom R E) (a : E) {n : Nat} : polyImage f a (pow a n) \elim n
  |  => transport (polyImage f a) func-ide (polyImage-ext f a )
  | suc n => rewrite *-comm $ polyImage-closed f a (pow a n, polyImage-pow f a)

\func polyImageHom {R : Ring} {E : CRing} (f : RingHom R E) (a : E) : RingHom R (IRing (polyImage f a)) \cowith
  | func x => (f x, polyImage-ext f a x)
  | func-+ => ext f.func-+
  | func-ide => ext f.func-ide
  | func-* => ext f.func-*

-- | A map `R[x] -> R[a]` given by `p |-> p(a)`.
\func polyImageHomPoly {R : Ring} {E : CRing} (f : RingHom R E) (a : E) : RingHom (PolyRing R) (IRing (polyImage f a)) \cowith
  | func p => (polyEval (polyMap f p) a, inP (p, idp))
  | func-+ => ext (polyMapEvalRingHom f a).func-+
  | func-ide => ext $ simplify f.func-ide
  | func-* => ext (polyMapEvalRingHom f a).func-*

\func mPolyImage {R E : CRing} (f : RingHom R E) (l : Array E) : SubRing E
  => ImageRing (mPolyEval l ∘ mPoly-mapHom f)

\lemma mPolyImage-ext {R E : CRing} (f : RingHom R E) (l : Array E) (b : R) : mPolyImage f l (f b)
  => inP (msMonomial b ide, simplify)

\func mPolyImage-element {R E : CRing} (f : RingHom R E) (l : Array E) (j : Fin l.len) : mPolyImage f l (l j)
  => inP (mVar j, unfold $ unfold $ rewrite f.func-ide simplify)

\func mPolyImageHom {R E : CRing} (f : RingHom R E) (l : Array E) : RingHom R (IRing (mPolyImage f l)) \cowith
  | func x => (f x, mPolyImage-ext f l x)
  | func-+ => ext f.func-+
  | func-ide => ext f.func-ide
  | func-* => ext f.func-*

\sfunc mPolyImage-finGen {R E : CRing} (f : RingHom R E) (l : Array E)
  : \Sigma (l' : Array (IRing (mPolyImage f l)) l.len) (RingHom.isAlgebraGenerated (mPolyImageHom f l) l')
  => \let l' => \lam j => ((l j, mPolyImage-element f l j) : IRing (mPolyImage f l))
     \in (l', \lam (x, inP (p,q)) => inP (p, ext (inv q *> pmap2 evalMS (later \case \elim p \with {
       | in~ pl => idp
     }) (ext \lam c => inv $ permSet-sum-natural {AbMonoid.fromCMonoid (ICRing (mPolyImage f l))} {AbMonoid.fromCMonoid E} IRing.embed *>
          pmap (permSet-sum {AbMonoid.fromCMonoid E}) permSet-map-comp) *> evalMS_map2 IRing.embed)))

\lemma monic-generated {R E : CRing} (f : RingHom R E) (a : E) (p : Poly R) (n : Nat) (dp : degree<= p n) (dm : polyCoef p n = ) (e : polyEval (polyMap f p) a = )
  : LModule.IsGenerated {homLModule (polyImageHom f a)} (\new Array _ n (\lam i => pow {IRing (polyImage f a)} (a, polyImage-element) i))
  => \lam (b, inP (g,ga)) =>
      \have (q,r,g=q*p+r,dr<n) => monicPolyDivision g p n dp dm
      \in inP (mkArray \lam j => polyCoef r j, (unfold,unfold) at ga $ ext $ inv ga *> rewrite (g=q*p+r,polyMapRingHom.func-+,polyEvalRingHom.func-+,polyMapRingHom.func-*,polyEvalRingHom.func-*,e,E.zro_*-right)
            (zro-left *> polyEval_polyCoef (degree<_polyMap dr<n) *> pmap AddMonoid.BigSum (arrayExt \lam j => pmap2 (*) polyCoef_polyMap (inv (polyImage f a).sub-pow)) *> inv SubAddMonoid.sub-BigSum))

\func isIntegral (f : RingHom) (x : f.Cod) : \Prop
  => ∃ (p : Poly f.Dom) (isMonic p) (polyEval (polyMap f p) x = )
  \where {
    \lemma fromInv {K R : CRing} {f : RingHom K R} {a : R} {p : Poly K} {n : Nat} (d : degree<= p n) (pi : Inv (polyCoef p n)) (pe : polyEval (polyMap f p) a = ) : isIntegral f a
      => inP (pi.inv *c p, inP (n, degree<=_*c d, polyCoef_*c *> pi.inv-left), polyMapEvalRingHom.polyMapEval_*c *> pmap (_ *) pe *> zro_*-right)

    \lemma fromPoly {K : DiscreteField} {R : CRing} {f : RingHom K R} {a : R} {p : Poly K} (p/=0 : p /= ) (pe : polyEval (polyMap f p) a = ) : isIntegral f a
      => inP (finv (leadCoef p) *c p, field-toMonic p/=0, polyMapEvalRingHom.polyMapEval_*c *> pmap (_ *) pe *> zro_*-right)
  }

\lemma module-integral {R E : CRing} (f : RingHom R E) (a : E) (S : SubRing E) (SR : \Pi (x : R) -> S (f x))
                       (Sg : LModule.IsFinitelyGenerated {homLModule (IRing.corestrict f SR)}) (Sa : S a) : isIntegral f a \elim Sg
  | inP (l,Sg) => TruncP.map (module-monic l Sg) \lam d => (d., inP (_, d., d.), d.)
  \where
    \lemma module-monic (l : Array (IRing S)) (Sg : LModule.IsGenerated {homLModule (IRing.corestrict f SR)} l)
      : ∃ (p : Poly R) (degree<= p l.len) (polyCoef p l.len = ) (polyEval (polyMap f p) a = )
      => \let | (inP Sg') => FinSet.finiteAC \lam j => Sg (a * (l j)., contains_* Sa (l j).)
              | (inP d) => Sg (,contains_ide)
              | A => mkMatrix (\lam i => (Sg' i).)
         \in inP (charPoly A, charPoly-degree A, charPoly-monic A, pmap (polyEval __ a) (charPoly_map f A) *> eigen-root (matrix-map f A) (
              inP (mkMatrix \lam i _ => (l i).,
                   \lam x p => inv ide-right *> pmap (x *) (pmap __. d. *> S.sub-BigSum) *> E.BigSum-ldistr *> E.BigSum_zro (\lam i => equation {usingOnly (pmap (__ i ) p)}),
                   matrixExt \lam i _ => pmap __. (Sg' i). *> S.sub-BigSum)))

\func isIntegralExt (f : RingHom) : \Prop
  => \Pi (a : f.Cod) -> isIntegral f a

\lemma finite-integralExt {R E : CRing} {f : RingHom R E} (gen : LModule.IsFinitelyGenerated {homLModule f}) : isIntegralExt f \elim gen
  | inP gen => \lam a => module-integral f a SubRing.max (\lam _ => ()) (inP (map SubRing.maxHom gen., \lam x => TruncP.map (gen. x.) \lam s => (s., ext (s. *> inv SubRing.max.sub-BigSum)))) ()

\lemma integral-generated {R E : CRing} (f : RingHom R E) (a : E) (ai : isIntegral f a) : LModule.IsFinitelyGenerated {homLModule (polyImageHom f a)} \elim ai
  | inP (p, inP t, pc) => inP (_, monic-generated f a p t. t. t. pc)

\lemma poly_integral {R E : CRing} (f : RingHom R E) (a : E) (ai : isIntegral f a) (q : Poly R)
  : isIntegral f (polyEval (polyMap f q) a) \elim ai
  | inP (p, inP t, pc) => TruncP.map (aux f a p t. t. t. pc q idp) \lam s => (s., inP (t.,s.,s.), s.)
  \where {
    \lemma aux {R E : CRing} (f : RingHom R E) (a : E) (p : Poly R) (n : Nat) (d : degree<= p n) (c : polyCoef p n = ) (pa : polyEval (polyMap f p) a = ) (q : Poly R) {b : E} (qb : polyEval (polyMap f q) a = b)
      : ∃ (p' : Poly R) (degree<= p' n) (polyCoef p' n = ) (polyEval (polyMap f p') b = )
      => module-integral.module-monic {R} {E} {f} {b} {polyImage f a} {polyImage-ext f a} {inP (q,qb)} _ (monic-generated f a p n d c pa)
  }

\lemma polyImage_integral {R E : CRing} (f : RingHom R E) (a : E) (ai : isIntegral f a) {x : E} (xi : polyImage f a x) : isIntegral f x \elim xi
  | inP (q,qe) => rewriteI qe (poly_integral f a ai q)

\lemma polyImage_integralExt {R E : CRing} {f : RingHom R E} (a : E) (ai : isIntegral f a) : isIntegralExt (polyImageHom f a) \elim ai
  | inP (p, inP t, pc) => \lam (x, inP (q,qa=x)) => TruncP.map (poly_integral.aux f a p t. t. t. pc q qa=x)
      \lam s => (s., inP (t.,s.,s.), ext $ inv (polyEval_polyMap {IRing.embed {polyImage f a}}) *> pmap (polyEval __ x) (later $ polyMap-comp _ _) *> s.)

\lemma integral_image-comp {R S E : Ring} {f : RingHom R S} (g : RingHom S E) {a : S} (ai : isIntegral f a) : isIntegral (g ∘ f) (g a) \elim ai
  | inP t => inP (t., t., pmap (polyEval __ _) (inv (polyMap-comp f g)) *> polyEval_polyMap *> pmap g t. *> g.func-zro)

\lemma integralExt-surj (f : RingHom) (s : IsSurj f) : isIntegralExt f
  => \lam a => TruncP.map (s a) \lam (b,fb=a) => (padd  (negative b), inP (, idp, idp), rewrite (f.func-ide,f.func-negative,fb=a) simplify)

\lemma integralExt_id {R : Ring} : isIntegralExt (id {R})
  => integralExt-surj _ \lam a => inP (a,idp)

\lemma integral_image (f : RingHom) (a : f.Dom) : isIntegral f (f a)
  => integral_image-comp f $ integralExt-surj id (\lam y => inP (y, idp)) a

\lemma poly-integralExt {R : CRing} {I : Ideal (PolyAlgebra R)} {p : Poly R} (pm : isMonic p) (Ip : I p) : isIntegralExt (factorHom {I} ∘ polyHom)
  => integralExt-finite-char {R} {FactorRing I} (in~ (padd  ) :: nil) (RingHom.isAlgebraGenerated-poly $ later \lam (in~ q) => inP (q, factorHom_polyMapEval))  
      \lam () => inP (p, pm, later $ factorHom_polyMapEval *> FactorRing.fequiv0 Ip)

\lemma integralExt_polyDiv {R E : CRing} {f : RingHom R E} (fi : isIntegralExt f) {p : Poly E} (pm : isMonic p) : ∃ (q : Poly R) (isMonic q) (LDiv p (polyMap f q))
  => \let | g => factorHom {Ideal.closure1 p} ∘ polyHom
          | fgi => integralExt-comp f g fi $ poly-integralExt pm (Ideal.closure1_LDiv. $ inP LDiv.id-div)
     \in \case fgi (in~ (padd  )) \with {
       | inP (q,qm,r) => TruncP.map (Ideal.closure1_LDiv. (FactorRing.unfequiv0 {Ideal.closure1 p} $ inv factorHom_polyMapEval *> pmap (polyEval __ _) (polyMap-comp f g) *> r)) \lam d => (q,qm,d)
     }

\lemma integralExt-left {R S E : Ring} (f : RingHom R S) (g : RingHom S E) (inj : IsInj g) (int : isIntegralExt (g ∘ f)) : isIntegralExt f
  => \lam x => TruncP.map (int (g x)) \lam t => (t., t., inj $ inv polyEval_polyMap *> pmap (polyEval __ _) (polyMap-comp f g) *> t. *> inv g.func-zro)

\lemma integral-right {R S E : Ring} (f : RingHom R S) (g : RingHom S E) (x : E) (int : isIntegral (g ∘ f) x) : isIntegral g x
  => TruncP.map int \lam t => (polyMap f t., polyMap_isMonic t., pmap (polyEval __ x) (polyMap-comp f g) *> t.)

\lemma integralExt-right {R S E : Ring} (f : RingHom R S) (g : RingHom S E) (int : isIntegralExt (g ∘ f)) : isIntegralExt g
  => \lam x => integral-right f g x (int x)

\lemma integralExt-generated {R S : CRing} (f : RingHom R S) {l : Array S} (fi : ∀ (x : l) (isIntegral f x)) (gen : RingHom.isAlgebraGenerated f l)
  : LModule.IsFinitelyGenerated {homLModule f} \elim l
  | nil => inP ( :: nil, \lam x => TruncP.map (gen x) \lam t => (mLastCoef t. :: nil, t. *> unfold (rewriteI {} (ret_f {MPoly_Empty {Fin } \case __} t.) $ pmap (+ ) simplify)))
  | a :: l =>
    \let | g => polyImageHom f a
         | h => IRing.embed {polyImage f a}
    \in LModule.generated-pullback g (integral-generated f a (fi )) $ integralExt-generated h (\lam j => integral-right g h (l j) (fi (suc j))) \lam x => TruncP.map (gen x) \lam t =>
          (polyEval (MPoly_Fin-suc (mPoly-map (polyImageHom f a) t.)) (msMonomial (later (a * , rewrite ide-right polyImage-element)) ide),
           t. *> inv (MPoly_Fin-suc.f_eval (mPoly-map f t.) l) *> pmap (mPolyEval l) (pmap2 polyEval (pmap MPoly_Fin-suc.f (later $ cases t. \with {
             | in~ l' => idp
           }) *> inv (MPoly_Fin-suc.f_polyMap h (\lam j => pmap (msMonomial __ _) h.func-ide) \lam b => idp)) (pmap (msMonomial __ _) (inv ide-right)) *> polyEval_polyMap {monoidSet-ringHom MonoidHom.id _}))

\lemma integralExt-finite-char {R E : CRing} {f : RingHom R E} (l : Array E) (gen : RingHom.isAlgebraGenerated f l)
  : TFAE (isIntegralExt f,
          ∀ (x : l) (isIntegral f x),
          LModule.IsFinitelyGenerated {homLModule f})
  => TFAE.cycle (\lam fi j => fi (l j), \lam ie => integralExt-generated f ie gen, finite-integralExt)

\lemma integral-comp {R S T : CRing} {f : RingHom R S} {g : RingHom S T} (fi : isIntegralExt f) {a : T} (ai : isIntegral g a) : isIntegral (g ∘ f) a \elim ai
  | inP (p, inP (d,dp,dc), pa=0) =>
    \case suc d \as d', idp : d' = suc d \with {
      | d', d'=d+1 =>
        \let | SR : SubRing S => mPolyImage f (\new Array S d' (\lam j => polyCoef p j))
             | S' => ICRing SR
             | f' : RingHom R S' => IRing.corestrict {SR} f \lam y => inP (msMonomial y ide, simplify)
             | fi' : isIntegralExt f' => integralExt-left f' IRing.embed (\lam q => ext q) fi
             | g' : RingHom S' T => g ∘ {S'} IRing.embed
             | l' => \new Array S' d' (\lam j => (polyCoef p j, mPolyImage-element f (\new Array S d' (\lam j => polyCoef p j)) j))
        \in module-integral (g' ∘ f') a (polyImage g' a) (\lam y => polyImage-ext (g ∘ IRing.embed {SR}) a (f y, inP (msMonomial y ide, simplify))) (LModule.generated-comp f' (polyImageHom g' a) (integralExt-generated f' {l'} (\lam j => fi' (l' j))
            (\lam x => TruncP.map x. \lam t => (t., ext $ inv t. *> unfold (unfold $ unfold $ pmap2 evalMS (later $ cases t. \with {
              | in~ l'' => idp
            }) (ext \case \elim __ \with {
              | in~ l'' => inv IRing.embed.func-BigProd
            }) *> evalMS_map2 IRing.embed)))) $
        integral-generated g' a $ inP (Poly.fromArray l', inP (d, degree<_degree<= $ rewriteI d'=d+1 fromArray_degree<,
           pmap (polyCoef _) (inv toFin=id) *> polyCoef_fromArray {_} {l'} {toFin d $ rewrite d'=d+1 id<suc} *>
           ext (pmap (polyCoef p) toFin=id *> dc)), pmap (polyEval __ a) (inv (polyMap-comp IRing.embed g) *>
           pmap (polyMap g) (polyMap_fromArray *> inv (fromArray_polyCoef $ rewrite d'=d+1 $ degree<=_degree< dp))) *> pa=0)) polyImage-element
    }

\lemma integralExt-comp {R S E : CRing} (f : RingHom R S) (g : RingHom S E) (fi : isIntegralExt f) (gi : isIntegralExt g) : isIntegralExt (g ∘ f)
  => \lam x => integral-comp fi (gi x)

\func integralClosure-subring {R E : CRing} (f : RingHom R E) : SubRing E \cowith
  | contains => isIntegral f
  | contains_zro => inP (monomial  , monomial-isMonic , rewrite f.func-zro $ zro-right *> E.zro_*-right)
  | contains_+ {a} {b} ai bi => integral_image-comp (IRing.embed {polyImage IRing.embed b}) $
      integral-combined f ai bi (a + b, inP $ (padd  (a, inP (padd  , equation.cRing {f.func-ide,f.func-zro})), equation.cRing))
  | contains_ide => inP (padd (padd pzero ) -1, inP (,idp,idp), rewrite (f.func-negative,f.func-ide) simplify)
  | contains_* {a} {b} ai bi => integral_image-comp (IRing.embed {polyImage IRing.embed b}) $
      integral-combined f ai bi (a * b, inP (padd (padd pzero (a, inP (padd  , equation.cRing {f.func-ide,f.func-zro}))) , equation.cRing))
  | contains_negative {a} ai => transport (isIntegral f) (later $ rewrite (f.func-negative,f.func-zro,f.func-ide) equation) $ poly_integral f a ai (padd (padd pzero -1) )
  \where
    \lemma integral-combined {R E : CRing} (f : RingHom R E) {a b : E} (ai : isIntegral f a) (bi : isIntegral f b)
      : isIntegralExt (polyImageHom (IRing.embed {polyImage f a}) b ∘ polyImageHom f a)
      => integralExt-comp {_} {ICRing (polyImage f a)} (polyImageHom f a) (polyImageHom (IRing.embed {polyImage f a}) b) (polyImage_integralExt a ai) $
          polyImage_integralExt b $ integral-right (polyImageHom f a) (IRing.embed {polyImage f a}) b bi

\func integralClosure {R E : CRing} (f : RingHom R E) : CRing
  => ICRing (integralClosure-subring f)

\func integralClosure-left {R E : CRing} (f : RingHom R E) : RingHom R (integralClosure f)
  => IRing.corestrict f \lam a => later (integral_image f a)

\func integralClosure-right {R E : CRing} (f : RingHom R E) : RingHom (integralClosure f) E
  => IRing.embed {integralClosure-subring f}

\func isIntegrallyClosed (f : RingHom)
  => \Pi (a : f.Cod) -> isIntegral f a -> ∃ (b : f.Dom) (f b = a)

\lemma integralClosure-integral {R E : CRing} (f : RingHom R E) : isIntegralExt (integralClosure-left f)
  => \lam a => TruncP.map a. \lam t => (t., t., ext $ inv (polyEval_polyMap {integralClosure-right f}) *> pmap (polyEval __ _) (later $ polyMap-comp _ _) *> t.)

\lemma integralClosure-closed {R E : CRing} (f : RingHom R E) : isIntegrallyClosed (integralClosure-right f)
  => \lam a ai => inP ((a, integral-comp {R} {integralClosure f} (integralClosure-integral f) ai ), idp)

-- | A map `R[x]/p -> R[a]` given by `[q]_~ |-> q(a)`.
\func integral_factor {R E : CRing} (f : RingHom R E) (a : E) (p : Poly R) (e : polyEval (polyMap f p) a = )
  : RingHom (FactorRing (Ideal.closure1 p)) (IRing (polyImage f a))
  => factor-lift (polyImageHomPoly f a) \lam {q} c => ext $ unfold \case Ideal.closure1-lem. c \with {
    | inP (d,q=pd) => rewrite (q=pd, (polyMapEvalRingHom f a).func-*) equation
  }

\lemma integralExt-directColimit.{s,p} {J : BottomJoinSemilattice.{s}} (F : Functor J RingCat.{p}) (p : \Pi {j j' : J} (f : j <= j') -> isIntegralExt (F.Func f)) (j : J) : isIntegralExt (RingLatticeColimit.inMap j)
  => \lam (in~ (j',a)) =>
      \let b => F.Func (join-right {_} {j}) a
      \in rewrite (SetColimit.~-cequiv {_} {Comp RingCat.forget F} {j', a} {j ∨ j', b} join-right idp) $
            transportInv {RingHom (F j) (RingLatticeColimit F)} (isIntegral __ _) (RingLatticeColimit.inMap-coh _) $
            integral_image-comp (RingLatticeColimit.inMap (j ∨ j')) (p join-left b)