Merge pull request #1959 from Alizter/finite-sums

finite sums of ring elements

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/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/KroneckerDelta.v

@@ -0,0 +1,148 @@
+Require Import Basics.Overture Basics.Decidable Spaces.Nat.
+Require Import Algebra.Rings.Ring.
+Require Import Classes.interfaces.abstract_algebra.
+
+(** ** Kronecker Delta *)
+
+Section AssumeDecidable.
+  (** Throughout this section, we assume that we have a type [A] with decidable equality. This will be our indexing type and can be thought of as [nat] for reading purposes. *)
+
+  Context {A : Type} `{DecidablePaths A}.
+
+  (** The Kronecker delta function is a function of elements of [A] 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 : A) : R
+    := if dec (i = j) then 1 else 0.
+
+  (** Kronecker delta with the same index is 1. *)
+  Definition kronecker_delta_refl {R : Ring} (i : A)
+    : kronecker_delta (R:=R) i i = 1.
+  Proof.
+    unfold kronecker_delta.
+    generalize (dec (i = i)).
+    by rapply decidable_paths_refl.
+  Defined.
+
+  (** Kronecker delta with differing indices is 0. *)
+  Definition kronecker_delta_neq {R : Ring} {i j : A} (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 : A)
+    : 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.
+
+  (** An injective endofunction on [A] preserves the Kronecker delta. *)
+  Definition kronecker_delta_map_inj {R : Ring} (i j : A) (f : A -> A)
+    `{!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 : A) (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.
+
+End AssumeDecidable.
+
+(** The following lemmas are specialised to when the indexing type is [nat]. *)
+
+(** 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.
+
+(** 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)
+  : 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).
+  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 ab_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 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)
+  : ab_sum n (fun j Hj => kronecker_delta j i * f j Hj) = f i Hi.
+Proof.
+  lhs nrapply path_ab_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)
+  : ab_sum n (fun j Hj => f j Hj * kronecker_delta i j) = f i Hi.
+Proof.
+  lhs nrapply path_ab_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)
+  : ab_sum n (fun j Hj => f j Hj * kronecker_delta j i) = f i Hi.
+Proof.
+  lhs nrapply path_ab_sum.
+  2: nrapply rng_sum_kronecker_delta_l'.
+  intros k Hk.
+  apply kronecker_delta_comm.
+Defined.

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,23 @@ Proof.
   refine ((rng_mult_assoc _ _ _)^ @ _).
   exact (ap (x *.) IHn).
 Defined.
+
+(** ** Finite Sums *)
+
+(** 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 * 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.
+  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)
+  : 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.
+  lhs nrapply rng_dist_r; simpl; f_ap.
+Defined.