Transposition of matrices
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Louis Wasserman.
Created on 2022-03-16.
Last modified on 2025-05-14.
module linear-algebra.transposition-matrices where
Imports
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.matrices open import lists.functoriality-tuples open import lists.tuples
Idea
The transposition of a matrix¶ is the operation on matrices that turns rows into columns and columns into rows.
Definition
transpose-matrix : {l : Level} → {A : UU l} → {m n : ℕ} → matrix A m n → matrix A n m transpose-matrix {n = zero-ℕ} x = empty-tuple transpose-matrix {n = succ-ℕ n} x = map-tuple head-tuple x ∷ transpose-matrix (map-tuple tail-tuple x)
Properties
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-tuple = 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))) where lemma-first-row : {l : Level} → {A : UU l} → {m n : ℕ} → (x : tuple A n) → (xs : matrix A m n) → Id x (map-tuple head-tuple (transpose-matrix (x ∷ xs))) lemma-first-row {n = zero-ℕ} empty-tuple _ = refl lemma-first-row {n = succ-ℕ m} (k ∷ ks) xs = ap (_∷_ k) (lemma-first-row ks (map-tuple tail-tuple xs)) lemma-rest : {l : Level} → {A : UU l} → {m n : ℕ} → (x : tuple A n) → (xs : matrix A m n) → Id (transpose-matrix xs) (map-tuple tail-tuple (transpose-matrix (x ∷ xs))) lemma-rest {n = zero-ℕ} empty-tuple xs = refl lemma-rest {n = succ-ℕ n} (k ∷ ks) xs = ap ( _∷_ (map-tuple head-tuple xs)) ( lemma-rest (tail-tuple (k ∷ ks)) (map-tuple tail-tuple xs))
External links
- Matrix transposition at Wikidata
Recent changes
- 2025-05-14. Louis Wasserman. Refactor linear algebra to use “tuples” for what was “vectors” (#1397).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).