\import Algebra.Group
\import Algebra.Group.Sub
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Ring.Poly
\import Algebra.Semiring.Sub
\import HLevel
\import Logic
\import Logic.Meta
\import Paths
\import Paths.Meta

\class SubRing \extends SubSemiring, SubAddGroup {
  \override S : Ring

  \func struct : Ring \cowith
    | Semiring => SubSemiring.struct
    | AbGroup => SubAddGroup.abStruct \this

  \func corestrict {R : Ring} (f : RingHom R S) (p : \Pi (x : R) -> contains (f x)) : RingHom R struct \cowith
    | func x => (f x, p x)
    | func-+ => ext f.func-+
    | func-ide => ext f.func-ide
    | func-* => ext f.func-*

  \func embed : RingHom struct S \cowith
    | func => __.
    | func-+ => idp
    | func-ide => idp
    | func-* => idp
} \where {
  \func cStruct {R : CRing} (S : SubRing R) : CRing \cowith
    | Ring => S.struct
    | *-comm => ext *-comm

  \func max {R : Ring} : SubRing \cowith
    | SubSemiring => SubSemiring.max {R}
    | SubAddGroup => SubAddGroup.max

  \lemma isContr {R : Ring} {S : SubRing R} (c : Contr R) : Contr S.struct \cowith
    | center => (c.center, rewrite (c.contraction ) contains_ide)
    | contraction x => ext (c.contraction _)

  \lemma comm-isContr {R : CRing} {S : SubRing R} (c : Contr R) : Contr (cStruct S) \cowith
    | center => (c.center, rewrite (c.contraction ) contains_ide)
    | contraction x => ext (c.contraction _)
}

\func ringHomImage (f : RingHom) : SubRing f.Cod \cowith
  | contains y => ∃ (x : f.Dom) (f x = y)
  | contains_zro => inP (, f.func-zro)
  | contains_+ (inP (x1,p1)) (inP (x2,p2)) => inP (x1 + x2, f.func-+ *> pmap2 (+) p1 p2)
  | contains_ide => inP (, f.func-ide)
  | contains_* (inP (x1,p1)) (inP (x2,p2)) => inP (x1 * x2, f.func-* *> pmap2 (*) p1 p2)
  | contains_negative (inP (x,p)) => inP (negative x, f.func-negative *> pmap negative p)