\import Algebra.Field
\import Algebra.Field.Algebraic
\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Pointed.Category
\import Algebra.Ring.Category
\import Algebra.Ring.Integral
\import Algebra.Ring.RingHom
\import Algebra.Ring.Ideal
\import Algebra.Ring.MPoly
\import Algebra.Ring.Poly
\import Algebra.Semiring
\import Arith.Nat
\import Category
\import Data.Array
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Set.Countable
\open Monoid \hiding (equals)

\type IsSplittingField {k K : DiscreteField} (p : Poly k) (f : RingHom k K)
  => ∃ (l : Array K) (c : K) (RingHom.isAlgebraGenerated f l) (polyMap f p = c PolyRing.*c Monoid.BigProd (map (\lam a => padd  (negative a)) l))

\lemma splitting-integral {k K : DiscreteField} {p : Poly k} {f : RingHom k K} (s : IsSplittingField p f) : isIntegralExt f \elim s
  | inP s => (finGenExt-char $ inP (s.,s.)). K.zeroDimensional

\lemma splitting-monic {k K : DiscreteField} {p : Poly k} (pm : isMonic p) {f : RingHom k K} (s : IsSplittingField p f)
  : ∃ (l : Array K) (RingHom.isAlgebraGenerated f l) (polyMap f p = Monoid.BigProd (map (\lam a => padd  (negative a)) l)) \elim pm, s
  | inP (n,pd,pc), inP (l : Array, c, lg, lq) => inP (l, lg, lq *> pmap (PolyRing.`*c _) (
    \have | pc1 : polyCoef (polyMap f p) n =  => polyCoef_polyMap *> pmap f pc *> func-ide
          | pc2 : polyCoef (polyMap f p) l.len = c => rewrite lq $ polyCoef_*c *> pmap (c *) (leadCoef_BigProd1 (\lam _ => idp) \lam _ => idp) *> ide-right
    \in \case LinearOrder.trichotomy l.len n \with {
      | less q => absurd $ K.zro/=ide $ inv (degree<=.toCoefs _ _ (rewrite lq $ degree<=_*c $ degree<=_BigProd1 \lam _ => idp) q) *> pc1
      | equals q => inv pc2 *> pmap (polyCoef _) q *> pc1
      | greater q => absurd $ K.zro/=ide $ pmap (polyCoef __ n) {pzero} (inv $ lq *> pmap (PolyRing.`*c _) (inv pc2 *> degree<=.toCoefs _ _ (degree<=_polyMap pd) q) *> PolyRing.zro_*c) *> pc1
    }) *> PolyRing.ide_*c)

\sfunc countableSplittingField {k : DiscreteField} (c : Countable k) {p : Poly k} : \Sigma (K : DiscreteField) (Countable K) (f : RingHom k K) (IsSplittingField p f)
  => CountableSplittingFieldData.makeSplittingField c ()
  \where \protected {
    \record RootFieldData (P : DiscreteField -> \Set) (k : DiscreteField) (p : Poly k)
      | RootField : DiscreteField
      | RootFieldP : P RootField
      | rootFieldHom : RingHom k RootField
      | root : RootField
      | isRoot : polyMapEval rootFieldHom p root = 
      | RootField-gen (x : RootField) : ∃ (q : Poly k) (polyMapEval rootFieldHom q root = x)

    \class SplittingFieldData \noclassifying
      (P : DiscreteField -> \Set) (S : \Pi {K : DiscreteField} -> Poly K -> \Prop)
      (S-hom : \Pi {K K' : DiscreteField} (f : RingHom K K') {p : Poly K} -> S p -> S (polyMap f p))
      (S-factor : \Pi {K : DiscreteField} {p q : Poly K} -> S (p * q) -> S p)
      (nextField : \Pi {K : DiscreteField} {p : Poly K} -> P K -> p /=  -> Not (Inv p) -> RootFieldData P K p) {

      \func makeSplittingField {k : DiscreteField} (Pk : P k) {p : Poly k} (Sp : S p) : \Sigma (K : DiscreteField) (P K) (f : RingHom k K) (IsSplittingField p f)
        => aux Pk idp Sp
        \where
          \func aux {k : DiscreteField} (Pk : P k) {p : Poly k} {n : Nat} (d : degree p = n) (Sp : S p) : \Sigma (K : DiscreteField) (P K) (f : RingHom k K) (IsSplittingField p f) \elim n
            |  => (k, Pk, RingCat.id k, inP (nil, polyCoef p , \lam x => inP (mConst x, simplify), rewrite {} (degree=0-lem d) $ pmap (padd pzero) $ leadCoef_polyCoef *> pmap (polyCoef p) d *> inv ide-right))
            | suc n => \let | p/=0 : p /=  => \case rewrite __ in d
                            | rfd : RootFieldData P k p => nextField Pk p/=0 \lam pi => \case polyInv pi \with {
                                                             | inP (r,q,_) => \case rewrite q in d
                                                           }
                            | (K,PK,f,Ks) => aux rfd.RootFieldP {_} {n} (pmap pred (inv (rewrite (decideEq/=_reduce $ /=-sym zro/=ide) in inv (degree_polyMap RingHom.field-isInj) *> degree_*_= (\lam q => p/=0 $ polyMap-inj RingHom.field-isInj q) (rootDiv_* rfd.isRoot)) *> d)) $ S-factor $ transport S (rootDiv_* rfd.isRoot) (S-hom rfd.rootFieldHom Sp)
                       \in (K, PK, f RingCat.∘ rfd.rootFieldHom, TruncP.map Ks \lam (l,c,fl,q) => later
                            (f rfd.root :: l, c, RingHom.isAlgebraGenerated-comp rfd.RootField-gen fl,
                             inv (polyMap-comp rfd.rootFieldHom f) *> pmap (polyMap f) (rootDiv_* rfd.isRoot) *> func-* {polyMapRingHom f} *> pmap (`* _) q *> inv PolyRing.*c-comm-left *>
                             pmap (c PolyRing.*c) (pmap (_ *) (pmap2 (\lam x y => padd (padd pzero x) y) func-ide AddGroupHom.func-negative) *> *-comm {_} {_} {padd  (negative (f root))})))
    }

    \func CountableSplittingFieldData : SplittingFieldData \cowith
      | P K => Countable K
      | S _ => \Sigma
      | S-hom _ _ => ()
      | S-factor _ => ()
      | nextField {k} {p} c p/=0 pc => \new RootFieldData {
        | RootField => FactorField {(poly-maximal-ideal c p pc).} (poly-maximal-ideal c p pc).
        | RootFieldP => factor-countable (Poly.poly-countable c)
        | rootFieldHom => factorHom RingCat.∘ polyHom
        | root => in~ (padd  )
        | isRoot => pmap (polyEval __ _) (inv (polyMap-comp polyHom factorHom)) *> polyEval_polyMap *>
                                                                                   FactorRing.fequiv0 (transportInv (poly-maximal-ideal c p pc). poly-eval (poly-maximal-ideal c p pc).)
        | RootField-gen (in~ q) => inP (q, pmap (polyEval __ _) (inv (polyMap-comp _ _)) *> polyEval_polyMap *> pmap FactorRing.inF poly-eval)
      }

      \lemma poly-eval {K : DiscreteField} {p : Poly K} : polyMapEval polyHom p (padd  ) = p \elim p
        | pzero => idp
        | padd p e => unfold polyMapEval $ rewrite poly-eval $ inv padd-expand
  }