Library HoTT.Algebra.Rings.ChineseRemainder

Require Import Classes.interfaces.canonical_names.
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 ).
  Proof.
    apply ring_product_corec.
    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.
  Proof.

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].
    revert a; srapply QuotientRing_ind_hprop; intro a.
    revert b; srapply QuotientRing_ind_hprop; intro 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].

We make this choice and show it maps as desired.

apply tr; ∃ (b × x + a × y).

Finally using some simple ring laws we can show it maps to our pair.

    rewrite rng_homo_plus.
    rewrite 2 rng_homo_mult.
    rewrite q1, q2.
    apply path_prod.
    + change ([b] × 0 + [a] × 1 = [a] :> R / I).
      by rewrite rng_mult_one_r, rng_mult_zero_r, rng_plus_zero_l.
    + change ([b] × 1 + [a] × 0 = [b] :> R / J).
      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).
    Proof.
      apply rng_moveR_Mr in p.
      rewrite rng_plus_comm in p.
      apply path_prod; apply qglue.
      - change (I (-x + 0)).
        apply ideal_in_negate_plus.
        1: assumption.
        apply ideal_in_zero.
      - change (J (-x + 1)).
        rewrite rng_plus_comm.
        by rewrite <- p.
    Defined.

    Lemma rng_homo_crt_beta_right : rng_homo_crt y = (1, 0).
    Proof.
      apply rng_moveR_rM in p.
      rewrite rng_plus_comm in p.
      apply path_prod; apply qglue.
      - change (I (-y + 1)).
        by rewrite <- p.
      - change (J (-y + 0)).
        apply ideal_in_negate_plus.
        1: assumption.
        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.
  Proof.
    intros c.

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.

Since the goal is a hprop we may strip the truncations.

strip_truncations.

Now we can break apart the data of this witness.

destruct c as [[[x ix] [y jy]] p];
change (x + y = 1) in p.

Now we apply all our previous lemmas

    apply (issurjection_rng_homo_crt' x y).
    1: exact (rng_homo_crt_beta_left x y ix jy p).
    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 ).
Proof.

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'.
    1: rapply rng_homo_crt.
    1: exact _.

Finally we must show the ideal of this map is the intersection.

    apply ideal_subset_antisymm.
    - intros r [i j].
      apply path_prod; apply qglue.
      1: change (I (- r + 0)).
      2: change (J (- r + 0)).
      1,2: rewrite rng_plus_comm.
      1,2: apply ideal_in_plus_negate.
      1,3: apply ideal_in_zero.
      1,2: assumption.
    - intros i p.
      apply equiv_path_prod in p.
      destruct p as [p q].
      apply ideal_in_negate'.
      rewrite <- rng_plus_zero_r.

Here we need to derive the relation from paths in the quotient. This is what requires univalence.

      split.
      1: exact (related_quotient_paths _ _ _ p).
      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 ).
Proof.
  etransitivity.
  { rapply rng_quotient_invar.
    symmetry.
    rapply ideal_intersection_is_product. }
  rapply chinese_remainder.
Defined.