\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Ring.Factor
\import Algebra.Ring.RingCategory
\import Algebra.Ring.RingHom
\import Category
\import Category.Subcat
\import Function (IsInj, IsSurj)
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence

\func ringKerImageHom {R : CRing} {S : CRing} (f : RingHom R S) : RingHom (FactorRing (RingHom.KernelC f)) f.Image.IRing \cowith
  | func (x : FactorRing (RingHom.KernelC f)) : f.Image.IRing \with {
    | in~ a => (f a, inP (a, idp))
    | ~-equiv x y r => ext $ inv $ rewrite (zro-left, +-assoc, negative-left, zro-right) in pmap (S.`+ f y) (rewrite r in f.func-minus {x} {y})
  }
  | func-+ {x} {y} => \case \elim x, \elim y \with {
    | in~ x, in~ y => ext $ rewrite f.func-+ idp
  }
  | func-ide => ext f.func-ide
  | func-* {x} {y} => \case \elim x, \elim y \with {
    | in~ x, in~ y => ext $ rewrite f.func-* idp
  }
  \where \protected {
    \lemma isSurj : IsSurj (func {R} {S} {f})
      => \lam (x, inP (r, A)) => inP (in~ r, ext A)

    \lemma isInj : IsInj (func {R} {S} {f})
      => \lam {in~ a} {in~ a'} p => FactorRing.fequiv (unfold (rewrite (AddGroupHom.func-minus {f}) (AddGroup.toZero (pmap (\lam x => x.) p))))
  }

\lemma ringKerImageHom-iso {R S : CRing} (f : RingHom R S) : Iso {CRingCat} {FactorRing (RingHom.KernelC f)} {(RingHom.ImageC f).ICRing} (ringKerImageHom f)
  => subCat-iso.conv $ (RingCat.Iso<->Inj+Surj (ringKerImageHom f)). (ringKerImageHom.isInj, ringKerImageHom.isSurj)