From f22e13aab7edd49879960b3e90904d02f78d586c Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 8 Sep 2024 15:49:36 -0400 Subject: [PATCH 1/4] Spaces/Int: add int_iter_homotopic, int_iter_agree --- theories/Spaces/Int.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v index a352b33d5a8..5657f5734bf 100644 --- a/theories/Spaces/Int.v +++ b/theories/Spaces/Int.v @@ -634,6 +634,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)) From 349a357937214870c34f7c5d948dfe93eaf05bc1 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 8 Sep 2024 15:50:22 -0400 Subject: [PATCH 2/4] Groups/Group: more results about grp_pow --- theories/Algebra/Groups/Group.v | 69 +++++++++++++++++++++++++++++++-- 1 file changed, 65 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 3bfcafdf39e..497ebf9885e 100644 --- a/theories/Algebra/Groups/Group.v +++ b/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. *) From a60114388cab3c870cef1ba6143fbd287b863624 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 8 Sep 2024 15:51:03 -0400 Subject: [PATCH 3/4] AbelianGroup: simplify proof of ab_mul --- theories/Algebra/AbGroups/AbelianGroup.v | 22 +--------------------- 1 file changed, 1 insertion(+), 21 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index e6f2d4fb734..6d2d7995b9d 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/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. *) From 9b73029584f796d94863f04078d88a893caf186f Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 8 Sep 2024 15:51:37 -0400 Subject: [PATCH 4/4] Rings/Z: add rng_int_mult_dist_l/r and simplify proof of issemigrouppreserving_mult_rng_int_mult --- theories/Algebra/Rings/Z.v | 39 ++++++++++++++++++++------------------ 1 file changed, 21 insertions(+), 18 deletions(-) diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v index 61f74885f74..8f8c8a25098 100644 --- a/theories/Algebra/Rings/Z.v +++ b/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 *)