# Matrices on rings

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

Created on 2022-03-22.

module linear-algebra.matrices-on-rings where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.constant-matrices
open import linear-algebra.functoriality-matrices
open import linear-algebra.matrices
open import linear-algebra.vectors
open import linear-algebra.vectors-on-rings

open import ring-theory.rings


## Definitions

### Matrices

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

matrix-Ring : ℕ → ℕ → UU l
matrix-Ring m n = matrix (type-Ring R) m n


### The zero matrix

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

zero-matrix-Ring : {m n : ℕ} → matrix-Ring R m n
zero-matrix-Ring = constant-matrix (zero-Ring R)


### Addition of matrices on rings

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

add-matrix-Ring : {m n : ℕ} (A B : matrix-Ring R m n) → matrix-Ring R m n


## Properties

### Addition of matrices is associative

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

{m n : ℕ} (A B C : matrix-Ring R m n) →
Id
associative-add-matrix-Ring empty-vec empty-vec empty-vec = refl
associative-add-matrix-Ring (v ∷ A) (w ∷ B) (z ∷ C) =
ap-binary _∷_
( associative-add-vec-Ring R v w z)


### Addition of matrices is commutative

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

{m n : ℕ} (A B : matrix-Ring R m n) →
commutative-add-matrix-Ring (v ∷ A) (w ∷ B) =
ap-binary _∷_


### Left unit law for addition of matrices

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

{m n : ℕ} (A : matrix-Ring R m n) →
Id (add-matrix-Ring R (zero-matrix-Ring R) A) A
ap-binary _∷_


### Right unit law for addition of matrices

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