# Diagonal matrices on rings

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Eléonore Mangel.

Created on 2022-03-24.

module linear-algebra.diagonal-matrices-on-rings where

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

open import foundation.universe-levels

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

open import ring-theory.rings


## Definitions

### Diagonal matrices

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

diagonal-matrix-Ring : (n : ℕ) → vec-Ring R n → matrix-Ring R n n
diagonal-matrix-Ring zero-ℕ v = empty-vec
diagonal-matrix-Ring (succ-ℕ n) (x ∷ v) =
( x ∷ zero-vec-Ring R) ∷
( map-vec (λ v' → zero-Ring R ∷ v') (diagonal-matrix-Ring n v))


### Scalar matrices

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

scalar-matrix-Ring : (n : ℕ) → type-Ring R → matrix-Ring R n n
scalar-matrix-Ring n x = diagonal-matrix-Ring R n (constant-vec x)

identity-matrix-Ring : (n : ℕ) → matrix-Ring R n n
identity-matrix-Ring n = scalar-matrix-Ring n (one-Ring R)