Require Import Classes.interfaces.canonical_names.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.
Require Import Modalities.ReflectiveSubuniverse.
Require Import Algebra.AbGroups.
Require Import Algebra.Rings.Ring.
Require Import Algebra.Rings.Ideal.
Require Import Algebra.Rings.QuotientRing.
Require Import Algebra.Rings.CRing.

(** * Chinese remainder theorem *)

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

Section ChineseRemainderTheorem.

  (** We assume [Univalence] in order to work with quotients. We also need it for [Funext] in a few places.*)
  Context `{Univalence}
    (** We need two coprime ideals [I] and [J] to state the theorem. We don't introduce the coprimeness assumption as of yet in order to show something slightly stronger. *)
    {R : Ring} (I J : Ideal R).

  (** We begin with the homomorphism which will show to be a surjection. Using the first isomorphism theorem for rings we can improve this to be the isomorphism we want. *)
  (** This is the corecursion of the two quotient maps *)
  Definition rng_homo_crt : R $-> (R / I) × (R / J).
H: Univalence
R: Ring
I, J: Ideal R
R $-> R / I × (R / J)
  Proof.
H: Univalence
R: Ring
I, J: Ideal R
R $-> R / I × (R / J)
    apply ring_product_corec.
H: Univalence
R: Ring
I, J: Ideal R
R $-> R / I
H: Univalence
R: Ring
I, J: Ideal R
R $-> R / J
    1,2: apply rng_quotient_map.
  Defined.

  (** Since we are working with quotients, we make the following notation to make working with the proof somewhat easier. *)
  Local Notation "[ x ]" := (rng_quotient_map _ x).

  (** We then need to prove the following lemma. The hypotheses here can be derived by coprimality of [I] and [J]. But we don't need that here. *)
  Lemma issurjection_rng_homo_crt' (x y : R)
    (q1 : rng_homo_crt x = (0, 1)) (q2 : rng_homo_crt y = (1, 0))
    : IsSurjection rng_homo_crt.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
IsConnMap (Tr (-1)) rng_homo_crt
  Proof.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
IsConnMap (Tr (-1)) rng_homo_crt
    (** In order to show that [rng_homo_crt] is a surjection, we need to show that its propositional truncation of the fiber at any point is contractible. *)
    intros [a b].
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a: R / I
b: R / J
IsConnected (Tr (-1)) (hfiber rng_homo_crt (a, b))
    revert a; srapply QuotientRing_ind_hprop; intro a.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
b: R / J
a: R
(fun r : R / I =>
 IsConnected (Tr (-1)) (hfiber rng_homo_crt (r, b)))
  [a]
    revert b; srapply QuotientRing_ind_hprop; intro b.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
(fun r : R / J =>
 (fun r0 : R / I =>
  IsConnected (Tr (-1)) (hfiber rng_homo_crt (r0, r)))
   [a]) [b]
    (** We can think of [a] and [b] as the pair [(a mod I, b mod J)]. We need to show that there merely exists some element in [R] that gets mapped by  [rng_homo_crt] to the pair. *)
    snrapply Build_Contr; [|intros z; strip_truncations; apply path_ishprop].
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
Tr (-1) (hfiber rng_homo_crt ([a], [b]))
    (** We make this choice and show it maps as desired. *)
    apply tr; exists (b * x + a * y).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
rng_homo_crt (b * x + a * y) = ([a], [b])
    (** Finally using some simple ring laws we can show it maps to our pair. *)
    rewrite rng_homo_plus.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
rng_homo_crt (b * x) + rng_homo_crt (a * y) =
([a], [b])
    rewrite 2 rng_homo_mult.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
rng_homo_crt b * rng_homo_crt x +
rng_homo_crt a * rng_homo_crt y = ([a], [b])
    rewrite q1, q2.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
rng_homo_crt b * (0, 1) + rng_homo_crt a * (1, 0) =
([a], [b])
    apply path_prod.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
fst
  (rng_homo_crt b * (0, 1) + rng_homo_crt a * (1, 0)) =
fst ([a], [b])
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
snd
  (rng_homo_crt b * (0, 1) + rng_homo_crt a * (1, 0)) =
snd ([a], [b])
    +
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
fst
  (rng_homo_crt b * (0, 1) + rng_homo_crt a * (1, 0)) =
fst ([a], [b]) change ([b] * 0 + [a] * 1 = [a] :> R / I).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
[b] * 0 + [a] * 1 = [a]
      by rewrite rng_mult_one_r, rng_mult_zero_r, rng_plus_zero_l.
    +
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
snd
  (rng_homo_crt b * (0, 1) + rng_homo_crt a * (1, 0)) =
snd ([a], [b]) change ([b] * 1 + [a] * 0 = [b] :> R / J).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
q1: rng_homo_crt x = (0, 1)
q2: rng_homo_crt y = (1, 0)
a, b: R
[b] * 1 + [a] * 0 = [b]
      by rewrite rng_mult_one_r, rng_mult_zero_r, rng_plus_zero_r.
  Defined.

  (** Now we show that if [x + y = 1] for [I x] and [J y] then we can satisfy the hypotheses of the previous lemma. *)
  Section rng_homo_crt_beta.

    Context (x y : R) (ix : I x) (iy : J y) (p : x + y = 1).

    Lemma rng_homo_crt_beta_left : rng_homo_crt x = (0, 1).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x + y = 1
rng_homo_crt x = (0, 1)
    Proof.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x + y = 1
rng_homo_crt x = (0, 1)
      apply rng_moveR_Mr in p.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = - x + 1
rng_homo_crt x = (0, 1)
      rewrite rng_plus_comm in p.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
rng_homo_crt x = (0, 1)
      apply path_prod; apply qglue.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x mon_unit
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} x 1
      -
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} x mon_unit change (I (-x + 0)).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
I (- x + 0)
        apply ideal_in_negate_plus.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
I x
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
I 0
        1: assumption.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
I 0
        apply ideal_in_zero.
      -
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} x 1 change (J (-x + 1)).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
J (- x + 1)
        rewrite rng_plus_comm.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: y = 1 - x
J (1 - x)
        by rewrite <- p.
    Defined.

    Lemma rng_homo_crt_beta_right : rng_homo_crt y = (1, 0).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x + y = 1
rng_homo_crt y = (1, 0)
    Proof.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x + y = 1
rng_homo_crt y = (1, 0)
      apply rng_moveR_rM in p.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = 1 - y
rng_homo_crt y = (1, 0)
      rewrite rng_plus_comm in p.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
rng_homo_crt y = (1, 0)
      apply path_prod; apply qglue.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y 1
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} y mon_unit
      -
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} y 1 change (I (-y + 1)).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
I (- y + 1)
        by rewrite <- p.
      -
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} y mon_unit change (J (-y + 0)).
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
J (- y + 0)
        apply ideal_in_negate_plus.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
J y
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
J 0
        1: assumption.
H: Univalence
R: Ring
I, J: Ideal R
x, y: R
ix: I x
iy: J y
p: x = - y + 1
J 0
        apply ideal_in_zero.
    Defined.

  End rng_homo_crt_beta.

  (** We can now show the map is surjective from coprimality of [I] and [J]. *)
  Global Instance issurjection_rng_homo_crt
    : Coprime I J -> IsSurjection rng_homo_crt.
H: Univalence
R: Ring
I, J: Ideal R
Coprime I J -> IsConnMap (Tr (-1)) rng_homo_crt
  Proof.
H: Univalence
R: Ring
I, J: Ideal R
Coprime I J -> IsConnMap (Tr (-1)) rng_homo_crt
    intros c.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
IsConnMap (Tr (-1)) rng_homo_crt
    (** First we turn the coprimality assumption into an equivalent assumption about the mere existence of two elements of each ideal which sum to one. *)
    apply equiv_coprime_sum in c.
H: Univalence
R: Ring
I, J: Ideal R
c: hexists
  (fun pat : {x : _ & I x} * {x : _ & J x} =>
   let x := pat in
   let fst := fst x in
   let snd := snd x in
   let fst0 := fst in
   let i := fst0.1 in
   let p := fst0.2 in
   let snd0 := snd in
   let j := snd0.1 in
   let q := snd0.2 in i + j = ring_one)
IsConnMap (Tr (-1)) rng_homo_crt
    (** Since the goal is a hprop we may strip the truncations. *)
    strip_truncations.
H: Univalence
R: Ring
I, J: Ideal R
c: {pat : {x : _ & I x} * {x : _ & J x} &
let x := pat in
let fst := fst x in
let snd := snd x in
let fst0 := fst in
let i := fst0.1 in
let p := fst0.2 in
let snd0 := snd in
let j := snd0.1 in
let q := snd0.2 in i + j = ring_one}
IsConnMap (Tr (-1)) rng_homo_crt
    (** Now we can break apart the data of this witness. *)
    destruct c as [[[x ix] [y jy]] p];
    change (x + y = 1) in p.
H: Univalence
R: Ring
I, J: Ideal R
x: R
ix: I x
y: R
jy: J y
p: x + y = 1
IsConnMap (Tr (-1)) rng_homo_crt
    (** Now we apply all our previous lemmas *)
    apply (issurjection_rng_homo_crt' x y).
H: Univalence
R: Ring
I, J: Ideal R
x: R
ix: I x
y: R
jy: J y
p: x + y = 1
rng_homo_crt x = (0, 1)
H: Univalence
R: Ring
I, J: Ideal R
x: R
ix: I x
y: R
jy: J y
p: x + y = 1
rng_homo_crt y = (1, 0)
    1: exact (rng_homo_crt_beta_left x y ix jy p).
H: Univalence
R: Ring
I, J: Ideal R
x: R
ix: I x
y: R
jy: J y
p: x + y = 1
rng_homo_crt y = (1, 0)
    exact (rng_homo_crt_beta_right x y ix jy p).
  Defined.

  (** Now suppose [I] and [J] are coprime. *)
  Context (c : Coprime I J).

  (** The Chinese Remainder Theorem *)
  Theorem chinese_remainder : R / (I ∩ J)%ideal ≅ (R / I) × (R / J).
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
R / (I ∩ J)%ideal ≅ R / I × (R / J)
  Proof.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
R / (I ∩ J)%ideal ≅ R / I × (R / J)
    (** We use the first isomorphism theorem. Coq can already infer which map we wish to use, so for clarity we tell it not to do so. *)
    snrapply rng_first_iso'.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
R $-> R / I × (R / J)
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
IsConnMap (Tr (-1)) ?f
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
(I ∩ J ↔ ideal_kernel ?f)%ideal
    1: rapply rng_homo_crt.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
IsConnMap (Tr (-1)) rng_homo_crt
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
(I ∩ J ↔ ideal_kernel rng_homo_crt)%ideal
    1: exact _.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
(I ∩ J ↔ ideal_kernel rng_homo_crt)%ideal
    (** Finally we must show the ideal of this map is the intersection. *)
    apply ideal_subset_antisymm.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
(I ∩ J ⊆ ideal_kernel rng_homo_crt)%ideal
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
(ideal_kernel rng_homo_crt ⊆ I ∩ J)%ideal
    -
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
(I ∩ J ⊆ ideal_kernel rng_homo_crt)%ideal intros r [i j].
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
ideal_kernel rng_homo_crt r
      apply path_prod; apply qglue.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
in_cosetL
  {|
    normalsubgroup_subgroup := I;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R I
  |} r mon_unit
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} r mon_unit
      1: change (I (- r + 0)).
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
I (- r + 0)
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
in_cosetL
  {|
    normalsubgroup_subgroup := J;
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup R J
  |} r mon_unit
      2: change (J (- r + 0)).
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
I (- r + 0)
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
J (- r + 0)
      1,2: rewrite rng_plus_comm.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
I (0 - r)
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
J (0 - r)
      1,2: apply ideal_in_plus_negate.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
I 0
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
I r
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
J 0
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
J r
      1,3: apply ideal_in_zero.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
I r
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
r: R
i: I r
j: J r
J r
      1,2: assumption.
    -
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
(ideal_kernel rng_homo_crt ⊆ I ∩ J)%ideal intros i p.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: ideal_kernel rng_homo_crt i
(I ∩ J)%ideal i
      apply equiv_path_prod in p.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: ((fst (rng_homo_crt i) = fst group_unit) *
 (snd (rng_homo_crt i) = snd group_unit))%type
(I ∩ J)%ideal i
      destruct p as [p q].
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: fst (rng_homo_crt i) = fst group_unit
q: snd (rng_homo_crt i) = snd group_unit
(I ∩ J)%ideal i
      apply ideal_in_negate'.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: fst (rng_homo_crt i) = fst group_unit
q: snd (rng_homo_crt i) = snd group_unit
(I ∩ J)%ideal (- i)
      rewrite <- rng_plus_zero_r.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: fst (rng_homo_crt i) = fst group_unit
q: snd (rng_homo_crt i) = snd group_unit
(I ∩ J)%ideal (- i + 0)
      (** Here we need to derive the relation from paths in the quotient. This is what requires univalence. *)
      split.
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: fst (rng_homo_crt i) = fst group_unit
q: snd (rng_homo_crt i) = snd group_unit
I (- i + 0)
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: fst (rng_homo_crt i) = fst group_unit
q: snd (rng_homo_crt i) = snd group_unit
J (- i + 0)
      1: exact (related_quotient_paths _ _ _ p).
H: Univalence
R: Ring
I, J: Ideal R
c: Coprime I J
i: R
p: fst (rng_homo_crt i) = fst group_unit
q: snd (rng_homo_crt i) = snd group_unit
J (- i + 0)
      1: exact (related_quotient_paths _ _ _ q).
  Defined.

End ChineseRemainderTheorem.

(** We also have the same for products of ideals when in a commuatative ring. *)
Theorem chinese_remainder_prod `{Univalence}
  {R : CRing} (I J : Ideal R) (c : Coprime I J)
  : R / (I ⋅ J)%ideal ≅ (R / I) × (R / J).
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
R / (I ⋅ J)%ideal ≅ R / I × (R / J)
Proof.
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
R / (I ⋅ J)%ideal ≅ R / I × (R / J)
  etransitivity.
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
R / (I ⋅ J)%ideal ≅ ?Goal
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
?Goal ≅ R / I × (R / J)
  {
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
R / (I ⋅ J)%ideal ≅ ?Goal rapply rng_quotient_invar.
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
(I ⋅ J ↔ ?Goal0)%ideal
    symmetry.
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
(?Goal0 ↔ I ⋅ J)%ideal
    rapply ideal_intersection_is_product. }
H: Univalence
R: CRing
I, J: Ideal R
c: Coprime I J
R / (I ∩ J)%ideal ≅ R / I × (R / J)
  rapply chinese_remainder.
Defined.