Cartesian products of semigroups

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-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

Recent changes