🔍

Equations Inline Footnotes

open import 1Lab.Prelude

open import Algebra.Monoid.Instances.Transformation
open import Algebra.Monoid.Category
open import Algebra.Monoid

open import Cat.Displayed.Univalence.Thin
open import Cat.Displayed.Total

open import Data.Vec.Properties
open import Data.Product.NAry
open import Data.Fin.Base
open import Data.Vec.Base

import Cat.Reasoning as Cr

module Algebra.Monoid.Instances.Transformation.Fin where

private module Monoids = Cr (Monoids lzero)

Finite full transformation monoids🔗

The finite full transformation monoid ${\mathcal{T}}_n$ represents the endomaps of the standard finite set $\mathrm{Fin}(n)\text{.}$

module _ (n : Nat) where
  open Monoid-on

  End[n] : Monoid lzero
  End[n] = (Fin n → Fin n) , End (el! (Fin n))

However, the definition of the full transformation monoid End[n] on $\mathrm{Fin}(n)$ has a few disadvantages. Firstly, elements of End[n], being functions, are awkward to write down. On a blackboard one often writes an element of ${\mathcal{T}}_n$ in the form

Here, $a$ is the transformation sending each element in the top row to the corresponding element in the bottom row. We would like to achieve something similar in Mikan. Secondly, the product of two elements of End[n] will typically not compute until it is actually applied to an element of $\mathrm{Fin}(n)\text{.}$ We would like equal elements of ${\mathcal{T}}_n$ to be definitionally equal whenever possible.

We can solve both these problems using the equivalence between the underlying set of End[n] and vectors of length $n$ with coordinates in $\mathrm{Fin}(n)\text{.}$

  End≃𝒯 : ⌞ End[n] ⌟ ≃ Vec (Fin n) n
  End≃𝒯 = Equiv.inverse Vec≃Fun

  𝒯 : Monoid lzero
  𝒯 = Vec (Fin n) n , monoid-transport End≃𝒯 (End[n] .snd)

Since the monoid structure on ${\mathcal{T}}_n$ was constructed directly from the monoid structure on End[n], it is clear that these give isomorphic monoids:

  End≅𝒯 : (el! (End[n] .fst) , End[n] .snd) Monoids.≅ (el! (𝒯 .fst) , 𝒯 .snd)
  End≅𝒯 = total-iso End≃𝒯 (monoid-transport-hom End≃𝒯 (End[n] .snd))

Using list syntax for vectors, the element $a$ above can be written as

module _ where private
  open Monoid-on (𝒯  .snd)

  a : ⌞ 𝒯  ⌟
  a = [  ,  ,  ,  ,  ]

Moreover, multiplication in ${\mathcal{T}}_n$ genuinely computes, so we can write equations such as

  _ : a ≡ [  ,  ,  ,  ,  ] ⋆ [  ,  ,  ,  ,  ]
  _ = refl