Telescoping sums in abelian groups (#1944)

Straightforward and small, hopefully.

Author: lowasser

src/group-theory/abelian-groups.lagda.md

@@ -364,6 +364,9 @@ module _
   right-subtraction-Ab : type-Ab A → type-Ab A → type-Ab A
   right-subtraction-Ab = right-div-Group (group-Ab A)
 
+  right-subtraction-Ab' : type-Ab A → type-Ab A → type-Ab A
+  right-subtraction-Ab' y x = right-subtraction-Ab x y
+
   ap-right-subtraction-Ab :
     {x x' y y' : type-Ab A} → x ＝ x' → y ＝ y' →
     right-subtraction-Ab x y ＝ right-subtraction-Ab x' y'

src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md

@@ -25,6 +25,8 @@ open import foundation.universe-levels
 
 open import group-theory.abelian-groups
 open import group-theory.commutative-monoids
+open import group-theory.function-abelian-groups
+open import group-theory.homomorphisms-abelian-groups
 open import group-theory.multiples-of-elements-abelian-groups
 open import group-theory.sums-of-finite-sequences-of-elements-commutative-monoids
 open import group-theory.sums-of-finite-sequences-of-elements-commutative-semigroups
@@ -33,6 +35,9 @@ open import group-theory.sums-of-finite-sequences-of-elements-groups
 open import linear-algebra.finite-sequences-in-abelian-groups
 open import linear-algebra.finite-sequences-in-commutative-monoids
 
+open import lists.finite-sequences
+open import lists.pairs-of-successive-elements-finite-sequences
+
 open import univalent-combinatorics.coproduct-types
 open import univalent-combinatorics.standard-finite-types
 ```
@@ -146,7 +151,7 @@ module _
     extend-sum-fin-sequence-type-Commutative-Monoid (commutative-monoid-Ab G)
 ```
 
-### Shifting a sum of elements in a monoid
+### Shifting a sum of elements in an abelian group
 
 ```agda
 module _
@@ -205,8 +210,7 @@ module _
 
   abstract
     preserves-sum-permutation-fin-sequence-type-Ab :
-      (n : ℕ) → (σ : Permutation n) →
-      (f : fin-sequence-type-Ab G n) →
+      (n : ℕ) (σ : Permutation n) (f : fin-sequence-type-Ab G n) →
       sum-fin-sequence-type-Ab G n f ＝
       sum-fin-sequence-type-Ab G n (f ∘ map-equiv σ)
     preserves-sum-permutation-fin-sequence-type-Ab =
@@ -225,6 +229,120 @@ abstract
     sum-constant-fin-sequence-type-Group (group-Ab G)
 ```
 
+### Interchanging sums and addition
+
+```agda
+module _
+  {l : Level}
+  (G : Ab l)
+  where
+
+  abstract
+    interchange-sum-add-fin-sequence-type-Ab :
+      (n : ℕ) (f g : fin-sequence-type-Ab G n) →
+      sum-fin-sequence-type-Ab G n (λ i → add-Ab G (f i) (g i)) ＝
+      add-Ab G (sum-fin-sequence-type-Ab G n f) (sum-fin-sequence-type-Ab G n g)
+    interchange-sum-add-fin-sequence-type-Ab =
+      interchange-sum-mul-fin-sequence-type-Commutative-Monoid
+        ( commutative-monoid-Ab G)
+```
+
+### The sum operation is an abelian group homomorphism
+
+```agda
+hom-sum-fin-sequence-type-Ab :
+  {l : Level} (G : Ab l) (n : ℕ) →
+  hom-Ab (function-Ab G (Fin n)) G
+hom-sum-fin-sequence-type-Ab G n =
+  ( sum-fin-sequence-type-Ab G n ,
+    interchange-sum-add-fin-sequence-type-Ab G n _ _)
+```
+
+### Negation distributes over sums
+
+```agda
+abstract
+  distributive-neg-sum-fin-sequence-type-Ab :
+    {l : Level} (G : Ab l) (n : ℕ) (u : fin-sequence-type-Ab G n) →
+    neg-Ab G (sum-fin-sequence-type-Ab G n u) ＝
+    sum-fin-sequence-type-Ab G n (neg-Ab G ∘ u)
+  distributive-neg-sum-fin-sequence-type-Ab G n u =
+    inv
+      ( preserves-negatives-hom-Ab
+        ( function-Ab G (Fin n))
+        ( G)
+        ( hom-sum-fin-sequence-type-Ab G n))
+```
+
+### Interchanging sums and subtraction
+
+```agda
+module _
+  {l : Level}
+  (G : Ab l)
+  where
+
+  abstract
+    interchange-sum-right-subtraction-fin-sequence-type-Ab :
+      (n : ℕ) (f g : fin-sequence-type-Ab G n) →
+      sum-fin-sequence-type-Ab G n (λ i → right-subtraction-Ab G (f i) (g i)) ＝
+      right-subtraction-Ab G
+        ( sum-fin-sequence-type-Ab G n f)
+        ( sum-fin-sequence-type-Ab G n g)
+    interchange-sum-right-subtraction-fin-sequence-type-Ab n f g =
+      ( interchange-sum-add-fin-sequence-type-Ab G n f (neg-Ab G ∘ g)) ∙
+      ( ap-add-Ab G
+        ( refl)
+        ( inv (distributive-neg-sum-fin-sequence-type-Ab G n g)))
+```
+
+### Telescoping sums
+
+A telescoping sum is a sum of the form `∑ aₙ₊₁ - aₙ` or `∑ aₙ - aₙ₊₁`.
+
+```agda
+module _
+  {l : Level}
+  (G : Ab l)
+  where
+
+  telescope-fin-sequence-type-Ab :
+    (n : ℕ) → fin-sequence-type-Ab G (succ-ℕ n) → fin-sequence-type-Ab G n
+  telescope-fin-sequence-type-Ab n u =
+    ind-Σ (right-subtraction-Ab G) ∘ pair-succ-fin-sequence n u
+
+  telescope-fin-sequence-type-Ab' :
+    (n : ℕ) → fin-sequence-type-Ab G (succ-ℕ n) → fin-sequence-type-Ab G n
+  telescope-fin-sequence-type-Ab' n u =
+    ind-Σ (right-subtraction-Ab' G) ∘ pair-succ-fin-sequence n u
+
+  abstract
+    sum-telescope-fin-sequence-type-Ab :
+      (n : ℕ) (u : fin-sequence-type-Ab G (succ-ℕ n)) →
+      sum-fin-sequence-type-Ab G n (telescope-fin-sequence-type-Ab n u) ＝
+      right-subtraction-Ab G (head-fin-sequence n u) (last-fin-sequence n u)
+    sum-telescope-fin-sequence-type-Ab 0 u =
+      inv (right-inverse-law-add-Ab G (head-fin-sequence 0 u))
+    sum-telescope-fin-sequence-type-Ab (succ-ℕ n) u =
+      ( ap-add-Ab G
+        ( sum-telescope-fin-sequence-type-Ab n (tail-fin-sequence (succ-ℕ n) u))
+        ( refl)) ∙
+      ( commutative-add-Ab G _ _) ∙
+      ( add-right-subtraction-Ab G _ _ _)
+
+    sum-telescope-fin-sequence-type-Ab' :
+      (n : ℕ) (u : fin-sequence-type-Ab G (succ-ℕ n)) →
+      sum-fin-sequence-type-Ab G n (telescope-fin-sequence-type-Ab' n u) ＝
+      right-subtraction-Ab G (last-fin-sequence n u) (head-fin-sequence n u)
+    sum-telescope-fin-sequence-type-Ab' n u =
+      ( htpy-sum-fin-sequence-type-Ab G
+        ( n)
+        ( λ i → inv (neg-right-subtraction-Ab G _ _))) ∙
+      ( inv (distributive-neg-sum-fin-sequence-type-Ab G n _)) ∙
+      ( ap (neg-Ab G) (sum-telescope-fin-sequence-type-Ab n u)) ∙
+      ( neg-right-subtraction-Ab G _ _)
+```
+
 ## See also
 
 - [Sums of finite families of elements in abelian groups](group-theory.sums-of-finite-families-of-elements-commutative-monoids.md)

src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md

@@ -24,6 +24,8 @@ open import foundation.identity-types
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.function-commutative-monoids
+open import group-theory.homomorphisms-commutative-monoids
 open import group-theory.powers-of-elements-commutative-monoids
 open import group-theory.sums-of-finite-sequences-of-elements-commutative-semigroups
 open import group-theory.sums-of-finite-sequences-of-elements-monoids
@@ -269,6 +271,48 @@ abstract
     sum-constant-fin-sequence-type-Monoid (monoid-Commutative-Monoid M)
 ```
 
+### Interchanging sums and monoid multiplication
+
+```agda
+module _
+  {l : Level}
+  (M : Commutative-Monoid l)
+  where
+
+  abstract
+    interchange-sum-mul-fin-sequence-type-Commutative-Monoid :
+      (n : ℕ) (f g : fin-sequence-type-Commutative-Monoid M n) →
+      sum-fin-sequence-type-Commutative-Monoid M n
+        ( λ i → mul-Commutative-Monoid M (f i) (g i)) ＝
+      mul-Commutative-Monoid M
+        ( sum-fin-sequence-type-Commutative-Monoid M n f)
+        ( sum-fin-sequence-type-Commutative-Monoid M n g)
+    interchange-sum-mul-fin-sequence-type-Commutative-Monoid 0 _ _ =
+      inv (right-unit-law-mul-Commutative-Monoid M _)
+    interchange-sum-mul-fin-sequence-type-Commutative-Monoid (succ-ℕ n) f g =
+      ( ap-mul-Commutative-Monoid M
+        ( interchange-sum-mul-fin-sequence-type-Commutative-Monoid
+          ( n)
+          ( f ∘ inl-Fin n)
+          ( g ∘ inl-Fin n))
+        ( refl)) ∙
+      ( interchange-mul-mul-Commutative-Monoid M _ _ _ _)
+```
+
+### The sum operation is a commutative monoid homomorphism
+
+```agda
+hom-sum-fin-sequence-type-Commutative-Monoid :
+  {l : Level} (M : Commutative-Monoid l) (n : ℕ) →
+  hom-Commutative-Monoid
+    ( function-Commutative-Monoid M (Fin n))
+    ( M)
+hom-sum-fin-sequence-type-Commutative-Monoid M n =
+  ( ( ( sum-fin-sequence-type-Commutative-Monoid M n) ,
+        interchange-sum-mul-fin-sequence-type-Commutative-Monoid M n _ _) ,
+    sum-zero-fin-sequence-type-Commutative-Monoid M n)
+```
+
 ## See also
 
 - [Sums of finite families of elements in commutative monoids](group-theory.sums-of-finite-families-of-elements-commutative-monoids.md)

src/lists.lagda.md

@@ -19,6 +19,7 @@ open import lists.functoriality-tuples public
 open import lists.functoriality-tuples-finite-sequences public
 open import lists.lists public
 open import lists.lists-discrete-types public
+open import lists.pairs-of-successive-elements-finite-sequences public
 open import lists.partial-sequences public
 open import lists.permutation-lists public
 open import lists.permutation-tuples public

src/lists/finite-sequences.lagda.md

@@ -54,12 +54,19 @@ module _
   empty-fin-sequence ()
 
   head-fin-sequence : (n : ℕ) → fin-sequence A (succ-ℕ n) → A
-  head-fin-sequence n v = v (inr star)
+  head-fin-sequence n v = v (neg-one-Fin n)
+
+  last-fin-sequence : (n : ℕ) → fin-sequence A (succ-ℕ n) → A
+  last-fin-sequence n v = v (zero-Fin n)
 
   tail-fin-sequence :
     (n : ℕ) → fin-sequence A (succ-ℕ n) → fin-sequence A n
   tail-fin-sequence n v = v ∘ (inl-Fin n)
 
+  init-fin-sequence :
+    (n : ℕ) → fin-sequence A (succ-ℕ n) → fin-sequence A n
+  init-fin-sequence n v = v ∘ skip-zero-Fin n
+
   cons-fin-sequence :
     (n : ℕ) → A → fin-sequence A n → fin-sequence A (succ-ℕ n)
   cons-fin-sequence n a v (inl x) = v x

src/lists/pairs-of-successive-elements-finite-sequences.lagda.md

@@ -0,0 +1,44 @@
+# Pairs of successive elements in a finite sequence
+
+```agda
+module lists.pairs-of-successive-elements-finite-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.cartesian-product-types
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import lists.finite-sequences
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+Given a nonempty [finite sequence](lists.finite-sequences.md) `a` with elements
+`a₀, a₁, ..., aₙ`, the
+{{#concept "sequence of pairs of successive elements" Agda=pair-succ-fin-sequence}}
+of `a` is the the sequence `(a₀, a₁), (a₁, a₂), ..., (aₙ₋₁, aₙ)`.
+
+## Definition
+
+```agda
+pair-succ-fin-sequence :
+  {l : Level} {A : UU l} (n : ℕ) →
+  fin-sequence A (succ-ℕ n) → fin-sequence (A × A) n
+pair-succ-fin-sequence n a i =
+  ( a (skip-zero-Fin n i) ,
+    a (inl-Fin n i))
+```