Matrices

module linear-algebra.matrices where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.functoriality-vectors
open import linear-algebra.vectors

Idea

An (m × n)-matrix of elements in A is an arrangement of elements of A with m rows and n columns. In other words, a matrix is vector of length m of vectors of length n of elements of A.

Definitions

Matrices

matrix : {l : Level} (A : UU l) → ℕ → ℕ → UU l
matrix A m n = vec (vec A n) m

The top row of a matrix

top-row-matrix :
  {l : Level} {m n : ℕ} {A : UU l} → matrix A (succ-ℕ m) n → vec A n
top-row-matrix (v ∷ M) = v

The left column of a matrix

left-column-matrix :
  {l : Level} {m n : ℕ} {A : UU l} → matrix A m (succ-ℕ n) → vec A m
left-column-matrix = map-vec head-vec

The vertical tail of a matrix

vertical-tail-matrix :
  {l : Level} {m n : ℕ} {A : UU l} → matrix A (succ-ℕ m) n → matrix A m n
vertical-tail-matrix M = tail-vec M

The horizontal tail of a matrix

horizontal-tail-matrix :
  {l : Level} {m n : ℕ} {A : UU l} → matrix A m (succ-ℕ n) → matrix A m n
horizontal-tail-matrix = map-vec tail-vec

The vertically empty matrix

vertically-empty-matrix :
  {l : Level} {n : ℕ} {A : UU l} → matrix A 0 n
vertically-empty-matrix = empty-vec

eq-vertically-empty-matrix :
  {l : Level} {n : ℕ} {A : UU l}
  (x : matrix A 0 n) → Id vertically-empty-matrix x
eq-vertically-empty-matrix empty-vec = refl

is-contr-matrix-zero-ℕ :
  {l : Level} {n : ℕ} {A : UU l} → is-contr (matrix A 0 n)
pr1 is-contr-matrix-zero-ℕ = vertically-empty-matrix
pr2 is-contr-matrix-zero-ℕ = eq-vertically-empty-matrix

The horizontally empty matrix

horizontally-empty-matrix :
  {l : Level} {m : ℕ} {A : UU l} → matrix A m 0
horizontally-empty-matrix {m = zero-ℕ} = empty-vec
horizontally-empty-matrix {m = succ-ℕ m} = empty-vec ∷ horizontally-empty-matrix

eq-horizontally-empty-matrix :
  {l : Level} {m : ℕ} {A : UU l}
  (x : matrix A m 0) → Id horizontally-empty-matrix x
eq-horizontally-empty-matrix {m = zero-ℕ} empty-vec = refl
eq-horizontally-empty-matrix {m = succ-ℕ m} (empty-vec ∷ M) =
  ap-binary _∷_ refl (eq-horizontally-empty-matrix M)

is-contr-matrix-zero-ℕ' :
  {l : Level} {m : ℕ} {A : UU l} → is-contr (matrix A m 0)
pr1 is-contr-matrix-zero-ℕ' = horizontally-empty-matrix
pr2 is-contr-matrix-zero-ℕ' = eq-horizontally-empty-matrix