Merge pull request #2000 from Alizter/ps/rr/switch_to_int_in_cring_z

switch to Int in cring_Z

test/Algebra/Rings/Matrix.v

@@ -1,7 +1,7 @@
 From HoTT Require Import Basics.
 From HoTT Require Import Algebra.Rings.Matrix.
 From HoTT Require Import Spaces.Nat.Core Spaces.List.Core.
-From HoTT Require Import Algebra.Rings.Z Spaces.BinInt.Core Algebra.Rings.CRing.
+From HoTT Require Import Algebra.Rings.Z Spaces.Int Algebra.Rings.CRing.
 From HoTT Require Import Classes.interfaces.canonical_names.
 
 Local Open Scope mc_scope.
@@ -38,7 +38,7 @@ Definition test2_B := Build_Matrix' nat 4 4
 
 Definition test2 : entries test2_A = entries test2_B := idpath.
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
 (** Matrices with ring entries can be multiplied *)
 

theories/Algebra/AbGroups/AbelianGroup.v

@@ -228,6 +228,20 @@ Proof.
     1-2: exact negate_involutive.
 Defined.
 
+(** This goal comes up twice in the proof of [ab_mul], so we factor it out. *)
+Local Definition ab_mul_helper {A : AbGroup} (a b x y z : A)
+  (p : x = y + z)
+  : a + b + x = a + y + (b + z).
+Proof.
+  lhs_V srapply grp_assoc.
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL.
+  rhs srapply grp_assoc.
+  rhs nrapply (ap (fun g => g + z) (ab_comm y b)).
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL, p.
+Defined.
+
 (** Multiplication by [n : Int] defines an endomorphism of any abelian group [A]. *)
 Definition ab_mul {A : AbGroup} (n : Int) : GroupHomomorphism A A.
 Proof.
@@ -236,32 +250,18 @@ Proof.
   intros a b.
   induction n; cbn.
   - exact (grp_unit_l _)^.
-  - destruct n.
-    + reflexivity.
-    + rhs_V srapply (associativity a).
-      rhs srapply (ap _ (associativity _ b _)).
-      rewrite (commutativity (nat_iter _ _ _) b).
-      rhs_V srapply (ap _ (associativity b _ _)).
-      rhs srapply (associativity a).
-      apply grp_cancelL.
-      exact IHn.
-  - destruct n.
-    + rewrite (commutativity (-a)).
-      exact (grp_inv_op a b).
-    + rhs_V srapply (associativity (-a)).
-      rhs srapply (ap _ (associativity _ (-b) _)).
-      rewrite (commutativity (nat_iter _ _ _) (-b)).
-      rhs_V srapply (ap _ (associativity (-b) _ _)).
-      rhs srapply (associativity (-a)).
-      rewrite (commutativity (-a) (-b)), <- (grp_inv_op a b).
-      apply grp_cancelL.
-      exact IHn.
+  - rewrite 3 grp_pow_succ.
+    by apply ab_mul_helper.
+  - rewrite 3 grp_pow_pred.
+    rewrite (grp_inv_op a b), (commutativity (-b) (-a)).
+    by apply ab_mul_helper.
 Defined.
 
-Definition ab_mul_homo {A B : AbGroup}
+(** [ab_mul n] is natural. *)
+Definition ab_mul_natural {A B : AbGroup}
   (f : GroupHomomorphism A B) (n : Int)
   : f o ab_mul n == ab_mul n o f
-  := grp_pow_homo f n.
+  := grp_pow_natural f n.
 
 (** The image of an inclusion is a normal subgroup. *)
 Definition ab_image_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f} : NormalSubgroup B
@@ -303,18 +303,17 @@ Proof.
 Defined.
 
 (** If the function is constant in the range of a finite sum then the sum is equal to the constant times [n]. This is a group power in the underlying group. *)
-Definition ab_sum_const {A : AbGroup} (n : nat) (r : A)
-  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = r)
-  : ab_sum n f = grp_pow r n.
+Definition ab_sum_const {A : AbGroup} (n : nat) (a : A)
+  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a)
+  : ab_sum n f = ab_mul n a.
 Proof.
   induction n as [|n IHn] in f, p |- *.
   - reflexivity.
   - rhs nrapply (ap@{Set _} _ (int_of_nat_succ_commute n)).
-    rhs nrapply grp_pow_int_add_1.
+    rhs nrapply grp_pow_succ.
     simpl. f_ap.
-    rewrite IHn.
-    + reflexivity.
-    + intros. apply p.
+    apply IHn.
+    intros. apply p.
 Defined.
 
 (** If the function is zero in the range of a finite sum then the sum is zero. *)

theories/Algebra/AbGroups/Cyclic.v

@@ -1,6 +1,6 @@
 Require Import Basics Types WildCat.Core Truncations.Core
   AbelianGroup AbHom Centralizer AbProjective
-  Groups.FreeGroup AbGroups.Z BinInt.Core Spaces.Int.
+  Groups.FreeGroup AbGroups.Z Spaces.Int.
 
 (** * Cyclic groups *)
 
@@ -48,7 +48,7 @@ Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
 Proof.
   induction n as [|n H].
   1: easy.
-  refine (grp_pow_homo _ _ _ @ _); simpl.
+  refine (grp_pow_natural _ _ _ @ _); simpl.
   by rewrite grp_unit_r.
 Defined.
 
@@ -71,7 +71,7 @@ Defined.
 
 (** The map sending the generator to [1 : Int]. *)
 Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z
-  := Z1_rec (G:=abgroup_Z) 1%binint.
+  := Z1_rec (G:=abgroup_Z) 1%int.
 
 (** TODO:  Prove that [Z1_to_Z] is a group isomorphism. *)
 

theories/Algebra/AbGroups/Z.v

@@ -1,5 +1,5 @@
 Require Import Basics.
-Require Import Spaces.Pos.Core Spaces.BinInt.
+Require Import Spaces.Pos.Core Spaces.Int.
 Require Import Algebra.AbGroups.AbelianGroup.
 
 Local Set Universe Minimization ToSet.
@@ -8,17 +8,25 @@ Local Set Universe Minimization ToSet.
 
 (** See also Cyclic.v for a definition of the integers as the free group on one generator. *)
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
-(** TODO: switch to [Int] *)
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
-  - refine (Build_Group BinInt binint_add 0 binint_negation _); repeat split.
+  - refine (Build_Group Int int_add 0 int_neg _); repeat split.
     + exact _.
-    + exact binint_add_assoc.
-    + exact binint_add_0_r.
-    + exact binint_add_negation_l.
-    + exact binint_add_negation_r.
-  - exact binint_add_comm.
+    + exact int_add_assoc.
+    + exact int_add_0_r.
+    + exact int_add_neg_l.
+    + exact int_add_neg_r.
+  - exact int_add_comm.
+Defined.
+
+(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. *)
+Definition grp_pow_homo {G : Group} (g : G)
+  : GroupHomomorphism abgroup_Z G.
+Proof.
+  snrapply Build_GroupHomomorphism.
+  1: exact (grp_pow g).
+  intros m n; apply grp_pow_add.
 Defined.

theories/Algebra/AbSES/SixTerm.v

@@ -211,7 +211,7 @@ Proof.
     apply moveR_equiv_V; symmetry.
     refine (ap f _ @ _).
     1: apply Z1_rec_beta.
-    exact (ab_mul_homo f n Z1_gen).
+    exact (ab_mul_natural f n Z1_gen).
   - (* we get rid of [equiv_Z1_hom] *)
     apply isexact_equiv_fiber.
     apply isexact_ext_cyclic_ab_iii.

theories/Algebra/Groups/Group.v

@@ -476,100 +476,63 @@ End GroupMovement.
 
 (** ** Power operation *)
 
-(** For a given [n : nat] we can define the [n]th power of a group element. *)
+(** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *)
 Definition grp_pow {G : Group} (g : G) (n : Int) : G
-  := match n with
-     | posS n => nat_iter n (g *.) g
-     | zero => mon_unit
-     | negS n => nat_iter n ((- g) *.) (- g)
-     end.
-
-(** Any homomorphism respects [grp_pow]. *)
-Lemma grp_pow_homo {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
+  := int_iter (g *.) n mon_unit.
+
+(** Any homomorphism respects [grp_pow]. In other words, [fun g => grp_pow g n] is natural. *)
+Lemma grp_pow_natural {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
   : f (grp_pow g n) = grp_pow (f g) n.
 Proof.
-  induction n.
-  - apply grp_homo_unit.
-  - destruct n; simpl in IHn |- *.
-    + reflexivity.
-    + lhs snrapply grp_homo_op.
-      apply ap.
-      exact IHn.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_homo_inv.
-    + lhs snrapply grp_homo_op.
-      apply ap011.
-      * apply grp_homo_inv.
-      * exact IHn.
+  lhs snrapply (int_iter_commute_map _ ((f g) *.)).
+  1: nrapply grp_homo_op.
+  apply (ap (int_iter _ n)), grp_homo_unit.
 Defined.
 
 (** All powers of the unit are the unit. *)
 Definition grp_pow_unit {G : Group} (n : Int)
   : grp_pow (G:=G) mon_unit n = mon_unit.
 Proof.
-  induction n.
+  snrapply (int_iter_invariant n _ (fun g => g = mon_unit)); cbn.
+  1, 2: apply paths_ind_r.
+  - apply grp_unit_r.
+  - lhs nrapply grp_unit_r. apply grp_inv_unit.
   - reflexivity.
-  - destruct n; simpl. 
-    + reflexivity.
-    + by lhs nrapply grp_unit_l.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_inv_unit.
-    + destruct IHn^.
-      rhs_V apply (@grp_inv_unit G).
-      apply grp_unit_r.
 Defined.
 
 (** Note that powers don't preserve the group operation as it is not commutative. This does hold in an abelian group so such a result will appear later. *)
 
-(** Helper functions for [grp_pow_int_add]. This is how we can unfold [grp_pow] once. *)
+(** The next two results tell us how [grp_pow] unfolds. *)
+Definition grp_pow_succ {G : Group} (n : Int) (g : G)
+  : grp_pow g (n.+1)%int = g * grp_pow g n
+  := int_iter_succ_l _ _ _.
 
-Definition grp_pow_int_add_1 {G : Group} (n : Int) (g : G)
-  : grp_pow g (n.+1)%int = g * grp_pow g n.
-Proof.
-  induction n; simpl.
-  - exact (grp_unit_r g)^.
-  - destruct n; reflexivity.
-  - destruct n.
-    + apply (grp_inv_r g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_r. 
-      apply (grp_unit_l _)^.
-Defined.
+Definition grp_pow_pred {G : Group} (n : Int) (g : G)
+  : grp_pow g (n.-1)%int = (- g) * grp_pow g n
+  := int_iter_pred_l _ _ _.
 
-Definition grp_pow_int_sub_1 {G : Group} (n : Int) (g : G)
-  : grp_pow g (n.-1)%int = (- g) * grp_pow g n.
+(** [grp_pow] satisfies an additive law of exponents. *)
+Definition grp_pow_add {G : Group} (m n : Int) (g : G)
+  : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.
 Proof.
-  induction n; simpl.
-  - exact (grp_unit_r (-g))^.
-  - destruct n.
-    + apply (grp_inv_l g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_l.
-      apply (grp_unit_l _)^.
-  - destruct n; reflexivity.
+  lhs nrapply int_iter_add.
+  induction n; cbn.
+  1: exact (grp_unit_l _)^.
+  1: rewrite int_iter_succ_l, grp_pow_succ.
+  2: rewrite int_iter_pred_l, grp_pow_pred; cbn.
+  1,2 : rhs_V srapply associativity;
+        apply ap, IHn.
 Defined.
 
 (** [grp_pow] commutes negative exponents to powers of the inverse *)
-Definition grp_pow_int_sign_commute {G : Group} (n : Int) (g : G)
+Definition grp_pow_neg {G : Group} (n : Int) (g : G)
   : grp_pow g (int_neg n) = grp_pow (- g) n.
 Proof.
-  induction n.
+  lhs nrapply int_iter_neg.
+  destruct n.
+  - cbn. by rewrite grp_inv_inv.
+  - reflexivity.
   - reflexivity.
-  - destruct n; reflexivity.
-  - destruct n; simpl; rewrite grp_inv_inv; reflexivity.
-Defined.
-
-(** [grp_pow] satisfies a law of exponents. *)
-Definition grp_pow_int_add {G : Group} (m n : Int) (g : G)
-  : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.
-Proof.
-  induction n; cbn.
-  1: exact (grp_unit_l _)^.
-  1: rewrite int_add_succ_l, 2 grp_pow_int_add_1.
-  2: rewrite int_add_pred_l, 2 grp_pow_int_sub_1.
-  1,2: rhs_V srapply associativity; 
-       snrapply (ap (_ *.));
-       exact IHn.
 Defined.
 
 (** ** The category of Groups *)