Reduced

\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Ring.Ideal
\import Algebra.Ring.RingHom
\import Arith.Nat
\import Function
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Paths
\import Paths.Meta
\open Monoid(LDiv,Inv)
\open equation(cRing)

\class ReducedRing \extends Ring {
  | isReduced {a : E} : a * a = 0 -> a = 0

  \lemma noNilpotent {a : E} {n : Nat} (p : pow a n = 0) : a = 0
    => aux $ pmap (pow a) (inv $ <=_exists $ LinearOrder.<_<= id<pow2) *> pow_+  *> pmap (`* pow a (NatSemiring.pow 2 n -' n)) p *> zro_*-left
    \where
      \lemma aux {a : E} {n : Nat} (p : pow a (NatSemiring.pow 2 n) = 0) : a = 0 \elim n
        | 0 => inv ide-left *> p
        | suc n => aux $ isReduced (inv pow_+ *> p)
}

\class ReducedCRing \extends ReducedRing, CRing {
  \lemma div_zero {a b : E} (d : LDiv a b) (p : a * b = 0) : b = 0
    => isReduced $ pmap (`* b) (inv d.inv-right *> *-comm) *> *-assoc *> pmap (d.inv *) p *> zro_*-right

  \lemma div_pow_zero {a b : E} {n : Nat} (d : LDiv a (pow b n)) (p : a * b = 0) : b = 0 \elim n
    | 0 => inv ide-left *> pmap (`* b) (inv d.inv-right *> *-comm) *> *-assoc *> pmap (d.inv *) p *> zro_*-right
    | suc n => noNilpotent {_} {_} {suc n} $ div_zero d $ pmap (a *) *-comm *> inv *-assoc *> pmap (`* _) p *> zro_*-left

  \lemma div-cancel {a b b' : E} (d : LDiv a b) (d' : LDiv a b') (p : a * b = a * b') : b = b'
    => div_pow-cancel {_} {a} {b} {b'} {1} {1} (rewrite ide-left d) (rewrite ide-left d') p

  \lemma div_pow-cancel {a b b' : E} {n n' : Nat} (d : LDiv a (pow b n)) (d' : LDiv a (pow b' n')) (p : a * b = a * b') : b = b'
    => \let | I : Ideal => Ideal.radical {Ideal.closure1 a}
            | (inP (k,c)) => I.contains_- (inP (n, Ideal.closure1_LDiv.2 $ inP d)) (inP (n', Ideal.closure1_LDiv.2 $ inP d'))
            | (inP dd) => Ideal.closure1_LDiv.1 c
       \in fromZero $ div_pow_zero dd $ ldistr_- *> toZero p

  \lemma div_div-cancel {a b b' : E} (d : LDiv a b) (d' : LDiv a b') (p : LDiv (a * b) (a * b')) : LDiv b b' p.inv
    => div_pow_div-cancel {_} {a} {b} {b'} {1} {1} (rewrite ide-left d) (rewrite ide-left d') p

  \lemma div_pow_div-cancel {a b b' : E} {n n' : Nat} (d : LDiv a (pow b n)) (d' : LDiv a (pow b' n')) (p : LDiv (a * b) (a * b')) : LDiv b b' p.inv \cowith
    | inv-right => div_pow-cancel {_} {a} (rewrite pow_*-comm $ LDiv.factor-left d) d' $ inv *-assoc *> p.inv-right
}

\class PPRing \extends ReducedCRing {
  | isPPRing (a : E) : ∃ (u : E) (a = u * a) ∀ {x} (a * x = 0 -> u * x = 0)

  | isReduced {a} aa=0 => \case isPPRing a \with {
    | inP s => s.2 *> s.3 aa=0
  }

  \lemma bezout->strictBezout (bez : IsBezout) : IsStrictBezout
    => \lam a b =>
        \let | (inP (s,t,(a',p),(b',q))) => bez a b
             | g => s * a + t * b
             | (inP (w,g=wg,f)) => isPPRing g
             | g[1-w]=0 : g * (1 - w) = 0 => cRing {1 g=wg}
        \in inP (w * t, w * s + (1 - w), w * b', w * a' + (1 - w),
                 cRing { f {b' * a - a' * b} $ cRing {p,q}, inv q, g[1-w]=0 },
                 cRing {
                   cRing {f {1 - w} g[1-w]=0} : w * w = w,
                   f {t * b' + s * a' - 1} $ cRing {p,q}
                 })
}

\class ImpotentRing \extends ReducedRing, NonZeroRing {
  | isImpotent {a : E} : a * a = a -> (a = 0) || (a = 1)

  \lemma decomp {a b : E} (a+b=1 : a + b = 1) (ab=0 : a * b = 0) : (\Sigma (a = 1) (b = 0)) || (\Sigma (a = 0) (b = 1))
    => \case isImpotent $ inv zro-left *> pmap (`+ _) (inv ab=0) *> inv rdistr *> pmap (`* b) a+b=1 *> ide-left \with {
      | byLeft b=0 => byLeft (inv zro-right *> pmap (a +) (inv b=0) *> a+b=1, b=0)
      | byRight b=1 => byRight (inv ide-right *> pmap (a *) (inv b=1) *> ab=0, b=1)
    }
} \where {
  \func subring {R : Ring} {E : ImpotentRing} (f : RingHom R E) (inj : IsInj f) : ImpotentRing { | Ring => R } \cowith
    | zro/=ide p => E.zro/=ide $ inv f.func-zro *> pmap f p *> f.func-ide
    | isReduced aa=0 => inj $ isReduced (inv f.func-* *> pmap f aa=0 *> f.func-zro) *> inv f.func-zro
    | isImpotent aa=a => \case isImpotent (inv f.func-* *> pmap f aa=a) \with {
      | byLeft fa=0 => byLeft $ inj (fa=0 *> inv f.func-zro)
      | byRight fa=1 => byRight $ inj (fa=1 *> inv f.func-ide)
    }
}

\class ImpotentCRing \extends ImpotentRing, ReducedCRing, NonZeroCRing
  \where {
    \func subring {R : CRing} {E : ImpotentRing} (f : RingHom R E) (inj : IsInj f) : ImpotentCRing { | CRing => R } \cowith
      | ImpotentRing => ImpotentRing.subring f inj
  }