Merge pull request #2071 from ndcroos/issue_2015

Work on issue #2015: grp_pow and related things

theories/Algebra/AbGroups/AbelianGroup.v

@@ -233,33 +233,13 @@ 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.
   snrapply Build_GroupHomomorphism.
   1: exact (fun a => grp_pow a n).
   intros a b.
-  induction n; cbn.
-  - exact (grp_unit_l _)^.
-  - 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.
+  apply grp_pow_mul, ab_comm.
 Defined.
 
 (** [ab_mul n] is natural. *)

theories/Algebra/Groups/Group.v

@@ -558,10 +558,42 @@ Definition grp_pow_neg {G : Group} (n : Int) (g : G)
   : grp_pow g (int_neg n) = grp_pow (- g) n.
 Proof.
   lhs nrapply int_iter_neg.
-  destruct n.
-  - cbn. by rewrite grp_inv_inv.
-  - reflexivity.
-  - reflexivity.
+  cbn; unfold grp_pow.
+  (* These agree, except for the proofs that [sg_op (-g)] is an equivalence. *)
+  apply int_iter_agree.
+Defined.
+
+(** Using a negative power in [grp_pow] is the same as first using a positive power and then inverting the result. *)
+Definition grp_pow_neg_inv {G: Group} (m : Int) (g : G) : grp_pow g (- m)%int = - grp_pow g m.
+Proof.
+  apply grp_moveL_1V.
+  lhs_V nrapply grp_pow_add.
+  by rewrite int_add_neg_l.
+Defined.
+
+(** Combining the two previous results gives that a power of an inverse is the inverse of the power. *)
+Definition grp_pow_neg_inv' {G: Group} (n: Int) (g : G) : grp_pow (- g) n = - grp_pow g n.
+Proof.
+  lhs_V nrapply grp_pow_neg.
+  apply grp_pow_neg_inv.
+Defined.
+
+(** [grp_pow] satisfies a multiplicative law of exponents. *)
+Definition grp_pow_int_mul {G : Group} (m n : Int) (g : G)
+  : grp_pow g (m * n)%int = grp_pow (grp_pow g m) n.
+Proof.
+  induction n.
+  - simpl.
+    by rewrite int_mul_0_r.
+  - rewrite int_mul_succ_r.
+    rewrite grp_pow_add.
+    rewrite grp_pow_succ.
+    apply grp_cancelL, IHn.
+  - rewrite int_mul_pred_r.
+    rewrite grp_pow_add.
+    rewrite grp_pow_neg_inv.
+    rewrite grp_pow_pred.
+    apply grp_cancelL, IHn.
 Defined.
 
 (** If [h] commutes with [g], then [h] commutes with [grp_pow g n]. *)
@@ -586,6 +618,35 @@ Proof.
   by apply grp_pow_commutes.
 Defined.
 
+(** If [g] and [h] commute, then [grp_pow (g * h) n] = (grp_pow g n) * (grp_pow h n)]. *)
+Definition grp_pow_mul {G : Group} (n : Int) (g h : G)
+  (c : g * h = h * g)
+  : grp_pow (g * h) n = (grp_pow g n) * (grp_pow h n).
+Proof.
+  induction n.
+  - simpl.
+    symmetry; nrapply grp_unit_r.
+  - rewrite 3 grp_pow_succ.
+    rewrite IHn.
+    rewrite 2 grp_assoc.
+    apply grp_cancelR.
+    rewrite <- 2 grp_assoc.
+    apply grp_cancelL.
+    apply grp_pow_commutes.
+    exact c^.
+  - simpl.
+    rewrite 3 grp_pow_pred.
+    rewrite IHn.
+    rewrite 2 grp_assoc.
+    apply grp_cancelR.
+    rewrite c.
+    rewrite grp_inv_op.
+    rewrite <- 2 grp_assoc.
+    apply grp_cancelL.
+    apply grp_pow_commutes.
+    symmetry; apply grp_commutes_inv, c.
+Defined.
+
 (** ** The category of Groups *)
 
 (** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *)

theories/Algebra/Rings/Z.v

@@ -4,7 +4,7 @@ Require Import Algebra.Rings.CRing.
 Require Import Spaces.Int Spaces.Pos.
 Require Import WildCat.Core.
 
-(** * In this file we define the ring [cring_Z] of integers with underlying abelian group [abroup_Z] defined in Algebra.AbGroups.Z. We also define multiplication by an integer in a general ring, and show that [cring_Z] is initial. *)
+(** * In this file we define the ring [cring_Z] of integers with underlying abelian group [abgroup_Z] defined in Algebra.AbGroups.Z. We also define multiplication by an integer in a general ring, and show that [cring_Z] is initial. *)
 
 (** The ring of integers *)
 Definition cring_Z : CRing.
@@ -27,29 +27,32 @@ Local Open Scope mc_scope.
 (** Given a ring element [r], we get a map [Int -> R] sending an integer to that multiple of [r]. *)
 Definition rng_int_mult (R : Ring) := grp_pow_homo : R -> Int -> R.
 
+(** Multiplying a ring element [r] by an integer [n] is equivalent to first multiplying the unit [1] of the ring by [n], and then multiplying the result by [r].  This is distributivity of right multiplication by [r] over the sum. *)
+Definition rng_int_mult_dist_r {R : Ring} (r : R) (n : cring_Z)
+  : rng_int_mult R r n = (rng_int_mult R 1 n) * r.
+Proof.
+  cbn.
+  rhs nrapply (grp_pow_natural (grp_homo_rng_right_mult r)); cbn.
+  by rewrite rng_mult_one_l.
+Defined.
+
+(** Similarly, there is a left-distributive law. *)
+Definition rng_int_mult_dist_l {R : Ring} (r : R) (n : cring_Z)
+  : rng_int_mult R r n = r * (rng_int_mult R 1 n).
+Proof.
+  cbn.
+  rhs nrapply (grp_pow_natural (grp_homo_rng_left_mult r)); cbn.
+  by rewrite rng_mult_one_r.
+Defined.
+
 (** [rng_int_mult R 1] preserves multiplication.  This requires that the specified ring element is the unit. *)
 Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
   : IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
   intros x y.
   cbn; unfold sg_op.
-  induction x as [|x|x].
-  - simpl.
-    by rhs nrapply rng_mult_zero_l.
-  - rewrite int_mul_succ_l.
-    rewrite grp_pow_add.
-    rewrite grp_pow_succ.
-    rhs nrapply rng_dist_r.
-    rewrite rng_mult_one_l.
-    f_ap.
-  - rewrite int_mul_pred_l.
-    rewrite grp_pow_add.
-    rewrite grp_pow_pred.
-    rhs nrapply rng_dist_r.
-    rewrite IHx.
-    f_ap.
-    lhs rapply (grp_homo_inv (grp_pow_homo 1)).
-    symmetry; apply rng_mult_negate.
+  lhs nrapply grp_pow_int_mul.
+  nrapply rng_int_mult_dist_l.
 Defined.
 
 (** [rng_int_mult R 1] is a ring homomorphism *)

theories/Spaces/Int.v

@@ -627,6 +627,17 @@ Proof.
     apply eisretr.
 Defined.
 
+(** In particular, homotopic maps have homotopic iterations. *)
+Definition int_iter_homotopic (n : Int) {A} (f f' : A -> A) `{!IsEquiv f} `{!IsEquiv f'}
+  (h : f == f')
+  : int_iter f n == int_iter f' n
+  := int_iter_commute_map f f' idmap h n.
+
+(** [int_iter f n x] doesn't depend on the proof that [f] is an equivalence. *)
+Definition int_iter_agree (n : Int) {A} (f : A -> A) {ief ief' : IsEquiv f}
+  : forall x, @int_iter A f ief n x = @int_iter A f ief' n x
+  := int_iter_homotopic n f f (fun _ => idpath).
+
 Definition int_iter_invariant (n : Int) {A} (f : A -> A) `{!IsEquiv f}
   (P : A -> Type)
   (Psucc : forall x, P x -> P (f x))