# Finite rings

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-05-25.

module finite-algebra.finite-rings where
Imports
open import elementary-number-theory.natural-numbers

open import finite-group-theory.finite-abelian-groups
open import finite-group-theory.finite-groups
open import finite-group-theory.finite-monoids

open import foundation.binary-embeddings
open import foundation.binary-equivalences
open import foundation.embeddings
open import foundation.equivalences
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.involutions
open import foundation.propositions
open import foundation.sets
open import foundation.unital-binary-operations
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.commutative-monoids
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups

open import lists.concatenation-lists
open import lists.lists

open import ring-theory.rings
open import ring-theory.semirings

open import univalent-combinatorics.cartesian-product-types
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types

## Idea

A finite ring is a ring where the underlying type is finite.

## Definitions

### Finite Rings

has-mul-Ab-𝔽 : {l1 : Level} (A : Ab-𝔽 l1)  UU l1
has-mul-Ab-𝔽 A = has-mul-Ab (ab-Ab-𝔽 A)

Ring-𝔽 : (l1 : Level)  UU (lsuc l1)
Ring-𝔽 l1 = Σ (Ab-𝔽 l1)  A  has-mul-Ab-𝔽 A)

finite-ring-is-finite-Ring :
{l : Level}  (R : Ring l)  is-finite (type-Ring R)  Ring-𝔽 l
pr1 (finite-ring-is-finite-Ring R f) =
finite-abelian-group-is-finite-Ab (ab-Ring R) f
pr2 (finite-ring-is-finite-Ring R f) = pr2 R

module _
{l : Level} (R : Ring-𝔽 l)
where

finite-ab-Ring-𝔽 : Ab-𝔽 l
finite-ab-Ring-𝔽 = pr1 R

ab-Ring-𝔽 : Ab l
ab-Ring-𝔽 = ab-Ab-𝔽 finite-ab-Ring-𝔽

ring-Ring-𝔽 : Ring l
pr1 ring-Ring-𝔽 = ab-Ring-𝔽
pr2 ring-Ring-𝔽 = pr2 R

finite-type-Ring-𝔽 : 𝔽 l
finite-type-Ring-𝔽 = finite-type-Ab-𝔽 finite-ab-Ring-𝔽

type-Ring-𝔽 : UU l
type-Ring-𝔽 = type-Ab-𝔽 finite-ab-Ring-𝔽

is-finite-type-Ring-𝔽 : is-finite type-Ring-𝔽
is-finite-type-Ring-𝔽 = is-finite-type-Ab-𝔽 finite-ab-Ring-𝔽

finite-group-Ring-𝔽 : Group-𝔽 l
finite-group-Ring-𝔽 = finite-group-Ab-𝔽 finite-ab-Ring-𝔽

group-Ring-𝔽 : Group l
group-Ring-𝔽 = group-Ab ab-Ring-𝔽

commutative-monoid-Ab ab-Ring-𝔽

set-Ring-𝔽 : Set l
set-Ring-𝔽 = set-Ab ab-Ring-𝔽

is-set-type-Ring-𝔽 : is-set type-Ring-𝔽
is-set-type-Ring-𝔽 = is-set-type-Ab ab-Ring-𝔽

module _
{l : Level} (R : Ring-𝔽 l)
where

add-Ring-𝔽 : type-Ring-𝔽 R  type-Ring-𝔽 R  type-Ring-𝔽 R

add-Ring-𝔽' : type-Ring-𝔽 R  type-Ring-𝔽 R  type-Ring-𝔽 R

{x y x' y' : type-Ring-𝔽 R}
Id x x'  Id y y'  Id (add-Ring-𝔽 x y) (add-Ring-𝔽 x' y')

(x y z : type-Ring-𝔽 R)

(x y : type-Ring-𝔽 R)  Id (add-Ring-𝔽 x y) (add-Ring-𝔽 y x)

(x y x' y' : type-Ring-𝔽 R)

(x y z : type-Ring-𝔽 R)

(x y z : type-Ring-𝔽 R)

### The zero element of a ring

module _
{l : Level} (R : Ring-𝔽 l)
where

has-zero-Ring-𝔽 = has-zero-Ring (ring-Ring-𝔽 R)

zero-Ring-𝔽 : type-Ring-𝔽 R
zero-Ring-𝔽 = zero-Ring (ring-Ring-𝔽 R)

is-zero-Ring-𝔽 : type-Ring-𝔽 R  UU l
is-zero-Ring-𝔽 = is-zero-Ring (ring-Ring-𝔽 R)

is-nonzero-Ring-𝔽 : type-Ring-𝔽 R  UU l
is-nonzero-Ring-𝔽 = is-nonzero-Ring (ring-Ring-𝔽 R)

is-zero-finite-ring-Prop : type-Ring-𝔽 R  Prop l
is-zero-finite-ring-Prop = is-zero-ring-Prop (ring-Ring-𝔽 R)

is-nonzero-finite-ring-Prop : type-Ring-𝔽 R  Prop l
is-nonzero-finite-ring-Prop = is-nonzero-ring-Prop (ring-Ring-𝔽 R)

(x : type-Ring-𝔽 R)  Id (add-Ring-𝔽 R zero-Ring-𝔽 x) x

(x : type-Ring-𝔽 R)  Id (add-Ring-𝔽 R x zero-Ring-𝔽) x

### Additive inverses in a ring

module _
{l : Level} (R : Ring-𝔽 l)
where

has-negatives-Ring-𝔽 :
is-group-is-unital-Semigroup
( has-zero-Ring-𝔽 R)
has-negatives-Ring-𝔽 = has-negatives-Ring (ring-Ring-𝔽 R)

neg-Ring-𝔽 : type-Ring-𝔽 R  type-Ring-𝔽 R
neg-Ring-𝔽 = neg-Ring (ring-Ring-𝔽 R)

(x : type-Ring-𝔽 R)  Id (add-Ring-𝔽 R (neg-Ring-𝔽 x) x) (zero-Ring-𝔽 R)

(x : type-Ring-𝔽 R)  Id (add-Ring-𝔽 R x (neg-Ring-𝔽 x)) (zero-Ring-𝔽 R)

neg-neg-Ring-𝔽 : (x : type-Ring-𝔽 R)  neg-Ring-𝔽 (neg-Ring-𝔽 x)  x
neg-neg-Ring-𝔽 = neg-neg-Ring (ring-Ring-𝔽 R)

(x y : type-Ring-𝔽 R)

### Multiplication in a ring

module _
{l : Level} (R : Ring-𝔽 l)
where

has-associative-mul-Ring-𝔽 : has-associative-mul-Set (set-Ring-𝔽 R)
has-associative-mul-Ring-𝔽 = has-associative-mul-Ring (ring-Ring-𝔽 R)

mul-Ring-𝔽 : type-Ring-𝔽 R  type-Ring-𝔽 R  type-Ring-𝔽 R
mul-Ring-𝔽 = mul-Ring (ring-Ring-𝔽 R)

mul-Ring-𝔽' : type-Ring-𝔽 R  type-Ring-𝔽 R  type-Ring-𝔽 R
mul-Ring-𝔽' = mul-Ring' (ring-Ring-𝔽 R)

ap-mul-Ring-𝔽 :
{x x' y y' : type-Ring-𝔽 R} (p : Id x x') (q : Id y y')
Id (mul-Ring-𝔽 x y) (mul-Ring-𝔽 x' y')
ap-mul-Ring-𝔽 = ap-mul-Ring (ring-Ring-𝔽 R)

associative-mul-Ring-𝔽 :
(x y z : type-Ring-𝔽 R)
Id (mul-Ring-𝔽 (mul-Ring-𝔽 x y) z) (mul-Ring-𝔽 x (mul-Ring-𝔽 y z))
associative-mul-Ring-𝔽 = associative-mul-Ring (ring-Ring-𝔽 R)

multiplicative-semigroup-Ring-𝔽 : Semigroup l
multiplicative-semigroup-Ring-𝔽 =
multiplicative-semigroup-Ring (ring-Ring-𝔽 R)

(x y z : type-Ring-𝔽 R)
mul-Ring-𝔽 x (add-Ring-𝔽 R y z)
add-Ring-𝔽 R (mul-Ring-𝔽 x y) (mul-Ring-𝔽 x z)

(x y z : type-Ring-𝔽 R)
mul-Ring-𝔽 (add-Ring-𝔽 R x y) z
add-Ring-𝔽 R (mul-Ring-𝔽 x z) (mul-Ring-𝔽 y z)

### Multiplicative units in a ring

module _
{l : Level} (R : Ring-𝔽 l)
where

is-unital-Ring-𝔽 : is-unital (mul-Ring-𝔽 R)
is-unital-Ring-𝔽 = is-unital-Ring (ring-Ring-𝔽 R)

multiplicative-monoid-Ring-𝔽 : Monoid l
multiplicative-monoid-Ring-𝔽 = multiplicative-monoid-Ring (ring-Ring-𝔽 R)

one-Ring-𝔽 : type-Ring-𝔽 R
one-Ring-𝔽 = one-Ring (ring-Ring-𝔽 R)

left-unit-law-mul-Ring-𝔽 :
(x : type-Ring-𝔽 R)  Id (mul-Ring-𝔽 R one-Ring-𝔽 x) x
left-unit-law-mul-Ring-𝔽 = left-unit-law-mul-Ring (ring-Ring-𝔽 R)

right-unit-law-mul-Ring-𝔽 :
(x : type-Ring-𝔽 R)  Id (mul-Ring-𝔽 R x one-Ring-𝔽) x
right-unit-law-mul-Ring-𝔽 = right-unit-law-mul-Ring (ring-Ring-𝔽 R)

### The zero laws for multiplication of a ring

module _
{l : Level} (R : Ring-𝔽 l)
where

left-zero-law-mul-Ring-𝔽 :
(x : type-Ring-𝔽 R)  Id (mul-Ring-𝔽 R (zero-Ring-𝔽 R) x) (zero-Ring-𝔽 R)
left-zero-law-mul-Ring-𝔽 =
left-zero-law-mul-Ring (ring-Ring-𝔽 R)

right-zero-law-mul-Ring-𝔽 :
(x : type-Ring-𝔽 R)  Id (mul-Ring-𝔽 R x (zero-Ring-𝔽 R)) (zero-Ring-𝔽 R)
right-zero-law-mul-Ring-𝔽 =
right-zero-law-mul-Ring (ring-Ring-𝔽 R)

### Rings are semirings

module _
{l : Level} (R : Ring-𝔽 l)
where

has-mul-Ring-𝔽 :
has-mul-Ring-𝔽 = has-mul-Ring (ring-Ring-𝔽 R)

zero-laws-mul-Ring-𝔽 :
zero-laws-Commutative-Monoid
( has-mul-Ring-𝔽)
zero-laws-mul-Ring-𝔽 = zero-laws-mul-Ring (ring-Ring-𝔽 R)

semiring-Ring-𝔽 : Semiring l
semiring-Ring-𝔽 = semiring-Ring (ring-Ring-𝔽 R)

### Computing multiplication with minus one in a ring

module _
{l : Level} (R : Ring-𝔽 l)
where

neg-one-Ring-𝔽 : type-Ring-𝔽 R
neg-one-Ring-𝔽 = neg-one-Ring (ring-Ring-𝔽 R)

mul-neg-one-Ring-𝔽 :
(x : type-Ring-𝔽 R)  mul-Ring-𝔽 R neg-one-Ring-𝔽 x  neg-Ring-𝔽 R x
mul-neg-one-Ring-𝔽 =
mul-neg-one-Ring (ring-Ring-𝔽 R)

mul-neg-one-Ring-𝔽' :
(x : type-Ring-𝔽 R)  mul-Ring-𝔽 R x neg-one-Ring-𝔽  neg-Ring-𝔽 R x
mul-neg-one-Ring-𝔽' =
mul-neg-one-Ring' (ring-Ring-𝔽 R)

is-involution-mul-neg-one-Ring-𝔽 :
is-involution (mul-Ring-𝔽 R neg-one-Ring-𝔽)
is-involution-mul-neg-one-Ring-𝔽 =
is-involution-mul-neg-one-Ring (ring-Ring-𝔽 R)

is-involution-mul-neg-one-Ring-𝔽' :
is-involution (mul-Ring-𝔽' R neg-one-Ring-𝔽)
is-involution-mul-neg-one-Ring-𝔽' =
is-involution-mul-neg-one-Ring' (ring-Ring-𝔽 R)

### Left and right negative laws for multiplication

module _
{l : Level} (R : Ring-𝔽 l)
where

left-negative-law-mul-Ring-𝔽 :
(x y : type-Ring-𝔽 R)
mul-Ring-𝔽 R (neg-Ring-𝔽 R x) y  neg-Ring-𝔽 R (mul-Ring-𝔽 R x y)
left-negative-law-mul-Ring-𝔽 =
left-negative-law-mul-Ring (ring-Ring-𝔽 R)

right-negative-law-mul-Ring-𝔽 :
(x y : type-Ring-𝔽 R)
mul-Ring-𝔽 R x (neg-Ring-𝔽 R y)  neg-Ring-𝔽 R (mul-Ring-𝔽 R x y)
right-negative-law-mul-Ring-𝔽 =
right-negative-law-mul-Ring (ring-Ring-𝔽 R)

mul-neg-Ring-𝔽 :
(x y : type-Ring-𝔽 R)
mul-Ring-𝔽 R (neg-Ring-𝔽 R x) (neg-Ring-𝔽 R y)  mul-Ring-𝔽 R x y
mul-neg-Ring-𝔽 =
mul-neg-Ring (ring-Ring-𝔽 R)

### Scalar multiplication of ring elements by a natural number

module _
{l : Level} (R : Ring-𝔽 l)
where

mul-nat-scalar-Ring-𝔽 :   type-Ring-𝔽 R  type-Ring-𝔽 R
mul-nat-scalar-Ring-𝔽 = mul-nat-scalar-Ring (ring-Ring-𝔽 R)

ap-mul-nat-scalar-Ring-𝔽 :
{m n : } {x y : type-Ring-𝔽 R}
(m  n)  (x  y)  mul-nat-scalar-Ring-𝔽 m x  mul-nat-scalar-Ring-𝔽 n y
ap-mul-nat-scalar-Ring-𝔽 = ap-mul-nat-scalar-Ring (ring-Ring-𝔽 R)

left-zero-law-mul-nat-scalar-Ring-𝔽 :
(x : type-Ring-𝔽 R)  mul-nat-scalar-Ring-𝔽 0 x  zero-Ring-𝔽 R
left-zero-law-mul-nat-scalar-Ring-𝔽 =
left-zero-law-mul-nat-scalar-Ring (ring-Ring-𝔽 R)

right-zero-law-mul-nat-scalar-Ring-𝔽 :
(n : )  mul-nat-scalar-Ring-𝔽 n (zero-Ring-𝔽 R)  zero-Ring-𝔽 R
right-zero-law-mul-nat-scalar-Ring-𝔽 =
right-zero-law-mul-nat-scalar-Ring (ring-Ring-𝔽 R)

left-unit-law-mul-nat-scalar-Ring-𝔽 :
(x : type-Ring-𝔽 R)  mul-nat-scalar-Ring-𝔽 1 x  x
left-unit-law-mul-nat-scalar-Ring-𝔽 =
left-unit-law-mul-nat-scalar-Ring (ring-Ring-𝔽 R)

left-nat-scalar-law-mul-Ring-𝔽 :
(n : ) (x y : type-Ring-𝔽 R)
mul-Ring-𝔽 R (mul-nat-scalar-Ring-𝔽 n x) y
mul-nat-scalar-Ring-𝔽 n (mul-Ring-𝔽 R x y)
left-nat-scalar-law-mul-Ring-𝔽 =
left-nat-scalar-law-mul-Ring (ring-Ring-𝔽 R)

right-nat-scalar-law-mul-Ring-𝔽 :
(n : ) (x y : type-Ring-𝔽 R)
mul-Ring-𝔽 R x (mul-nat-scalar-Ring-𝔽 n y)
mul-nat-scalar-Ring-𝔽 n (mul-Ring-𝔽 R x y)
right-nat-scalar-law-mul-Ring-𝔽 =
right-nat-scalar-law-mul-Ring (ring-Ring-𝔽 R)

(n : ) (x y : type-Ring-𝔽 R)
mul-nat-scalar-Ring-𝔽 n (add-Ring-𝔽 R x y)
add-Ring-𝔽 R (mul-nat-scalar-Ring-𝔽 n x) (mul-nat-scalar-Ring-𝔽 n y)

(m n : ) (x : type-Ring-𝔽 R)
mul-nat-scalar-Ring-𝔽 (m +ℕ n) x
add-Ring-𝔽 R (mul-nat-scalar-Ring-𝔽 m x) (mul-nat-scalar-Ring-𝔽 n x)

### Addition of a list of elements in an abelian group

module _
{l : Level} (R : Ring-𝔽 l)
where

add-list-Ring-𝔽 : list (type-Ring-𝔽 R)  type-Ring-𝔽 R

(l1 l2 : list (type-Ring-𝔽 R))
Id

## Properties

### There is a finite number of ways to equip a finite type with the structure of a ring

module _
{l : Level}
(X : 𝔽 l)
where

structure-ring-𝔽 : UU l
structure-ring-𝔽 =
Σ ( structure-abelian-group-𝔽 X)
( λ m  has-mul-Ab-𝔽 (finite-abelian-group-structure-abelian-group-𝔽 X m))

finite-ring-structure-ring-𝔽 :
structure-ring-𝔽  Ring-𝔽 l
pr1 (finite-ring-structure-ring-𝔽 (m , c)) =
finite-abelian-group-structure-abelian-group-𝔽 X m
pr2 (finite-ring-structure-ring-𝔽 (m , c)) = c

is-finite-structure-ring-𝔽 :
is-finite structure-ring-𝔽
is-finite-structure-ring-𝔽 =
is-finite-Σ
( is-finite-structure-abelian-group-𝔽 X)
( λ a
is-finite-Σ
( is-finite-Σ
( is-finite-Π
( is-finite-type-𝔽 X)
( λ _
is-finite-Π
( is-finite-type-𝔽 X)
( λ _  is-finite-type-𝔽 X)))
( λ m
is-finite-Π
( is-finite-type-𝔽 X)
( λ x
is-finite-Π
( is-finite-type-𝔽 X)
( λ y
is-finite-Π
( is-finite-type-𝔽 X)
( λ z  is-finite-eq-𝔽 X)))))
( λ a
is-finite-product
( is-finite-is-unital-Semigroup-𝔽 (X , a))
( is-finite-product
( is-finite-Π
( is-finite-type-𝔽 X)
( λ _
is-finite-Π
( is-finite-type-𝔽 X)
( λ _
is-finite-Π
( is-finite-type-𝔽 X)
( λ _  is-finite-eq-𝔽 X))))
( is-finite-Π
( is-finite-type-𝔽 X)
( λ _
is-finite-Π
( is-finite-type-𝔽 X)
( λ _
is-finite-Π
( is-finite-type-𝔽 X)
( λ _  is-finite-eq-𝔽 X)))))))