From 0eb264368aa42bb824a7a9024c3be2c51616c242 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 2 Jul 2024 17:33:01 -0400 Subject: [PATCH] Algebra/*: Use int_iter for grp_pow --- theories/Algebra/AbGroups/AbelianGroup.v | 39 ++++++------ theories/Algebra/Groups/Group.v | 81 +++++++----------------- theories/Algebra/Rings/Z.v | 3 +- theories/Spaces/Int.v | 16 +++++ 4 files changed, 59 insertions(+), 80 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 21983e60b41..1d850ddd8fd 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/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,26 +250,11 @@ 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_int_add_1. + by apply ab_mul_helper. + - rewrite 3 grp_pow_int_sub_1. + rewrite (grp_inv_op a b), (commutativity (-b) (-a)). + by apply ab_mul_helper. Defined. (** [ab_mul n] is natural. *) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 4093c25ad80..dcef27dbb68 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -478,98 +478,61 @@ End GroupMovement. (** 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. + := 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_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. + : grp_pow g (n.+1)%int = g * grp_pow g n + := int_iter_succ_l _ _ _. Definition grp_pow_int_sub_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. - + apply (grp_inv_l g)^. - + rhs srapply associativity. - rewrite grp_inv_l. - apply (grp_unit_l _)^. - - destruct n; reflexivity. -Defined. + : grp_pow g (n.-1)%int = (- g) * grp_pow g n + := int_iter_pred_l _ _ _. (** [grp_pow] commutes negative exponents to powers of the inverse *) Definition grp_pow_int_sign_commute {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 an additive 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. + lhs nrapply int_iter_add. 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. + 1: rewrite int_iter_succ_l, grp_pow_int_add_1. + 2: rewrite int_iter_pred_l, grp_pow_int_sub_1; cbn. + 1,2 : rhs_V srapply associativity; + apply ap, IHn. Defined. (** ** The category of Groups *) diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v index ea1470e6b73..cfe74590276 100644 --- a/theories/Algebra/Rings/Z.v +++ b/theories/Algebra/Rings/Z.v @@ -32,7 +32,7 @@ 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. + cbn; unfold sg_op. induction x as [|x|x]. - simpl. by rhs nrapply rng_mult_zero_l. @@ -59,6 +59,7 @@ Proof. 1: exact (rng_int_mult R 1). repeat split. 1,2: exact _. + apply rng_plus_zero_r. Defined. (** The integers are the initial commutative ring *) diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v index 6b4a8130b99..da60ce1c189 100644 --- a/theories/Spaces/Int.v +++ b/theories/Spaces/Int.v @@ -634,6 +634,22 @@ Proof. apply eisretr. Defined. +Definition int_iter_invariant (n : Int) {A} (f : A -> A) `{!IsEquiv f} + (P : A -> Type) + (Psucc : forall x, P x -> P (f x)) + (Ppred : forall x, P x -> P (f^-1 x)) + : forall x, P x -> P (int_iter f n x). +Proof. + induction n as [|n IHn|n IHn]; intro x. + - exact idmap. + - intro H. + rewrite int_iter_succ_l. + apply Psucc, IHn, H. + - intro H. + rewrite int_iter_pred_l. + apply Ppred, IHn, H. +Defined. + (** ** Exponentiation of loops *) Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)