Timings for CRing.v
(* 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.
lhs rapply commutativity.
lhs rapply simple_distribute_l.
(** ** 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.
1: symmetry; rapply rng_mult_one_l.
rewrite (rng_mult_assoc (A:=R)).
rewrite <- (rng_mult_assoc (A:=R) x _ y).
rewrite (rng_mult_comm (rng_power (R:=R) x n) y).
rewrite <- (rng_mult_assoc _ (rng_power (R:=R) x n)).
(** ** Ideals in commutative rings *)
(** 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. *)
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.
induction p as [r p | |].
2: by apply ideal_in_plus_negate.
(** 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.
apply ideal_subset_antisymm;
apply ideal_product_subset_product_commutative.
(** 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.
2: rapply ideal_sum_self.
2: rapply ideal_sum_subset_pres_r.
2: rapply ideal_product_comm.
apply ideal_product_intersection_sum_subset.
(** 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.
apply ideal_product_unit_r.
1: rapply (ideal_product_subset_pres_r _ _ _ p).
rapply ideal_product_intersection_sum_subset'.
(** 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.
apply ideal_subset_antisymm.
apply ideal_intersection_subset_product.
apply ideal_product_subset_intersection.
Lemma ideal_quotient_product (I J K : Ideal R)
: (I :: J) :: K ↔ (I :: (J ⋅ K)).
apply ideal_subset_antisymm.
intros x [p q]; strip_truncations; split; apply tr;
intros r; rapply Trunc_rec; intros jk.
induction jk as [y [z z' j k] | | ? ? ? ? ? ? ].
rewrite (rng_mult_comm z z').
destruct (p z' k) as [p' ?].
revert p'; apply Trunc_rec; intros p'.
change (I (x * (g - h))).
rewrite rng_mult_negate_r.
by apply ideal_in_plus_negate.
induction jk as [y [z z' j k] | | ? ? ? ? ? ? ].
rewrite <- rng_mult_assoc.
rewrite (rng_mult_comm z).
destruct (q z' k) as [q' ?].
revert q'; apply Trunc_rec; intros q'.
change (I ((g - h) * x)).
rewrite rng_mult_negate_l.
by apply ideal_in_plus_negate.
intros x [p q]; strip_truncations; split; apply tr;
intros r k; split; apply tr; intros z j.
rewrite <- rng_mult_assoc.
rewrite (rng_mult_comm r z).
by apply p, tr, sgt_in, ipn_in.
change (I (z * (x * r))).
rewrite (rng_mult_comm x).
by apply q, tr, sgt_in, ipn_in.
rewrite <- rng_mult_assoc.
rewrite (rng_mult_comm r).
rewrite <- rng_mult_assoc.
by apply p, tr, sgt_in, ipn_in.
change (I (z * (r * x))).
by apply p, tr, sgt_in, ipn_in.
(** 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).
intros p r i; split; apply tr; intros s j; cbn in s, r.
by apply p, tr, sgt_in, ipn_in.
rewrite (rng_mult_comm s r).
by apply p, tr, sgt_in; rapply ipn_in.
induction q as [r x | | ].
specialize (p x s); destruct p as [p q].
revert p; apply Trunc_rec; intros p.
by apply ideal_in_plus_negate.
(** Ideal quotients partially cancel *)
Lemma ideal_quotient_product_left (I J : Ideal R)
: (I :: J) ⋅ J ⊆ I.
by apply ideal_quotient_subset_prod.
(** ** 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.