generalize sums from rings to abgroups

Signed-off-by: Ali Caglayan <[email protected]>

theories/Algebra/AbGroups/AbelianGroup.v

@@ -1,4 +1,5 @@
 Require Import Basics Types.
+Require Import Spaces.Nat.Core.
 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.
@@ -34,6 +35,9 @@ Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit.
 Global Instance plus_abgroup (A : AbGroup) : Plus A := group_sgop.
 Global Instance negate_abgroup (A : AbGroup) : Negate A := group_inverse.
 
+Definition ab_comm {A : AbGroup} (x y : A) : x + y = y + x
+  := commutativity x y.
+
 (** ** Paths between abelian groups *)
 
 Definition equiv_path_abgroup `{Univalence} {A B : AbGroup@{u}}
@@ -270,3 +274,74 @@ Proof.
   induction q.
   exact (p g).
 Defined.
+
+(** ** Finite Sums *)
+
+(** Indexed finite sum of abelian group elements. *)
+Definition ab_sum {A : AbGroup} (n : nat) (f : forall k, (k < n)%nat -> A) : A.
+Proof.
+  induction n as [|n IHn].
+  - exact zero.
+  - refine (f n _ + IHn _).
+    intros k Hk.
+    refine (f k _).
+    apply leq_S.
+    exact Hk.
+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.
+Proof.
+  induction n as [|n IHn] in f, p |- *.
+  1: reflexivity.
+  simpl; f_ap.
+  apply IHn.
+  intros k Hk.
+  apply p.
+Defined.
+
+(** If the function is zero in the range of a finite sum then the sum is zero. *)
+Definition ab_sum_zero {A : AbGroup} (n : nat)
+  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = 0)
+  : ab_sum n f = 0.
+Proof.
+  lhs nrapply (ab_sum_const _ 0 f p).
+  apply grp_pow_unit.
+Defined.
+
+(** Finite sums distribute over addition. *)
+Definition ab_sum_plus {A : AbGroup} (n : nat) (f g : forall k, (k < n)%nat -> A)
+  : ab_sum n (fun k Hk => f k Hk + g k Hk)
+    = ab_sum n (fun k Hk => f k Hk) + ab_sum n (fun k Hk => g k Hk).
+Proof.
+  induction n as [|n IHn].
+  1: by rewrite grp_unit_l.
+  simpl.
+  rewrite <- !grp_assoc; f_ap.
+  rewrite IHn, ab_comm, <- grp_assoc; f_ap.
+  by rewrite ab_comm.
+Defined.
+
+(** Double finite sums commute. *)
+Definition ab_sum_sum {A : AbGroup} (m n : nat)
+  (f : forall i j, (i < m)%nat -> (j < n)%nat -> A)
+  : ab_sum m (fun i Hi => ab_sum n (fun j Hj => f i j Hi Hj))
+   = ab_sum n (fun j Hj => ab_sum m (fun i Hi => f i j Hi Hj)).
+Proof.
+  induction n as [|n IHn] in m, f |- *.
+  1: by nrapply ab_sum_zero.
+  lhs nrapply ab_sum_plus; cbn; f_ap.
+Defined.
+
+(** Finite sums are equal if the functions are equal in the range. *)
+Definition path_ab_sum {A : AbGroup} {n : nat} {f g : forall k, (k < n)%nat -> A}
+  (p : forall k Hk, f k Hk = g k Hk)
+  : ab_sum n f = ab_sum n g.
+Proof.
+  induction n as [|n IHn].
+  1: reflexivity.
+  cbn; f_ap.
+  by apply IHn.
+Defined.

theories/Algebra/Rings/KroneckerDelta.v

@@ -89,7 +89,7 @@ Defined.
 (** Kronecker delta can be used to extract a single term from a finite sum. *)
 Definition rng_sum_kronecker_delta_l {R : Ring} (n i : nat) (Hi : (i < n)%nat)
   (f : forall k, (k < n)%nat -> R)
-  : rng_sum n (fun j Hj => kronecker_delta i j * f j Hj) = f i Hi.
+  : ab_sum n (fun j Hj => kronecker_delta i j * f j Hj) = f i Hi.
 Proof.
   induction n as [|n IHn] in i, Hi, f |- *.
   1: destruct (not_leq_Sn_0 _ Hi).
@@ -99,7 +99,7 @@ Proof.
     rewrite rng_mult_one_l.
     rewrite <- rng_plus_zero_r.
     f_ap; [f_ap; rapply path_ishprop|].
-    nrapply rng_sum_zero.
+    nrapply ab_sum_zero.
     intros k Hk.
     rewrite (kronecker_delta_gt Hk).
     apply rng_mult_zero_l.
@@ -110,16 +110,16 @@ Proof.
       contradiction (lt_implies_not_geq Hi).
     + rewrite (kronecker_delta_neq p).
       rewrite rng_mult_zero_l.
-      rewrite rng_plus_zero_l.
+      rewrite grp_unit_l.
       f_ap; apply path_ishprop.
 Defined.
 
 (** Variant of [rng_sum_kronecker_delta_l] where the indexing is swapped. *)
 Definition rng_sum_kronecker_delta_l' {R : Ring} (n i : nat) (Hi : (i < n)%nat)
   (f : forall k, (k < n)%nat -> R)
-  : rng_sum n (fun j Hj => kronecker_delta j i * f j Hj) = f i Hi.
+  : ab_sum n (fun j Hj => kronecker_delta j i * f j Hj) = f i Hi.
 Proof.
-  lhs nrapply path_rng_sum.
+  lhs nrapply path_ab_sum.
   2: nrapply rng_sum_kronecker_delta_l.
   intros k Hk.
   cbn; f_ap; apply kronecker_delta_symm.
@@ -128,9 +128,9 @@ Defined.
 (** Variant of [rng_sum_kronecker_delta_l] where the Kronecker delta appears on the right. *)
 Definition rng_sum_kronecker_delta_r {R : Ring} (n i : nat) (Hi : (i < n)%nat)
   (f : forall k, (k < n)%nat -> R)
-  : rng_sum n (fun j Hj => f j Hj * kronecker_delta i j) = f i Hi.
+  : ab_sum n (fun j Hj => f j Hj * kronecker_delta i j) = f i Hi.
 Proof.
-  lhs nrapply path_rng_sum.
+  lhs nrapply path_ab_sum.
   2: nrapply rng_sum_kronecker_delta_l.
   intros k Hk.
   apply kronecker_delta_comm.
@@ -139,9 +139,9 @@ Defined.
 (** Variant of [rng_sum_kronecker_delta_r] where the indexing is swapped. *)
 Definition rng_sum_kronecker_delta_r' {R : Ring} (n i : nat) (Hi : (i < n)%nat)
   (f : forall k, (k < n)%nat -> R)
-  : rng_sum n (fun j Hj => f j Hj * kronecker_delta j i) = f i Hi.
+  : ab_sum n (fun j Hj => f j Hj * kronecker_delta j i) = f i Hi.
 Proof.
-  lhs nrapply path_rng_sum.
+  lhs nrapply path_ab_sum.
   2: nrapply rng_sum_kronecker_delta_l'.
   intros k Hk.
   apply kronecker_delta_comm.

theories/Algebra/Rings/Ring.v

@@ -471,82 +471,9 @@ Defined.
 
 (** ** Finite Sums *)
 
-(** Indexed finite sum of ring elements. *)
-Definition rng_sum {R : Ring} (n : nat) (f : forall k, (k < n)%nat -> R) : R.
-Proof.
-  induction n as [|n IHn].
-  - exact ring_zero.
-  - refine (f n _ + IHn _).
-    intros k Hk.
-    refine (f k _).
-    apply leq_S.
-    exact Hk.
-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 abelian group. *)
-Definition rng_sum_const {R : Ring} (n : nat) (r : R)
-  (f : forall k, (k < n)%nat -> R) (p : forall k Hk, f k Hk = r)
-  : rng_sum n f = grp_pow r n.
-Proof.
-  induction n as [|n IHn] in f, p |- *.
-  1: reflexivity.
-  simpl; f_ap.
-  apply IHn.
-  intros k Hk.
-  apply p.
-Defined.
-
-(** If the function is zero in the range of a finite sum then the sum is zero. *)
-Definition rng_sum_zero {R : Ring} (n : nat)
-  (f : forall k, (k < n)%nat -> R) (p : forall k Hk, f k Hk = 0)
-  : rng_sum n f = 0.
-Proof.
-  lhs nrapply (rng_sum_const _ 0 f p).
-  apply grp_pow_unit.
-Defined.
-
-(** Finite sums distribute over addition. *)
-Definition rng_sum_plus {R : Ring} (n : nat) (f g : forall k, (k < n)%nat -> R)
-  : rng_sum n (fun k Hk => f k Hk + g k Hk)
-    = rng_sum n (fun k Hk => f k Hk) + rng_sum n (fun k Hk => g k Hk).
-Proof.
-  induction n as [|n IHn].
-  1: by rewrite rng_plus_zero_l.
-  simpl.
-  rhs_V nrapply rng_plus_assoc.
-  rhs nrapply (ap (_ +)).
-  2: lhs nrapply rng_plus_assoc.
-  2: nrapply (ap (+ _)).
-  2: apply rng_plus_comm.
-  lhs_V nrapply rng_plus_assoc; f_ap.
-  rhs_V nrapply rng_plus_assoc; f_ap.
-Defined.
-
-(** Double finite sums commute. *)
-Definition rng_sum_sum {R : Ring} (m n : nat)
-  (f : forall i j, (i < m)%nat -> (j < n)%nat -> R)
-  : rng_sum m (fun i Hi => rng_sum n (fun j Hj => f i j Hi Hj))
-   = rng_sum n (fun j Hj => rng_sum m (fun i Hi => f i j Hi Hj)).
-Proof.
-  induction n as [|n IHn] in m, f |- *.
-  1: by nrapply rng_sum_zero.
-  lhs nrapply rng_sum_plus; cbn; f_ap.
-Defined.
-
-(** Finite sums are equal if the functions are equal in the range. *)
-Definition path_rng_sum {R : Ring} {n : nat} {f g : forall k, (k < n)%nat -> R}
-  (p : forall k Hk, f k Hk = g k Hk)
-  : rng_sum n f = rng_sum n g.
-Proof.
-  induction n as [|n IHn].
-  1: reflexivity.
-  cbn; f_ap.
-  by apply IHn.
-Defined.
-
 (** Ring multiplication distributes over finite sums on the left. *)
 Definition rng_sum_dist_l {R : Ring} (n : nat) (f : forall k, (k < n)%nat -> R) (r : R)
-  : r * rng_sum n f = rng_sum n (fun k Hk => r * f k Hk).
+  : r * ab_sum n f = ab_sum n (fun k Hk => r * f k Hk).
 Proof.
   induction n as [|n IHn].
   1: apply rng_mult_zero_r.
@@ -555,7 +482,7 @@ Defined.
 
 (** Ring multiplication distributes over finite sums on the right. *)
 Definition rng_sum_dist_r {R : Ring} (n : nat) (f : forall k, (k < n)%nat -> R) (r : R)
-  : rng_sum n f * r = rng_sum n (fun k Hk => f k Hk * r).
+  : ab_sum n f * r = ab_sum n (fun k Hk => f k Hk * r).
 Proof.
   induction n as [|n IHn].
   1: apply rng_mult_zero_l.