# Algebras over rings

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

Created on 2022-10-18.

module ring-theory.algebras-rings where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import ring-theory.modules-rings
open import ring-theory.rings


## Idea

An algebra over a ring R consists of an R-module M equipped with a binary operation x y ↦ xy : M → M → M such that

  (xy)z  = x(yz)
r(xy)  = (rx)y
r(xy)  = x(ry)
(x+y)z = xz+yz
x(y+z) = xy+xz


## Definitions

### Nonunital algebras over a ring

has-bilinear-mul-left-module-Ring :
{l1 l2 : Level} (R : Ring l1) (M : left-module-Ring l2 R) → UU (l1 ⊔ l2)
has-bilinear-mul-left-module-Ring R M =
Σ ( (x y : type-left-module-Ring R M) → type-left-module-Ring R M)
( λ μ →
( (x y z : type-left-module-Ring R M) → μ (μ x y) z ＝ μ x (μ y z)) ×
( ( ( (r : type-Ring R) (x y : type-left-module-Ring R M) →
mul-left-module-Ring R M r (μ x y) ＝
μ (mul-left-module-Ring R M r x) y) ×
( (r : type-Ring R) (x y : type-left-module-Ring R M) →
mul-left-module-Ring R M r (μ x y) ＝
μ x (mul-left-module-Ring R M r y))) ×
( ( (x y z : type-left-module-Ring R M) →
μ (add-left-module-Ring R M x y) z ＝
add-left-module-Ring R M (μ x z) (μ y z)) ×
( (x y z : type-left-module-Ring R M) →
μ x (add-left-module-Ring R M y z) ＝
add-left-module-Ring R M (μ x y) (μ x z)))))

Nonunital-Left-Algebra-Ring :
{l1 : Level} (l2 : Level) (R : Ring l1) → UU (l1 ⊔ lsuc l2)
Nonunital-Left-Algebra-Ring l2 R =
Σ ( left-module-Ring l2 R) (has-bilinear-mul-left-module-Ring R)

module _
{l1 l2 : Level} (R : Ring l1) (A : Nonunital-Left-Algebra-Ring l2 R)
where

left-module-Nonunital-Left-Algebra-Ring : left-module-Ring l2 R
left-module-Nonunital-Left-Algebra-Ring = pr1 A

bilinear-mul-Nonunital-Left-Algebra-Ring :
has-bilinear-mul-left-module-Ring R left-module-Nonunital-Left-Algebra-Ring
bilinear-mul-Nonunital-Left-Algebra-Ring = pr2 A

type-Nonunital-Left-Algebra-Ring : UU l2
type-Nonunital-Left-Algebra-Ring =
type-left-module-Ring R left-module-Nonunital-Left-Algebra-Ring

zero-Nonunital-Left-Algebra-Ring : type-Nonunital-Left-Algebra-Ring
zero-Nonunital-Left-Algebra-Ring =
zero-left-module-Ring R left-module-Nonunital-Left-Algebra-Ring

(x y : type-Nonunital-Left-Algebra-Ring) → type-Nonunital-Left-Algebra-Ring

neg-Nonunital-Left-Algebra-Ring :
type-Nonunital-Left-Algebra-Ring → type-Nonunital-Left-Algebra-Ring
neg-Nonunital-Left-Algebra-Ring =
neg-left-module-Ring R left-module-Nonunital-Left-Algebra-Ring

action-Nonunital-Left-Algebra-Ring :
(r : type-Ring R) →
type-Nonunital-Left-Algebra-Ring → type-Nonunital-Left-Algebra-Ring
action-Nonunital-Left-Algebra-Ring =
mul-left-module-Ring R left-module-Nonunital-Left-Algebra-Ring

mul-Nonunital-Left-Algebra-Ring :
(x y : type-Nonunital-Left-Algebra-Ring) → type-Nonunital-Left-Algebra-Ring
mul-Nonunital-Left-Algebra-Ring =
pr1 bilinear-mul-Nonunital-Left-Algebra-Ring

(x y z : type-Nonunital-Left-Algebra-Ring) →

(x : type-Nonunital-Left-Algebra-Ring) →

(x : type-Nonunital-Left-Algebra-Ring) →
left-module-Nonunital-Left-Algebra-Ring

(x : type-Nonunital-Left-Algebra-Ring) →
zero-Nonunital-Left-Algebra-Ring
left-module-Nonunital-Left-Algebra-Ring

(x : type-Nonunital-Left-Algebra-Ring) →
zero-Nonunital-Left-Algebra-Ring
left-module-Nonunital-Left-Algebra-Ring

(r : type-Ring R) (x y : type-Nonunital-Left-Algebra-Ring) →
action-Nonunital-Left-Algebra-Ring r
( action-Nonunital-Left-Algebra-Ring r x)
( action-Nonunital-Left-Algebra-Ring r y)
left-module-Nonunital-Left-Algebra-Ring

(r s : type-Ring R) (x : type-Nonunital-Left-Algebra-Ring) →
action-Nonunital-Left-Algebra-Ring (add-Ring R r s) x ＝
( action-Nonunital-Left-Algebra-Ring r x)
( action-Nonunital-Left-Algebra-Ring s x)
left-module-Nonunital-Left-Algebra-Ring

associative-action-Nonunital-Left-Algebra-Ring :
(r s : type-Ring R) (x : type-Nonunital-Left-Algebra-Ring) →
action-Nonunital-Left-Algebra-Ring (mul-Ring R r s) x ＝
action-Nonunital-Left-Algebra-Ring r
( action-Nonunital-Left-Algebra-Ring s x)
associative-action-Nonunital-Left-Algebra-Ring =
associative-mul-left-module-Ring R
left-module-Nonunital-Left-Algebra-Ring

left-zero-law-action-Nonunital-Left-Algebra-Ring :
(x : type-Nonunital-Left-Algebra-Ring) →
action-Nonunital-Left-Algebra-Ring (zero-Ring R) x ＝
zero-Nonunital-Left-Algebra-Ring
left-zero-law-action-Nonunital-Left-Algebra-Ring =
left-zero-law-mul-left-module-Ring R
left-module-Nonunital-Left-Algebra-Ring

right-zero-law-action-Nonunital-Left-Algebra-Ring :
(r : type-Ring R) →
action-Nonunital-Left-Algebra-Ring r zero-Nonunital-Left-Algebra-Ring ＝
zero-Nonunital-Left-Algebra-Ring
right-zero-law-action-Nonunital-Left-Algebra-Ring =
right-zero-law-mul-left-module-Ring R
left-module-Nonunital-Left-Algebra-Ring

left-negative-law-action-Nonunital-Left-Algebra-Ring :
(r : type-Ring R) (x : type-Nonunital-Left-Algebra-Ring) →
action-Nonunital-Left-Algebra-Ring (neg-Ring R r) x ＝
neg-Nonunital-Left-Algebra-Ring (action-Nonunital-Left-Algebra-Ring r x)
left-negative-law-action-Nonunital-Left-Algebra-Ring =
left-negative-law-mul-left-module-Ring R
left-module-Nonunital-Left-Algebra-Ring

right-negative-law-action-Nonunital-Left-Algebra-Ring :
(r : type-Ring R) (x : type-Nonunital-Left-Algebra-Ring) →
action-Nonunital-Left-Algebra-Ring r (neg-Nonunital-Left-Algebra-Ring x) ＝
neg-Nonunital-Left-Algebra-Ring (action-Nonunital-Left-Algebra-Ring r x)
right-negative-law-action-Nonunital-Left-Algebra-Ring =
right-negative-law-mul-left-module-Ring R
left-module-Nonunital-Left-Algebra-Ring


### Unital algebras over a ring

This remains to be defined. #740