Localization

\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Monoid.Sub
\import Algebra.Ring
\import Algebra.Ring.Graded
\import Algebra.Ring.Localization
\import Algebra.Ring.Sub
\import Arith.Nat
\import Function.Meta
\import Logic
\import Logic.Meta
\import Paths
\import Paths.Meta

\func HomogenLocRing {R : GradedCRing} (S : SubMonoid R) : CRing
  => SubRing.cStruct subRing
  \where {
    \func subRing : SubRing (LocRing S) \cowith
      | contains x => ∃ (y : LocRing.SType S) (x = inl~ y) (n : Nat) (isHomogen y.1 n) (isHomogen y.2 n)
      | contains_zro => inP ((0, 1, S.contains_ide), idp, 0, homogen-zro, R.homogen-ide)
      | contains_+ (inP (x',x~x',n,x'1h,x'2h)) (inP (y',y~y',m,y'1h,y'2h)) => inP ((x'.1 * y'.2 + y'.1 * x'.2, x'.2 * y'.2, contains_* x'.3 y'.3), pmap2 (+) x~x' y~y', n + m, homogen-+ (homogen-* x'1h y'2h) (rewrite NatSemiring.+-comm $ homogen-* y'1h x'2h), homogen-* x'2h y'2h)
      | contains_ide => inP ((1, 1, S.contains_ide), idp, 0, R.homogen-ide, R.homogen-ide)
      | contains_* (inP (x',x~x',n,x'1h,x'2h)) (inP (y',y~y',m,y'1h,y'2h)) => inP ((x'.1 * y'.1, x'.2 * y'.2, contains_* x'.3 y'.3), pmap2 (*) x~x' y~y', n + m, homogen-* x'1h y'1h, homogen-* x'2h y'2h)
      | contains_negative (inP (x',x~x',n,x'1h,x'2h)) => inP ((negative x'.1, x'.2, x'.3), pmap negative x~x', n, R.homogen-negative x'1h, x'2h)

    \func fromSType (y : LocRing.SType S) {n : Nat} (\property y1h : isHomogen y.1 n) (\property y2h : isHomogen y.2 n) : HomogenLocRing S
      => (inl~ y, inP (y, idp, n, y1h, y2h))
      \where {
        \lemma equality (x : LocRing S) (x=[y] : x = inl~ y) : fromSType y y1h y2h = (x, inP (y,x=[y],n,y1h,y2h))
          => ext (inv x=[y])
      }
  }