Merge pull request #2089 from Alizter/ps/rr/localizations_of_commutat…

…ive_rings

localizations of commutative rings

theories/Algebra/AbGroups/AbelianGroup.v

@@ -29,6 +29,28 @@ Proof.
   split; exact _.
 Defined.
 
+(** Easier way to build abelian groups without redundant information. *)
+Definition Build_AbGroup' (G : Type)
+  `{Zero G, Negate G, Plus G, IsHSet G}
+  (comm : Commutative (A:=G) (+))
+  (assoc : Associative (A:=G) (+))
+  (unit_l : LeftIdentity (A:=G) (+) 0)
+  (inv_l : LeftInverse (A:=G) (+) (-) 0)
+  : AbGroup.
+Proof.
+  snrapply Build_AbGroup.
+  - (* TODO: introduce smart constructor for [Build_Group] *)
+    rapply (Build_Group G).
+    repeat split; only 1-3, 5: exact _.
+    + intros x.
+      lhs nrapply comm.
+      exact (unit_l x).
+    + intros x.
+      lhs nrapply comm.
+      exact (inv_l x).
+  - exact comm.
+Defined.
+
 Definition issig_abgroup : _ <~> AbGroup := ltac:(issig).
 
 Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit.
@@ -91,11 +113,7 @@ Global Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
 Proof.
   nrapply Build_IsAbGroup.
   1: exact _.
-  intro x.
-  srapply Quotient_ind_hprop.
-  intro y; revert x.
-  srapply Quotient_ind_hprop.
-  intro x.
+  srapply Quotient_ind2_hprop; intros x y.
   apply (ap (class_of _)).
   apply commutativity.
 Defined.

theories/Algebra/AbGroups/Z.v

@@ -12,14 +12,16 @@ Local Open Scope int_scope.
 
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
-  snrapply Build_AbGroup.
-  - refine (Build_Group Int int_add 0 int_neg _); repeat split.
-    + exact _.
-    + exact int_add_assoc.
-    + exact int_add_0_r.
-    + exact int_add_neg_l.
-    + exact int_add_neg_r.
+  snrapply Build_AbGroup'.
+  - exact Int.
+  - exact 0.
+  - exact int_neg.
+  - exact int_add.
+  - exact _.
   - exact int_add_comm.
+  - exact int_add_assoc.
+  - exact int_add_0_l.
+  - exact int_add_neg_l.
 Defined.
 
 (** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism.  See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *)

theories/Algebra/AbSES/Core.v

@@ -737,8 +737,7 @@ Proof.
   - apply isequiv_surj_emb.
     1: rapply cancelR_conn_map.
     apply isembedding_isinj_hset.
-    srapply Quotient_ind_hprop; intro x.
-    srapply Quotient_ind_hprop; intro y.
+    srapply Quotient_ind2_hprop; intros x y.
     intro p.
     apply qglue; cbn.
     refine (isexact_preimage (Tr (-1)) _ _ (-x + y) _).

theories/Algebra/Groups/QuotientGroup.v

@@ -27,23 +27,12 @@ Section GroupCongruenceQuotient.
 
   Global Instance congquot_sgop : SgOp CongruenceQuotient.
   Proof.
-    intros x.
-    srapply Quotient_rec.
-    { intro y; revert x.
-      srapply Quotient_rec.
-      { intros x.
-        apply class_of.
-        exact (x * y). }
-      intros a b r.
-      cbn.
+    srapply Quotient_rec2.
+    - intros x y.
+      exact (class_of _ (x * y)).
+    - intros x x' p y y' q.
       apply qglue.
-      by apply iscong. }
-    intros a b r.
-    revert x.
-    srapply Quotient_ind_hprop.
-    intro x.
-    apply qglue.
-    by apply iscong.
+      by apply iscong.
   Defined.
 
   Global Instance congquot_mon_unit : MonUnit CongruenceQuotient.
@@ -72,10 +61,7 @@ Section GroupCongruenceQuotient.
 
   Global Instance congquot_sgop_associative : Associative congquot_sgop.
   Proof.
-    intros x y.
-    srapply Quotient_ind_hprop; intro a; revert y.
-    srapply Quotient_ind_hprop; intro b; revert x.
-    srapply Quotient_ind_hprop; intro c.
+    srapply Quotient_ind3_hprop; intros x y z.
     simpl; by rewrite associativity.
   Qed.
 

theories/Algebra/Rings/CRing.v

@@ -2,7 +2,7 @@ Require Import WildCat.
 (* 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.
+Require Export Algebra.Rings.Ring Algebra.Rings.Ideal Algebra.Rings.QuotientRing.
 
 (** * Commutative Rings *)
 
@@ -23,17 +23,21 @@ 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)
+Definition Build_CRing' (R : AbGroup) `(!One R, !Mult R)
+  (comm : Commutative (.*.)) (assoc : Associative (.*.))
+  (dist_l : LeftDistribute (.*.) (+)) (unit_l : LeftIdentity (.*.) 1)
   : CRing.
 Proof.
   snrapply Build_CRing.
-  - snrapply (Build_Ring R).
-    1-3,5: exact _.
-    intros x y z.
-    lhs rapply commutativity.
-    lhs rapply simple_distribute_l.
-    f_ap.
+  - rapply (Build_Ring R); only 1: exact _.
+    2: repeat split; only 1-3: exact _.
+    + intros x y z.
+      lhs nrapply comm.
+      lhs rapply dist_l.
+      f_ap.
+    + intros x.
+      lhs rapply comm.
+      apply unit_l.
   - exact _.
 Defined.
 
@@ -56,6 +60,38 @@ Proof.
   f_ap.
 Defined.
 
+Definition rng_mult_permute_2_3 {R : CRing} (x y z : R)
+  : x * y * z = x * z * y.
+Proof.
+  lhs_V nrapply rng_mult_assoc.
+  rhs_V nrapply rng_mult_assoc.
+  apply ap, rng_mult_comm.
+Defined.
+
+Definition rng_mult_move_left_assoc {R : CRing} (x y z : R)
+  : x * y * z = y * x * z.
+Proof.
+  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).
+Proof.
+  refine (rng_mult_assoc _ _ _ @ _ @ (rng_mult_assoc _ _ _)^).
+  apply rng_mult_move_left_assoc.
+Defined.
+
+Definition isinvertible_cring (R : CRing) (x : R)
+  (inv : R) (inv_l : inv * x = 1)
+  : IsInvertible R x.
+Proof.
+  snrapply Build_IsInvertible.
+  - exact inv.
+  - exact inv_l.
+  - lhs nrapply rng_mult_comm.
+    exact inv_l.
+Defined.
+
 (** ** Ideals in commutative rings *)
 
 Section IdealCRing.
@@ -223,3 +259,23 @@ 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.
+
+(** ** Quotient rings *)
+
+Global Instance commutative_quotientring_mult (R : CRing) (I : Ideal R)
+  : Commutative (A:=QuotientRing R I) (.*.).
+Proof.
+  intros x; srapply QuotientRing_ind_hprop; intros y; revert x.
+  srapply QuotientRing_ind_hprop; intros x; hnf.
+  lhs_V nrapply rng_homo_mult.
+  rhs_V nrapply rng_homo_mult.
+  snrapply ap.
+  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.