\import Algebra.Field
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Ideal
\import Algebra.Ring.Local
\import Algebra.Ring.Nakayama
\import Algebra.Ring.Poly
\import Algebra.Ring.Reduced
\import Arith.Nat
\import Function.Meta
\import Logic
\import Logic.Meta
\import Logic.TFAE
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\open Monoid

\lemma zeroDimensional-char {R : CRing} : TFAE (
  R.IsZeroDimensional,
  R.Dim<= ,
  \Pi (a : R) -> ∃ (b : R) (k : Nat) (k /= ) (b * b = b) (LDiv (pow a k) b) (LDiv b (pow a k))
) => TFAE.cycle (
  \lam zd x => \case zd (x ) \with {
    | inP (b,n,p) => inP (b :: nil, n :: nil, equation)
  },
  \lam zd x => \case zd (x :: nil) \with {
    | inP (a,m,p) => cases (m  arg addPath) \with {
      | , q => inP (, , (\case __), ide-left, LDiv.make (a ) (equation {usingOnly (rewrite q in p)}), LDiv.ide-div)
      | suc n, q => \have t => rewrite CMonoid.pow_*-comm in aux {_} {pow x (m )} {x * a } (m ) equation
                    \in inP (pow x (m ) * pow (a ) (m ), m , rewrite q (\case __), equation, LDiv.factor-left LDiv.id-div, LDiv.make (pow x (m )) equation)
    }
  }, \lam c a => TruncP.map (c a) \lam s =>
    (LDiv.inv {s.} * pow a (pred s.), s., inv (LDiv.idempt s. s.) *> *-comm *>
      pmap (_ *) (inv (LDiv.inv-right {s.}) *> *-comm *> pmap (_ * pow a __) (inv $ suc_pred s.) *> inv *-assoc *> *-comm) *> inv *-assoc))
  \where
    \lemma aux {x c : R} (n : Nat) (p : x = x * c) : x = x * pow c n \elim n
      |  => inv ide-right
      | suc n => aux n p *> pmap (`* _) p *> *-assoc *> pmap (x *) *-comm

\lemma zeroDimensional_local-char {R : CRing} : TFAE (
  \Sigma R.IsZeroDimensional (\Pi (a : R) -> Inv a || Inv (a + )),
  \Sigma R.IsZeroDimensional R.IsConnected,
  \Pi (a : R) -> Inv a || (\Sigma (n : Nat) (pow a n = ))
) => TFAE.cycle (
  \lam s => (s., LocalRing.local=>connected s.),
  \lam s a => \case zeroDimensional-char   s. a \with {
    | inP r => \case s. r. r. \with {
      | byLeft r1=0 => byRight (r., inv (LDiv.inv-right {r.}) *> pmap (`* _) r1=0 *> R.zro_*-left)
      | byRight r1=1 => byLeft $ Inv.cfactor-right $ rewrite (inv $ suc_pred r.) in Inv.lmake (LDiv.inv {r.}) (*-comm *> LDiv.inv-right {r.} *> r1=1)
    }
  }, \lam s => (\lam a => \case s a \with {
    | byLeft (r : Inv) => inP (r.inv, , inv $ simplify r.inv-right)
    | byRight r => inP (, r., rewrite r. simplify)
  }, \lam a => \case s (a + ) \with {
    | byLeft r => byRight r
    | byRight r => byLeft
      \let | p => pow {PolyRing R} (padd  ) r.
           | t : polyEval p a =  => (polyEvalRingHom a).func-pow *> pmap (pow __ r.) equation *> r.
      \in Inv.ldiv $ transport (LDiv a) (lastCoef_pow *> pow_ide) (poly-root-div t)
  }))

\lemma vonNeumann_idempotent {R : CRing} (vn : R.IsVonNeumannRegular) (a : R) : ∃ (u : R) (u * u = u) (LDiv a u) (a = u * a)
  => TruncP.map (vn a) \lam (b,p) => (a * b, equation, LDiv.factor-left LDiv.id-div, p)

\lemma vonNeumann-char {R : CRing} : TFAE (
{- 0 -} R.IsVonNeumannRegular,
{- 1 -} \Sigma R.IsZeroDimensional (ReducedRing { | Ring => R }),
{- 2 -} \Pi (I : Ideal R) -> I.IsFinitelyGenerated -> ∃ (u : R) (u * u = u) (I.IsGeneratedBy1 u),
{- 3 -} \Pi (I : Ideal R) -> I IdealMonoid.* I = I,
{- 4 -} \Pi (I J : Ideal R) -> I ∧ J = I IdealMonoid.* J
) => TFAE.proof (
  ((,), \lam c => (\lam a => TruncP.map (c a) \lam s => (s., , equation {usingOnly s.}),
                     \new ReducedRing { | isReduced {a} p => \case c a \with {
                       | inP (b,q) => equation
                     } })),
  ((,), \lam (zd, red : ReducedRing) => \lam a => \case zd a \with {
    | inP (b, , p) => inP (b, equation)
    | inP (b, suc n, p) => inP (b, inv ide-right *> R.fromZero (inv R.ldistr_- *>
      red.noNilpotent {_} {suc n} (R.pow_*-comm {_} {_} {suc n} *> equation)) *> inv *-assoc)
  }
  ),
  ((,), \lam c a => \case c (closure1 a) (principal->finitelyGenerated closure1-principal) \with {
    | inP (u,uu=u,(a|u',f)) =>
      \have | (inP (a|u : LDiv a u)) => closure1_LDiv. a|u'
            | (inP u|a) => f {a} (closure-superset {_} {_} {\lam _ => a} ())
      \in inP (a|u.inv, equation {using (a|u.inv-right, R.idempotent_LDiv uu=u u|a)})
  }),
  ((,), \lam v I J => <=-antisymmetric (\lam {a} c =>
    \case v a \with {
      | inP (b,p) => rewrite p $ closure-superset {_} {_} {IdealMonoid.func I J} $ later (a * b, a, ideal-right (IdealLattice.meet-left c), IdealLattice.meet-right c)
    }) IdealMonoid.product_meet),
  ((,), \lam f I => inv (f I I) *> IdealLattice.meet-idemp),
  ((,), \lam f I Ifg => nakayama-ideal Ifg (=_<= (inv (f I))))
)
  \where \open Ideal

\lemma vonNeumann_Bezout {R : CRing} (vn : R.IsVonNeumannRegular) : R.IsBezout
  => R.bezout_finitelyGenerated_principal. \lam {I} Ifg => TruncP.map (vonNeumann-char   vn I Ifg) \lam s => (s.,s.)

\lemma zeroDim->inv {R : ImpotentCRing} (zd : R.IsZeroDimensional) (x : R) : (x = ) || Inv x
  => \case zeroDimensional-char   zd x \with {
    | inP (u,k,k/=0,uu=u,x^k|u,u|x^k) => \case isImpotent uu=u \with {
      | byLeft u=0 => byLeft $ R.noNilpotent $ R.ldiv=0 u|x^k u=0
      | byRight u=1 => byRight \case \elim k, \elim x^k|u, \elim k/=0 \with {
        | , d, p => absurd (p idp)
        | suc k, d, _ => Inv.cfactor-right $ Inv.ldiv (rewrite u=1 in d)
      }
    }
  }

\func zeroDim->field {R : ImpotentCRing} (zd : R.IsZeroDimensional) : DiscreteField { | CRing => R } \cowith
  | zro/=ide => R.zro/=ide
  | eitherZeroOrInv => zeroDim->inv zd