\import Algebra.Domain
\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Localization
\import Algebra.Monoid.MonoidHom
\import Algebra.Monoid.SubMonoid
\import Algebra.Pointed
\import Algebra.Pointed.PointedHom
\import Algebra.Pointed.SubPointed
\import Algebra.Ring
\import Algebra.Ring.Ideal
\import Algebra.Ring.Local
\import Algebra.Ring.RingHom
\import Equiv
\import Function.Meta
\import Logic.Meta
\import Logic.Unique
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\open Monoid
\open SubMonoid

-- TODO: Make constructor class
\record RingLocalization \extends Localization {
  \override B : CRing
  \override L : CRing
  \override inL : RingHom B L

  \func liftHom {T : CRing} (f : RingHom B T) (l : \Pi {x : B} -> S x -> Inv (f x)) : RingHom L T \cowith
    | MonoidHom => liftMonoidHom f l
    | func-+ {x} {y} => \case localization-surj x, localization-surj y \with {
      | inP (y1,c1,Sc1,p1), inP (y2,c2,Sc2,p2) => (l (contains_* Sc1 Sc2)).inv-cancel-right $ inv $ T.rdistr *>
          pmap2 (T.+) (pmap (_ *) f.func-* *> inv *-assoc *> pmap (* _) (lift_inL-quot Sc1 p1) *> inv f.func-*)
                      (pmap (_ *) (f.func-* *> *-comm) *> inv *-assoc *> pmap (* _) (lift_inL-quot Sc2 p2) *> inv f.func-*) *>
          inv f.func-+ *> inv (lift_inL-quot (contains_* Sc1 Sc2) $ Ring.rdistr *>
            pmap2 (+) (pmap (x *) func-* *> inv *-assoc *> pmap (* _) p1 *> inv func-*)
                      (pmap (y *) (func-* *> *-comm) *> inv *-assoc *> pmap (* _) p2 *> inv func-*) *>
            inv func-+)
    }

  \lemma zro-char {x : B} : (inL x = 0) <-> ∃ (c : B) (S c) (x * c = 0)
    => (\lam x=0 => \case localization-inj $ x=0 *> inv func-zro \with {
      | inP (c,Sc,p) => inP (c, Sc, p *> Ring.zro_*-left)
    }, \lam (inP (c,Sc,xc=0)) => (localization-inv Sc).inv-cancel-right $ inv func-* *> pmap inL xc=0 *> func-zro *> inv Ring.zro_*-left)

  \lemma loc-trivial-char : (0 = {L} 1) <-> S 0
    => <->trans (\lam p => func-ide *> inv p, \lam p => inv p *> func-ide) $ <->trans zro-char
        (\lam (inP (c,Sc,p)) => transport S (inv ide-left *> p) Sc, \lam S0 => inP (0, S0, ide-left))

  \lemma nilpotent-trivial {x : B} (n : Ring.IsNilpotent x) (Sx : S x) : 0 = {L} 1 \elim n
    | inP (n,p) => loc-trivial-char.2 $ transport S p (S.contains_pow Sx)

  \lemma isLocal-char : Ring.IsLocal {L} <-> ∀ {x} {y} (S (x + y)) ∃ (r : B) (S (x * r) || S (y * r))
    => <->trans Ring.isLocal-sum-char $ later (\lam l Sx+y => \case l (inv Ring.rdistr *> pmap (* _) (inv func-+) *> (localization-inv Sx+y).inv-right) \with {
      | byLeft [x/x+y]-inv => \case inv-char.1 $ Inv.cfactor-left [x/x+y]-inv \with {
        | inP (r,Sxr) => inP (r, byLeft Sxr)
      }
      | byRight [y/x+y]-inv => \case inv-char.1 $ Inv.cfactor-left [y/x+y]-inv \with {
        | inP (r,Syr) => inP (r, byRight Syr)
      }
    }, \lam l {a} {b} a+b=1 => \case localization-surj a, localization-surj b \with {
      | inP (x,c,Sc,ac=x), inP (y,d,Sd,bd=y) =>
        \have lem : inL x * inL d + inL y * inL c = inL c * inL d => equation.cRing {inv ac=x, inv bd=y, a+b=1}
        \in \case localization-inj $ func-+ *> pmap2 (+) func-* func-* *> lem *> inv func-* \with {
          | inP (e,Se,[xd+yc]e=cde) => \case l $ transport S (inv [xd+yc]e=cde *> Ring.rdistr) $ contains_* (contains_* Sc Sd) Se \with {
            | inP (r, byLeft Sxder) => byLeft $ Inv.cfactor-left $ transportInv Inv ac=x $ inv-char.2 $ inP (_, transport S (*-assoc *> *-assoc) Sxder)
            | inP (r, byRight Sycer) => byRight $ Inv.cfactor-left $ transportInv Inv bd=y $ inv-char.2 $ inP (_, transport S (*-assoc *> *-assoc) Sycer)
          }
        }
    })

  \lemma isEpiHom {T : CRing} {g h : RingHom L T} (d : \Pi (a : B) -> g (inL a) = h (inL a)) : g = h
    => exts \lam x => isEpi g h d
} \where {
  \func fromLocalization {B R : CRing} {f : RingHom B R} (L : Localization {B} { | L => R | inL => f }) : RingLocalization \cowith
    | Localization => L

  \func liftHom1 {B R : CRing} {f : RingHom B R} {a : B} (L : Localization (powers a) R f) {T : CRing} (f : RingHom B T) (ai : Inv (f a)) : RingHom R T
    => (fromLocalization L).liftHom f \box (\lam {_} (inP (n,idp)) => transportInv Inv f.func-pow $ Inv.Inv_pow ai)
}

\instance LocRing {R : CRing} (S : SubMonoid R) : CRing \cowith
  | CMonoid => LocMonoid S
  | zro => in~ (zro, ide, contains_ide)
  | + (a b : LocType S) : LocType S \with {
    | in~ (r1,s1,p1), in~ (r2,s2,p2) => in~ (r1 * s2 R.+ r2 * s1, s1 * s2, contains_* p1 p2)
    | ~-equiv x y p, in~ z => ~-lequiv1 (equation.cRing {p})
    | in~ x, ~-equiv y z p => ~-lequiv1 (equation.cRing {p})
  }
  | zro-left {in~ _} => ~-lequiv1 simplify
  | +-assoc {in~ _} {in~ _} {in~ _} => ~-lequiv1 equation.cRing
  | +-comm {in~ _} {in~ _} => ~-lequiv1 equation.cRing
  | ldistr {in~ _} {in~ _} {in~ _} => ~-lequiv1 equation.cRing
  | negative (a : LocType S) : LocType S \with {
    | in~ (r,s,p) => in~ (R.negative r, s, p)
    | ~-equiv x y p => ~-lequiv1 (equation.cRing {p})
  }
  | negative-left {in~ _} => ~-lequiv1 simplify
  | natCoef n => in~ (R.natCoef n, 1, contains_ide)
  | natCoefZero => path (\lam i => in~ (R.natCoefZero i, 1, contains_ide))
  | natCoefSuc n => ~-lequiv1 $ simplify (R.natCoefSuc n)
  \where {
    \lemma isLocalization : RingLocalization S (LocRing S) locR \cowith
      | Localization => LocMonoid.isLocalization
  }

\lemma loc_unequals_domain {D : IntegralDomain} (S : SubMonoid D) (nz : \Pi (x : D) -> S x -> x /= 0) {a b : \Sigma (x y : D) (S y)} (p : inl~ a = inl~ b) : a.1 * b.2 = b.1 * a.2
  => \case ~-unlequiv p \with {
    | inP (c,c1,p) => Domain.nonZero-cancel-right (nz c c1) p
  }

\func locR {R : CRing} {S : SubMonoid R} : RingHom R (LocRing S) \cowith
  | MonoidHom => locM
  | func-+ => ~-lequiv1 $ path \lam i => (inv ide-right i + inv ide-right i) * ide-right i
  | func-* => ~-lequiv1 simplify

\lemma locR-isEpi {R : CRing} {S : SubMonoid R} {T : CRing} {g h : RingHom (LocRing S) T} (p : g RingHom.∘ locR = h RingHom.∘ locR) : g = h
  => exts \lam x => LocMonoid.isLocalization.isEpi g h \lam y => path \lam i => p i y

\lemma localization-zro-char {R : CRing} {S : SubMonoid R} {a : \Sigma (x y : R) (S y)} : (inl~ a = 0) <-> ∃ (c : R) (S c) (a.1 * c = 0)
  => (\case ~-unlequiv __ \with {
    | inP (c,Sc,p) => inP (c, Sc, simplify in p)
  }, \lam (inP (c,Sc,p)) => ~-lequiv c Sc (simplify p))

\instance FieldOfQuotients (D : IntegralDomain.Dec) : DiscreteField \cowith
  | CRing => LocRing D.subMonoid
  | zro/=ide p => \case LocMonoid.isLocalization.localization-inj p \with {
    | inP (c,c#0,q) => D.#0-zro $ transportInv D.#0 (simplify in q) c#0
  }
  | eitherZeroOrInv => \case \elim __ \with {
    | in~ x => \case decideEq x.1 0 \with {
      | yes e => byLeft $ ~-lequiv1 $ ide-right *> e *> inv D.zro_*-left
      | no q => byRight $ Inv.lmake (inl~ (x.2, x.1, AddGroup.nonZeroApart q)) $ unfold $ ~-lequiv1 (simplify *-comm)
    }
  }

\func LocalizationIdeal (I : Ideal) {R : CRing} (f : RingHom I.S R) {S : SubMonoid I.S} (L : Localization S R f) : Ideal R \cowith
  | contains a => ∃ (b : S.contains) (c : I.contains) (a * f b = f c)
  | contains_zro => inP (1, contains_ide, 0, contains_zro, R.zro_*-left *> inv func-zro)
  | contains_+ (inP (b,Sb,c,Ic,p)) (inP (b',Sb',c',Ic',p')) => inP (b * b', contains_* Sb Sb', c * b' + c' * b, contains_+ (ideal-right Ic) (ideal-right Ic'),
    R.rdistr *> pmap2 (+) (pmap (_ *) func-* *> inv *-assoc *> pmap (* _) p *> inv func-*) (pmap (_ *) (func-* *> *-comm) *> inv *-assoc *> pmap (* _) p' *> inv func-*) *> inv func-+)
  | ideal-left {r} (inP (b,Sb,c,Ic,p)) => \case L.localization-surj r \with {
    | inP (r',d,Sd,q) => inP (b * d, contains_* Sb Sd, r' * c, ideal-left Ic, pmap (_ *) func-* *> *-assoc *> pmap (_ *) (inv *-assoc *> pmap (* _) p *> *-comm) *> inv *-assoc *> pmap (* _) q *> inv func-*)
  }
  \where {
    \lemma unit-char (L : Localization S R f) : LocalizationIdeal I f L 1 <-> ∃ (x : I.S) (S x) (I x)
      => (\lam (inP (b,Sb,c,Ic,p)) => \case L.localization-inj (inv ide-left *> p) \with {
        | inP (d,Sd,bd=cd) => inP (b * d, contains_* Sb Sd, transportInv I bd=cd $ ideal-right Ic)
      }, \lam (inP (x,Sx,Ix)) => inP (x, Sx, x, Ix, ide-left))

    \lemma sclosure-char {T R : CRing} {U : T -> \Prop} {f : RingHom T R} {S : SubMonoid T} (L : Localization S R f) {x : R}
      : LocalizationIdeal (Ideal.sclosure U) f L x <-> Ideal.sclosure (SetIm f U) x
      => (\lam (inP (b,Sb,c,Uc,p)) => transportInv (Ideal.sclosure _) ((L.localization-inv Sb).rotate-inv-right p) $ ideal-right $ PseudoRingHom.func-Ideal_sclosure f Uc,
          Ideal.sclosure-univ $ SetIm-elim \lam {a} Ua => inP $ later (1, contains_ide, a, Ideal.sclosure-superset Ua, pmap (_ *) func-ide *> ide-right))
  }