\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Localization
\import Algebra.Monoid.SubMonoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Graded
\import Algebra.Ring.Localization
\import Algebra.Ring.SubRing
\import Arith.Nat
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\open Monoid
\open SubMonoid

\func HomogenLocRing {R : GradedCRing} (S : SubMonoid R) : CRing
  => ICRing subRing
  \where {
    \func subRing : SubRing (LocRing S) \cowith
      | contains x => ∃ (y : \Sigma (x y : R) (S y)) (x = inl~ y) (n : Nat) (isHomogen y. n) (isHomogen y. n)
      | contains_zro => inP ((, , S.contains_ide), idp, , 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'. * y'. + y'. * x'., x'. * y'., contains_* x'. y'.), 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 ((, , S.contains_ide), idp, , 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'. * y'., x'. * y'., contains_* x'. y'.), 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'., x'., x'.), pmap negative x~x', n, R.homogen-negative x'1h, x'2h)

    \func fromSType (y : \Sigma (x y : R) (S y)) {n : Nat} (\property y1h : isHomogen y. n) (\property y2h : isHomogen y. 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])
      }

    \lemma homogen-Inv {S : SubMonoid R} (Sh : ∀ {y : S.contains} ∃ (k : Nat) (isHomogen y k)) {x : HomogenLocRing S} (xi : Inv x.) : Inv {HomogenLocRing S} x \elim x, xi
      | (_, inP (x,idp,n,x1h,x2h)), (in~ y, yp, _) => \case ~-unlequiv yp \with {
        | inP (c,Sc,cp) => \case Sh y., Sh Sc \with {
          | inP (y2n,y2h), inP (cn,ch) => \case R.homogen-factor (LDiv.make y. $ *-comm *> inv *-assoc *> (simplify in cp)) (inP (_, homogen-* (homogen-* y2h x2h) ch)) (inP (_, homogen-* x1h ch)) \with {
            | inP (z,zn,zh,zp) => \case R.degree-unique {y. * x. * c} {y2n + n + cn} {n + cn + zn} (homogen-* (homogen-* y2h x2h) ch) $ transportInv (isHomogen __ _) zp $ homogen-* (homogen-* x1h ch) zh \with {
              | inl q => Inv.lmake  $ ext $ LocRing.isLocalization.trivial-char R.zro_*-left   $ transport S q $ contains_* (contains_* y. x.) Sc
              | inr e => Inv.lmake (later (_, inP ((z, y., y.), idp, zn, zh, transport (isHomogen _) (NatSemiring.cancel-left cn $ +-comm *> NatSemiring.cancel-left n (inv +-assoc *> pmap (+ _) +-comm *> e *> +-assoc)) y2h))) $ ext $ ~-lequiv c Sc $ equation.cMonoid {zp}
            }
          }
        }
      }

    \lemma homogen-Inv1 {a : R} (ah : ∃ (k : Nat) (isHomogen a k)) {x : HomogenLocRing (powers a)} (xi : Inv x.) : Inv {HomogenLocRing (powers a)} x \elim ah
      | inP (k,ah) => homogen-Inv (later \lam {_} (inP (n,idp)) => inP (k * n, R.homogen-pow ah)) xi
  }