Require Import WildCat.Core WildCat.Equiv.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Algebra.Congruence.
Require Import Algebra.AbGroups.
Require Import Classes.interfaces.abstract_algebra.
Require Import Algebra.Rings.Ring.
Require Import Algebra.Rings.Ideal.

(** * Quotient Rings *)

(** In this file we define the quotient of a ring by an ideal. *)

Import Ideal.Notation.
Local Open Scope ring_scope.
Local Open Scope wc_iso_scope.

Section QuotientRing.

  Context (R : Ring) (I : Ideal R).

  Instance plus_quotient_group : Plus (QuotientAbGroup R I) := group_sgop.

  Instance iscong_mult_incosetL
    : @IsCongruence R ring_mult (in_cosetL I).
R: Ring
I: Ideal R
IsCongruence (in_cosetL I)
  Proof.
R: Ring
I: Ideal R
IsCongruence (in_cosetL I)
    snrapply Build_IsCongruence.
R: Ring
I: Ideal R
forall x x' y y' : R,
in_cosetL I x x' ->
in_cosetL I y y' ->
in_cosetL I (sg_op x y) (sg_op x' y')
    intros x x' y y' p q.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
in_cosetL I (sg_op x y) (sg_op x' y')
    change (I ( - (x * y) + (x' * y'))).
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I (- (x * y) + x' * y')
    rewrite <- (rng_plus_zero_l (x' * y')).
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I (- (x * y) + (0 + x' * y'))
    rewrite <- (rng_plus_negate_r (x' * y)).
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I (- (x * y) + (x' * y - x' * y + x' * y'))
    rewrite 2 rng_plus_assoc.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I (- (x * y) + x' * y - x' * y + x' * y')
    rewrite <- rng_mult_negate_l.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I (- x * y + x' * y - x' * y + x' * y')
    rewrite <- rng_dist_r.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I ((- x + x') * y - x' * y + x' * y')
    rewrite <- rng_plus_assoc.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I ((- x + x') * y + (- (x' * y) + x' * y'))
    rewrite <- rng_mult_negate_r.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I ((- x + x') * y + (x' * - y + x' * y'))
    rewrite <- rng_dist_l.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I ((- x + x') * y + x' * (- y + y'))
    rapply subgroup_in_op.
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I ((- x + x') * y)
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I (x' * (- y + y'))
    -
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I ((- x + x') * y) by rapply isrightideal.
    -
R: Ring
I: Ideal R
x, x', y, y': R
p: in_cosetL I x x'
q: in_cosetL I y y'
I (x' * (- y + y')) by rapply isleftideal.
  Defined.

  Instance mult_quotient_group : Mult (QuotientAbGroup R I).
R: Ring
I: Ideal R
Mult (QuotientAbGroup R I)
  Proof.
R: Ring
I: Ideal R
Mult (QuotientAbGroup R I)
    intro x.
R: Ring
I: Ideal R
x: QuotientAbGroup R I
QuotientAbGroup R I -> QuotientAbGroup R I
    srapply Quotient_rec.
R: Ring
I: Ideal R
x: QuotientAbGroup R I
R -> QuotientAbGroup R I
R: Ring
I: Ideal R
x: QuotientAbGroup R I
forall x0 y : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x0 y -> ?pclass x0 = ?pclass y
    {
R: Ring
I: Ideal R
x: QuotientAbGroup R I
R -> QuotientAbGroup R I intro y; revert x.
R: Ring
I: Ideal R
y: R
QuotientAbGroup R I -> QuotientAbGroup R I
      srapply Quotient_rec.
R: Ring
I: Ideal R
y: R
R -> QuotientAbGroup R I
R: Ring
I: Ideal R
y: R
forall x y0 : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x y0 -> ?pclass x = ?pclass y0
      {
R: Ring
I: Ideal R
y: R
R -> QuotientAbGroup R I intro x.
R: Ring
I: Ideal R
y, x: R
QuotientAbGroup R I
        apply class_of.
R: Ring
I: Ideal R
y, x: R
R
        exact (x * y). }
R: Ring
I: Ideal R
y: R
forall x y0 : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x y0 ->
(fun x0 : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x0 * y)) x =
(fun x0 : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x0 * y)) y0
      intros x x' p.
R: Ring
I: Ideal R
y, x, x': R
p: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x x'
(fun x : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) x =
(fun x : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) x'
      apply qglue.
R: Ring
I: Ideal R
y, x, x': R
p: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x x'
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} (x * y) (x' * y)
      by rapply iscong. }
R: Ring
I: Ideal R
x: QuotientAbGroup R I
forall x0 y : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x0 y ->
(fun y0 : R =>
 Quotient_rec
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (QuotientAbGroup R I)
   (fun x : R =>
    class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) (x * y0))
   (fun (x x' : R)
      (p : in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |} x x') =>
    qglue (iscong p (reflexive_in_cosetL I y0))) x) x0 =
(fun y0 : R =>
 Quotient_rec
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (QuotientAbGroup R I)
   (fun x : R =>
    class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) (x * y0))
   (fun (x x' : R)
      (p : in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |} x x') =>
    qglue (iscong p (reflexive_in_cosetL I y0))) x) y
    intros y y' q.
R: Ring
I: Ideal R
x: QuotientAbGroup R I
y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
(fun y : R =>
 Quotient_rec
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (QuotientAbGroup R I)
   (fun x : R =>
    class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) (x * y))
   (fun (x x' : R)
      (p : in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |} x x') =>
    qglue (iscong p (reflexive_in_cosetL I y))) x) y =
(fun y : R =>
 Quotient_rec
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (QuotientAbGroup R I)
   (fun x : R =>
    class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) (x * y))
   (fun (x x' : R)
      (p : in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |} x x') =>
    qglue (iscong p (reflexive_in_cosetL I y))) x) y'
    revert x.
R: Ring
I: Ideal R
y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
forall x : QuotientAbGroup R I,
(fun y : R =>
 Quotient_rec
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (QuotientAbGroup R I)
   (fun x0 : R =>
    class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) (x0 * y))
   (fun (x0 x' : R)
      (p : in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |} x0 x') =>
    qglue (iscong p (reflexive_in_cosetL I y))) x) y =
(fun y : R =>
 Quotient_rec
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (QuotientAbGroup R I)
   (fun x0 : R =>
    class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) (x0 * y))
   (fun (x0 x' : R)
      (p : in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |} x0 x') =>
    qglue (iscong p (reflexive_in_cosetL I y))) x) y'
    srapply Quotient_ind_hprop.
R: Ring
I: Ideal R
y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
forall x : R,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun y : R =>
  Quotient_rec
    (in_cosetL
       {|
         normalsubgroup_subgroup := I;
         normalsubgroup_isnormal :=
           isnormal_ab_subgroup R I
       |}) (QuotientAbGroup R I)
    (fun x0 : R =>
     class_of
       (in_cosetL
          {|
            normalsubgroup_subgroup := I;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup R I
          |}) (x0 * y))
    (fun (x0 x' : R)
       (p : in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |} x0 x') =>
     qglue (iscong p (reflexive_in_cosetL I y))) q) y =
 (fun y : R =>
  Quotient_rec
    (in_cosetL
       {|
         normalsubgroup_subgroup := I;
         normalsubgroup_isnormal :=
           isnormal_ab_subgroup R I
       |}) (QuotientAbGroup R I)
    (fun x0 : R =>
     class_of
       (in_cosetL
          {|
            normalsubgroup_subgroup := I;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup R I
          |}) (x0 * y))
    (fun (x0 x' : R)
       (p : in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |} x0 x') =>
     qglue (iscong p (reflexive_in_cosetL I y))) q) y')
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
    intro x.
R: Ring
I: Ideal R
y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
x: R
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun y : R =>
  Quotient_rec
    (in_cosetL
       {|
         normalsubgroup_subgroup := I;
         normalsubgroup_isnormal :=
           isnormal_ab_subgroup R I
       |}) (QuotientAbGroup R I)
    (fun x : R =>
     class_of
       (in_cosetL
          {|
            normalsubgroup_subgroup := I;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup R I
          |}) (x * y))
    (fun (x x' : R)
       (p : in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |} x x') =>
     qglue (iscong p (reflexive_in_cosetL I y))) q) y =
 (fun y : R =>
  Quotient_rec
    (in_cosetL
       {|
         normalsubgroup_subgroup := I;
         normalsubgroup_isnormal :=
           isnormal_ab_subgroup R I
       |}) (QuotientAbGroup R I)
    (fun x : R =>
     class_of
       (in_cosetL
          {|
            normalsubgroup_subgroup := I;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup R I
          |}) (x * y))
    (fun (x x' : R)
       (p : in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |} x x') =>
     qglue (iscong p (reflexive_in_cosetL I y))) q) y')
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
    simpl.
R: Ring
I: Ideal R
y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
x: R
class_of (fun x y : R => I (sg_op (- x) y)) (x * y) =
class_of (fun x y : R => I (sg_op (- x) y)) (x * y')
    apply qglue.
R: Ring
I: Ideal R
y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
x: R
I (sg_op (- (x * y)) (x * y'))
    by rapply iscong.
  Defined.

  Instance one_quotient_abgroup : One (QuotientAbGroup R I) := class_of _ one.

  Instance isring_quotient_abgroup : IsRing (QuotientAbGroup R I).
R: Ring
I: Ideal R
IsRing (QuotientAbGroup R I)
  Proof.
R: Ring
I: Ideal R
IsRing (QuotientAbGroup R I)
    split.
R: Ring
I: Ideal R
IsAbGroup (QuotientAbGroup R I)
R: Ring
I: Ideal R
IsMonoid (QuotientAbGroup R I)
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    1: exact _.
R: Ring
I: Ideal R
IsMonoid (QuotientAbGroup R I)
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    1: repeat split.
R: Ring
I: Ideal R
IsHSet (QuotientAbGroup R I)
R: Ring
I: Ideal R
Associative sg_op
R: Ring
I: Ideal R
LeftIdentity sg_op mon_unit
R: Ring
I: Ideal R
RightIdentity sg_op mon_unit
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    1: exact _.
R: Ring
I: Ideal R
Associative sg_op
R: Ring
I: Ideal R
LeftIdentity sg_op mon_unit
R: Ring
I: Ideal R
RightIdentity sg_op mon_unit
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    (** Associativity follows from the underlying operation *)
    {
R: Ring
I: Ideal R
Associative sg_op intros x y.
R: Ring
I: Ideal R
x, y: QuotientAbGroup R I
forall z : QuotientAbGroup R I,
sg_op x (sg_op y z) = sg_op (sg_op x y) z
      snrapply Quotient_ind_hprop; [exact _ | intro z; revert y].
R: Ring
I: Ideal R
x: QuotientAbGroup R I
z: R
forall y : QuotientAbGroup R I,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 sg_op x (sg_op y q) = sg_op (sg_op x y) q)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) z)
      snrapply Quotient_ind_hprop; [exact _ | intro y; revert x].
R: Ring
I: Ideal R
z, y: R
forall x : QuotientAbGroup R I,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun
    q0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |}) =>
  sg_op x (sg_op q q0) = sg_op (sg_op x q) q0)
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) z))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) y)
      snrapply Quotient_ind_hprop; [exact _ | intro x ].
R: Ring
I: Ideal R
z, y, x: R
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun
    q0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |}) =>
  (fun
     q1 : Quotient
            (in_cosetL
               {|
                 normalsubgroup_subgroup := I;
                 normalsubgroup_isnormal :=
                   isnormal_ab_subgroup R I
               |}) =>
   sg_op q (sg_op q0 q1) = sg_op (sg_op q q0) q1)
    (class_of
       (in_cosetL
          {|
            normalsubgroup_subgroup := I;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup R I
          |}) z))
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) y))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
      unfold sg_op, mult_is_sg_op, mult_quotient_group; simpl.
R: Ring
I: Ideal R
z, y, x: R
class_of (fun x y : R => I (sg_op (- x) y))
  (x * (y * z)) =
class_of (fun x y : R => I (sg_op (- x) y))
  (x * y * z)
      apply ap.
R: Ring
I: Ideal R
z, y, x: R
x * (y * z) = x * y * z
      apply associativity. }
R: Ring
I: Ideal R
LeftIdentity sg_op mon_unit
R: Ring
I: Ideal R
RightIdentity sg_op mon_unit
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    (* Left and right identity follow from the underlying structure *)
    1,2: snrapply Quotient_ind_hprop; [exact _ | intro x].
R: Ring
I: Ideal R
x: R
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) => sg_op mon_unit q = q)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
R: Ring
I: Ideal R
x: R
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) => sg_op q mon_unit = q)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    1-2: unfold sg_op, mult_is_sg_op, mult_quotient_group; simpl.
R: Ring
I: Ideal R
x: R
class_of (fun x y : R => I (sg_op (- x) y)) (1 * x) =
class_of (fun x y : R => I (sg_op (- x) y)) x
R: Ring
I: Ideal R
x: R
class_of (fun x y : R => I (sg_op (- x) y)) (x * 1) =
class_of (fun x y : R => I (sg_op (- x) y)) x
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    1-2: apply ap.
R: Ring
I: Ideal R
x: R
1 * x = x
R: Ring
I: Ideal R
x: R
x * 1 = x
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    1: apply left_identity.
R: Ring
I: Ideal R
x: R
x * 1 = x
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    1: apply right_identity.
R: Ring
I: Ideal R
LeftDistribute mult plus
R: Ring
I: Ideal R
RightDistribute mult plus
    (** Finally distributivity also follows *)
    {
R: Ring
I: Ideal R
LeftDistribute mult plus intros x y.
R: Ring
I: Ideal R
x, y: QuotientAbGroup R I
forall c : QuotientAbGroup R I,
x * (y + c) = x * y + x * c
      snrapply Quotient_ind_hprop; [exact _ | intro z; revert y].
R: Ring
I: Ideal R
x: QuotientAbGroup R I
z: R
forall y : QuotientAbGroup R I,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) => x * (y + q) = x * y + x * q)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) z)
      snrapply Quotient_ind_hprop; [exact _ | intro y; revert x].
R: Ring
I: Ideal R
z, y: R
forall x : QuotientAbGroup R I,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun
    q0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |}) => x * (q + q0) = x * q + x * q0)
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) z))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) y)
      snrapply Quotient_ind_hprop; [exact _ | intro x ].
R: Ring
I: Ideal R
z, y, x: R
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun
    q0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |}) =>
  (fun
     q1 : Quotient
            (in_cosetL
               {|
                 normalsubgroup_subgroup := I;
                 normalsubgroup_isnormal :=
                   isnormal_ab_subgroup R I
               |}) => q * (q0 + q1) = q * q0 + q * q1)
    (class_of
       (in_cosetL
          {|
            normalsubgroup_subgroup := I;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup R I
          |}) z))
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) y))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
      unfold sg_op, mult_is_sg_op, mult_quotient_group,
        plus, mult, plus_quotient_group; simpl.
R: Ring
I: Ideal R
z, y, x: R
class_of (fun x y : R => I (sg_op (- x) y))
  (ring_mult x (sg_op y z)) =
class_of (fun x y : R => I (sg_op (- x) y))
  (sg_op (ring_mult x y) (ring_mult x z))
      apply ap.
R: Ring
I: Ideal R
z, y, x: R
ring_mult x (sg_op y z) =
sg_op (ring_mult x y) (ring_mult x z)
      apply simple_distribute_l. }
R: Ring
I: Ideal R
RightDistribute mult plus
    {
R: Ring
I: Ideal R
RightDistribute mult plus intros x y.
R: Ring
I: Ideal R
x, y: QuotientAbGroup R I
forall c : QuotientAbGroup R I,
(x + y) * c = x * c + y * c
      snrapply Quotient_ind_hprop; [exact _ | intro z; revert y].
R: Ring
I: Ideal R
x: QuotientAbGroup R I
z: R
forall y : QuotientAbGroup R I,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) => (x + y) * q = x * q + y * q)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) z)
      snrapply Quotient_ind_hprop; [exact _ | intro y; revert x].
R: Ring
I: Ideal R
z, y: R
forall x : QuotientAbGroup R I,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun
    q0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |}) => (x + q) * q0 = x * q0 + q * q0)
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) z))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) y)
      snrapply Quotient_ind_hprop; [exact _ | intro x ].
R: Ring
I: Ideal R
z, y, x: R
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) =>
 (fun
    q0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := I;
                normalsubgroup_isnormal :=
                  isnormal_ab_subgroup R I
              |}) =>
  (fun
     q1 : Quotient
            (in_cosetL
               {|
                 normalsubgroup_subgroup := I;
                 normalsubgroup_isnormal :=
                   isnormal_ab_subgroup R I
               |}) => (q + q0) * q1 = q * q1 + q0 * q1)
    (class_of
       (in_cosetL
          {|
            normalsubgroup_subgroup := I;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup R I
          |}) z))
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := I;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup R I
         |}) y))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
      unfold sg_op, mult_is_sg_op, mult_quotient_group,
        plus, mult, plus_quotient_group; simpl.
R: Ring
I: Ideal R
z, y, x: R
class_of (fun x y : R => I (sg_op (- x) y))
  (ring_mult (sg_op x y) z) =
class_of (fun x y : R => I (sg_op (- x) y))
  (sg_op (ring_mult x z) (ring_mult y z))
      apply ap.
R: Ring
I: Ideal R
z, y, x: R
ring_mult (sg_op x y) z =
sg_op (ring_mult x z) (ring_mult y z)
      apply simple_distribute_r. }
  Defined.

  Definition QuotientRing : Ring 
    := Build_Ring (QuotientAbGroup R I) _ _ _ _ _.

End QuotientRing.

Infix "/" := QuotientRing : ring_scope.

(** Quotient map *)
Definition rng_quotient_map {R : Ring} (I : Ideal R)
  : RingHomomorphism R (R / I).
R: Ring
I: Ideal R
RingHomomorphism R (R / I)
Proof.
R: Ring
I: Ideal R
RingHomomorphism R (R / I)
  snrapply Build_RingHomomorphism'.
R: Ring
I: Ideal R
GroupHomomorphism R (R / I)
R: Ring
I: Ideal R
IsMonoidPreserving ?map
  1: rapply grp_quotient_map.
R: Ring
I: Ideal R
IsMonoidPreserving grp_quotient_map
  repeat split.
Defined.

Global Instance issurj_rng_quotient_map {R : Ring} (I : Ideal R)
  : IsSurjection (rng_quotient_map I).
R: Ring
I: Ideal R
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (rng_quotient_map I)
Proof.
R: Ring
I: Ideal R
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (rng_quotient_map I)
  exact _.
Defined.

(** *** Specialized induction principles *)

(** We provide some specialized induction principes for [QuotientRing] that require cleaner hypotheses than the ones given by [Quotient_ind]. *)
Definition QuotientRing_ind {R : Ring} {I : Ideal R} (P : R / I -> Type)
  `{forall x, IsHSet (P x)}
  (c : forall (x : R), P (rng_quotient_map I x))
  (g : forall (x y : R) (h : I (- x + y)), qglue h # c x = c y)
  : forall (r : R / I), P r
  := Quotient_ind _ P c g.

(** And a version eliminating into hprops. This one is especially useful. *)
Definition QuotientRing_ind_hprop {R : Ring} {I : Ideal R} (P : R / I -> Type)
  `{forall x, IsHProp (P x)} (c : forall (x : R), P (rng_quotient_map I x))
  : forall (r : R / I), P r
  := Quotient_ind_hprop _ P c.

(** ** Quotient thoery *)

(** First isomorphism theorem for commutative rings *)
Definition rng_first_iso `{Funext} {A B : Ring} (f : A $-> B)
  : A / ideal_kernel f ≅ rng_image f.
H: Funext
A, B: Ring
f: A $-> B
A / ideal_kernel f ≅ rng_image f
Proof.
H: Funext
A, B: Ring
f: A $-> B
A / ideal_kernel f ≅ rng_image f
  snrapply Build_RingIsomorphism''.
H: Funext
A, B: Ring
f: A $-> B
GroupIsomorphism (A / ideal_kernel f) (rng_image f)
H: Funext
A, B: Ring
f: A $-> B
IsMonoidPreserving ?e
  1: rapply abgroup_first_iso.
H: Funext
A, B: Ring
f: A $-> B
IsMonoidPreserving (abgroup_first_iso f)
  split.
H: Funext
A, B: Ring
f: A $-> B
IsSemiGroupPreserving (abgroup_first_iso f)
H: Funext
A, B: Ring
f: A $-> B
IsUnitPreserving (abgroup_first_iso f)
  {
H: Funext
A, B: Ring
f: A $-> B
IsSemiGroupPreserving (abgroup_first_iso f) intros x y.
H: Funext
A, B: Ring
f: A $-> B
x, y: A / ideal_kernel f
abgroup_first_iso f (sg_op x y) =
sg_op (abgroup_first_iso f x) (abgroup_first_iso f y)
    revert y; srapply QuotientRing_ind_hprop; intros y.
H: Funext
A, B: Ring
f: A $-> B
x: A / ideal_kernel f
y: A
(fun r : A / ideal_kernel f =>
 abgroup_first_iso f (sg_op x r) =
 sg_op (abgroup_first_iso f x) (abgroup_first_iso f r))
  (rng_quotient_map (ideal_kernel f) y)
    revert x; srapply QuotientRing_ind_hprop; intros x.
H: Funext
A, B: Ring
f: A $-> B
y, x: A
(fun r : A / ideal_kernel f =>
 (fun r0 : A / ideal_kernel f =>
  abgroup_first_iso f (sg_op r r0) =
  sg_op (abgroup_first_iso f r)
    (abgroup_first_iso f r0))
   (rng_quotient_map (ideal_kernel f) y))
  (rng_quotient_map (ideal_kernel f) x)
    srapply path_sigma_hprop.
H: Funext
A, B: Ring
f: A $-> B
y, x: A
(abgroup_first_iso f
   (sg_op (rng_quotient_map (ideal_kernel f) x)
      (rng_quotient_map (ideal_kernel f) y))).1 =
(sg_op
   (abgroup_first_iso f
      (rng_quotient_map (ideal_kernel f) x))
   (abgroup_first_iso f
      (rng_quotient_map (ideal_kernel f) y))).1
    exact (rng_homo_mult _ _ _). }
H: Funext
A, B: Ring
f: A $-> B
IsUnitPreserving (abgroup_first_iso f)
  srapply path_sigma_hprop.
H: Funext
A, B: Ring
f: A $-> B
(abgroup_first_iso f mon_unit).1 = mon_unit.1
  exact (rng_homo_one _).
Defined.

(** Invariance of equal ideals *)
Lemma rng_quotient_invar {R : Ring} {I J : Ideal R} (p : (I ↔ J)%ideal)
  : R / I ≅ R / J.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
R / I ≅ R / J
Proof.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
R / I ≅ R / J
  snrapply Build_RingIsomorphism'.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
R / I <~> R / J
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
IsSemiRingPreserving ?e
  {
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
R / I <~> R / J srapply equiv_quotient_functor'.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
R <~> R
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
forall x y : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x y <->
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} (?f x) (?f y)
    1: exact equiv_idmap.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
forall x y : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x y <->
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} (1%equiv x) (1%equiv y)
    intros x y; cbn.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
I (sg_op (- x) y) <-> J (sg_op (- x) y)
    apply p. }
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
IsSemiRingPreserving
  (equiv_quotient_functor'
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |})
     (in_cosetL
        {|
          normalsubgroup_subgroup := J;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R J
        |}) 1
     (fun x y : R =>
      p (sg_op (- x) y)
      :
      in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |} x y <->
      in_cosetL
        {|
          normalsubgroup_subgroup := J;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R J
        |} (1%equiv x) (1%equiv y)))
  repeat split.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
IsSemiGroupPreserving
  (equiv_quotient_functor'
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |})
     (in_cosetL
        {|
          normalsubgroup_subgroup := J;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R J
        |}) 1 (fun x y : R => p (sg_op (- x) y)))
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
IsSemiGroupPreserving
  (equiv_quotient_functor'
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |})
     (in_cosetL
        {|
          normalsubgroup_subgroup := J;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R J
        |}) 1 (fun x y : R => p (sg_op (- x) y)))
  1,2: intros x; simpl.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x: R / I
forall
y : Quotient (fun x y : R => I (sg_op (- x) y)),
Quotient_functor (fun x y0 : R => I (sg_op (- x) y0))
  (fun x y0 : R => J (sg_op (- x) y0)) idmap
  (fun x y0 : R => fst (p (sg_op (- x) y0)))
  (sg_op x y) =
sg_op
  (Quotient_functor
     (fun x y0 : R => I (sg_op (- x) y0))
     (fun x y0 : R => J (sg_op (- x) y0)) idmap
     (fun x y0 : R => fst (p (sg_op (- x) y0))) x)
  (Quotient_functor
     (fun x y0 : R => I (sg_op (- x) y0))
     (fun x y0 : R => J (sg_op (- x) y0)) idmap
     (fun x y0 : R => fst (p (sg_op (- x) y0))) y)
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x: R / I
forall
y : Quotient (fun x y : R => I (sg_op (- x) y)),
Quotient_functor (fun x y0 : R => I (sg_op (- x) y0))
  (fun x y0 : R => J (sg_op (- x) y0)) idmap
  (fun x y0 : R => fst (p (sg_op (- x) y0)))
  (sg_op x y) =
sg_op
  (Quotient_functor
     (fun x y0 : R => I (sg_op (- x) y0))
     (fun x y0 : R => J (sg_op (- x) y0)) idmap
     (fun x y0 : R => fst (p (sg_op (- x) y0))) x)
  (Quotient_functor
     (fun x y0 : R => I (sg_op (- x) y0))
     (fun x y0 : R => J (sg_op (- x) y0)) idmap
     (fun x y0 : R => fst (p (sg_op (- x) y0))) y)
  1,2: srapply QuotientRing_ind_hprop.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x: R / I
forall x0 : R,
(fun r : R / I =>
 Quotient_functor (fun x y : R => I (sg_op (- x) y))
   (fun x y : R => J (sg_op (- x) y)) idmap
   (fun x y : R => fst (p (sg_op (- x) y)))
   (sg_op x r) =
 sg_op
   (Quotient_functor
      (fun x y : R => I (sg_op (- x) y))
      (fun x y : R => J (sg_op (- x) y)) idmap
      (fun x y : R => fst (p (sg_op (- x) y))) x)
   (Quotient_functor
      (fun x y : R => I (sg_op (- x) y))
      (fun x y : R => J (sg_op (- x) y)) idmap
      (fun x y : R => fst (p (sg_op (- x) y))) r))
  (rng_quotient_map I x0)
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x: R / I
forall x0 : R,
(fun r : R / I =>
 Quotient_functor (fun x y : R => I (sg_op (- x) y))
   (fun x y : R => J (sg_op (- x) y)) idmap
   (fun x y : R => fst (p (sg_op (- x) y)))
   (sg_op x r) =
 sg_op
   (Quotient_functor
      (fun x y : R => I (sg_op (- x) y))
      (fun x y : R => J (sg_op (- x) y)) idmap
      (fun x y : R => fst (p (sg_op (- x) y))) x)
   (Quotient_functor
      (fun x y : R => I (sg_op (- x) y))
      (fun x y : R => J (sg_op (- x) y)) idmap
      (fun x y : R => fst (p (sg_op (- x) y))) r))
  (rng_quotient_map I x0)
  1,2: intros y; revert x.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y: R
forall x : R / I,
(fun r : R / I =>
 Quotient_functor (fun x0 y : R => I (sg_op (- x0) y))
   (fun x0 y : R => J (sg_op (- x0) y)) idmap
   (fun x0 y : R => fst (p (sg_op (- x0) y)))
   (sg_op x r) =
 sg_op
   (Quotient_functor
      (fun x0 y : R => I (sg_op (- x0) y))
      (fun x0 y : R => J (sg_op (- x0) y)) idmap
      (fun x0 y : R => fst (p (sg_op (- x0) y))) x)
   (Quotient_functor
      (fun x0 y : R => I (sg_op (- x0) y))
      (fun x0 y : R => J (sg_op (- x0) y)) idmap
      (fun x0 y : R => fst (p (sg_op (- x0) y))) r))
  (rng_quotient_map I y)
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y: R
forall x : R / I,
(fun r : R / I =>
 Quotient_functor (fun x0 y : R => I (sg_op (- x0) y))
   (fun x0 y : R => J (sg_op (- x0) y)) idmap
   (fun x0 y : R => fst (p (sg_op (- x0) y)))
   (sg_op x r) =
 sg_op
   (Quotient_functor
      (fun x0 y : R => I (sg_op (- x0) y))
      (fun x0 y : R => J (sg_op (- x0) y)) idmap
      (fun x0 y : R => fst (p (sg_op (- x0) y))) x)
   (Quotient_functor
      (fun x0 y : R => I (sg_op (- x0) y))
      (fun x0 y : R => J (sg_op (- x0) y)) idmap
      (fun x0 y : R => fst (p (sg_op (- x0) y))) r))
  (rng_quotient_map I y)
  1,2: srapply QuotientRing_ind_hprop.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y: R
forall x : R,
(fun r : R / I =>
 (fun r0 : R / I =>
  Quotient_functor
    (fun x0 y : R => I (sg_op (- x0) y))
    (fun x0 y : R => J (sg_op (- x0) y)) idmap
    (fun x0 y : R => fst (p (sg_op (- x0) y)))
    (sg_op r r0) =
  sg_op
    (Quotient_functor
       (fun x0 y : R => I (sg_op (- x0) y))
       (fun x0 y : R => J (sg_op (- x0) y)) idmap
       (fun x0 y : R => fst (p (sg_op (- x0) y))) r)
    (Quotient_functor
       (fun x0 y : R => I (sg_op (- x0) y))
       (fun x0 y : R => J (sg_op (- x0) y)) idmap
       (fun x0 y : R => fst (p (sg_op (- x0) y))) r0))
   (rng_quotient_map I y)) (rng_quotient_map I x)
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y: R
forall x : R,
(fun r : R / I =>
 (fun r0 : R / I =>
  Quotient_functor
    (fun x0 y : R => I (sg_op (- x0) y))
    (fun x0 y : R => J (sg_op (- x0) y)) idmap
    (fun x0 y : R => fst (p (sg_op (- x0) y)))
    (sg_op r r0) =
  sg_op
    (Quotient_functor
       (fun x0 y : R => I (sg_op (- x0) y))
       (fun x0 y : R => J (sg_op (- x0) y)) idmap
       (fun x0 y : R => fst (p (sg_op (- x0) y))) r)
    (Quotient_functor
       (fun x0 y : R => I (sg_op (- x0) y))
       (fun x0 y : R => J (sg_op (- x0) y)) idmap
       (fun x0 y : R => fst (p (sg_op (- x0) y))) r0))
   (rng_quotient_map I y)) (rng_quotient_map I x)
  1,2: intros x; rapply qglue.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J (sg_op (- sg_op x y) (sg_op x y))
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J (sg_op (- (x * y)) (x * y))
  1: change (J ( - (x + y) + (x + y))).
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J (- (x + y) + (x + y))
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J (sg_op (- (x * y)) (x * y))
  2: change (J (- ( x * y) + (x * y))).
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J (- (x + y) + (x + y))
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J (- (x * y) + x * y)
  1,2: rewrite rng_plus_negate_l.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J 0
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
y, x: R
J 0
  1,2: apply ideal_in_zero.
Defined.

(** We phrase the first ring isomorphism theroem in a slightly differnt way so that it is easier to use. This form specifically asks for a surjective map *)
Definition rng_first_iso' `{Funext} {A B : Ring} (f : A $-> B)
  (issurj_f : IsSurjection f)
  (I : Ideal A) (p : (I ↔ ideal_kernel f)%ideal)
  : A / I ≅ B.
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
A / I ≅ B
Proof.
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
A / I ≅ B
  etransitivity.
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
A / I ≅ ?Goal
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
?Goal ≅ B
  1: apply (rng_quotient_invar p).
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
A / ideal_kernel f ≅ B
  etransitivity.
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
A / ideal_kernel f ≅ ?Goal
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
?Goal ≅ B
  2: rapply (rng_image_issurj f).
H: Funext
A, B: Ring
f: A $-> B
issurj_f: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
I: Ideal A
p: (I ↔ ideal_kernel f)%ideal
A / ideal_kernel f ≅ rng_image f
  apply rng_first_iso.
Defined.