integer group powers

theories/Algebra/AbGroups/AbelianGroup.v

@@ -1,5 +1,5 @@
 Require Import Basics Types.
-Require Import Spaces.Nat.Core.
+Require Import Spaces.Nat.Core Spaces.Int.
 Require Export Classes.interfaces.canonical_names (Zero, zero, Plus).
 Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
 Require Export Algebra.Groups.Group.
@@ -228,26 +228,32 @@ Proof.
     1-2: exact negate_involutive.
 Defined.
 
-(** Multiplication by [n : nat] defines an endomorphism of any abelian group [A]. *)
-Definition ab_mul_nat {A : AbGroup} (n : nat) : GroupHomomorphism A A.
+(** 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.
-  1: exact (grp_unit_l _)^.
-  refine (_ @ associativity _ _ _).
-  refine (_ @ ap _ (associativity _ _ _)^).
-  rewrite (commutativity (grp_pow a n) b).
-  refine (_ @ ap _ (associativity _ _ _)).
-  refine (_ @ (associativity _ _ _)^).
-  apply grp_cancelL.
-  assumption.
+  - exact (grp_unit_l _)^.
+  - destruct n.
+    + cbn; by rewrite !grp_unit_r.
+    + simpl in IHn |- *.
+      rewrite IHn.
+      rewrite !simple_associativity.
+      do 2 f_ap.
+      rewrite (commutativity a).
+      rewrite <- 2 simple_associativity.
+      rewrite (commutativity b).
+      by rewrite !simple_associativity.
+  - (** TODO *)
+    Axiom transparent_admit : Empty.
+    snrapply (Empty_rec transparent_admit).
 Defined.
 
-Definition ab_mul_nat_homo {A B : AbGroup}
-  (f : GroupHomomorphism A B) (n : nat)
-  : f o ab_mul_nat n == ab_mul_nat n o f
+Definition ab_mul_homo {A B : AbGroup}
+  (f : GroupHomomorphism A B) (n : Int)
+  : f o ab_mul n == ab_mul n o f
   := grp_pow_homo f n.
 
 (** The image of an inclusion is a normal subgroup. *)
@@ -297,9 +303,12 @@ Proof.
   induction n as [|n IHn] in f, p |- *.
   1: reflexivity.
   simpl; f_ap.
-  apply IHn.
-  intros k Hk.
-  apply p.
+  destruct n.
+  1: reflexivity.
+  rewrite IHn.
+  - reflexivity.
+  - intros k Hk.
+    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.
+  Groups.FreeGroup AbGroups.Z BinInt.Core Spaces.Int.
 
 (** * Cyclic groups *)
 
@@ -44,7 +44,7 @@ Definition Z1_mul_nat `{Funext} (n : nat) : ab_Z1 $-> ab_Z1
   := Z1_rec (nat_to_Z1 n).
 
 Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
-  : Z1_rec a (nat_to_Z1 n) = ab_mul_nat n a.
+  : Z1_rec a (nat_to_Z1 n) = ab_mul n a.
 Proof.
   induction n as [|n H].
   1: easy.

theories/Algebra/AbGroups/Z.v

@@ -2,16 +2,15 @@ Require Import Basics.
 Require Import Spaces.Pos.Core Spaces.BinInt.
 Require Import Algebra.AbGroups.AbelianGroup.
 
+Local Set Universe Minimization ToSet.
+
 (** * The group of integers *)
 
 (** See also Cyclic.v for a definition of the integers as the free group on one generator. *)
 
 Local Open Scope binint_scope.
 
-Section MinimizationToSet.
-
-Local Set Universe Minimization ToSet.
-
+(** TODO: switch to [Int] *)
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
@@ -23,34 +22,3 @@ Proof.
     + exact binint_add_negation_r.
   - exact binint_add_comm.
 Defined.
-
-End MinimizationToSet.
-
-(** We can multiply by [n : Int] in any abelian group. *)
-Definition ab_mul (n : BinInt) {A : AbGroup} : GroupHomomorphism A A.
-Proof.
-  induction n.
-  - exact (grp_homo_compose ab_homo_negation (ab_mul_nat (pos_to_nat p))).
-  - exact grp_homo_const.
-  - exact (ab_mul_nat (pos_to_nat p)).
-Defined.
-
-(** Homomorphisms respect multiplication. *)
-Lemma ab_mul_homo {A B : AbGroup} (n : BinInt) (f : GroupHomomorphism A B)
-  : grp_homo_compose f (ab_mul n) == grp_homo_compose (ab_mul n) f.
-Proof.
-  intro x.
-  induction n.
-  - cbn. refine (grp_homo_inv _ _ @ _).
-    refine (ap negate _).
-    apply grp_pow_homo.
-  - cbn. apply grp_homo_unit.
-  - cbn. apply grp_pow_homo.
-Defined.
-
-(** Multiplication by zero gives the constant group homomorphism. *)
-Definition ab_mul_const `{Funext} {A : AbGroup} : ab_mul 0 (A:=A) = grp_homo_const.
-Proof.
-  apply equiv_path_grouphomomorphism.
-  reflexivity.
-Defined.

theories/Algebra/AbSES/SixTerm.v

@@ -1,6 +1,6 @@
 Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv
   Modalities.ReflectiveSubuniverse Truncations.Core Truncations.SeparatedTrunc
-  AbGroups Homotopy.ExactSequence
+  AbGroups Homotopy.ExactSequence Spaces.Int
   AbSES.Core AbSES.Pullback AbSES.Pushout BaerSum Ext PullbackFiberSequence.
 
 (** * The contravariant six-term sequence of Ext *)
@@ -194,7 +194,7 @@ Local Definition isexact_ext_cyclic_ab_iii@{u v w | u < v, v < w} `{Univalence}
 Local Definition ext_cyclic_exact@{u v w} `{Univalence}
   (n : nat) `{IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
   : IsExact@{v v v v v} (Tr (-1))
-      (ab_mul_nat (A:=A) n)
+      (ab_mul (A:=A) n)
       (abses_pushout_ext@{u w v} (abses_from_inclusion (Z1_mul_nat n))
          o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
 Proof.
@@ -211,7 +211,7 @@ Proof.
     apply moveR_equiv_V; symmetry.
     refine (ap f _ @ _).
     1: apply Z1_rec_beta.
-    exact (ab_mul_nat_homo f n Z1_gen).
+    exact (ab_mul_homo f n Z1_gen).
   - (* we get rid of [equiv_Z1_hom] *)
     apply isexact_equiv_fiber.
     apply isexact_ext_cyclic_ab_iii.
@@ -220,12 +220,12 @@ Defined.
 (** The main result of this section. *)
 Theorem ext_cyclic_ab@{u v w | u < v, v < w} `{Univalence}
   (n : nat) `{emb : IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
-  : ab_cokernel@{v w} (ab_mul_nat (A:=A) n)
+  : ab_cokernel@{v w} (ab_mul (A:=A) n)
       $<~> ab_ext@{u v} (cyclic'@{u v} n) A.
   (* We take a large cokernel in order to apply [abses_cokernel_iso]. *)
 Proof.
   pose (E := abses_from_inclusion (Z1_mul_nat n)).
-  snrefine (abses_cokernel_iso (ab_mul_nat n) _).
+  snrefine (abses_cokernel_iso (ab_mul n) _).
   - exact (grp_homo_compose
              (abses_pushout_ext E)
              (grp_iso_inverse (equiv_Z1_hom A))).

theories/Algebra/Groups/Group.v

@@ -17,7 +17,7 @@ Require Export Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, n
 Require Export Classes.theory.groups.
 Require Import Pointed.Core.
 Require Import WildCat.
-Require Import Spaces.Nat.Core.
+Require Import Spaces.Nat.Core Spaces.Int.
 Require Import Truncations.Core.
 
 Local Set Polymorphic Inductive Cumulativity.
@@ -390,6 +390,9 @@ Section GroupEquations.
 
   (** Inverses distribute over the group operation. *)
   Definition grp_inv_op : - (x * y) = -y * -x := negate_sg_op x y.
+
+  (** The inverse of the unit is the unit. *)
+  Definition grp_inv_unit : -mon_unit = mon_unit := negate_mon_unit (G :=G).
 
 End GroupEquations.
 
@@ -474,28 +477,61 @@ End GroupMovement.
 (** ** Power operation *)
 
 (** For a given [n : nat] we can define the [n]th power of a group element. *)
-Definition grp_pow {G : Group} (g : G) (n : nat) : G := nat_iter n (g *.) mon_unit.
+Definition grp_pow {G : Group} (g : G) (n : Int) : G
+  := match n with
+     | posS n => nat_iter n.+1%nat (g *.) mon_unit
+     | zero => mon_unit
+     | negS n => nat_iter n.+1%nat (fun x => -x * g) mon_unit
+     end.
 
 (** Any homomorphism respects [grp_pow]. *)
-Lemma grp_pow_homo {G H : Group} (f : GroupHomomorphism G H)
-  (n : nat) (g : G) : f (grp_pow g n) = grp_pow (f g) n.
+Lemma grp_pow_homo {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
+  : f (grp_pow g n) = grp_pow (f g) n.
 Proof.
   induction n.
-  + cbn. apply grp_homo_unit.
-  + cbn. refine ((grp_homo_op f g (grp_pow g n)) @ _).
-    exact (ap (fun m => f g + m) IHn).
+  - apply grp_homo_unit.
+  - destruct n.
+    + lhs nrapply grp_homo_op.
+      snrapply ap.
+      apply grp_homo_unit.
+    + lhs nrapply grp_homo_op.
+      snrapply ap.
+      assumption.
+  - destruct n.
+    + lhs snrapply grp_homo_op.
+      cbn; snrapply (ap (.* _)).
+      lhs nrapply grp_homo_inv; apply ap.
+      apply grp_homo_unit.
+    + lhs nrapply grp_homo_op.
+      cbn; snrapply (ap (.* _)).
+      lhs nrapply grp_homo_inv; apply ap.
+      assumption.
 Defined.
 
 (** All powers of the unit are the unit. *)
-Definition grp_pow_unit {G : Group} (n : nat)
+Definition grp_pow_unit {G : Group} (n : Int)
   : grp_pow (G:=G) mon_unit n = mon_unit.
 Proof.
   induction n.
-  1: reflexivity.
-  lhs rapply left_identity.
-  exact IHn.
+  - reflexivity.
+  - destruct n; by lhs nrapply grp_unit_l.
+  - destruct n.
+    + lhs nrapply grp_unit_r.
+      apply grp_inv_unit.
+    + lhs nrapply grp_unit_r.
+      rhs_V nrapply grp_inv_unit.
+      by snrapply ap.
 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. *)
+
+(** [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.
+  (** TODO: *)
+Abort.
+
 (** ** The category of Groups *)
 
 (** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *)