{- | 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.1 isBezout (Ifg n) | isKaplansky => adequate_kaplansky \lam a/=0 => adequate'_adequate (domain_adequate' divChain a/=0) \lemma is1Dim : Dim<= 1 => bezout_1Dim<->adequate'.2 \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.2, LDiv.make s.1 (*-comm *> inv s.4), s.6, \lam d d|a d_b => coprime_*_div (rewrite s.4 in d|a)$ IsCoprime.factor-right s.5 $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))} (1, inv ide-left, LDiv.id-div) (\lam {m} {x} r => (r.1 * gcd x b, r.2 *> pmap (r.1 *) (inv$ LDiv.inv-right {g x}) *> inv *-assoc, LDiv.product r.3 (GCD.gcd|val2 {gcdC x b}))) n
| c => iterr f n a
\in inP (s.1, c, n, s.2, s.3, 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 /= 0) : IsAdequate' a
=> \lam b => \case decideEq b 0 \with {
| yes b=0 => inP (a, 1, 1, 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.1, a2.1, n, pmap __.1 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<= 1) {a : R} (a/=0 : a /= 0) : IsAdequate' a => \lam b => \have | (inP (v,n,d)) => R.oneDimensional-char.1 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<= 1 <-> (\Pi {a : R} -> a /= 0 -> IsAdequate' a) => (oneDim_adequate', \lam f => oneDimensional-char.2 \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 /= 0 -> IsAdequate a) : SmithRing.IsKaplansky R => \lam a b c a_b_c => \case coprime_bezoutArray a_b_c, decideEq a 0 \with { | inP (s,p), yes a=0 => inP (s 1, s 2, BezoutRing.bezout_coprime {_} {0} {1} equation) | _, no a/=0 => \have | (inP R) => adeq a/=0 c | (inP (c',c*,cp)) => gcd_bezout (IsCoprime.=>gcd R.3) \in inP (1, c* * (1 - 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* * (1 - b)) equation, LDiv.make x2 p2) | d_R : IsCoprime d R.1 => BezoutRing.bezout_coprime {_} {y} {(1 - b) * c'} equation \in d_R d LDiv.id-div$ LDiv_TruncP \$ R.4 d d1 d_c)
}
}