Sesquilinear form #

This file defines the conversion between sesquilinear forms and matrices.

Main definitions #

Matrix.toLinearMap₂ given a basis define a bilinear form
Matrix.toLinearMap₂' define the bilinear form on n → R
LinearMap.toMatrix₂: calculate the matrix coefficients of a bilinear form
LinearMap.toMatrix₂': calculate the matrix coefficients of a bilinear form on n → R

Todos #

At the moment this is quite a literal port from Matrix.BilinearForm. Everything should be generalized to fully semibilinear forms.

Tags #

sesquilinear_form, matrix, basis

source

def Matrix.toLinearMap₂'Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (f : Matrix n m R) :

(n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R

The map from Matrix n n R to bilinear forms on n → R.

This is an auxiliary definition for the equivalence Matrix.toLinearMap₂'.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Matrix.toLinearMap₂'Aux_stdBasis {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) [DecidableEq n] [DecidableEq m] (f : Matrix n m R) (i : n) (j : m) :

((Matrix.toLinearMap₂'Aux σ₁ σ₂ f) ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) = f i j

source

def LinearMap.toMatrix₂Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (b₁ : n → M₁) (b₂ : m → M₂) :

(M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) →ₗ[R] Matrix n m R

The linear map from sesquilinear forms to Matrix n m R given an n-indexed basis for M₁ and an m-indexed basis for M₂.

This is an auxiliary definition for the equivalence Matrix.toLinearMapₛₗ₂'.

Equations

LinearMap.toMatrix₂Aux b₁ b₂ = { toFun := fun (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) => Matrix.of fun (i : n) (j : m) => (f (b₁ i)) (b₂ j), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.toMatrix₂Aux_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) (b₁ : n → M₁) (b₂ : m → M₂) (i : n) (j : m) :

(LinearMap.toMatrix₂Aux b₁ b₂) f i j = (f (b₁ i)) (b₂ j)

source

theorem LinearMap.toLinearMap₂'Aux_toMatrix₂Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R) :

Matrix.toLinearMap₂'Aux σ₁ σ₂ ((LinearMap.toMatrix₂Aux (fun (i : n) => (LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1) fun (j : m) => (LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) f) = f

source

theorem Matrix.toMatrix₂Aux_toLinearMap₂'Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : Matrix n m R) :

(LinearMap.toMatrix₂Aux (fun (i : n) => (LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1) fun (j : m) => (LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) (Matrix.toLinearMap₂'Aux σ₁ σ₂ f) = f

Bilinear forms over `n → R` #

This section deals with the conversion between matrices and sesquilinear forms on n → R.

source

def LinearMap.toMatrixₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} :

((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R) ≃ₗ[R] Matrix n m R

The linear equivalence between sesquilinear forms and n × m matrices

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def LinearMap.toMatrix₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :

((n → R) →ₗ[R] (m → R) →ₗ[R] R) ≃ₗ[R] Matrix n m R

The linear equivalence between bilinear forms and n × m matrices

Equations

LinearMap.toMatrix₂' = LinearMap.toMatrixₛₗ₂'

Instances For

source

def Matrix.toLinearMapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :

Matrix n m R ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R

The linear equivalence between n × n matrices and sesquilinear forms on n → R

Equations

Matrix.toLinearMapₛₗ₂' σ₁ σ₂ = LinearMap.toMatrixₛₗ₂'.symm

Instances For

source

def Matrix.toLinearMap₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :

Matrix n m R ≃ₗ[R] (n → R) →ₗ[R] (m → R) →ₗ[R] R

The linear equivalence between n × n matrices and bilinear forms on n → R

Equations

Matrix.toLinearMap₂' = LinearMap.toMatrix₂'.symm

Instances For

source

theorem Matrix.toLinearMapₛₗ₂'_aux_eq {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) :

Matrix.toLinearMap₂'Aux σ₁ σ₂ M = (Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M

source

theorem Matrix.toLinearMapₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) (x : n → R₁) (y : m → R₂) :

(((Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M) x) y = Finset.univ.sum fun (i : n) => Finset.univ.sum fun (j : m) => σ₁ (x i) * M i j * σ₂ (y j)

source

theorem Matrix.toLinearMap₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) (x : n → R) (y : m → R) :

((Matrix.toLinearMap₂' M) x) y = Finset.univ.sum fun (i : n) => Finset.univ.sum fun (j : m) => x i * M i j * y j

source

theorem Matrix.toLinearMap₂'_apply' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) (v : n → R) (w : m → R) :

((Matrix.toLinearMap₂' M) v) w = Matrix.dotProduct v (M.mulVec w)

source

@[simp]

theorem Matrix.toLinearMapₛₗ₂'_stdBasis {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) (i : n) (j : m) :

(((Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M) ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) = M i j

source

@[simp]

theorem Matrix.toLinearMap₂'_stdBasis {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) (i : n) (j : m) :

((Matrix.toLinearMap₂' M) ((LinearMap.stdBasis R (fun (x : n) => R) i) 1)) ((LinearMap.stdBasis R (fun (x : m) => R) j) 1) = M i j

source

@[simp]

theorem LinearMap.toMatrixₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :

LinearMap.toMatrixₛₗ₂'.symm = Matrix.toLinearMapₛₗ₂' σ₁ σ₂

source

@[simp]

theorem Matrix.toLinearMapₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :

(Matrix.toLinearMapₛₗ₂' σ₁ σ₂).symm = LinearMap.toMatrixₛₗ₂'

source

@[simp]

theorem Matrix.toLinearMapₛₗ₂'_toMatrix' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R) :

(Matrix.toLinearMapₛₗ₂' σ₁ σ₂) (LinearMap.toMatrixₛₗ₂' B) = B

source

@[simp]

theorem Matrix.toLinearMap₂'_toMatrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) :

Matrix.toLinearMap₂' (LinearMap.toMatrix₂' B) = B

source

@[simp]

theorem LinearMap.toMatrix'_toLinearMapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) :

LinearMap.toMatrixₛₗ₂' ((Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M) = M

source

@[simp]

theorem LinearMap.toMatrix'_toLinearMap₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) :

LinearMap.toMatrix₂' (Matrix.toLinearMap₂' M) = M

source

@[simp]

theorem LinearMap.toMatrixₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Semiring R₁] [Semiring R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R) (i : n) (j : m) :

LinearMap.toMatrixₛₗ₂' B i j = (B ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1)

source

@[simp]

theorem LinearMap.toMatrix₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (i : n) (j : m) :

LinearMap.toMatrix₂' B i j = (B ((LinearMap.stdBasis R (fun (x : n) => R) i) 1)) ((LinearMap.stdBasis R (fun (x : m) => R) j) 1)

source

@[simp]

theorem LinearMap.toMatrix₂'_compl₁₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (l : (n' → R) →ₗ[R] n → R) (r : (m' → R) →ₗ[R] m → R) :

LinearMap.toMatrix₂' (B.compl₁₂ l r) = (LinearMap.toMatrix' l).transpose * LinearMap.toMatrix₂' B * LinearMap.toMatrix' r

source

theorem LinearMap.toMatrix₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [DecidableEq n'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (f : (n' → R) →ₗ[R] n → R) :

LinearMap.toMatrix₂' (B ∘ₗ f) = (LinearMap.toMatrix' f).transpose * LinearMap.toMatrix₂' B

source

theorem LinearMap.toMatrix₂'_compl₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype m'] [DecidableEq m'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (f : (m' → R) →ₗ[R] m → R) :

LinearMap.toMatrix₂' (B.compl₂ f) = LinearMap.toMatrix₂' B * LinearMap.toMatrix' f

source

theorem LinearMap.mul_toMatrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R) :

M * LinearMap.toMatrix₂' B * N = LinearMap.toMatrix₂' (B.compl₁₂ (Matrix.toLin' M.transpose) (Matrix.toLin' N))

source

theorem LinearMap.mul_toMatrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [DecidableEq n'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix n' n R) :

M * LinearMap.toMatrix₂' B = LinearMap.toMatrix₂' (B ∘ₗ Matrix.toLin' M.transpose)

source

theorem LinearMap.toMatrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype m'] [DecidableEq m'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix m m' R) :

LinearMap.toMatrix₂' B * M = LinearMap.toMatrix₂' (B.compl₂ (Matrix.toLin' M))

source

theorem Matrix.toLinearMap₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :

(Matrix.toLinearMap₂' M).compl₁₂ (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toLinearMap₂' (P.transpose * M * Q)

Bilinear forms over arbitrary vector spaces #

This section deals with the conversion between matrices and bilinear forms on a module with a fixed basis.

source

noncomputable def LinearMap.toMatrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :

(M₁ →ₗ[R] M₂ →ₗ[R] R) ≃ₗ[R] Matrix n m R

LinearMap.toMatrix₂ b₁ b₂ is the equivalence between R-bilinear forms on M and n-by-m matrices with entries in R, if b₁ and b₂ are R-bases for M₁ and M₂, respectively.

Equations

LinearMap.toMatrix₂ b₁ b₂ = (b₁.equivFun.arrowCongr (b₂.equivFun.arrowCongr (LinearEquiv.refl R R))).trans LinearMap.toMatrix₂'

Instances For

source

noncomputable def Matrix.toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :

Matrix n m R ≃ₗ[R] M₁ →ₗ[R] M₂ →ₗ[R] R

Matrix.toLinearMap₂ b₁ b₂ is the equivalence between R-bilinear forms on M and n-by-m matrices with entries in R, if b₁ and b₂ are R-bases for M₁ and M₂, respectively; this is the reverse direction of LinearMap.toMatrix₂ b₁ b₂.

Equations

Matrix.toLinearMap₂ b₁ b₂ = (LinearMap.toMatrix₂ b₁ b₂).symm

Instances For

source

@[simp]

theorem LinearMap.toMatrix₂_apply {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (i : n) (j : m) :

(LinearMap.toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)

source

@[simp]

theorem Matrix.toLinearMap₂_apply {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m R) (x : M₁) (y : M₂) :

(((Matrix.toLinearMap₂ b₁ b₂) M) x) y = Finset.univ.sum fun (i : n) => Finset.univ.sum fun (j : m) => (b₁.repr x) i * M i j * (b₂.repr y) j

source

theorem LinearMap.toMatrix₂Aux_eq {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :

(LinearMap.toMatrix₂Aux ⇑b₁ ⇑b₂) B = (LinearMap.toMatrix₂ b₁ b₂) B

source

@[simp]

theorem LinearMap.toMatrix₂_symm {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :

(LinearMap.toMatrix₂ b₁ b₂).symm = Matrix.toLinearMap₂ b₁ b₂

source

@[simp]

theorem Matrix.toLinearMap₂_symm {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :

(Matrix.toLinearMap₂ b₁ b₂).symm = LinearMap.toMatrix₂ b₁ b₂

source

theorem Matrix.toLinearMap₂_basisFun {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] :

Matrix.toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLinearMap₂'

source

theorem LinearMap.toMatrix₂_basisFun {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommSemiring R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] :

LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = LinearMap.toMatrix₂'

source

@[simp]

theorem Matrix.toLinearMap₂_toMatrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :

(Matrix.toLinearMap₂ b₁ b₂) ((LinearMap.toMatrix₂ b₁ b₂) B) = B

source

@[simp]

theorem LinearMap.toMatrix₂_toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m R) :

(LinearMap.toMatrix₂ b₁ b₂) ((Matrix.toLinearMap₂ b₁ b₂) M) = M

source

theorem LinearMap.toMatrix₂_compl₁₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] [AddCommMonoid M₂'] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (l : M₁' →ₗ[R] M₁) (r : M₂' →ₗ[R] M₂) :

(LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ l r) = ((LinearMap.toMatrix b₁' b₁) l).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) r

source

theorem LinearMap.toMatrix₂_comp {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] (b₁' : Basis n' R M₁') [Fintype n'] [DecidableEq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₁' →ₗ[R] M₁) :

(LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((LinearMap.toMatrix b₁' b₁) f).transpose * (LinearMap.toMatrix₂ b₁ b₂) B

source

theorem LinearMap.toMatrix₂_compl₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₂'] [Module R M₂'] (b₂' : Basis m' R M₂') [Fintype m'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₂' →ₗ[R] M₂) :

(LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ f) = (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) f

source

@[simp]

theorem LinearMap.toMatrix₂_mul_basis_toMatrix {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (c₁ : Basis n' R M₁) (c₂ : Basis m' R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :

(b₁.toMatrix ⇑c₁).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (LinearMap.toMatrix₂ c₁ c₂) B

source

theorem LinearMap.mul_toMatrix₂_mul {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] [AddCommMonoid M₂'] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R) :

M * (LinearMap.toMatrix₂ b₁ b₂) B * N = (LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ ((Matrix.toLin b₁' b₁) M.transpose) ((Matrix.toLin b₂' b₂) N))

source

theorem LinearMap.mul_toMatrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] (b₁' : Basis n' R M₁') [Fintype n'] [DecidableEq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) :

M * (LinearMap.toMatrix₂ b₁ b₂) B = (LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ (Matrix.toLin b₁' b₁) M.transpose)

source

theorem LinearMap.toMatrix₂_mul {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₂'] [Module R M₂'] (b₂' : Basis m' R M₂') [Fintype m'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix m m' R) :

(LinearMap.toMatrix₂ b₁ b₂) B * M = (LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ ((Matrix.toLin b₂' b₂) M))

source

theorem Matrix.toLinearMap₂_compl₁₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] [AddCommMonoid M₂'] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :

((Matrix.toLinearMap₂ b₁ b₂) M).compl₁₂ ((Matrix.toLin b₁' b₁) P) ((Matrix.toLin b₂' b₂) Q) = (Matrix.toLinearMap₂ b₁' b₂') (P.transpose * M * Q)

Adjoint pairs #

source

def Matrix.IsAdjointPair {R : Type u_1} {n : Type u_9} {n' : Type u_11} [CommRing R] [Fintype n] [Fintype n'] (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) :

Prop

The condition for the matrices A, A' to be an adjoint pair with respect to the square matrices J, J₃.

Equations

J.IsAdjointPair J' A A' = (A.transpose * J' = J * A')

Instances For

source

def Matrix.IsSelfAdjoint {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) :

Prop

The condition for a square matrix A to be self-adjoint with respect to the square matrix J.

Equations

J.IsSelfAdjoint A₁ = J.IsAdjointPair J A₁ A₁

Instances For

source

def Matrix.IsSkewAdjoint {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) :

Prop

The condition for a square matrix A to be skew-adjoint with respect to the square matrix J.

Equations

J.IsSkewAdjoint A₁ = J.IsAdjointPair J A₁ (-A₁)

Instances For

source

@[simp]

theorem isAdjointPair_toLinearMap₂' {R : Type u_1} {n : Type u_9} {n' : Type u_11} [CommRing R] [Fintype n] [Fintype n'] (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) [DecidableEq n] [DecidableEq n'] :

(Matrix.toLinearMap₂' J).IsAdjointPair (Matrix.toLinearMap₂' J') (Matrix.toLin' A) (Matrix.toLin' A') ↔ J.IsAdjointPair J' A A'

source

@[simp]

theorem isAdjointPair_toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {n' : Type u_11} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Fintype n] [Fintype n'] (b₁ : Basis n R M₁) (b₂ : Basis n' R M₂) (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) [DecidableEq n] [DecidableEq n'] :

((Matrix.toLinearMap₂ b₁ b₁) J).IsAdjointPair ((Matrix.toLinearMap₂ b₂ b₂) J') ((Matrix.toLin b₁ b₂) A) ((Matrix.toLin b₂ b₁) A') ↔ J.IsAdjointPair J' A A'

source

theorem Matrix.isAdjointPair_equiv {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) (A₂ : Matrix n n R) [DecidableEq n] (P : Matrix n n R) (h : IsUnit P) :

(P.transpose * J * P).IsAdjointPair (P.transpose * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

source

def pairSelfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (J₂ : Matrix n n R) [DecidableEq n] :

Submodule R (Matrix n n R)

The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to given matrices J, J₂.

Equations

pairSelfAdjointMatricesSubmodule J J₂ = Submodule.map (↑LinearMap.toMatrix') ((Matrix.toLinearMap₂' J).isPairSelfAdjointSubmodule (Matrix.toLinearMap₂' J₂))

Instances For

source

@[simp]

theorem mem_pairSelfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (J₂ : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] :

A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁

source

def selfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) [DecidableEq n] :

Submodule R (Matrix n n R)

The submodule of self-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations

selfAdjointMatricesSubmodule J = pairSelfAdjointMatricesSubmodule J J

Instances For

source

@[simp]

theorem mem_selfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] :

A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁

source

def skewAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) [DecidableEq n] :

Submodule R (Matrix n n R)

The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations

skewAdjointMatricesSubmodule J = pairSelfAdjointMatricesSubmodule (-J) J

Instances For

source

@[simp]

theorem mem_skewAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] :

A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁

Nondegenerate bilinear forms #

source

theorem Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :

(Matrix.toLinearMap₂' M).SeparatingLeft ↔ ((Matrix.toLinearMap₂ b b) M).SeparatingLeft

source

theorem Matrix.Nondegenerate.toLinearMap₂' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (h : M.Nondegenerate) :

(Matrix.toLinearMap₂' M).SeparatingLeft

source

@[simp]

theorem Matrix.separatingLeft_toLinearMap₂'_iff {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} :

(Matrix.toLinearMap₂' M).SeparatingLeft ↔ M.Nondegenerate

source

theorem Matrix.Nondegenerate.toLinearMap₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (h : M.Nondegenerate) (b : Basis ι R₁ M₁) :

((Matrix.toLinearMap₂ b b) M).SeparatingLeft

source

@[simp]

theorem Matrix.separatingLeft_toLinearMap₂_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :

((Matrix.toLinearMap₂ b b) M).SeparatingLeft ↔ M.Nondegenerate

source

@[simp]

theorem LinearMap.nondegenerate_toMatrix₂'_iff {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁} :

(LinearMap.toMatrix₂' B).Nondegenerate ↔ B.SeparatingLeft

source

theorem LinearMap.SeparatingLeft.toMatrix₂' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁} (h : B.SeparatingLeft) :

(LinearMap.toMatrix₂' B).Nondegenerate

source

@[simp]

theorem LinearMap.nondegenerate_toMatrix_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) :

((LinearMap.toMatrix₂ b b) B).Nondegenerate ↔ B.SeparatingLeft

source

theorem LinearMap.SeparatingLeft.toMatrix₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (h : B.SeparatingLeft) (b : Basis ι R₁ M₁) :

((LinearMap.toMatrix₂ b b) B).Nondegenerate

source