The map of a matrix on Euclidean space #

Two ingredients of a linear change of variables on EuclideanSpace 𝕜 ι.

Pulling the quadratic form x ↦ ⟪x, B x⟫ of a square matrix B back along the linear map of a rectangular matrix A gives the quadratic form of the congruent matrix Aᴴ * B * A. This is the change-of-variables identity behind every computation of a quadratic statistic after a linear transformation of the underlying vector.

The rank of a matrix is the rank of the linear map it induces, in both the ℕ-valued and the Cardinal-valued sense; this is what lets a matrix-rank statement be read off an operator-rank one.

An invertible square matrix induces not just a map but a continuous linear equivalence, whose inverse is the map of the inverse matrix. That is the form a substitution needs: it supplies the inverse substitution and, through LinearMap.det_toLpLin, the Jacobian.

Main results #

Matrix.inner_toEuclideanLin_toEuclideanLin — the quadratic form of B at A x is the quadratic form of Aᴴ * B * A at x;
Matrix.rank_eq_finrank_range_toEuclideanLin, Matrix.rank_coe_toEuclideanCLM — the matrix rank is the dimension of the range of the induced map, and the LinearMap.rank of the induced continuous linear map;
Matrix.toEuclideanCLE — the continuous linear equivalence of an invertible matrix, with its apply, symm_apply, coercion and determinant lemmas.

source

theorem Matrix.inner_toEuclideanLin_toEuclideanLin {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (A : Matrix κ ι 𝕜) (B : Matrix κ κ 𝕜) (x : EuclideanSpace 𝕜 ι) :

inner 𝕜 ((toEuclideanLin A) x) ((toEuclideanLin B) ((toEuclideanLin A) x)) = inner 𝕜 x ((toEuclideanLin (A.conjTranspose * B * A)) x)

Pulling the quadratic form of B back along the linear map of A gives the quadratic form of the congruent matrix Aᴴ * B * A.

source

theorem Matrix.rank_eq_finrank_range_toEuclideanLin {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Finite κ] (A : Matrix κ ι 𝕜) :

A.rank = Module.finrank 𝕜 ↥(toEuclideanLin A).range

The rank of a matrix is the dimension of the range of the linear map it induces on Euclidean space.

source

theorem Matrix.rank_coe_toEuclideanCLM {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι 𝕜) :

(↑(toEuclideanCLM A)).rank = ↑A.rank

The Cardinal-valued rank of the continuous linear map of a square matrix is its matrix rank. This is the bridge that turns an operator-rank statement into a matrix-rank one.

source

noncomputable def Matrix.toEuclideanCLE {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι 𝕜) (hA : A.det ≠ 0) :

EuclideanSpace 𝕜 ι ≃L[𝕜] EuclideanSpace 𝕜 ι

The continuous linear equivalence of an invertible matrix on Euclidean space, defined when A.det is a unit. It acts as A does, and its inverse is the map of A⁻¹, so a change of variables along it substitutes A⁻¹.

Equations