From a50f23074c6a6f63e309c6ce5c6a1361073ead30 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 14 Nov 2024 21:37:50 +0000 Subject: [PATCH] reorganise finite sums (in abgroups) into their own file Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups.v | 1 + theories/Algebra/AbGroups/AbelianGroup.v | 70 --------------------- theories/Algebra/AbGroups/FiniteSum.v | 78 ++++++++++++++++++++++++ 3 files changed, 79 insertions(+), 70 deletions(-) create mode 100644 theories/Algebra/AbGroups/FiniteSum.v diff --git a/theories/Algebra/AbGroups.v b/theories/Algebra/AbGroups.v index a664c93ddb4..4d06aa684fb 100644 --- a/theories/Algebra/AbGroups.v +++ b/theories/Algebra/AbGroups.v @@ -10,6 +10,7 @@ Require Export HoTT.Algebra.AbGroups.Biproduct. Require Export HoTT.Algebra.AbGroups.AbHom. Require Export HoTT.Algebra.AbGroups.Cyclic. Require Export HoTT.Algebra.AbGroups.Centralizer. +Require Export HoTT.Algebra.AbGroups.FiniteSum. (* The theory of Ext groups of abelian groups is in HoTT.Algebra.AbSES. *) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 0e84f177736..2a58a7d0c14 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -290,73 +290,3 @@ 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. - exact (f k _). -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) (a : A) - (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a) - : ab_sum n f = ab_mul n a. -Proof. - induction n as [|n IHn] in f, p |- *. - - reflexivity. - - rhs_V nrapply (ap@{Set _} _ (int_nat_succ n)). - rhs nrapply grp_pow_succ. - simpl. f_ap. - apply IHn. - intros. 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/AbGroups/FiniteSum.v b/theories/Algebra/AbGroups/FiniteSum.v new file mode 100644 index 00000000000..1010f391da5 --- /dev/null +++ b/theories/Algebra/AbGroups/FiniteSum.v @@ -0,0 +1,78 @@ +Require Import Basics.Overture Basics.Tactics. +Require Import Spaces.Nat.Core Spaces.Int. +Require Export Classes.interfaces.canonical_names (Zero, zero, Plus). +Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative). +Require Import AbelianGroup. + +Local Open Scope mc_scope. +Local Open Scope mc_add_scope. + +(** * 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. + exact (f k _). +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) (a : A) + (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a) + : ab_sum n f = ab_mul n a. +Proof. + induction n as [|n IHn] in f, p |- *. + - reflexivity. + - rhs_V nrapply (ap@{Set _} _ (int_nat_succ n)). + rhs nrapply grp_pow_succ. + simpl. f_ap. + apply IHn. + intros. 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.