# Cartesian products of monoids

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-05-21.
Last modified on 2024-02-06.

module group-theory.cartesian-products-monoids where

Imports
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

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


## Idea

The cartesian product of two monoids M and N consists of the product M × N of the underlying sets and the componentwise operation on it.

## Definition

module _
{l1 l2 : Level} (M : Monoid l1) (N : Monoid l2)
where

semigroup-product-Monoid : Semigroup (l1 ⊔ l2)
semigroup-product-Monoid =
product-Semigroup (semigroup-Monoid M) (semigroup-Monoid N)

set-product-Monoid : Set (l1 ⊔ l2)
set-product-Monoid = set-Semigroup semigroup-product-Monoid

type-product-Monoid : UU (l1 ⊔ l2)
type-product-Monoid = type-Semigroup semigroup-product-Monoid

is-set-type-product-Monoid : is-set type-product-Monoid
is-set-type-product-Monoid = is-set-type-Semigroup semigroup-product-Monoid

mul-product-Monoid : (x y : type-product-Monoid) → type-product-Monoid
mul-product-Monoid = mul-Semigroup semigroup-product-Monoid

associative-mul-product-Monoid :
(x y z : type-product-Monoid) →
Id
( mul-product-Monoid (mul-product-Monoid x y) z)
( mul-product-Monoid x (mul-product-Monoid y z))
associative-mul-product-Monoid =
associative-mul-Semigroup semigroup-product-Monoid

unit-product-Monoid : type-product-Monoid
pr1 unit-product-Monoid = unit-Monoid M
pr2 unit-product-Monoid = unit-Monoid N

left-unit-law-mul-product-Monoid :
(x : type-product-Monoid) → Id (mul-product-Monoid unit-product-Monoid x) x
left-unit-law-mul-product-Monoid (pair x y) =
eq-pair (left-unit-law-mul-Monoid M x) (left-unit-law-mul-Monoid N y)

right-unit-law-mul-product-Monoid :
(x : type-product-Monoid) → Id (mul-product-Monoid x unit-product-Monoid) x
right-unit-law-mul-product-Monoid (pair x y) =
eq-pair (right-unit-law-mul-Monoid M x) (right-unit-law-mul-Monoid N y)

product-Monoid : Monoid (l1 ⊔ l2)
pr1 product-Monoid = semigroup-product-Monoid
pr1 (pr2 product-Monoid) = unit-product-Monoid
pr1 (pr2 (pr2 product-Monoid)) = left-unit-law-mul-product-Monoid
pr2 (pr2 (pr2 product-Monoid)) = right-unit-law-mul-product-Monoid