Multiples of elements in large abelian groups

Content created by Louis Wasserman.

Created on 2025-10-17.
Last modified on 2025-10-17.

module group-theory.multiples-of-elements-large-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.transport-along-identifications
open import foundation.universe-levels

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

Idea

The multiplication operation on a large abelian group is the map n x ↦ n · x, which is defined by iteratively adding x with itself n times. This file describes this operation where n ranges over the natural numbers.

Definition

module _
  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
  where

  multiple-Large-Ab : {l : Level} → ℕ → type-Large-Ab G l → type-Large-Ab G l
  multiple-Large-Ab = power-Large-Group (large-group-Large-Ab G)

Properties

n · 0 ＝ 0

module _
  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
  where

  abstract
    raise-multiple-zero-Large-Ab :
      (l : Level) (n : ℕ) →
      multiple-Large-Ab G n (raise-zero-Large-Ab G l) ＝ raise-zero-Large-Ab G l
    raise-multiple-zero-Large-Ab =
      raise-power-unit-Large-Group (large-group-Large-Ab G)

(n + 1) ∙ x ＝ n ∙ x + x

module _
  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
  where

  abstract
    multiple-succ-Large-Ab :
      {l : Level} (n : ℕ) (x : type-Large-Ab G l) →
      multiple-Large-Ab G (succ-ℕ n) x ＝
      add-Large-Ab G (multiple-Large-Ab G n x) x
    multiple-succ-Large-Ab = power-succ-Large-Group (large-group-Large-Ab G)

(n + 1) ∙ x ＝ x + n ∙ x

module _
  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
  where

  abstract
    multiple-succ-Large-Ab' :
      {l : Level} (n : ℕ) (x : type-Large-Ab G l) →
      multiple-Large-Ab G (succ-ℕ n) x ＝
      add-Large-Ab G x (multiple-Large-Ab G n x)
    multiple-succ-Large-Ab' = power-succ-Large-Group' (large-group-Large-Ab G)

Multiples by sums of natural numbers are sums of multiples

module _
  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
  where

  abstract
    right-distributive-multiple-add-Large-Ab :
      {l : Level} (m n : ℕ) {x : type-Large-Ab G l} →
      multiple-Large-Ab G (m +ℕ n) x ＝
      add-Large-Ab G (multiple-Large-Ab G m x) (multiple-Large-Ab G n x)
    right-distributive-multiple-add-Large-Ab =
      distributive-power-add-Large-Group (large-group-Large-Ab G)

Multiples distribute over the sum of elements

module _
  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
  where

  abstract
    left-distributive-multiple-add-Large-Ab :
      {l1 l2 : Level} (n : ℕ) →
      {x : type-Large-Ab G l1} {y : type-Large-Ab G l2} →
      multiple-Large-Ab G n (add-Large-Ab G x y) ＝
      add-Large-Ab G (multiple-Large-Ab G n x) (multiple-Large-Ab G n y)
    left-distributive-multiple-add-Large-Ab n {x} {y} =
      distributive-power-mul-Large-Group
        ( large-group-Large-Ab G)
        ( n)
        ( commutative-add-Large-Ab G x y)

Multiplication by products of natural numbers is iterated multiplication

module _
  {α : Level → Level} {β : Level → Level → Level} (G : Large-Ab α β)
  where

  abstract
    multiple-mul-Large-Ab :
      {l : Level} (m n : ℕ) {x : type-Large-Ab G l} →
      multiple-Large-Ab G (m *ℕ n) x ＝
      multiple-Large-Ab G n (multiple-Large-Ab G m x)
    multiple-mul-Large-Ab = power-mul-Large-Group (large-group-Large-Ab G)

See also

Recent changes