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)
    snapply 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)
    srapply Quotient_rec2.
R: Ring
I: Ideal R
R -> R -> QuotientAbGroup R I
R: Ring
I: Ideal R
forall a a' b : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} a a' -> ?dclass a b = ?dclass a' b
R: Ring
I: Ideal R
forall a b b' : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} b b' -> ?dclass a b = ?dclass a b'
    -
R: Ring
I: Ideal R
R -> R -> QuotientAbGroup R I exact (fun x y => class_of _ (x * y)).
    -
R: Ring
I: Ideal R
forall a a' b : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} a a' ->
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) a b =
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) a' b intros x x' y p.
R: Ring
I: Ideal R
x, x', y: R
p: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x x'
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) x y =
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) x' y apply qglue.
R: Ring
I: Ideal R
x, x', y: 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 apply iscong.
    -
R: Ring
I: Ideal R
forall a b b' : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} b b' ->
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) a b =
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) a b' intros x y y' q.
R: Ring
I: Ideal R
x, y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) x y =
(fun x y : R =>
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |}) (x * y)) x y' apply qglue.
R: Ring
I: Ideal R
x, y, y': R
q: in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y y'
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} (x * y) (x * y') by apply 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 srapply Quotient_ind3_hprop; intros x y z.
R: Ring
I: Ideal R
x, y, z: R
(fun
   x y
    z : Quotient
          (in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |}) =>
 sg_op x (sg_op y z) = sg_op (sg_op x y) z)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
  (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
        |}) z)
      unfold mult, sg_op; simpl.
R: Ring
I: Ideal R
x, y, z: R
class_of (fun x y : R => I (sg_op (inv x) y))
  (x * (y * z)) =
class_of (fun x y : R => I (sg_op (inv x) y))
  (x * y * z)
      apply ap.
R: Ring
I: Ideal R
x, y, z: 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: snapply Quotient_ind_hprop; [exact _ | intro x].
R: Ring
I: Ideal R
x: R
(fun
   x : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) => sg_op mon_unit x = x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
R: Ring
I: Ideal R
x: R
(fun
   x : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := I;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup R I
            |}) => sg_op x mon_unit = x)
  (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 mult, sg_op; simpl.
R: Ring
I: Ideal R
x: R
class_of (fun x y : R => I (sg_op (inv x) y)) (1 * x) =
class_of (fun x y : R => I (sg_op (inv x) y)) x
R: Ring
I: Ideal R
x: R
class_of (fun x y : R => I (sg_op (inv x) y)) (x * 1) =
class_of (fun x y : R => I (sg_op (inv 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 srapply Quotient_ind3_hprop; intros x y z.
R: Ring
I: Ideal R
x, y, z: R
(fun
   x y
    z : Quotient
          (in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |}) => x * (y + z) = x * y + x * z)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
  (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
        |}) z)
      unfold sg_op, mult_is_sg_op, mult_quotient_group,
        plus, mult, plus_quotient_group; simpl.
R: Ring
I: Ideal R
x, y, z: R
class_of (fun x y : R => I (sg_op (inv x) y))
  (ring_mult x (sg_op y z)) =
class_of (fun x y : R => I (sg_op (inv x) y))
  (sg_op (ring_mult x y) (ring_mult x z))
      napply ap.
R: Ring
I: Ideal R
x, y, z: 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 srapply Quotient_ind3_hprop; intros x y z.
R: Ring
I: Ideal R
x, y, z: R
(fun
   x y
    z : Quotient
          (in_cosetL
             {|
               normalsubgroup_subgroup := I;
               normalsubgroup_isnormal :=
                 isnormal_ab_subgroup R I
             |}) => (x + y) * z = x * z + y * z)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := I;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup R I
        |}) x)
  (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
        |}) z)
      unfold sg_op, mult_is_sg_op, mult_quotient_group,
        plus, mult, plus_quotient_group; simpl.
R: Ring
I: Ideal R
x, y, z: R
class_of (fun x y : R => I (sg_op (inv x) y))
  (ring_mult (sg_op x y) z) =
class_of (fun x y : R => I (sg_op (inv x) y))
  (sg_op (ring_mult x z) (ring_mult y z))
      napply ap.
R: Ring
I: Ideal R
x, y, z: 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)
  snapply Build_RingHomomorphism'.
R: Ring
I: Ideal R
GroupHomomorphism R (R / I)
R: Ring
I: Ideal R
IsMonoidPreserving ?map
  1: exact grp_quotient_map.
R: Ring
I: Ideal R
IsMonoidPreserving grp_quotient_map
  repeat split.
Defined.

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 principles 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.

Definition QuotientRing_ind2_hprop {R : Ring} {I : Ideal R} (P : R / I -> R / I -> Type)
  `{forall x y, IsHProp (P x y)}
  (c : forall (x y : R), P (rng_quotient_map I x) (rng_quotient_map I y))
  : forall (r s : R / I), P r s
  := Quotient_ind2_hprop _ P c.

Definition QuotientRing_rec {R : Ring} {I : Ideal R} (S : Ring)
  (f : R $-> S) (H : forall x, I x -> f x = 0) 
  : R / I $-> S.
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
R / I $-> S
Proof.
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
R / I $-> S
  snapply Build_RingHomomorphism'.
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
GroupHomomorphism (R / I) S
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
IsMonoidPreserving ?map
  -
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
GroupHomomorphism (R / I) S snapply (grp_quotient_rec _ _ f).
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
forall n : R,
{|
  normalsubgroup_subgroup := I;
  normalsubgroup_isnormal := isnormal_ab_subgroup R I
|} n -> f n = mon_unit
    exact H.
  -
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
IsMonoidPreserving
  (grp_quotient_rec R
     {|
       normalsubgroup_subgroup := I;
       normalsubgroup_isnormal :=
         isnormal_ab_subgroup R I
     |} f H) split.
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
IsSemiGroupPreserving
  (grp_quotient_rec R
     {|
       normalsubgroup_subgroup := I;
       normalsubgroup_isnormal :=
         isnormal_ab_subgroup R I
     |} f H)
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
IsUnitPreserving
  (grp_quotient_rec R
     {|
       normalsubgroup_subgroup := I;
       normalsubgroup_isnormal :=
         isnormal_ab_subgroup R I
     |} f H)
    +
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
IsSemiGroupPreserving
  (grp_quotient_rec R
     {|
       normalsubgroup_subgroup := I;
       normalsubgroup_isnormal :=
         isnormal_ab_subgroup R I
     |} f H) srapply QuotientRing_ind2_hprop.
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
forall x y : R,
(fun r s : R / I =>
 grp_quotient_rec R
   {|
     normalsubgroup_subgroup := I;
     normalsubgroup_isnormal :=
       isnormal_ab_subgroup R I
   |} f H (sg_op r s) =
 sg_op
   (grp_quotient_rec R
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |} f H r)
   (grp_quotient_rec R
      {|
        normalsubgroup_subgroup := I;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup R I
      |} f H s)) (rng_quotient_map I x)
  (rng_quotient_map I y)
      napply rng_homo_mult.
    +
R: Ring
I: Ideal R
S: Ring
f: R $-> S
H: forall x : R, I x -> f x = 0
IsUnitPreserving
  (grp_quotient_rec R
     {|
       normalsubgroup_subgroup := I;
       normalsubgroup_isnormal :=
         isnormal_ab_subgroup R I
     |} f H) napply rng_homo_one.
Defined.

(** ** Quotient theory *)

(** 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
  snapply 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) srapply QuotientRing_ind2_hprop; intros x y.
H: Funext
A, B: Ring
f: A $-> B
x, y: A
(fun r s : A / ideal_kernel f =>
 abgroup_first_iso f (sg_op r s) =
 sg_op (abgroup_first_iso f r) (abgroup_first_iso f s))
  (rng_quotient_map (ideal_kernel f) x)
  (rng_quotient_map (ideal_kernel f) y)
    srapply path_sigma_hprop.
H: Funext
A, B: Ring
f: A $-> B
x, y: 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
  snapply 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 a b : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} a b <->
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} (?f a) (?f b)
    1: exact equiv_idmap.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
forall a b : R,
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} a b <->
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} (1%equiv a) (1%equiv b)
    intros x y; cbn.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
I (sg_op (inv x) y) <-> J (sg_op (inv 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 (inv 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 (inv 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 (inv x) y)))
  1,2: srapply Quotient_ind2_hprop; intros x y; rapply qglue.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} (1%equiv (sg_op x y))
  (sg_op (1%equiv x) (1%equiv y))
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} (1%equiv (x * y)) (1%equiv x * 1%equiv y)
  1: change (J ( - (x + y) + (x + y))).
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
J (- (x + y) + (x + y))
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} (1%equiv (x * y)) (1%equiv x * 1%equiv y)
  2: change (J (- ( x * y) + (x * y))).
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
J (- (x + y) + (x + y))
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
J (- (x * y) + x * y)
  1,2: rewrite rng_plus_negate_l.
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
J 0
R: Ring
I, J: Ideal R
p: (I ↔ J)%ideal
x, y: R
J 0
  1,2: apply ideal_in_zero.
Defined.

(** We phrase the first ring isomorphism theorem in a slightly different 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: exact (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: exact (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.