From 9cbbffd1b6c44c60167f5e1601fdd1cacd7a0f66 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 14 May 2024 17:02:25 +0100 Subject: [PATCH] finite sums of ring elements Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Group.v | 10 ++ theories/Algebra/Rings/Ring.v | 235 +++++++++++++++++++++++++++++++- 2 files changed, 242 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index f8c96181a9a..aeb779eeb54 100644 --- a/theories/Algebra/Groups/Group.v +++ b/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. *) diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index c2210905914..d3043e9487b 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/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.