Tuples on monoids

Content created by Louis Wasserman.

Created on 2025-06-03.
Last modified on 2025-06-03.

module linear-algebra.tuples-on-monoids where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.monoids
open import group-theory.semigroups

open import linear-algebra.constant-tuples

open import lists.functoriality-tuples
open import lists.tuples

Idea

Given a monoid M, the type tuple n M of n-tuples of elements of M is a monoid given by componentwise multiplication.

We use additive terminology for tuples, as is standard in linear algebra contexts, despite using multiplicative terminology for monoids.

Definitions

module _
  {l : Level} (M : Monoid l)
  where

  tuple-Monoid :   UU l
  tuple-Monoid = tuple (type-Monoid M)

  head-tuple-Monoid : {n : }  tuple-Monoid (succ-ℕ n)  type-Monoid M
  head-tuple-Monoid v = head-tuple v

  tail-tuple-Monoid : {n : }  tuple-Monoid (succ-ℕ n)  tuple-Monoid n
  tail-tuple-Monoid v = tail-tuple v

  snoc-tuple-Monoid :
    {n : }  tuple-Monoid n  type-Monoid M  tuple-Monoid (succ-ℕ n)
  snoc-tuple-Monoid v r = snoc-tuple v r

The tuple of zeros

module _
  {l : Level} (M : Monoid l)
  where

  zero-tuple-Monoid : {n : }  tuple-Monoid M n
  zero-tuple-Monoid = constant-tuple (unit-Monoid M)

Componentwise addition of tuples on a monoid

module _
  {l : Level} (M : Monoid l)
  where

  add-tuple-Monoid :
    {n : }  tuple-Monoid M n  tuple-Monoid M n  tuple-Monoid M n
  add-tuple-Monoid = binary-map-tuple (mul-Monoid M)

  associative-add-tuple-Monoid :
    {n : } (v1 v2 v3 : tuple-Monoid M n) 
    add-tuple-Monoid (add-tuple-Monoid v1 v2) v3 
    add-tuple-Monoid v1 (add-tuple-Monoid v2 v3)
  associative-add-tuple-Monoid empty-tuple empty-tuple empty-tuple = refl
  associative-add-tuple-Monoid (x  v1) (y  v2) (z  v3) =
    ap-binary _∷_
      ( associative-mul-Monoid M x y z)
      ( associative-add-tuple-Monoid v1 v2 v3)

  semigroup-tuple-Monoid :   Semigroup l
  pr1 (semigroup-tuple-Monoid n) = tuple-Set (set-Monoid M) n
  pr1 (pr2 (semigroup-tuple-Monoid n)) = add-tuple-Monoid
  pr2 (pr2 (semigroup-tuple-Monoid n)) = associative-add-tuple-Monoid

  left-unit-law-add-tuple-Monoid :
    {n : } (v : tuple-Monoid M n) 
    add-tuple-Monoid (zero-tuple-Monoid M) v  v
  left-unit-law-add-tuple-Monoid empty-tuple = refl
  left-unit-law-add-tuple-Monoid (x  v) =
    ap-binary _∷_
      ( left-unit-law-mul-Monoid M x)
      ( left-unit-law-add-tuple-Monoid v)

  right-unit-law-add-tuple-Monoid :
    {n : } (v : tuple-Monoid M n) 
    add-tuple-Monoid v (zero-tuple-Monoid M)  v
  right-unit-law-add-tuple-Monoid empty-tuple = refl
  right-unit-law-add-tuple-Monoid (x  v) =
    ap-binary _∷_
      ( right-unit-law-mul-Monoid M x)
      ( right-unit-law-add-tuple-Monoid v)

  monoid-tuple-Monoid :   Monoid l
  pr1 (monoid-tuple-Monoid n) = semigroup-tuple-Monoid n
  pr1 (pr2 (monoid-tuple-Monoid n)) = zero-tuple-Monoid M
  pr1 (pr2 (pr2 (monoid-tuple-Monoid n))) = left-unit-law-add-tuple-Monoid
  pr2 (pr2 (pr2 (monoid-tuple-Monoid n))) = right-unit-law-add-tuple-Monoid

Recent changes