Field

\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\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 Algebra.Semiring
\import Function.Meta
\import Logic
\import Meta
\import Order.Lattice
\import Order.LinearOrder
\import Order.StrictOrder
\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.1 * r)) : Inv (inl~ a) (in~ (a.2 * r, a.1 * r, p))
  => Inv.lmake (inl~ (a.2 * r, a.1 * r, p)) (equals1 equation)
  \where {
    \lemma converse (j : Inv (inl~ a)) : TruncP (\Sigma (r : R) (S (a.1 * r)))
      => \let | (in~ b \as i) => j.inv
              | p : inl~ a * i = ide => j.inv-right
              | (inP (c,cs,q)) => unequals p
         \in inP (b.1 * (ide * c), rewriteEq q (contains_* (contains_* S.contains_ide (contains_* a.3 b.3)) cs))
  }

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

\lemma localization-nonTrivial {R : CRing} (S : SubMonoid R) (p : Not (S zro)) : 0 /= {LocRing S} 1
  => \case unequals __ \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.1 x.2 x.3 \with {
    | byLeft (r,c) => byLeft (localization-inv S x r c)
    | byRight (r,c) => byRight (localization-inv S (x.1 * ide + ide * x.2, x.2 * ide, contains_* x.3 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.1 (\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.1 \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.3) (positive_* y>0 x.3)
  | ide>zro => ide>zro
  | <_+-comparison (in~ x) (in~ y) x+y>0 => ||.map (OrderedRing.pos_*-cancel-left __ y.3) (OrderedRing.pos_*-cancel-left __ x.3) (<_+-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.1} {y.1}
  | positive=>#0 {in~ x} x>0 => localization-inv (positiveSubset R) x ide (simplify x>0)
  | #0=>eitherPosOrNeg {in~ x} => \case localization-inv.converse __ \with {
    | inP (r, x*r>0) => ||.map __.1 __.1 (positive_*-cancel x*r>0)
  }
  | meet (x y : Type {R} {positiveSubset R}) : Type {R} {positiveSubset R} \with {
    | in~ s, in~ t => in~ ((s.1 * t.2) ∧ (t.1 * s.2), s.2 * t.2, positive_* s.3 t.3)
    | in~ s, ~-equiv x y r => equals1 $ pmap (_ *) *-comm *> inv *-assoc *> pmap (`* _) (meet_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∧) equation equation *> inv (meet_*-right (<_<= $ pos_>0 x.3))) *> *-assoc *> pmap (_ *) *-comm
    | ~-equiv x y r, in~ t => equals1 $ inv *-assoc *> pmap (`* _) (meet_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∧) equation equation *> inv (meet_*-right $ <_<= $ pos_>0 x.3)) *> *-assoc
  }
  | meet-left {x} {y} => \case \elim x, \elim y \with {
    | in~ s, in~ t => \lam p => \case positive_*-cancel $ rewrite (R.*-comm {s.2} {t.2}, inv *-assoc, inv rdistr) in unfolds p \with {
      | byLeft (q,_) => meet-left {_} {s.1 * t.2} $ rewrite R.negative_*-left in q
      | byRight (_,c) => <-irreflexive $ pos_>0 s.3 <∘ R.neg_<0 c
    }
  }
  | meet-right {x} {y} => \case \elim x, \elim y \with {
    | in~ s, in~ t => \lam p => \case positive_*-cancel $ rewrite (inv *-assoc, inv rdistr) in unfolds p \with {
      | byLeft (q,_) => meet-right {_} {s.1 * t.2} $ rewrite R.negative_*-left in q
      | byRight (_,c) => <-irreflexive $ pos_>0 t.3 <∘ R.neg_<0 c
    }
  }
  | meet-univ {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ s, in~ t, in~ u => \lam u<=s u<=t p => R.meet-univ
        (\have u<=s' : u.1 * s.2 <= s.1 * u.2 => \lam p => u<=s $ unfolds $ rewrite R.negative_*-left p
         \in transport2 (<=) *-assoc equation $ <=_*_positive-left u<=s' $ <_<= $ pos_>0 t.3)
        (\have u<=t' : u.1 * t.2 <= t.1 * u.2 => \lam p => u<=t $ unfolds $ rewrite R.negative_*-left p
         \in transport2 (<=) equation equation $ <=_*_positive-left u<=t' $ <_<= $ pos_>0 s.3)
        (rewrite (R.negative_*-left, meet_*-right $ <_<= $ pos_>0 u.3) in unfolds p)
  }
  | join (x y : Type {R} {positiveSubset R}) : Type {R} {positiveSubset R} \with {
    | in~ s, in~ t => in~ ((s.1 * t.2) ∨ (t.1 * s.2), s.2 * t.2, positive_* s.3 t.3)
    | in~ s, ~-equiv x y r => equals1 $ pmap (_ *) *-comm *> inv *-assoc *> pmap (`* _) (join_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∨) equation equation *> inv (join_*-right $ <_<= $ pos_>0 x.3)) *> *-assoc *> pmap (_ *) *-comm
    | ~-equiv x y r, in~ t => equals1 $ inv *-assoc *> pmap (`* _) (join_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∨) equation equation *> inv (join_*-right $ <_<= $ pos_>0 x.3)) *> *-assoc
  }
  | join-left {x} {y} => \case \elim x, \elim y \with {
    | in~ s, in~ t => \lam p => \case positive_*-cancel $ rewrite (R.*-comm {s.2} {t.2}, inv *-assoc, inv rdistr) in unfolds p \with {
      | byLeft (q,_) => join-left {_} {s.1 * t.2} q
      | byRight (_,c) => <-irreflexive $ pos_>0 s.3 <∘ R.neg_<0 c
    }
  }
  | join-right {x} {y} => \case \elim x, \elim y \with {
    | in~ s, in~ t => \lam p => \case positive_*-cancel $ rewrite (inv *-assoc, inv rdistr) in unfolds p \with {
      | byLeft (q,_) => join-right {_} {s.1 * t.2} q
      | byRight (_,c) => <-irreflexive $ pos_>0 t.3 <∘ R.neg_<0 c
    }
  }
  | join-univ {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ s, in~ t, in~ u => \lam s<=u t<=u p => R.join-univ {s.1 * t.2 * u.2} {t.1 * s.2 * u.2} {u.1 * (s.2 * t.2)}
        (\have s<=u' : s.1 * u.2 <= u.1 * s.2 => \lam p => s<=u $ unfolds $ rewrite R.negative_*-left p
         \in transport2 (<=) equation *-assoc $ <=_*_positive-left s<=u' $ <_<= $ pos_>0 t.3)
        (\have t<=u' : t.1 * u.2 <= u.1 * t.2 => \lam p => t<=u $ unfolds $ rewrite R.negative_*-left p
         \in transport2 (<=) equation equation $ <=_*_positive-left t<=u' $ <_<= $ pos_>0 s.3)
        (rewrite (R.negative_*-left, join_*-right $ <_<= $ pos_>0 u.3) in unfolds p)
  }
  \where {
    \open OrderedAddGroup
    \open LinearOrder
    \open LinearlyOrderedSemiring \hiding (Dec)

    \func positiveSubset (R : OrderedCRing) : SubMonoid R \cowith
      | contains => isPos
      | contains_ide => ide>zro
      | contains_* => positive_*

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

-- | 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