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 Algebra.Rings.QuotientRing.

(** * 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).

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

Definition Build_CRing' (R : AbGroup) `(!One R, !Mult R)
  (comm : Commutative (.*.)) (assoc : Associative (.*.))
  (dist_l : LeftDistribute (.*.) (+)) (unit_l : LeftIdentity (.*.) 1)
  : CRing.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
CRing
Proof.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
CRing
  snapply Build_CRing.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
Ring
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
Commutative mult
  -
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
Ring rapply (Build_Ring R); only 1,2,4: exact _.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
RightDistribute mult plus
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
RightIdentity mult 1
    +
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
RightDistribute mult plus intros x y z.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
x, y, z: R
(x + y) * z = x * z + y * z
      lhs napply comm.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
x, y, z: R
z * (x + y) = x * z + y * z
      lhs rapply dist_l.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
x, y, z: R
z * x + z * y = x * z + y * z
      f_ap.
    +
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
RightIdentity mult 1 intros x.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
x: R
x * 1 = x
      lhs rapply comm.
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
x: R
1 * x = x
      apply unit_l.
  -
R: AbGroup
One0: One R
Mult0: Mult R
comm: Commutative mult
assoc: Associative mult
dist_l: LeftDistribute mult plus
unit_l: LeftIdentity mult 1
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.

Definition rng_mult_permute_2_3 {R : CRing} (x y z : R)
  : x * y * z = x * z * y.
R: CRing
x, y, z: R
x * y * z = x * z * y
Proof.
R: CRing
x, y, z: R
x * y * z = x * z * y
  lhs_V napply rng_mult_assoc.
R: CRing
x, y, z: R
x * (y * z) = x * z * y
  rhs_V napply rng_mult_assoc.
R: CRing
x, y, z: R
x * (y * z) = x * (z * y)
  apply ap, rng_mult_comm.
Defined.

Definition rng_mult_move_left_assoc {R : CRing} (x y z : R)
  : x * y * z = y * x * z.
R: CRing
x, y, z: R
x * y * z = y * x * z
Proof.
R: CRing
x, y, z: R
x * y * z = y * x * z
  f_ap; apply rng_mult_comm.
Defined.

Definition rng_mult_move_right_assoc {R : CRing} (x y z : R)
  : x * (y * z) = y * (x * z).
R: CRing
x, y, z: R
x * (y * z) = y * (x * z)
Proof.
R: CRing
x, y, z: R
x * (y * z) = y * (x * z)
  refine (rng_mult_assoc _ _ _ @ _ @ (rng_mult_assoc _ _ _)^).
R: CRing
x, y, z: R
x * y * z = y * x * z
  apply rng_mult_move_left_assoc.
Defined.

Definition isinvertible_cring (R : CRing) (x : R)
  (inv : R) (inv_l : inv * x = 1)
  : IsInvertible R x.
R: CRing
x, inv: R
inv_l: inv * x = 1
IsInvertible R x
Proof.
R: CRing
x, inv: R
inv_l: inv * x = 1
IsInvertible R x
  snapply Build_IsInvertible.
R: CRing
x, inv: R
inv_l: inv * x = 1
R
R: CRing
x, inv: R
inv_l: inv * x = 1
?inv * x = 1
R: CRing
x, inv: R
inv_l: inv * x = 1
x * ?inv = 1
  -
R: CRing
x, inv: R
inv_l: inv * x = 1
R exact inv.
  -
R: CRing
x, inv: R
inv_l: inv * x = 1
inv * x = 1 exact inv_l.
  -
R: CRing
x, inv: R
inv_l: inv * x = 1
x * inv = 1 lhs napply rng_mult_comm.
R: CRing
x, inv: R
inv_l: inv * x = 1
inv * x = 1
    exact inv_l.
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 (inv 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 (inv 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: exact (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)
      exact 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 (inv 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 (inv 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 (plus (x * g) (x * - h))
          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 (inv 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 (inv 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 (plus (g * x) (- h * x))
          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 (inv 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 (inv 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 (inv 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. *)

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

(** ** Quotient rings *)

Instance commutative_quotientring_mult (R : CRing) (I : Ideal R)
  : Commutative (A:=QuotientRing R I) (.*.).
R: CRing
I: Ideal R
Commutative mult
Proof.
R: CRing
I: Ideal R
Commutative mult
  intros x; srapply QuotientRing_ind_hprop; intros y; revert x.
R: CRing
I: Ideal R
y: R
forall x : R / I,
(fun r : R / I => x * r = r * x)
  (rng_quotient_map I y)
  srapply QuotientRing_ind_hprop; intros x; hnf.
R: CRing
I: Ideal R
y, x: R
rng_quotient_map I x * rng_quotient_map I y =
rng_quotient_map I y * rng_quotient_map I x
  lhs_V napply rng_homo_mult.
R: CRing
I: Ideal R
y, x: R
rng_quotient_map I (x * y) =
rng_quotient_map I y * rng_quotient_map I x
  rhs_V napply rng_homo_mult.
R: CRing
I: Ideal R
y, x: R
rng_quotient_map I (x * y) =
rng_quotient_map I (y * x)
  snapply ap.
R: CRing
I: Ideal R
y, x: R
x * y = y * x
  apply commutativity.
Defined.

Definition cring_quotient (R : CRing) (I : Ideal R) : CRing
  := Build_CRing (QuotientRing R I) _.

Definition cring_quotient_map {R : CRing} (I : Ideal R)
  : R $-> cring_quotient R I
  := rng_quotient_map I.