Multiples of elements in abelian groups

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-08-21.
Last modified on 2023-09-21.

module group-theory.multiples-of-elements-abelian-groups where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.powers-of-elements-groups

Idea

The multiplication operation on an abelian group is the map n x ↦ n · x, which is defined by iteratively adding x with itself n times. We define this operation where n ranges over the natural numbers, as well as where n ranges over the integers.

Definition

Natural number multiples of abelian group elements

module _
  {l : Level} (A : Ab l)
  where

  multiple-Ab : ℕ → type-Ab A → type-Ab A
  multiple-Ab = power-Group (group-Ab A)

The predicate of being a natural multiple of an element in an abelian group

We say that an element y is a multiple of an element x if there exists a number n such that nx ＝ y.

module _
  {l : Level} (A : Ab l)
  where

  is-multiple-of-element-prop-Ab :
    (x y : type-Ab A) → Prop l
  is-multiple-of-element-prop-Ab =
    is-power-of-element-prop-Group (group-Ab A)

  is-multiple-of-element-Ab :
    (x y : type-Ab A) → UU l
  is-multiple-of-element-Ab =
    is-power-of-element-Group (group-Ab A)

  is-prop-is-multiple-of-element-Ab :
    (x y : type-Ab A) →
    is-prop (is-multiple-of-element-Ab x y)
  is-prop-is-multiple-of-element-Ab =
    is-prop-is-power-of-element-Group (group-Ab A)

Properties

n · 0 ＝ 0

module _
  {l : Level} (A : Ab l)
  where

  multiple-zero-Ab :
    (n : ℕ) → multiple-Ab A n (zero-Ab A) ＝ zero-Ab A
  multiple-zero-Ab = power-unit-Group (group-Ab A)

(n + 1) · x = n · x + x

module _
  {l : Level} (A : Ab l)
  where

  multiple-succ-Ab :
    (n : ℕ) (x : type-Ab A) →
    multiple-Ab A (succ-ℕ n) x ＝ add-Ab A (multiple-Ab A n x) x
  multiple-succ-Ab = power-succ-Group (group-Ab A)

(n + 1) · x ＝ x + n · x

module _
  {l : Level} (A : Ab l)
  where

  multiple-succ-Ab' :
    (n : ℕ) (x : type-Ab A) →
    multiple-Ab A (succ-ℕ n) x ＝ add-Ab A x (multiple-Ab A n x)
  multiple-succ-Ab' = power-succ-Group' (group-Ab A)

Multiples by sums of natural numbers are products of multiples

module _
  {l : Level} (A : Ab l)
  where

  right-distributive-multiple-add-Ab :
    (m n : ℕ) {x : type-Ab A} →
    multiple-Ab A (m +ℕ n) x ＝
    add-Ab A (multiple-Ab A m x) (multiple-Ab A n x)
  right-distributive-multiple-add-Ab = distributive-power-add-Group (group-Ab A)

Multiples distribute over the sum of x and y

module _
  {l : Level} (A : Ab l)
  where

  left-distributive-multiple-add-Ab :
    (n : ℕ) {x y : type-Ab A} →
    multiple-Ab A n (add-Ab A x y) ＝
    add-Ab A (multiple-Ab A n x) (multiple-Ab A n y)
  left-distributive-multiple-add-Ab n =
    distributive-power-mul-Group (group-Ab A) n (commutative-add-Ab A _ _)

Multiples by products of natural numbers are iterated multiples

module _
  {l : Level} (A : Ab l)
  where

  multiple-mul-Ab :
    (m n : ℕ) {x : type-Ab A} →
    multiple-Ab A (m *ℕ n) x ＝ multiple-Ab A n (multiple-Ab A m x)
  multiple-mul-Ab = power-mul-Group (group-Ab A)

Recent changes