Products of finite sequences of elements in monoids

Content created by Louis Wasserman.

Created on 2026-04-29.
Last modified on 2026-04-29.

module group-theory.products-of-finite-sequences-of-elements-monoids where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import group-theory.monoids
open import group-theory.powers-of-elements-monoids

open import linear-algebra.finite-sequences-in-monoids

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.standard-finite-types

Idea

The product operation operation extends the binary operation on a monoid M to any finite sequence of elements of M.

Definition

product-fin-sequence-type-Monoid :
  {l : Level} (M : Monoid l) (n : ℕ) →
  (fin-sequence-type-Monoid M n) → type-Monoid M
product-fin-sequence-type-Monoid M zero-ℕ f = unit-Monoid M
product-fin-sequence-type-Monoid M (succ-ℕ n) f =
  mul-Monoid M
    ( product-fin-sequence-type-Monoid M n (f ∘ inl-Fin n))
    ( f (inr star))

Properties

Products of one and two elements

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

  compute-product-one-element-Monoid :
    (f : fin-sequence-type-Monoid M 1) →
    product-fin-sequence-type-Monoid M 1 f ＝ head-fin-sequence-type-Monoid M 0 f
  compute-product-one-element-Monoid f =
    left-unit-law-mul-Monoid M (f (inr star))

  compute-product-two-elements-Monoid :
    (f : fin-sequence-type-Monoid M 2) →
    product-fin-sequence-type-Monoid M 2 f ＝
    mul-Monoid M (f (zero-Fin 1)) (f (one-Fin 1))
  compute-product-two-elements-Monoid f =
    ( associative-mul-Monoid M
      (unit-Monoid M) (f (zero-Fin 1)) (f (one-Fin 1))) ∙
    ( left-unit-law-mul-Monoid M
      ( mul-Monoid M (f (zero-Fin 1)) (f (one-Fin 1))))

Products are homotopy invariant

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

  abstract
    htpy-product-fin-sequence-type-Monoid :
      (n : ℕ) {f g : fin-sequence-type-Monoid M n} →
      (f ~ g) →
      product-fin-sequence-type-Monoid M n f ＝
      product-fin-sequence-type-Monoid M n g
    htpy-product-fin-sequence-type-Monoid zero-ℕ H = refl
    htpy-product-fin-sequence-type-Monoid (succ-ℕ n) H =
      ap-mul-Monoid M
        ( htpy-product-fin-sequence-type-Monoid n (H ·r inl-Fin n))
        ( H (inr star))

Product are equal to the product of the zero-th term and the rest

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

  cons-product-fin-sequence-type-Monoid :
    (n : ℕ) (f : fin-sequence-type-Monoid M (succ-ℕ n)) →
    {x : type-Monoid M} → head-fin-sequence-type-Monoid M n f ＝ x →
    product-fin-sequence-type-Monoid M (succ-ℕ n) f ＝
    mul-Monoid M (product-fin-sequence-type-Monoid M n (f ∘ inl-Fin n)) x
  cons-product-fin-sequence-type-Monoid n f refl = refl

  snoc-product-fin-sequence-type-Monoid :
    (n : ℕ) (f : fin-sequence-type-Monoid M (succ-ℕ n)) →
    {x : type-Monoid M} → f (zero-Fin n) ＝ x →
    product-fin-sequence-type-Monoid M (succ-ℕ n) f ＝
    mul-Monoid M
      ( x)
      ( product-fin-sequence-type-Monoid M n (f ∘ inr-Fin n))
  snoc-product-fin-sequence-type-Monoid zero-ℕ f refl =
    ( compute-product-one-element-Monoid M f) ∙
    ( inv (right-unit-law-mul-Monoid M (f (zero-Fin 0))))
  snoc-product-fin-sequence-type-Monoid (succ-ℕ n) f refl =
    ( ap
      ( mul-Monoid' M (head-fin-sequence-type-Monoid M (succ-ℕ n) f))
      ( snoc-product-fin-sequence-type-Monoid
        ( n)
        ( f ∘ inl-Fin (succ-ℕ n))
        ( refl))) ∙
    ( associative-mul-Monoid M _ _ _)

Extending a product of elements in a monoid

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

  extend-product-fin-sequence-type-Monoid :
    (n : ℕ) (f : fin-sequence-type-Monoid M n) →
    product-fin-sequence-type-Monoid M
      ( succ-ℕ n)
      ( cons-fin-sequence-type-Monoid M n (unit-Monoid M) f) ＝
    product-fin-sequence-type-Monoid M n f
  extend-product-fin-sequence-type-Monoid n f =
    right-unit-law-mul-Monoid M (product-fin-sequence-type-Monoid M n f)

Shifting a product of elements in a monoid

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

  shift-product-fin-sequence-type-Monoid :
    (n : ℕ) (f : fin-sequence-type-Monoid M n) →
    product-fin-sequence-type-Monoid M
      ( succ-ℕ n)
      ( snoc-fin-sequence-type-Monoid M n f
        ( unit-Monoid M)) ＝
    product-fin-sequence-type-Monoid M n f
  shift-product-fin-sequence-type-Monoid zero-ℕ f =
    left-unit-law-mul-Monoid M (unit-Monoid M)
  shift-product-fin-sequence-type-Monoid (succ-ℕ n) f =
    ap
      ( mul-Monoid' M
        ( head-fin-sequence-type-Monoid M n f))
      ( shift-product-fin-sequence-type-Monoid n
        ( tail-fin-sequence-type-Monoid M n f))

A product of units is the unit

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

  product-unit-fin-sequence-type-Monoid :
    (n : ℕ) →
    product-fin-sequence-type-Monoid M n (zero-fin-sequence-type-Monoid M n) ＝
    unit-Monoid M
  product-unit-fin-sequence-type-Monoid zero-ℕ = refl
  product-unit-fin-sequence-type-Monoid (succ-ℕ n) =
    right-unit-law-mul-Monoid M _ ∙ product-unit-fin-sequence-type-Monoid n

Splitting products of n + m elements into a product of n elements and a product of m elements

abstract
  split-product-fin-sequence-type-Monoid :
    {l : Level} (M : Monoid l)
    (n m : ℕ) (f : fin-sequence-type-Monoid M (n +ℕ m)) →
    product-fin-sequence-type-Monoid M (n +ℕ m) f ＝
    mul-Monoid M
      ( product-fin-sequence-type-Monoid M n (f ∘ inl-coproduct-Fin n m))
      ( product-fin-sequence-type-Monoid M m (f ∘ inr-coproduct-Fin n m))
  split-product-fin-sequence-type-Monoid M n zero-ℕ f =
    inv (right-unit-law-mul-Monoid M (product-fin-sequence-type-Monoid M n f))
  split-product-fin-sequence-type-Monoid M n (succ-ℕ m) f =
    ( ap
      ( mul-Monoid' M (f (inr star)))
      ( split-product-fin-sequence-type-Monoid M n m (f ∘ inl))) ∙
    ( associative-mul-Monoid M _ _ _)

Constant products are powers

abstract
  product-constant-fin-sequence-type-Monoid :
    {l : Level} (M : Monoid l) (n : ℕ) (x : type-Monoid M) →
    product-fin-sequence-type-Monoid M n (λ _ → x) ＝ power-Monoid M n x
  product-constant-fin-sequence-type-Monoid M 0 x = refl
  product-constant-fin-sequence-type-Monoid M 1 x =
    compute-product-one-element-Monoid M (λ _ → x)
  product-constant-fin-sequence-type-Monoid M (succ-ℕ n@(succ-ℕ _)) x =
    ap-mul-Monoid M
      ( product-constant-fin-sequence-type-Monoid M n x)
      ( refl)

Recent changes