{- | Adequate rings were defined in
 -   Olaf Helmer, The elementary divisor theorem for certain rings without chain condition, 1943
 -
 -   The proof that adequate rings satisfy the Kaplansky condition is taken from
 -   Irving Kaplansky, Elementary divisors and modules, 1949
-}

\import Algebra.Domain
\import Algebra.Domain.Bezout
\import Algebra.Domain.GCD
\import Algebra.Group
\import Algebra.Linear.Matrix.Smith
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Monoid.GCD
\import Algebra.Ring.Ideal
\import Algebra.Ring.Noetherian
\import Function
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\open DivQuotient \hiding (~)
\open Monoid

\class PID \extends SmithDomain, NoetherianCRing {
  | divChain : CMonoid.DivChain {DivQuotientMonoid nonZeroMonoid}
  | isNoetherian I Ifg => Ideal.fromMonoidChainCondition (IntegralDomain.Dec.fromNonZeroDivChain divChain) I \lam n => bezout_finitelyGenerated_principal. isBezout (Ifg n)
  | isKaplansky => adequate_kaplansky \lam a/=0 => adequate'_adequate (domain_adequate' divChain a/=0)

  \lemma is1Dim : Dim<= 
    => bezout_1Dim<->adequate'. \lam a/=0 => domain_adequate' divChain a/=0
} \where {
  \type IsAdequate {M : CMonoid} (a : M) => \Pi (b : M) -> ∃ (c : E) (LDiv c a) (IsCoprime c b) ∀ d (LDiv d a -> IsCoprime d b -> TruncP (LDiv d c))

  \type IsAdequate' {M : CMonoid} (a : M) => \Pi (b : M) -> ∃ (a1 a2 : M) (n : Nat) (a = a1 * a2) (LDiv a1 (pow b n)) (IsCoprime a2 b)

  \lemma adequate'_adequate {M : GCDMonoid} {a : M} (adeq : IsAdequate' a) : IsAdequate a
    => \lam b => \case adeq b \with {
      | inP s => inP (s., LDiv.make s. (*-comm *> inv s.), s., \lam d d|a d_b => coprime_*_div (rewrite s. in d|a) $ IsCoprime.factor-right s. $ M.IsCoprime_pow-right d_b)
    }

  \open UnitlessGCDMonoid

  \lemma unitless_adequate' {M : UnitlessGCDMonoid} (dc : M.DivChain) (a : M) : IsAdequate' a
    => \lam b =>
        \let | g x => GCD.gcd|val1 {gcdC x b}
             | f x => LDiv.inv {g x}
             | (inP (n, d : LDiv)) => dc (iterr f __ a) \lam i => inP $ LDiv.swap $ g (iterr f i a)
             | s => iterr-index-ind {_} {\lam n x => \Sigma (d : M) (a = d * x) (LDiv d (pow b n))} (, inv ide-left, LDiv.id-div) (\lam {m} {x} r => (r. * gcd x b, r. *> pmap (r. *) (inv $ LDiv.inv-right {g x}) *> inv *-assoc, LDiv.product r. (GCD.gcd|val2 {gcdC x b}))) n
             | c => iterr f n a
        \in inP (s., c, n, s., s., IsCoprime.<=gcd $ transport (GCD c b) (uniqueUnit $ Inv.lmake d.inv $ cancel_*-left c $ inv *-assoc *> pmap (`* g c) d.inv-right *> *-comm *> LDiv.inv-right {g c} *> inv ide-right) (gcdC c b))

  \lemma monoid_adequate' {M : CancelGCDMonoid} (dc : DivChain {DivQuotientMonoid M}) (a : M) : IsAdequate' a
    => \lam b => \case unitless_adequate' dc (inD a) (inD b) \with {
      | inP (in~ a1, in~ a2, n, a=a1a2, a1|b^n, a2_b) =>
        \have (c : Inv, p) => equivalent-associates a (a1 * a2) (make~ a=a1a2)
        \in inP (c * a1, a2, n, p *> inv *-assoc, LDiv.trans (LDiv.make c.inv $ *-comm *> inv *-assoc *> pmap (`* _) c.inv-left *> ide-left) (div-from~ $ transportInv (LDiv _) (MonoidHom.func-pow {inDHom M}) a1|b^n), IsCoprime.<=gcd $ gcd-from~ $ IsCoprime.=>gcd a2_b)
    }

  \lemma domain_adequate' {M : GCDDomain.Dec} (dc : DivChain {DivQuotientMonoid M.nonZeroMonoid}) {a : M} (a/=0 : a /= ) : IsAdequate' a
    => \lam b => \case decideEq b  \with {
      | yes b=0 => inP (a, , , inv ide-right, rewrite b=0 $ simplify zero-div, IsCoprime.IsCoprime_ide-left)
      | no b/=0 => TruncP.map (monoid_adequate' dc (a, nonZeroApart a/=0) (b, nonZeroApart b/=0)) \lam (a1,a2,n,a=a1a2,a1|b^n,a2_b) =>
          (a1., a2., n, pmap __. a=a1a2, transport (LDiv _) subMonoid.embed.func-pow (nonZero_ldiv a1|b^n),
           \lam z z|a2 z|b => nonZero_inv $ a2_b (z, nonZeroApart $ ldiv/=0 b/=0 z|b) (ldiv_nonZero z|a2) (ldiv_nonZero z|b))
    }

  \lemma oneDim_adequate' {R : GCDDomain.Dec} (d : R.Dim<= ) {a : R} (a/=0 : a /= ) : IsAdequate' a
    => \lam b =>
        \have | (inP (v,n,d)) => R.oneDimensional-char. d a b a/=0
              | (inP (a1,a2,a=a1a2,a1|b^n,(c,p))) => split_* d
        \in inP (a1, a2, n, a=a1a2, a1|b^n, BezoutRing.bezout_coprime {_} {c} {v} equation)

  \lemma bezout_1Dim<->adequate' {R : BezoutDomain.Dec} : R.Dim<=  <-> (\Pi {a : R} -> a /=  -> IsAdequate' a)
    => (oneDim_adequate', \lam f => oneDimensional-char. \lam a u a/=0 =>
        \have | (inP (a1,a2,n,a=a1a2,a1|u^n,a2_u)) => f a/=0 u
              | (inP (s,v,p)) => gcd_bezout (IsCoprime.=>gcd a2_u)
        \in inP (v, n, rewrite a=a1a2 $ LDiv.product a1|u^n $ LDiv.make s equation))

  \lemma adequate_kaplansky {R : BezoutDomain.Dec} (adeq : \Pi {a : R} -> a /=  -> IsAdequate a) : SmithRing.IsKaplansky R
    => \lam a b c a_b_c => \case coprime_bezoutArray a_b_c, decideEq a  \with {
      | inP (s,p), yes a=0 => inP (s , s , BezoutRing.bezout_coprime {_} {} {} equation)
      | _, no a/=0 =>
        \have | (inP R) => adeq a/=0 c
              | (inP (c',c*,cp)) => gcd_bezout (IsCoprime.=>gcd R.)
        \in inP (, c* * ( - b), simplify \lam d d1 (y,p) =>
            \have | d_c : IsCoprime d c => \lam z (x1,p1) (x2,p2) => a_b_c z
                            (LDiv.trans (LDiv.make x1 p1) d1, LDiv.make (x1 * y - x2 * c* * ( - b)) equation, LDiv.make x2 p2)
                  | d_R : IsCoprime d R. => BezoutRing.bezout_coprime {_} {y} {( - b) * c'} equation
            \in d_R d LDiv.id-div $ LDiv_TruncP $ R. d d1 d_c)
    }
}