Require Import WildCat.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
(* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
Require Import Classes.interfaces.abstract_algebra.
Require Import Algebra.AbGroups.
Require Export Algebra.Rings.Ring Algebra.Rings.Ideal.

(** * Commutative Rings *)

Local Open Scope ring_scope.
Local Open Scope wc_iso_scope.

(** A commutative ring consists of the following data: *)
Record CRing := {
  (** An underlying ring. *)
  cring_ring :> Ring;
  (** Such that they satisfy the axioms of a commutative ring. *)
  cring_commutative :: Commutative (A:=cring_ring) (.*.);
}.

Definition issig_CRing : _ <~> CRing := ltac:(issig).

Global Instance cring_plus {R : CRing} : Plus R := plus_abgroup R.
Global Instance cring_zero {R : CRing} : Zero R := zero_abgroup R.
Global Instance cring_negate {R : CRing} : Negate R := negate_abgroup R.

Definition Build_CRing' (R : AbGroup)
  `(!One R, !Mult R, !Commutative (.*.), !LeftDistribute (.*.) (+), @IsMonoid R (.*.) 1)
  : CRing.
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
CRing
Proof.
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
CRing
  snrapply Build_CRing.
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
Ring
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
Commutative mult
  -
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
Ring snrapply (Build_Ring R).
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
Mult R
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
One R
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
LeftDistribute mult group_sgop
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
RightDistribute mult group_sgop
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
IsMonoid R
    1-3,5: exact _.
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
RightDistribute mult group_sgop
    intros x y z.
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
x, y, z: R
group_sgop x y * z = group_sgop (x * z) (y * z)
    lhs rapply commutativity.
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
x, y, z: R
z * group_sgop x y = group_sgop (x * z) (y * z)
    lhs rapply simple_distribute_l.
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
x, y, z: R
z * x + z * y = group_sgop (x * z) (y * z)
    f_ap.
  -
R: AbGroup
One0: One R
Mult0: Mult R
Commutative0: Commutative mult
LeftDistribute0: LeftDistribute mult plus
H: IsMonoid R
Commutative mult exact _.
Defined.

(** ** Properties of commutative rings *)

Definition rng_mult_comm {R : CRing} (x y : R) : x * y = y * x := commutativity x y.

(** Powers commute with multiplication *)
Lemma rng_power_mult {R : CRing} (x y : R) (n : nat)
  : rng_power (R:=R) (x * y) n = rng_power (R:=R) x n * rng_power (R:=R) y n.
R: CRing
x, y: R
n: nat
rng_power (x * y) n = rng_power x n * rng_power y n
Proof.
R: CRing
x, y: R
n: nat
rng_power (x * y) n = rng_power x n * rng_power y n
  induction n.
R: CRing
x, y: R
rng_power (x * y) 0 = rng_power x 0 * rng_power y 0
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
rng_power (x * y) n.+1 =
rng_power x n.+1 * rng_power y n.+1
  1: symmetry; rapply rng_mult_one_l.
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
rng_power (x * y) n.+1 =
rng_power x n.+1 * rng_power y n.+1
  simpl.
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
x * y * rng_power (x * y) n =
x * rng_power x n * (y * rng_power y n)
  rewrite (rng_mult_assoc (A:=R)).
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
x * y * rng_power (x * y) n =
x * rng_power x n * y * rng_power y n
  rewrite <- (rng_mult_assoc (A:=R) x _ y).
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
x * y * rng_power (x * y) n =
x * (rng_power x n * y) * rng_power y n
  rewrite (rng_mult_comm (rng_power (R:=R) x n) y).
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
x * y * rng_power (x * y) n =
x * (y * rng_power x n) * rng_power y n
  rewrite rng_mult_assoc.
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
x * y * rng_power (x * y) n =
x * y * rng_power x n * rng_power y n
  rewrite <- (rng_mult_assoc _ (rng_power (R:=R) x n)).
R: CRing
x, y: R
n: nat
IHn: rng_power (x * y) n = rng_power x n * rng_power y n
x * y * rng_power (x * y) n =
x * y * (rng_power x n * rng_power y n)
  f_ap.
Defined.

(** ** Ideals in commutative rings *)

Section IdealCRing.
  Context {R : CRing}.

  (** The section is meant to complement the IdealLemmas section in Algebra.Rings.Ideal. Since the results here only hold in commutative rings, they have to be kept here. *)

  (** We import ideal notations as used in Algebra.Rings.Ideal but only for this section. Important to note is that [↔] corresponds to equality of ideals. *)
  Import Ideal.Notation.
  Local Open Scope ideal_scope.

  (** In a commutative ring, the product of two ideals is a subset of the reversed product. *)
  Lemma ideal_product_subset_product_commutative (I J : Ideal R)
    : I ⋅ J ⊆ J ⋅ I.
R: CRing
I, J: Ideal R
I ⋅ J ⊆ J ⋅ I
  Proof.
R: CRing
I, J: Ideal R
I ⋅ J ⊆ J ⋅ I
    intros r p.
R: CRing
I, J: Ideal R
r: R
p: (I ⋅ J) r
(J ⋅ I) r
    strip_truncations.
R: CRing
I, J: Ideal R
r: R
p: subgroup_generated_type
  (ideal_product_naive_type I J) r
(J ⋅ I) r
    induction p as [r p | |].
R: CRing
I, J: Ideal R
r: R
p: ideal_product_naive_type I J r
(J ⋅ I) r
R: CRing
I, J: Ideal R
(J ⋅ I) mon_unit
R: CRing
I, J: Ideal R
g, h: R
p1: subgroup_generated_type
  (ideal_product_naive_type I J) g
p2: subgroup_generated_type
  (ideal_product_naive_type I J) h
IHp1: (J ⋅ I) g
IHp2: (J ⋅ I) h
(J ⋅ I) (sg_op g (- h))
    2: apply ideal_in_zero.
R: CRing
I, J: Ideal R
r: R
p: ideal_product_naive_type I J r
(J ⋅ I) r
R: CRing
I, J: Ideal R
g, h: R
p1: subgroup_generated_type
  (ideal_product_naive_type I J) g
p2: subgroup_generated_type
  (ideal_product_naive_type I J) h
IHp1: (J ⋅ I) g
IHp2: (J ⋅ I) h
(J ⋅ I) (sg_op g (- h))
    2: by apply ideal_in_plus_negate.
R: CRing
I, J: Ideal R
r: R
p: ideal_product_naive_type I J r
(J ⋅ I) r
    destruct p as [s t p q].
R: CRing
I, J: Ideal R
s, t: R
p: I s
q: J t
(J ⋅ I) (s * t)
    rewrite rng_mult_comm.
R: CRing
I, J: Ideal R
s, t: R
p: I s
q: J t
(J ⋅ I) (t * s)
    apply tr.
R: CRing
I, J: Ideal R
s, t: R
p: I s
q: J t
subgroup_generated_type (ideal_product_naive_type J I)
  (t * s)
    apply sgt_in.
R: CRing
I, J: Ideal R
s, t: R
p: I s
q: J t
ideal_product_naive_type J I (t * s)
    by rapply ipn_in.
  Defined.

  (** Ideal products are commutative in commutative rings. Note that we are using ideal notations here and [↔] corresponds to equality of ideals. Essentially a subset in each direction. *)
  Lemma ideal_product_comm (I J : Ideal R) : I ⋅ J ↔ J ⋅ I.
R: CRing
I, J: Ideal R
I ⋅ J ↔ J ⋅ I
  Proof.
R: CRing
I, J: Ideal R
I ⋅ J ↔ J ⋅ I
    apply ideal_subset_antisymm;
    apply ideal_product_subset_product_commutative.
  Defined.

  (** Product of intersection and sum is a subset of product. Note that this is a generalization of lcm * gcd = product *)
  Lemma ideal_product_intersection_sum_subset' (I J : Ideal R)
    : (I ∩ J) ⋅ (I + J) ⊆ I ⋅ J.
R: CRing
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ I ⋅ J
  Proof.
R: CRing
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ I ⋅ J
    etransitivity.
R: CRing
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ ?Goal
R: CRing
I, J: Ideal R
?Goal ⊆ I ⋅ J
    2: rapply ideal_sum_self.
R: CRing
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + I ⋅ J)
    etransitivity.
R: CRing
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ ?Goal
R: CRing
I, J: Ideal R
?Goal ⊆ (I ⋅ J + I ⋅ J)
    2: rapply ideal_sum_subset_pres_r.
R: CRing
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + ?Goal0)
R: CRing
I, J: Ideal R
?Goal0 ⊆ I ⋅ J
    2: rapply ideal_product_comm.
R: CRing
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I)
    apply ideal_product_intersection_sum_subset.
  Defined.

  (** If the sum of ideals is the whole ring then their intersection is a subset of their product. *)
  Lemma ideal_intersection_subset_product (I J : Ideal R)
    : ideal_unit R ⊆ (I + J) -> I ∩ J ⊆ I ⋅ J.
R: CRing
I, J: Ideal R
ideal_unit R ⊆ (I + J) -> I ∩ J ⊆ I ⋅ J
  Proof.
R: CRing
I, J: Ideal R
ideal_unit R ⊆ (I + J) -> I ∩ J ⊆ I ⋅ J
    intros p.
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
I ∩ J ⊆ I ⋅ J
    etransitivity.
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
I ∩ J ⊆ ?Goal
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
?Goal ⊆ I ⋅ J
    {
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
I ∩ J ⊆ ?Goal apply ideal_eq_subset.
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
I ∩ J ↔ ?Goal
      symmetry.
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
?Goal ↔ I ∩ J
      apply ideal_product_unit_r. }
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
(I ∩ J) ⋅ ideal_unit R ⊆ I ⋅ J
    etransitivity.
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
(I ∩ J) ⋅ ideal_unit R ⊆ ?Goal
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
?Goal ⊆ I ⋅ J
    1: rapply (ideal_product_subset_pres_r _ _ _ p).
R: CRing
I, J: Ideal R
p: ideal_unit R ⊆ (I + J)
(I ∩ J) ⋅ (I + J) ⊆ I ⋅ J
    rapply ideal_product_intersection_sum_subset'.
  Defined.

  (** This can be combined into a sufficient (but not necessary) condition for equality of intersections and products. *)
  Lemma ideal_intersection_is_product (I J : Ideal R)
    : Coprime I J -> I ∩ J ↔ I ⋅ J.
R: CRing
I, J: Ideal R
Coprime I J -> I ∩ J ↔ I ⋅ J
  Proof.
R: CRing
I, J: Ideal R
Coprime I J -> I ∩ J ↔ I ⋅ J
    intros p.
R: CRing
I, J: Ideal R
p: Coprime I J
I ∩ J ↔ I ⋅ J
    apply ideal_subset_antisymm.
R: CRing
I, J: Ideal R
p: Coprime I J
I ∩ J ⊆ I ⋅ J
R: CRing
I, J: Ideal R
p: Coprime I J
I ⋅ J ⊆ I ∩ J
    -
R: CRing
I, J: Ideal R
p: Coprime I J
I ∩ J ⊆ I ⋅ J apply ideal_intersection_subset_product.
R: CRing
I, J: Ideal R
p: Coprime I J
ideal_unit R ⊆ (I + J)
      unfold Coprime in p.
R: CRing
I, J: Ideal R
p: I + J ↔ ideal_unit R
ideal_unit R ⊆ (I + J)
      apply symmetry in p.
R: CRing
I, J: Ideal R
p: ideal_unit R ↔ I + J
ideal_unit R ⊆ (I + J)
      rapply p.
    -
R: CRing
I, J: Ideal R
p: Coprime I J
I ⋅ J ⊆ I ∩ J apply ideal_product_subset_intersection.
  Defined.

  Lemma ideal_quotient_product (I J K : Ideal R)
    : (I :: J) :: K ↔ (I :: (J ⋅ K)).
R: CRing
I, J, K: Ideal R
(I :: J) :: K ↔ I :: J ⋅ K
  Proof.
R: CRing
I, J, K: Ideal R
(I :: J) :: K ↔ I :: J ⋅ K
    apply ideal_subset_antisymm.
R: CRing
I, J, K: Ideal R
((I :: J) :: K) ⊆ (I :: J ⋅ K)
R: CRing
I, J, K: Ideal R
(I :: J ⋅ K) ⊆ ((I :: J) :: K)
    -
R: CRing
I, J, K: Ideal R
((I :: J) :: K) ⊆ (I :: J ⋅ K) intros x [p q]; strip_truncations; split; apply tr;
      intros r; rapply Trunc_rec; intros jk.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
r: R
jk: subgroup_generated_type
  (ideal_product_naive_type J K) r
I (x * r)
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
r: rng_op R
jk: subgroup_generated_type
  (ideal_product_naive_type J K) r
I (x * r)
      +
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
r: R
jk: subgroup_generated_type
  (ideal_product_naive_type J K) r
I (x * r) induction jk as [y [z z' j k] | | ? ? ? ? ? ? ].
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (x * (z * z'))
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I (x * mon_unit)
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (x * sg_op g (- h))
        *
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (x * (z * z')) rewrite (rng_mult_comm z z').
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (x * (z' * z))
          rewrite rng_mult_assoc.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (x * z' * z)
          destruct (p z' k) as [p' ?].
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
p': leftideal_quotient I J (x * z')
snd: rightideal_quotient I J (x * z')
I (x * z' * z)
          revert p'; apply Trunc_rec; intros p'.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
snd: rightideal_quotient I J (x * z')
p': forall x0 : R, J x0 -> I (x * z' * x0)
I (x * z' * z)
          exact (p' z j).
        *
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I (x * mon_unit) change (I (x * 0)).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I (x * 0)
          rewrite rng_mult_zero_r.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I 0
          apply ideal_in_zero.
        *
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (x * sg_op g (- h)) change (I (x * (g - h))).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (x * (g - h))
          rewrite rng_dist_l.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (x * g + x * - h)%mc
          rewrite rng_mult_negate_r.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (x * g - x * h)
          by apply ideal_in_plus_negate.
      +
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
r: rng_op R
jk: subgroup_generated_type
  (ideal_product_naive_type J K) r
I (x * r) induction jk as [y [z z' j k] | | ? ? ? ? ? ? ].
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (x * (z * z'))
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I (x * mon_unit)
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (x * sg_op g (- h))
        *
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (x * (z * z')) change (I (z * z' * x)).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (z * z' * x)
          rewrite <- rng_mult_assoc.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (z * (z' * x))
          rewrite (rng_mult_comm z).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
I (z' * x * z)
          destruct (q z' k) as [q' ?].
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
q': leftideal_quotient I J (x * z')
snd: rightideal_quotient I J (x * z')
I (z' * x * z)
          revert q'; apply Trunc_rec; intros q'.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
y, z, z': R
j: J z
k: K z'
snd: rightideal_quotient I J (x * z')
q': forall x0 : R, J x0 -> I (x * z' * x0)
I (z' * x * z)
          exact (q' z j).
        *
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I (x * mon_unit) change (I (0 * x)).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I (0 * x)
          rewrite rng_mult_zero_l.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
I 0
          apply ideal_in_zero.
        *
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (x * sg_op g (- h)) change (I ((g - h) * x)).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I ((g - h) * x)
          rewrite rng_dist_r.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (g * x + - h * x)%mc
          rewrite rng_mult_negate_l.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, K x0 -> (I :: J) (x * x0)
p: forall x0 : R, K x0 -> (I :: J) (x * x0)
g, h: R
jk1: subgroup_generated_type (ideal_product_naive_type J K) g
jk2: subgroup_generated_type (ideal_product_naive_type J K) h
IHjk1: I (x * g)
IHjk2: I (x * h)
I (g * x - h * x)
          by apply ideal_in_plus_negate.
    -
R: CRing
I, J, K: Ideal R
(I :: J ⋅ K) ⊆ ((I :: J) :: K) intros x [p q]; strip_truncations; split; apply tr;
      intros r k; split; apply tr; intros z j.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * r * z)
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: rng_op R
j: J z
I (x * r * z)
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: rng_op R
k: K r
z: R
j: J z
I (x * r * z)
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: rng_op R
k: K r
z: rng_op R
j: J z
I (x * r * z)
      +
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * r * z) rewrite <- rng_mult_assoc.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * (r * z))
        rewrite (rng_mult_comm r z).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * (z * r))
        by apply p, tr, sgt_in, ipn_in.
      +
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: rng_op R
j: J z
I (x * r * z) cbn in z.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * r * z)
        change (I (z * (x * r))).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (z * (x * r))
        rewrite (rng_mult_comm x).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (z * (r * x))
        rewrite rng_mult_assoc.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (z * r * x)
        by apply q, tr, sgt_in, ipn_in.
      +
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: rng_op R
k: K r
z: R
j: J z
I (x * r * z) cbn in r.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * r * z)
        change (I (r * x * z)).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (r * x * z)
        rewrite <- rng_mult_assoc.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (r * (x * z))
        rewrite (rng_mult_comm r).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * z * r)
        rewrite <- rng_mult_assoc.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * (z * r))
        by apply p, tr, sgt_in, ipn_in.
      +
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: rng_op R
k: K r
z: rng_op R
j: J z
I (x * r * z) cbn in r, z.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * r * z)
        change (I (z * (r * x))).
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (z * (r * x))
        rewrite rng_mult_assoc.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (z * r * x)
        rewrite rng_mult_comm.
R: CRing
I, J, K: Ideal R
x: R
q: forall x0 : rng_op R, (J ⋅ K) x0 -> I (x * x0)
p: forall x0 : R, (J ⋅ K) x0 -> I (x * x0)
r: R
k: K r
z: R
j: J z
I (x * (z * r))
        by apply p, tr, sgt_in, ipn_in.
  Defined.

  (** The ideal quotient is a right adjoint to the product in the monoidal lattice of ideals. *)
  Lemma ideal_quotient_subset_prod (I J K : Ideal R)
    : I ⋅ J ⊆ K <-> I ⊆ (K :: J).
R: CRing
I, J, K: Ideal R
I ⋅ J ⊆ K <-> I ⊆ (K :: J)
  Proof.
R: CRing
I, J, K: Ideal R
I ⋅ J ⊆ K <-> I ⊆ (K :: J)
    split.
R: CRing
I, J, K: Ideal R
I ⋅ J ⊆ K -> I ⊆ (K :: J)
R: CRing
I, J, K: Ideal R
I ⊆ (K :: J) -> I ⋅ J ⊆ K
    -
R: CRing
I, J, K: Ideal R
I ⋅ J ⊆ K -> I ⊆ (K :: J) intros p r i; split; apply tr; intros s j; cbn in s, r.
R: CRing
I, J, K: Ideal R
p: I ⋅ J ⊆ K
r: R
i: I r
s: R
j: J s
K (r * s)
R: CRing
I, J, K: Ideal R
p: I ⋅ J ⊆ K
r: R
i: I r
s: R
j: J s
K (r * s)
      +
R: CRing
I, J, K: Ideal R
p: I ⋅ J ⊆ K
r: R
i: I r
s: R
j: J s
K (r * s) by apply p, tr, sgt_in, ipn_in.
      +
R: CRing
I, J, K: Ideal R
p: I ⋅ J ⊆ K
r: R
i: I r
s: R
j: J s
K (r * s) change (K (s * r)).
R: CRing
I, J, K: Ideal R
p: I ⋅ J ⊆ K
r: R
i: I r
s: R
j: J s
K (s * r)
        rewrite (rng_mult_comm s r).
R: CRing
I, J, K: Ideal R
p: I ⋅ J ⊆ K
r: R
i: I r
s: R
j: J s
K (r * s)
        by apply p, tr, sgt_in; rapply ipn_in.
    -
R: CRing
I, J, K: Ideal R
I ⊆ (K :: J) -> I ⋅ J ⊆ K intros p x.
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
x: R
(I ⋅ J) x -> K x
      apply Trunc_rec.
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
x: R
subgroup_generated_type (ideal_product_naive_type I J)
  x -> K x
      intros q.
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
x: R
q: subgroup_generated_type
  (ideal_product_naive_type I J) x
K x
      induction q as [r x | | ].
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
r: R
x: ideal_product_naive_type I J r
K r
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
K mon_unit
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
g, h: R
q1: subgroup_generated_type
  (ideal_product_naive_type I J) g
q2: subgroup_generated_type
  (ideal_product_naive_type I J) h
IHq1: K g
IHq2: K h
K (sg_op g (- h))
      {
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
r: R
x: ideal_product_naive_type I J r
K r destruct x.
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
x, y: R
s: I x
s0: J y
K (x * y)
        specialize (p x s); destruct p as [p q].
R: CRing
I, J, K: Ideal R
x: R
p: leftideal_quotient K J x
q: rightideal_quotient K J x
y: R
s: I x
s0: J y
K (x * y)
        revert p; apply Trunc_rec; intros p.
R: CRing
I, J, K: Ideal R
x: R
q: rightideal_quotient K J x
y: R
s: I x
s0: J y
p: forall x0 : R, J x0 -> K (x * x0)
K (x * y)
        by apply p. }
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
K mon_unit
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
g, h: R
q1: subgroup_generated_type
  (ideal_product_naive_type I J) g
q2: subgroup_generated_type
  (ideal_product_naive_type I J) h
IHq1: K g
IHq2: K h
K (sg_op g (- h))
      1: apply ideal_in_zero.
R: CRing
I, J, K: Ideal R
p: I ⊆ (K :: J)
g, h: R
q1: subgroup_generated_type
  (ideal_product_naive_type I J) g
q2: subgroup_generated_type
  (ideal_product_naive_type I J) h
IHq1: K g
IHq2: K h
K (sg_op g (- h))
      by apply ideal_in_plus_negate.
  Defined.

  (** Ideal quotients partially cancel *)
  Lemma ideal_quotient_product_left (I J : Ideal R)
    : (I :: J) ⋅ J ⊆ I.
R: CRing
I, J: Ideal R
(I :: J) ⋅ J ⊆ I
  Proof.
R: CRing
I, J: Ideal R
(I :: J) ⋅ J ⊆ I
    by apply ideal_quotient_subset_prod.
  Defined.

End IdealCRing.

(** ** Category of commutative rings. *)

Global Instance isgraph_CRing : IsGraph CRing := isgraph_induced cring_ring.
Global Instance is01cat_CRing : Is01Cat CRing := is01cat_induced cring_ring.
Global Instance is2graph_CRing : Is2Graph CRing := is2graph_induced cring_ring.
Global Instance is1cat_CRing : Is1Cat CRing := is1cat_induced cring_ring.
Global Instance hasequiv_CRing : HasEquivs CRing := hasequivs_induced cring_ring.