Transposition of matrices

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

Created on 2022-03-16.
Last modified on 2023-06-10.

module linear-algebra.transposition-matrices where
open import elementary-number-theory.natural-numbers

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

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


The transposition of a matrix is the operation that turns rows into columns and columns into rows.


transpose-matrix :
  {l : Level}  {A : UU l}  {m n : }  matrix A m n  matrix A n m
transpose-matrix {n = zero-ℕ} x = empty-vec
transpose-matrix {n = succ-ℕ n} x =
  map-vec head-vec x  transpose-matrix (map-vec tail-vec x)


is-involution-transpose-matrix :
  {l : Level}  {A : UU l}  {m n : } 
  (x : matrix A m n)  Id x (transpose-matrix (transpose-matrix x))
is-involution-transpose-matrix {m = zero-ℕ} empty-vec = refl
is-involution-transpose-matrix {m = succ-ℕ m} (r  rs) =
  ( ap (_∷_ r) (is-involution-transpose-matrix rs)) 
  ( ap-binary _∷_
    ( lemma-first-row r rs) (ap transpose-matrix (lemma-rest r rs)))
  lemma-first-row :
    {l : Level}  {A : UU l}  {m n : }  (x : vec A n)  (xs : matrix A m n) 
    Id x (map-vec head-vec (transpose-matrix (x  xs)))
  lemma-first-row {n = zero-ℕ} empty-vec _ = refl
  lemma-first-row {n = succ-ℕ m} (k  ks) xs =
    ap (_∷_ k) (lemma-first-row ks (map-vec tail-vec xs))

  lemma-rest :
    {l : Level}  {A : UU l}  {m n : }  (x : vec A n)  (xs : matrix A m n) 
    Id (transpose-matrix xs) (map-vec tail-vec (transpose-matrix (x  xs)))
  lemma-rest {n = zero-ℕ} empty-vec xs = refl
  lemma-rest {n = succ-ℕ n} (k  ks) xs =
      ( _∷_ (map-vec head-vec xs))
      ( lemma-rest (tail-vec (k  ks)) (map-vec tail-vec xs))

Recent changes