opposite rings

test/Algebra/Rings/Ring.v

@@ -0,0 +1,21 @@
+From HoTT Require Import Basics.Overture Algebra.Rings.Ring Algebra.Rings.CRing.
+From HoTT.Algebra Require Import Groups.Group AbGroups.AbelianGroup.
+From HoTT Require Import abstract_algebra.
+
+Local Open Scope path_scope.
+
+(** Test that opposite rings are definitionally involutive. *)
+Definition test1 (R : Ring) : R = (rng_op (rng_op R)) :> Ring := 1.
+Definition test2 (R : CRing) : R = (rng_op (rng_op R)) :> CRing := 1.
+
+Axiom fake_comm : forall (R : CRing) (x y : R), x * y = y * x.
+Definition augment (R : CRing) : CRing.
+Proof.
+  snrapply Build_CRing.
+  - exact R.
+  - exact (fake_comm R).
+Defined.
+
+Fail Definition test3 (R : CRing) : R = augment R :> CRing := 1.
+(* !? *)
+Definition test4 (R : CRing) : R = (rng_op (rng_op (augment R))) :> CRing := 1.

theories/Algebra/Rings/CRing.v

@@ -11,35 +11,30 @@ Local Open Scope wc_iso_scope.
 
 (** A commutative ring consists of the following data: *)
 Record CRing := {
-  (** An underlying abelian group. *)
-  cring_abgroup :> AbGroup;
-  (** A multiplication operation. *)
-  cring_mult :: Mult cring_abgroup;
-  (** A multiplicative identity. *)
-  cring_one :: One cring_abgroup;
-  (** Such that they satisfy the axioms of a ring. *)
-  cring_iscring :: IsCRing cring_abgroup;
+  (** An underlying ring. *)
+  cring_ring :> Ring;
+  (** Such that they satisfy the axioms of a commutative ring. *)
+  cring_commutative :: Commutative (A:=cring_ring) (.*.);
 }.
 
-Arguments cring_mult {_}.
-Arguments cring_one {_}.
-Arguments cring_iscring {_}.
-
 Definition issig_CRing : _ <~> CRing := ltac:(issig).
 
-Global Instance cring_plus {R : CRing} : Plus R := plus_abgroup (cring_abgroup R).
-Global Instance cring_zero {R : CRing} : Zero R := zero_abgroup (cring_abgroup R).
-Global Instance cring_negate {R : CRing} : Negate R := negate_abgroup (cring_abgroup R).
-
-Definition ring_cring : CRing -> Ring
-  := fun R => Build_Ring (cring_abgroup R) (cring_mult) (cring_one) _.
-Coercion ring_cring : CRing >-> Ring.
+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 : Ring) (H : Commutative (@ring_mult R)) : CRing.
+Definition Build_CRing' (R : AbGroup)
+  `(!One R, !Mult R, !Commutative (.*.), !LeftDistribute (.*.) (+), @IsMonoid R (.*.) 1)
+  : CRing.
 Proof.
-  rapply (Build_CRing R).
-  split; try exact _.
-  split; exact _.
+  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.
+  - exact _.
 Defined.
 
 (** ** Properties of commutative rings *)
@@ -200,7 +195,7 @@ End IdealCRing.
 
 (** ** Category of commutative rings. *)
 
-Global Instance isgraph_CRing : IsGraph CRing := isgraph_induced ring_cring.
-Global Instance is01cat_CRing : Is01Cat CRing := is01cat_induced ring_cring.
-Global Instance is2graph_CRing : Is2Graph CRing := is2graph_induced ring_cring.
-Global Instance is1cat_CRing : Is1Cat CRing := is1cat_induced ring_cring.
+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.

theories/Algebra/Rings/QuotientRing.v

@@ -101,7 +101,7 @@ Section QuotientRing.
   Defined.
 
   Definition QuotientRing : Ring 
-    := Build_Ring (QuotientAbGroup R I) _ _ _.
+    := Build_Ring (QuotientAbGroup R I) _ _ _ _ _.
 
 End QuotientRing.
 

theories/Algebra/Rings/Ring.v

@@ -15,7 +15,7 @@ Local Open Scope ring_scope.
 Local Open Scope wc_iso_scope.
 
 (** A ring consists of the following data: *)
-Record Ring := {
+Record Ring := Build_Ring' {
   (** An underlying abelian group. *)
   ring_abgroup :> AbGroup;
   (** A multiplication operation. *)
@@ -24,6 +24,8 @@ Record Ring := {
   ring_one :: One ring_abgroup;
   (** Such that all they all satisfy the axioms of a ring. *)
   ring_isring :: IsRing ring_abgroup;
+  (** This field only exists so that opposite rings are definitionally involutive and can safely be ignored. *)
+  ring_mult_assoc_opp : forall x y z, (x * y) * z = x * (y * z);
 }.
 
 
@@ -175,11 +177,11 @@ Definition Build_RingIsomorphism'' (A B : Ring) (e : GroupIsomorphism A B)
   := @Build_RingIsomorphism' A B e (Build_IsSemiRingPreserving e _ H).
 
 (** Here is an alternative way to build a commutative ring using the underlying abelian group. *)
-Definition Build_Ring' (R : AbGroup)
+Definition Build_Ring (R : AbGroup)
   `(Mult R, One R, LeftDistribute R mult (@group_sgop R), RightDistribute R mult (@group_sgop R))
   (iscomm : @IsMonoid R mult one)
   : Ring
-  := Build_Ring R _ _ (Build_IsRing _ _ _  _ _).
+  := Build_Ring' R _ _ (Build_IsRing _ _ _  _ _) (fun x y z => (associativity x y z)^).
 
 (** ** Ring movement lemmas *)
 
@@ -277,7 +279,7 @@ Defined.
 Definition ring_product : Ring -> Ring -> Ring.
 Proof.
   intros R S.
-  snrapply Build_Ring'.
+  snrapply Build_Ring.
   1: exact (ab_biprod R S).
   1: exact (fun '(r1 , s1) '(r2 , s2) => (r1 * r2 , s1 * s2)).
   1: exact (ring_one , ring_one).
@@ -353,7 +355,7 @@ Defined.
 (** The image of a ring homomorphism *)
 Definition rng_image {R S : Ring} (f : R $-> S) : Ring.
 Proof.
-  snrapply (Build_Ring' (abgroup_image f)).
+  snrapply (Build_Ring (abgroup_image f)).
   { simpl.
     intros [x p] [y q].
     exists (x * y).
@@ -395,7 +397,33 @@ Proof.
   exact _.
 Defined. 
 
-(** *** More Ring laws *)
+(** ** Opposite Ring *)
+
+(** Given a ring [R] we can reverse the order of the multiplication to get another ring [R^op]. *)
+Definition rng_op : Ring -> Ring.
+Proof.
+  (** Let's carefully pull apart the ring structure and put it back together. Unfortunately, our definition of ring has some redundant data such as multiple hset assumptions, due to the mixing of algebraic strucutres. This isn't a problem in practice, but it does mean using typeclass inference here will pick up the wrong instance, therefore we carefully put it back together. See test/Algebra/Rings/Ring.v for a test checking this operation is definitionally involutive. *)
+  intros [R mult one
+    [is_abgroup [[monoid_ishset mult_assoc] li ri] ld rd]
+    mult_assoc_opp].
+  snrapply Build_Ring'.
+  4: split.
+  5: split.
+  5: split.
+  - exact R.
+  - exact (flip mult).
+  - exact one.
+  - exact is_abgroup.
+  - exact monoid_ishset.
+  - exact (fun x y z => mult_assoc_opp z y x).
+  - exact ri.
+  - exact li.
+  - exact (fun x y z => rd y z x).
+  - exact (fun x y z => ld z x y).
+  - exact (fun x y z => mult_assoc z y x).
+Defined.
+
+(** ** More Ring laws *)
 
 (** Powers of ring elements *)
 Definition rng_power {R : Ring} (x : R) (n : nat) : R := nat_iter n (x *.) ring_one.

theories/Algebra/Rings/Z.v

@@ -9,12 +9,18 @@ Require Import WildCat.Core.
 (** The ring of integers *)
 Definition cring_Z : CRing.
 Proof.
-  snrapply (Build_CRing abgroup_Z int_mul 1%int); repeat split; try exact _.
-  + exact int_mul_assoc.
-  + exact int_mul_1_l.
-  + exact int_mul_1_r.
-  + exact int_mul_comm.
-  + exact int_mul_add_distr_l.
+  snrapply Build_CRing'.
+  - exact abgroup_Z.
+  - exact 1%int.
+  - exact int_mul.
+  - exact int_mul_comm.
+  - exact int_mul_add_distr_l.
+  - split.
+    + split.
+      * exact _.
+      * exact int_mul_assoc.
+    + exact int_mul_1_l.
+    + exact int_mul_1_r.
 Defined.
 
 Local Open Scope mc_scope.
@@ -184,7 +190,7 @@ Qed.
 
 (** Preservation of * (multiplication) *)
 Global Instance issemigrouppreserving_cring_catamorphism_fun_mult (R : CRing)
-  : IsSemiGroupPreserving (Aop:=cring_mult) (Bop:=cring_mult)
+  : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.))
       (cring_catamorphism_fun R : cring_Z -> R).
 Proof.
   hnf. intros [x| |x] [y| |y].