# Dependent products of abelian groups

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-13.

module group-theory.dependent-products-abelian-groups where

Imports
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.dependent-products-groups
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups


## Idea

Given a family of abelian groups Aᵢ indexed by i : I, the dependent product Π(i : I), Aᵢ is an abelian group consisting of dependent functions taking i : I to an element of the underlying type of Aᵢ. The multiplicative operation and the unit are given pointwise.

## Definition

module _
{l1 l2 : Level} (I : UU l1) (A : I → Ab l2)
where

group-Π-Ab : Group (l1 ⊔ l2)
group-Π-Ab = Π-Group I (λ i → group-Ab (A i))

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

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

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

add-Π-Ab : (f g : type-Π-Ab) → type-Π-Ab

(f g h : type-Π-Ab) →

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

is-unital-Π-Ab : is-unital-Semigroup semigroup-Π-Ab
is-unital-Π-Ab = is-unital-Group group-Π-Ab

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

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

(f : type-Π-Ab) → add-Π-Ab (neg-Π-Ab f) f ＝ zero-Π-Ab

(f : type-Π-Ab) → add-Π-Ab f (neg-Π-Ab f) ＝ zero-Π-Ab

is-group-Π-Ab : is-group-Semigroup semigroup-Π-Ab
is-group-Π-Ab = is-group-Group group-Π-Ab