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
- 2025-06-03. Louis Wasserman. Sums and products over arbitrary finite types (#1367).