# Cartesian products of semigroups

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

Created on 2022-05-21.

module group-theory.cartesian-products-semigroups 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.semigroups


## Idea

The cartesian product of two semigroups A and B consists of the cartesian product of its underlying sets and the componentwise multiplication

## Definition

module _
{l1 l2 : Level} (A : Semigroup l1) (B : Semigroup l2)
where

set-product-Semigroup : Set (l1 ⊔ l2)
set-product-Semigroup = product-Set (set-Semigroup A) (set-Semigroup B)

type-product-Semigroup : UU (l1 ⊔ l2)
type-product-Semigroup = type-Set set-product-Semigroup

is-set-type-product-Semigroup : is-set type-product-Semigroup
is-set-type-product-Semigroup = is-set-type-Set set-product-Semigroup

mul-product-Semigroup :
type-product-Semigroup → type-product-Semigroup → type-product-Semigroup
pr1 (mul-product-Semigroup (pair x1 y1) (pair x2 y2)) = mul-Semigroup A x1 x2
pr2 (mul-product-Semigroup (pair x1 y1) (pair x2 y2)) = mul-Semigroup B y1 y2

associative-mul-product-Semigroup :
(x y z : type-product-Semigroup) →
Id
( mul-product-Semigroup (mul-product-Semigroup x y) z)
( mul-product-Semigroup x (mul-product-Semigroup y z))
associative-mul-product-Semigroup (pair x1 y1) (pair x2 y2) (pair x3 y3) =
eq-pair
( associative-mul-Semigroup A x1 x2 x3)
( associative-mul-Semigroup B y1 y2 y3)

product-Semigroup : Semigroup (l1 ⊔ l2)
pr1 product-Semigroup = set-product-Semigroup
pr1 (pr2 product-Semigroup) = mul-product-Semigroup
pr2 (pr2 product-Semigroup) = associative-mul-product-Semigroup