\import Algebra.Field
\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Monoid.Sub
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Local
\import Algebra.Ring.Localization
\import Data.Or
\import Logic
\import Order.LinearOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\open Monoid \hiding (equals)
\open LocRing

\lemma localization-inv {R : CRing} (S : SubMonoid R) (a : SType S) (r : R) (p : S (a. * r)) : Inv (inl~ a) (in~ (a. * r, a. * r, p))
  => Inv.lmake {LocRing S} (in~ (a. * r, a. * r, p))
               (path (~-equiv {SType S} _ _ (
                 ((a. * r) * a.) * ide ==< ide-right >==
                 (a. * r) * a.         ==< *-comm >==
                 a. * (a. * r)         ==< inv *-assoc >==
                 (a. * a.) * r         ==< pmap (`* r) *-comm >==
                 (a. * a.) * r         ==< *-assoc >==
                 a. * (a. * r)         ==< *-comm >==
                 (a. * r) * a.         ==< inv ide-left >==
                 ide * ((a. * r) * a.) `qed)))
  \where {
    \lemma converse (j : Inv (inl~ a)) : TruncP (\Sigma (r : R) (S (a. * r)))
      => \let | (in~ b \as i) => j.inv
              | p : inl~ a * i = ide => j.inv-right
              | (inP (c,cs,q)) => unequals S p
         \in inP (b. * (ide * c), rewriteEq q (contains_* (contains_* S.contains_ide (contains_* a. b.)) cs))
  }

\lemma localization-zro {R : CRing} (S : SubMonoid R) (a : SType S) (s : R) (c : S s) (p : a. * s = zro) : inl~ a = zro
  => equals-lem S s c (
    (a. * ide) * s   ==< simplify >==
    a. * s           ==< p >==
    zro               ==< simplify >==
    (zro * a.) * s `qed)

\lemma localization-nonTrivial {R : CRing} (S : SubMonoid R) (p : Not (S zro)) :  /= {LocRing S} 
  => \case unequals S __ \with {
    | inP (c, s, q) => p (transport S (
      c               ==< simplify >==
      (ide * ide) * c ==< inv q >==
      (zro * ide) * c ==< simplify >==
      zro             `qed) s)
  }

\lemma localization-isLocal {R : CRing} (S : SubMonoid R) (nt : Not (S zro))
                            (loc : \Pi (x y : R) -> S y -> (\Sigma (r : R) (S (x * r))) || (\Sigma (r : R) (S ((x + y) * r))))
  : LocalCRing { | CRing => LocRing S } \cowith
  | zro/=ide => localization-nonTrivial S nt
  | locality (in~ x) => \case loc x. x. x. \with {
    | byLeft (r,c) => byLeft (localization-inv S x r c)
    | byRight (r,c) => byRight (localization-inv S (x. * ide + ide * x., x. * ide, contains_* x. S.contains_ide) r (simplify c))
  }

\lemma localization-isField {R : CRing} (S : SubMonoid R) (nt : Not (S zro))
                            (loc : \Pi (x y : R) -> S y -> (\Sigma (r : R) (S (x * r))) || (\Sigma (r : R) (S ((x + y) * r))))
                            (fp : \Pi (x : R) -> (\Pi (r : R) -> Not (S (x * r))) -> TruncP (\Sigma (s : R) (S s) (x * s = zro)))
  : Field { | CRing => LocRing S } \cowith
  | LocalCRing => localization-isLocal S nt loc
  | #0-tight {in~ x} x-ni => \case fp x. (\lam r c[x*r] => x-ni (localization-inv S x r c[x*r])) \with {
    | inP (s,c,p) => localization-zro S x s c p
  }

\func localization-isDiscreteField {R : CRing} (S : SubMonoid R) (nt : Not (S zro))
                                   (fp : \Pi (x : R) -> (\Sigma (s : R) (S s) (x * s = zro)) || (\Sigma (r : R) (S (x * r))))
  : DiscreteField { | CRing => LocRing S } \cowith
  | zro/=ide => localization-nonTrivial S nt
  | eitherZeroOrInv (in~ x) => \case fp x. \with {
    | byLeft (s, cs, x*s=0) => byLeft (localization-zro S x s cs x*s=0)
    | byRight (r, c[x*r]) => byRight (localization-inv S x r c[x*r])
  }

-- | The localization of an ordering commutative ring at the set of positive elements is an ordered field.
\func localization-isOrderedField (R : OrderedCRing) : OrderedField \cowith
  | Field => localization-isField (positiveSubset R) zro/>0
    (\lam x y y>0 => \case <_+-comparison (negative x) (x + y) (transport isPos simplify y>0) \with {
      | byLeft -x>0 => byLeft (negative ide, simplify -x>0)
      | byRight x+y>0 => byRight (ide, simplify x+y>0)
    })
    (\lam x x-ni => inP (ide, ide>zro, ide-right *> <_+-connectedness (\lam x>0 => x-ni ide (simplify x>0)) (\lam -x>0 => x-ni (negative ide) (simplify -x>0))))
  | isPos => isPositive
  | zro/>0 => zro/>0
  | positive_+ {in~ x} {in~ y} x>0 y>0 => positive_+ (positive_* x>0 y.) (positive_* y>0 x.)
  | ide>zro => ide>zro
  | <_+-comparison (in~ x) (in~ y) x+y>0 => ||.map (OrderedRing.positive_*-cancel-left __ y.) (OrderedRing.positive_*-cancel-left __ x.) (<_+-comparison _ _ x+y>0)
  | <_+-connectedness {in~ x} x/>0 -x/>0 => localization-zro (positiveSubset R) x ide ide>zro (ide-right *> <_+-connectedness x/>0 -x/>0)
  | positive_* {in~ x} {in~ y} => positive_* {_} {x.} {y.}
  | positive=>#0 {in~ x} x>0 => localization-inv (positiveSubset R) x ide (simplify x>0)
  | #0=>eitherPosOrNeg {in~ x} => \case localization-inv.converse (positiveSubset R) x __ \with {
    | inP (r, x*r>0) => ||.map __. __. (positive_*-cancel x*r>0)
  }
  \where {
    \func positiveSubset (R : OrderedCRing) : SubMonoid R \cowith
      | contains => isPos
      | contains_ide => ide>zro
      | contains_* => positive_*

    \func isPositive {R : OrderedCRing} (x : Type (positiveSubset R)) : \Prop \elim x
      | in~ x => isPos x.
      | ~-equiv x y x~y => propExt
          (\lam x>0 => OrderedRing.positive_*-cancel-left (transport isPos x~y (positive_* x>0 y.)) x.)
          (\lam y>0 => OrderedRing.positive_*-cancel-left (transport isPos (inv x~y) (positive_* y>0 x.)) y.)
  }

-- | The localization of a decidable ordered commutative ring at the set of positive elements is a discrete ordered field.
\func localization-isDiscreteOrderedField (R : OrderedCRing.Dec) : DiscreteOrderedField \cowith
  | DiscreteField => localization-isDiscreteField (localization-isOrderedField.positiveSubset R) zro/>0 (\lam x => \case +_trichotomy x \with {
    | less x<0 => byRight (negative ide, simplify (R.<0_neg x<0))
    | equals x=0 => byLeft (ide, ide>zro, simplify x=0)
    | greater x>0 => byRight (ide, simplify (R.>0_pos x>0))
  })
  | OrderedField => localization-isOrderedField R
  \where \open OrderedRing