# Cartesian products of abelian groups

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

Created on 2022-05-21.

module group-theory.cartesian-products-abelian-groups 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.abelian-groups
open import group-theory.cartesian-products-groups
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups


## Idea

The cartesian product of two abelian groups A and B is an abelian group structure on the cartesian product of the underlying sets.

## Definition

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

group-product-Ab : Group (l1 ⊔ l2)
group-product-Ab = product-Group (group-Ab A) (group-Ab B)

monoid-product-Ab : Monoid (l1 ⊔ l2)
monoid-product-Ab = monoid-Group group-product-Ab

semigroup-product-Ab : Semigroup (l1 ⊔ l2)
semigroup-product-Ab = semigroup-Group group-product-Ab

set-product-Ab : Set (l1 ⊔ l2)
set-product-Ab = set-Group group-product-Ab

type-product-Ab : UU (l1 ⊔ l2)
type-product-Ab = type-Group group-product-Ab

is-set-type-product-Ab : is-set type-product-Ab
is-set-type-product-Ab = is-set-type-Group group-product-Ab

add-product-Ab : (x y : type-product-Ab) → type-product-Ab

zero-product-Ab : type-product-Ab
zero-product-Ab = unit-Group group-product-Ab

neg-product-Ab : type-product-Ab → type-product-Ab
neg-product-Ab = inv-Group group-product-Ab

(x y z : type-product-Ab) →
Id

(x : type-product-Ab) → Id (add-product-Ab zero-product-Ab x) x

(x : type-product-Ab) → Id (add-product-Ab x zero-product-Ab) x

(x : type-product-Ab) →
Id (add-product-Ab (neg-product-Ab x) x) zero-product-Ab

(x : type-product-Ab) →
Id (add-product-Ab x (neg-product-Ab x)) zero-product-Ab