finite sums of ring elements

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

theories/Algebra/Groups/Group.v

@@ -486,6 +486,16 @@ Proof.
     exact (ap (fun m => f g + m) IHn).
 Defined.
 
+(** All powers of the unit are the unit. *)
+Definition grp_pow_unit {G : Group} (n : nat)
+  : grp_pow (G:=G) mon_unit n = mon_unit.
+Proof.
+  induction n.
+  1: reflexivity.
+  lhs rapply left_identity.
+  exact IHn.
+Defined.
+
 (** ** The category of Groups *)
 
 (** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *)

theories/Algebra/Rings/Ring.v

@@ -1,8 +1,8 @@
 Require Import WildCat.
-Require Import Spaces.Nat.Core.
+Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.abstract_algebra.
-Require Import Algebra.AbGroups.
+Require Export Algebra.AbGroups.
 Require Export Classes.theory.rings.
 Require Import Modalities.ReflectiveSubuniverse.
 
@@ -454,7 +454,7 @@ Proof.
   - intros R S T f g; cbn; reflexivity.
 Defined.
 
-(** ** More Ring laws *)
+(** ** Powers *)
 
 (** Powers of ring elements *)
 Definition rng_power {R : Ring} (x : R) (n : nat) : R := nat_iter n (x *.) ring_one.
@@ -468,3 +468,232 @@ Proof.
   refine ((rng_mult_assoc _ _ _)^ @ _).
   exact (ap (x *.) IHn).
 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).
+Proof.
+  induction n as [|n IHn].
+  1: apply rng_mult_zero_r.
+  lhs nrapply rng_dist_l; simpl; f_ap.
+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).
+Proof.
+  induction n as [|n IHn].
+  1: apply rng_mult_zero_l.
+  lhs nrapply rng_dist_r; simpl; f_ap.
+Defined.
+
+(** ** Kronecker Delta *)
+
+(** The Kronecker delta function is a function of two natural numbers that is 1 when the two numbers are equal and 0 otherwise. It is useful for working with finite sums of ring elements. *)
+Definition kronecker_delta {R : Ring} (i j : nat) : R
+  := if dec (i = j) then 1 else 0.
+
+(** Kronecker delta with the same index is 1. This holds definitionally for a given natural number, but not definitionally for an arbitrary one. *)
+Definition kronecker_delta_refl {R : Ring} (i : nat)
+  : kronecker_delta (R:=R) i i = 1.
+Proof.
+  unfold kronecker_delta.
+  generalize (dec (i = i)).
+  by rapply decidable_paths_refl.
+Defined.
+
+(** Kronecker delta with different indices is 0. *)
+Definition kronecker_delta_neq {R : Ring} {i j : nat} (p : i <> j)
+  : kronecker_delta (R:=R) i j = 0.
+Proof.
+  unfold kronecker_delta.
+  by decidable_false (dec (i = j)) p.
+Defined.
+
+(** Kronecker delta is symmetric in its arguments. *)
+Definition kronecker_delta_symm {R : Ring} (i j : nat)
+  : kronecker_delta (R:=R) i j = kronecker_delta j i.
+Proof.
+  unfold kronecker_delta.
+  destruct (dec (i = j)) as [p|q].
+  - by decidable_true (dec (j = i)) p^.
+  - by decidable_false (dec (j = i)) (symmetric_neq q).
+Defined.
+
+(** Kronecker delta where the first index is strictly less than the second is 0. *)
+Definition kronecker_delta_lt {R : Ring} {i j : nat} (p : (i < j)%nat)
+  : kronecker_delta (R:=R) i j = 0.
+Proof.
+  apply kronecker_delta_neq.
+  intros q; destruct q.
+  by apply not_lt_n_n in p.
+Defined.
+
+(** Kronecker delta where the first index is strictly greater than the second is 0. *)
+Definition kronecker_delta_gt {R : Ring} {i j : nat} (p : (j < i)%nat)
+  : kronecker_delta (R:=R) i j = 0.
+Proof.
+  apply kronecker_delta_neq.
+  intros q; destruct q.
+  by apply not_lt_n_n in p.
+Defined.
+
+(** An injective endofunction on nat preserves the Kronecker delta. *)
+Definition kronecker_delta_map_inj {R : Ring} (i j : nat) (f : nat -> nat)
+  `{!IsInjective f}
+  : kronecker_delta (R:=R) (f i) (f j) = kronecker_delta i j.
+Proof.
+  unfold kronecker_delta.
+  destruct (dec (i = j)) as [p|p].
+  - by decidable_true (dec (f i = f j)) (ap f p).
+  - destruct (dec (f i = f j)) as [q|q].
+    + apply (injective f) in q.
+      contradiction.
+    + reflexivity.
+Defined.
+
+(** Kronecker delta commutes with any ring element. *)
+Definition kronecker_delta_comm {R : Ring} (i j : nat) (r : R)
+  :  r * kronecker_delta i j = kronecker_delta i j * r.
+Proof.
+  unfold kronecker_delta.
+  destruct (dec (i = j)).
+  - exact (rng_mult_one_r _ @ (rng_mult_one_l _)^).
+  - exact (rng_mult_zero_r _ @ (rng_mult_zero_l _)^).
+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.
+Proof.
+  induction n as [|n IHn] in i, Hi, f |- *.
+  1: destruct (not_leq_Sn_0 _ Hi).
+  destruct (dec (i = n)) as [p|p].
+  - destruct p; simpl.
+    rewrite kronecker_delta_refl.
+    rewrite rng_mult_one_l.
+    rewrite <- rng_plus_zero_r.
+    f_ap; [f_ap; rapply path_ishprop|].
+    nrapply rng_sum_zero.
+    intros k Hk.
+    rewrite (kronecker_delta_gt Hk).
+    apply rng_mult_zero_l.
+  - simpl; lhs nrapply ap.
+    + nrapply IHn.
+      apply diseq_implies_lt in p.
+      destruct p; [assumption|].
+      contradiction (lt_implies_not_geq Hi).
+    + rewrite (kronecker_delta_neq p).
+      rewrite rng_mult_zero_l.
+      rewrite rng_plus_zero_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.
+Proof.
+  lhs nrapply path_rng_sum.
+  2: nrapply rng_sum_kronecker_delta_l.
+  intros k Hk.
+  cbn; f_ap; apply kronecker_delta_symm.
+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.
+Proof.
+  lhs nrapply path_rng_sum.
+  2: nrapply rng_sum_kronecker_delta_l.
+  intros k Hk.
+  apply kronecker_delta_comm.
+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.
+Proof.
+  lhs nrapply path_rng_sum.
+  2: nrapply rng_sum_kronecker_delta_l'.
+  intros k Hk.
+  apply kronecker_delta_comm.
+Defined.