Field

\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Localization
\import Algebra.Monoid.SubMonoid
\import Algebra.Ordered
\import Algebra.Ring.RingHom
\import Algebra.StrictlyOrdered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Local
\import Algebra.Ring.Localization
\import Algebra.Semiring
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.LinearOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\open Monoid
\open LocRing(isLocalization \as LR)

\lemma localization-isField {R : CRing} (S : SubMonoid R) (nt : Not (S zro))
                            (loc : ∀ {x} {y} (S (x + y)) ∃ (r : R) (S (x * r) || S (y * r)))
                            (fp : ∀ x (∀ r (Not (S (x * r)))) ∃ (s : R) (S s) (x * s = zro))
  : Field { | CRing => LocRing S } \cowith
  | zro/=ide => \lam p => nt $ LR.loc-trivial-char.1 p
  | locality => LR.isLocal-char.2 loc
  | #0-tight {in~ x} x-ni => localization-zro-char.2 $ fp x.1 \lam r Sxr => x-ni $ localiaztion-inv-char.2 $ inP (r,Sxr)

\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 => \lam p => nt $ LR.loc-trivial-char.1 p
  | eitherZeroOrInv (in~ x) => \case fp x.1 \with {
    | byLeft r => byLeft $ localization-zro-char.2 (inP r)
    | byRight r => byRight $ localiaztion-inv-char.2 (inP 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} x+y>0 => inP (1, \case <_+-comparison x y x+y>0 \with {
    | byLeft x>0 => byLeft (transportInv isPos ide-right x>0)
    | byRight y>0 => byRight (transportInv isPos ide-right 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-right __ y.3) (OrderedRing.pos_*-cancel-right __ x.3) (<_+-comparison _ _ x+y>0)
  | <_+-connectedness {in~ x} x/>0 -x/>0 => localization-zro-char.2 $ inP (1, 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 => localiaztion-inv-char.2 $ inP (1, transportInv isPos ide-right x>0)
  | #0=>eitherPosOrNeg {in~ x} => \case localiaztion-inv-char.1 __ \with {
    | inP (c,xc>0) => ||.map __.1 __.1 (positive_*-cancel xc>0)
  }
  | meet (x y : LocType (positiveSubset R)) : LocType (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 => ~-lequiv1 $ 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 => ~-lequiv1 $ 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 : LocType (positiveSubset R)) : LocType (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 => ~-lequiv1 $ 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 => ~-lequiv1 $ 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 : LocType (positiveSubset R)) : \Prop \elim x
      | in~ x => isPos x.1
      | ~-equiv x y x~y => propExt
          (\lam x>0 => OrderedRing.pos_*-cancel-right (transport isPos x~y (positive_* x>0 y.3)) x.3)
          (\lam y>0 => OrderedRing.pos_*-cancel-right (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