Function groups of abelian groups

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-13.

module group-theory.function-abelian-groups where

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


Idea

Given an abelian group G and a type X, the function group G^X consists of functions from X to the underlying type of G. The group operations are given pointwise.

Definition

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

function-Ab : Ab (l1 ⊔ l2)
function-Ab = Π-Ab X (λ _ → A)

group-function-Ab : Group (l1 ⊔ l2)
group-function-Ab = group-Π-Ab X (λ _ → A)

semigroup-function-Ab : Semigroup (l1 ⊔ l2)
semigroup-function-Ab = semigroup-Π-Ab X (λ _ → A)

set-function-Ab : Set (l1 ⊔ l2)
set-function-Ab = set-Π-Ab X (λ _ → A)

type-function-Ab : UU (l1 ⊔ l2)
type-function-Ab = type-Π-Ab X (λ _ → A)

(f g : type-function-Ab) → type-function-Ab

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

zero-function-Ab : type-function-Ab
zero-function-Ab = zero-Π-Ab X (λ _ → A)

(f : type-function-Ab) → add-function-Ab zero-function-Ab f ＝ f

(f : type-function-Ab) → add-function-Ab f zero-function-Ab ＝ f

monoid-function-Ab : Monoid (l1 ⊔ l2)
monoid-function-Ab = monoid-Π-Ab X (λ _ → A)

neg-function-Ab : type-function-Ab → type-function-Ab
neg-function-Ab = neg-Π-Ab X (λ _ → A)

(f : type-function-Ab) →
add-function-Ab (neg-function-Ab f) f ＝ zero-function-Ab
left-inverse-law-add-Π-Ab X (λ _ → A)