# Function rings

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-13.

module ring-theory.function-rings 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.monoids

open import ring-theory.dependent-products-rings
open import ring-theory.rings


## Idea

Given a ring R and a type X, the exponent ring R^X consists of functions from X into the underlying type of R. The operations on R^X are defined pointwise.

## Definition

module _
{l1 l2 : Level} (R : Ring l1) (X : UU l2)
where

function-Ring : Ring (l1 ⊔ l2)
function-Ring = Π-Ring X (λ _ → R)

ab-function-Ring : Ab (l1 ⊔ l2)
ab-function-Ring = ab-Π-Ring X (λ _ → R)

multiplicative-monoid-function-Ring : Monoid (l1 ⊔ l2)
multiplicative-monoid-function-Ring =
multiplicative-monoid-Π-Ring X (λ _ → R)

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

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

zero-function-Ring : type-function-Ring
zero-function-Ring = zero-Π-Ring X (λ _ → R)

one-function-Ring : type-function-Ring
one-function-Ring = one-Π-Ring X (λ _ → R)

add-function-Ring : (f g : type-function-Ring) → type-function-Ring

neg-function-Ring : type-function-Ring → type-function-Ring
neg-function-Ring = neg-Π-Ring X (λ _ → R)

mul-function-Ring : (f g : type-function-Ring) → type-function-Ring
mul-function-Ring = mul-Π-Ring X (λ _ → R)

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

(f g : type-function-Ring) →

(f : type-function-Ring) →
left-unit-law-add-Π-Ring X (λ _ → R)

(f : type-function-Ring) →
right-unit-law-add-Π-Ring X (λ _ → R)

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

(f : type-function-Ring) →
add-function-Ring f (neg-function-Ring f) ＝ zero-function-Ring
right-inverse-law-add-Π-Ring X (λ _ → R)

associative-mul-function-Ring :
(f g h : type-function-Ring) →
mul-function-Ring (mul-function-Ring f g) h ＝
mul-function-Ring f (mul-function-Ring g h)
associative-mul-function-Ring =
associative-mul-Π-Ring X (λ _ → R)

left-unit-law-mul-function-Ring :
(f : type-function-Ring) →
mul-function-Ring one-function-Ring f ＝ f
left-unit-law-mul-function-Ring =
left-unit-law-mul-Π-Ring X (λ _ → R)

right-unit-law-mul-function-Ring :
(f : type-function-Ring) →
mul-function-Ring f one-function-Ring ＝ f
right-unit-law-mul-function-Ring =
right-unit-law-mul-Π-Ring X (λ _ → R)

(f g h : type-function-Ring) →
mul-function-Ring f (add-function-Ring g h) ＝
add-function-Ring (mul-function-Ring f g) (mul-function-Ring f h)