# Finite Commutative monoids

Content created by Fredrik Bakke.

Created on 2024-02-07.

module finite-group-theory.finite-commutative-monoids where
Imports
open import finite-group-theory.finite-monoids

open import foundation.identity-types
open import foundation.sets
open import foundation.unital-binary-operations
open import foundation.universe-levels

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

open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types

## Idea

A finite commutative monoid is a finite monoid M in which xy = yx holds for all x y : M.

## Definition

### Finite commutative monoids

is-commutative-Monoid-𝔽 :
{l : Level} (M : Monoid-𝔽 l)  UU l
is-commutative-Monoid-𝔽 M =
is-commutative-Monoid (monoid-Monoid-𝔽 M)

Commutative-Monoid-𝔽 : (l : Level)  UU (lsuc l)
Commutative-Monoid-𝔽 l = Σ (Monoid-𝔽 l) is-commutative-Monoid-𝔽

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

finite-monoid-Commutative-Monoid-𝔽 : Monoid-𝔽 l
finite-monoid-Commutative-Monoid-𝔽 = pr1 M

monoid-Commutative-Monoid-𝔽 : Monoid l
monoid-Commutative-Monoid-𝔽 =
monoid-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

finite-type-Commutative-Monoid-𝔽 : 𝔽 l
finite-type-Commutative-Monoid-𝔽 =
finite-type-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

type-Commutative-Monoid-𝔽 : UU l
type-Commutative-Monoid-𝔽 =
type-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

is-finite-type-Commutative-Monoid-𝔽 : is-finite type-Commutative-Monoid-𝔽
is-finite-type-Commutative-Monoid-𝔽 =
is-finite-type-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

semigroup-Commutative-Monoid-𝔽 : Semigroup l
semigroup-Commutative-Monoid-𝔽 =
semigroup-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

set-Commutative-Monoid-𝔽 : Set l
set-Commutative-Monoid-𝔽 =
set-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

is-set-type-Commutative-Monoid-𝔽 : is-set type-Commutative-Monoid-𝔽
is-set-type-Commutative-Monoid-𝔽 =
is-set-type-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

### The multiplicative operation of a commutative monoid

has-associative-mul-Commutative-Monoid-𝔽 :
has-associative-mul-Set set-Commutative-Monoid-𝔽
has-associative-mul-Commutative-Monoid-𝔽 =
has-associative-mul-Semigroup semigroup-Commutative-Monoid-𝔽

mul-Commutative-Monoid-𝔽 :
(x y : type-Commutative-Monoid-𝔽)  type-Commutative-Monoid-𝔽
mul-Commutative-Monoid-𝔽 = mul-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

mul-Commutative-Monoid-𝔽' :
(x y : type-Commutative-Monoid-𝔽)  type-Commutative-Monoid-𝔽
mul-Commutative-Monoid-𝔽' =
mul-Monoid-𝔽' finite-monoid-Commutative-Monoid-𝔽

ap-mul-Commutative-Monoid-𝔽 :
{x x' y y' : type-Commutative-Monoid-𝔽}
x  x'  y  y'
mul-Commutative-Monoid-𝔽 x y  mul-Commutative-Monoid-𝔽 x' y'
ap-mul-Commutative-Monoid-𝔽 =
ap-mul-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

associative-mul-Commutative-Monoid-𝔽 :
(x y z : type-Commutative-Monoid-𝔽)
( mul-Commutative-Monoid-𝔽 (mul-Commutative-Monoid-𝔽 x y) z)
( mul-Commutative-Monoid-𝔽 x (mul-Commutative-Monoid-𝔽 y z))
associative-mul-Commutative-Monoid-𝔽 =
associative-mul-Monoid-𝔽 finite-monoid-Commutative-Monoid-𝔽

commutative-mul-Commutative-Monoid-𝔽 :
(x y : type-Commutative-Monoid-𝔽)
mul-Commutative-Monoid-𝔽 x y  mul-Commutative-Monoid-𝔽 y x
commutative-mul-Commutative-Monoid-𝔽 = pr2 M

commutative-monoid-Commutative-Monoid-𝔽 : Commutative-Monoid l
pr1 commutative-monoid-Commutative-Monoid-𝔽 = monoid-Commutative-Monoid-𝔽
pr2 commutative-monoid-Commutative-Monoid-𝔽 =
commutative-mul-Commutative-Monoid-𝔽

interchange-mul-mul-Commutative-Monoid-𝔽 :
(x y x' y' : type-Commutative-Monoid-𝔽)
( mul-Commutative-Monoid-𝔽
( mul-Commutative-Monoid-𝔽 x y)
( mul-Commutative-Monoid-𝔽 x' y'))
( mul-Commutative-Monoid-𝔽
( mul-Commutative-Monoid-𝔽 x x')
( mul-Commutative-Monoid-𝔽 y y'))
interchange-mul-mul-Commutative-Monoid-𝔽 =
interchange-mul-mul-Commutative-Monoid
commutative-monoid-Commutative-Monoid-𝔽

right-swap-mul-Commutative-Monoid-𝔽 :
(x y z : type-Commutative-Monoid-𝔽)
mul-Commutative-Monoid-𝔽 (mul-Commutative-Monoid-𝔽 x y) z
mul-Commutative-Monoid-𝔽 (mul-Commutative-Monoid-𝔽 x z) y
right-swap-mul-Commutative-Monoid-𝔽 =
right-swap-mul-Commutative-Monoid
commutative-monoid-Commutative-Monoid-𝔽

left-swap-mul-Commutative-Monoid-𝔽 :
(x y z : type-Commutative-Monoid-𝔽)
mul-Commutative-Monoid-𝔽 x (mul-Commutative-Monoid-𝔽 y z)
mul-Commutative-Monoid-𝔽 y (mul-Commutative-Monoid-𝔽 x z)
left-swap-mul-Commutative-Monoid-𝔽 =
left-swap-mul-Commutative-Monoid
commutative-monoid-Commutative-Monoid-𝔽

### The unit element of a commutative monoid

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

has-unit-Commutative-Monoid-𝔽 : is-unital (mul-Commutative-Monoid-𝔽 M)
has-unit-Commutative-Monoid-𝔽 =
has-unit-Monoid (monoid-Commutative-Monoid-𝔽 M)

unit-Commutative-Monoid-𝔽 : type-Commutative-Monoid-𝔽 M
unit-Commutative-Monoid-𝔽 = unit-Monoid (monoid-Commutative-Monoid-𝔽 M)

left-unit-law-mul-Commutative-Monoid-𝔽 :
(x : type-Commutative-Monoid-𝔽 M)
mul-Commutative-Monoid-𝔽 M unit-Commutative-Monoid-𝔽 x  x
left-unit-law-mul-Commutative-Monoid-𝔽 =
left-unit-law-mul-Monoid (monoid-Commutative-Monoid-𝔽 M)

right-unit-law-mul-Commutative-Monoid-𝔽 :
(x : type-Commutative-Monoid-𝔽 M)
mul-Commutative-Monoid-𝔽 M x unit-Commutative-Monoid-𝔽  x
right-unit-law-mul-Commutative-Monoid-𝔽 =
right-unit-law-mul-Monoid (monoid-Commutative-Monoid-𝔽 M)

## Properties

### There is a finite number of ways to equip a finite type with the structure of a finite commutative monoid

module _
{l : Level}
(X : 𝔽 l)
where

structure-commutative-monoid-𝔽 : UU l
structure-commutative-monoid-𝔽 =
Σ ( structure-monoid-𝔽 X)
( λ m  is-commutative-Monoid-𝔽 (finite-monoid-structure-monoid-𝔽 X m))

finite-commutative-monoid-structure-commutative-monoid-𝔽 :
structure-commutative-monoid-𝔽  Commutative-Monoid-𝔽 l
pr1 (finite-commutative-monoid-structure-commutative-monoid-𝔽 (m , c)) =
finite-monoid-structure-monoid-𝔽 X m
pr2 (finite-commutative-monoid-structure-commutative-monoid-𝔽 (m , c)) = c

is-finite-structure-commutative-monoid-𝔽 :
is-finite structure-commutative-monoid-𝔽
is-finite-structure-commutative-monoid-𝔽 =
is-finite-Σ
( is-finite-structure-monoid-𝔽 X)
( λ m
is-finite-Π
( is-finite-type-𝔽 X)
( λ x  is-finite-Π ( is-finite-type-𝔽 X) ( λ y  is-finite-eq-𝔽 X)))