From 38c8dca762529390bb4a2d1d7d53db0f219b4eec Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 14 May 2024 17:02:25 +0100 Subject: [PATCH 1/3] 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. From 67117a9c9f27f420d4ce17bcacbe09629c59c90c Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 18 May 2024 01:52:59 +0100 Subject: [PATCH 2/3] split off and generalize Kronecker Delta in own file Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/KroneckerDelta.v | 148 ++++++++++++++++++++++++ theories/Algebra/Rings/Ring.v | 136 ---------------------- 2 files changed, 148 insertions(+), 136 deletions(-) create mode 100644 theories/Algebra/Rings/KroneckerDelta.v diff --git a/theories/Algebra/Rings/KroneckerDelta.v b/theories/Algebra/Rings/KroneckerDelta.v new file mode 100644 index 00000000000..3c849fd1076 --- /dev/null +++ b/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) + : 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. diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index d3043e9487b..06a0002c228 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/theories/Algebra/Rings/Ring.v @@ -561,139 +561,3 @@ Proof. 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. From 0c75086357a53b78a4fd92a4ef820ce132e3ec43 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 18 May 2024 17:47:32 +0100 Subject: [PATCH 3/3] generalize sums from rings to abgroups Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbelianGroup.v | 75 +++++++++++++++++++++++ theories/Algebra/Rings/KroneckerDelta.v | 18 +++--- theories/Algebra/Rings/Ring.v | 77 +----------------------- 3 files changed, 86 insertions(+), 84 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 7e6e01fa7bf..3a79d54ad6f 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/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. diff --git a/theories/Algebra/Rings/KroneckerDelta.v b/theories/Algebra/Rings/KroneckerDelta.v index 3c849fd1076..6f103efe5ef 100644 --- a/theories/Algebra/Rings/KroneckerDelta.v +++ b/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. diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v index 06a0002c228..5cc287be6d8 100644 --- a/theories/Algebra/Rings/Ring.v +++ b/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.