# 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

def Matrix.toLinearMap₂'Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [] [Semiring R₁] [Semiring R₂] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (f : Matrix n m R) :
(nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] 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
• = LinearMap.mk₂'ₛₗ σ₁ σ₂ (fun (v : nR₁) (w : mR₂) => i : n, j : m, σ₁ (v i) * f i j * σ₂ (w j))
Instances For
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} [] [Semiring R₁] [Semiring R₂] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) [] [] (f : Matrix n m R) (i : n) (j : m) :
(() ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) = f i j
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} [] [Semiring R₁] [Semiring R₂] [] [Module R₁ M₁] [] [Module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (b₁ : nM₁) (b₂ : mM₂) :
(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
• = { toFun := fun (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) => Matrix.of fun (i : n) (j : m) => (f (b₁ i)) (b₂ j), map_add' := , map_smul' := }
Instances For
@[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} [] [Semiring R₁] [Semiring R₂] [] [Module R₁ M₁] [] [Module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) (b₁ : nM₁) (b₂ : mM₂) (i : n) (j : m) :
() f i j = (f (b₁ i)) (b₂ j)
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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] 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
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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] {σ₁ : 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) () = f

### Bilinear forms over n → R#

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

def LinearMap.toMatrixₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [] [Semiring R₁] [Semiring R₂] [] [] [] [] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} :
((nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] 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
def LinearMap.toMatrix₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] :
((nR) →ₗ[R] (mR) →ₗ[R] R) ≃ₗ[R] Matrix n m R

The linear equivalence between bilinear forms and n × m matrices

Equations
• LinearMap.toMatrix₂' = LinearMap.toMatrixₛₗ₂'
Instances For
def Matrix.toLinearMapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
Matrix n m R ≃ₗ[R] (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R

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

Equations
• = LinearMap.toMatrixₛₗ₂'.symm
Instances For
def Matrix.toLinearMap₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] :
Matrix n m R ≃ₗ[R] (nR) →ₗ[R] (mR) →ₗ[R] R

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

Equations
• Matrix.toLinearMap₂' = LinearMap.toMatrix₂'.symm
Instances For
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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) :
= () M
theorem Matrix.toLinearMapₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) (x : nR₁) (y : mR₂) :
((() M) x) y = i : n, j : m, σ₁ (x i) * M i j * σ₂ (y j)
theorem Matrix.toLinearMap₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] (M : Matrix n m R) (x : nR) (y : mR) :
((Matrix.toLinearMap₂' M) x) y = i : n, j : m, x i * M i j * y j
theorem Matrix.toLinearMap₂'_apply' {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] (M : Matrix n m R) (v : nR) (w : mR) :
((Matrix.toLinearMap₂' M) v) w = Matrix.dotProduct v (M.mulVec w)
@[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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) (i : n) (j : m) :
((() M) ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) = M i j
@[simp]
theorem Matrix.toLinearMap₂'_stdBasis {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] (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
@[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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
LinearMap.toMatrixₛₗ₂'.symm =
@[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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
().symm = LinearMap.toMatrixₛₗ₂'
@[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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R) :
() (LinearMap.toMatrixₛₗ₂' B) = B
@[simp]
theorem Matrix.toLinearMap₂'_toMatrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) :
Matrix.toLinearMap₂' (LinearMap.toMatrix₂' B) = B
@[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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) :
LinearMap.toMatrixₛₗ₂' (() M) = M
@[simp]
theorem LinearMap.toMatrix'_toLinearMap₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] (M : Matrix n m R) :
LinearMap.toMatrix₂' (Matrix.toLinearMap₂' M) = M
@[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} [] [Semiring R₁] [Semiring R₂] [] [] [] [] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] 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)
@[simp]
theorem LinearMap.toMatrix₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] (B : (nR) →ₗ[R] (mR) →ₗ[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)
@[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} [] [] [] [] [] [Fintype n'] [Fintype m'] [] [] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (l : (n'R) →ₗ[R] nR) (r : (m'R) →ₗ[R] mR) :
LinearMap.toMatrix₂' (B.compl₁₂ l r) = (LinearMap.toMatrix' l).transpose * LinearMap.toMatrix₂' B * LinearMap.toMatrix' r
theorem LinearMap.toMatrix₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [] [] [] [] [] [Fintype n'] [] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (f : (n'R) →ₗ[R] nR) :
LinearMap.toMatrix₂' (B ∘ₗ f) = (LinearMap.toMatrix' f).transpose * LinearMap.toMatrix₂' B
theorem LinearMap.toMatrix₂'_compl₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [] [] [] [] [] [Fintype m'] [] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (f : (m'R) →ₗ[R] mR) :
LinearMap.toMatrix₂' (B.compl₂ f) = LinearMap.toMatrix₂' B * LinearMap.toMatrix' f
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} [] [] [] [] [] [Fintype n'] [Fintype m'] [] [] (B : (nR) →ₗ[R] (mR) →ₗ[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))
theorem LinearMap.mul_toMatrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [] [] [] [] [] [Fintype n'] [] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (M : Matrix n' n R) :
M * LinearMap.toMatrix₂' B = LinearMap.toMatrix₂' (B ∘ₗ Matrix.toLin' M.transpose)
theorem LinearMap.toMatrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [] [] [] [] [] [Fintype m'] [] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (M : Matrix m m' R) :
LinearMap.toMatrix₂' B * M = LinearMap.toMatrix₂' (B.compl₂ (Matrix.toLin' M))
theorem Matrix.toLinearMap₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [] [] [] [] [] [Fintype n'] [Fintype 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.

noncomputable def LinearMap.toMatrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [] [] [Module R M₁] [] [Module R 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
• = (b₁.equivFun.arrowCongr (b₂.equivFun.arrowCongr ())).trans LinearMap.toMatrix₂'
Instances For
noncomputable def Matrix.toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [] [] [Module R M₁] [] [Module R 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
• = ().symm
Instances For
@[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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (i : n) (j : m) :
() B i j = (B (b₁ i)) (b₂ j)
@[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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m R) (x : M₁) (y : M₂) :
((() M) x) y = i : n, j : m, (b₁.repr x) i * M i j * (b₂.repr y) j
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
(LinearMap.toMatrix₂Aux b₁ b₂) B = () B
@[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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
().symm =
@[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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
().symm =
theorem Matrix.toLinearMap₂_basisFun {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] :
Matrix.toLinearMap₂ () () = Matrix.toLinearMap₂'
theorem LinearMap.toMatrix₂_basisFun {R : Type u_1} {n : Type u_9} {m : Type u_10} [] [] [] [] [] :
LinearMap.toMatrix₂ () () = LinearMap.toMatrix₂'
@[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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
() (() B) = B
@[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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m R) :
() (() M) = M
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [] [Module R M₁'] [] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype 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 * () B * (LinearMap.toMatrix b₂' b₂) r
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [] [Module R M₁'] (b₁' : Basis n' R M₁') [Fintype n'] [] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₁' →ₗ[R] M₁) :
(LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((LinearMap.toMatrix b₁' b₁) f).transpose * () B
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [] [Module R M₂'] (b₂' : Basis m' R M₂') [Fintype m'] [] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₂' →ₗ[R] M₂) :
(LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ f) = () B * (LinearMap.toMatrix b₂' b₂) f
@[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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [Fintype n'] [Fintype m'] [] [] (c₁ : Basis n' R M₁) (c₂ : Basis m' R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
(b₁.toMatrix c₁).transpose * () B * b₂.toMatrix c₂ = () B
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [] [Module R M₁'] [] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [] [] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R) :
M * () B * N = (LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ ((Matrix.toLin b₁' b₁) M.transpose) ((Matrix.toLin b₂' b₂) N))
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [] [Module R M₁'] (b₁' : Basis n' R M₁') [Fintype n'] [] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) :
M * () B = (LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ (Matrix.toLin b₁' b₁) M.transpose)
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [] [Module R M₂'] (b₂' : Basis m' R M₂') [Fintype m'] [] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix m m' R) :
() B * M = (LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ ((Matrix.toLin b₂' b₂) M))
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} [] [] [Module R M₁] [] [Module R M₂] [] [] [] [] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [] [Module R M₁'] [] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [] [] (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :
(() M).compl₁₂ ((Matrix.toLin b₁' b₁) P) ((Matrix.toLin b₂' b₂) Q) = (Matrix.toLinearMap₂ b₁' b₂') (P.transpose * M * Q)

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

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
def Matrix.IsSelfAdjoint {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) (A₁ : Matrix n n R) :

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

Equations
Instances For
def Matrix.IsSkewAdjoint {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) (A₁ : Matrix n n R) :

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

Equations
Instances For
@[simp]
theorem isAdjointPair_toLinearMap₂' {R : Type u_1} {n : Type u_9} {n' : Type u_11} [] [] [Fintype n'] (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) [] [] :
(Matrix.toLinearMap₂' J).IsAdjointPair (Matrix.toLinearMap₂' J') (Matrix.toLin' A) (Matrix.toLin' A') J.IsAdjointPair J' A A'
@[simp]
theorem isAdjointPair_toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {n' : Type u_11} [] [] [Module R M₁] [] [Module R M₂] [] [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) [] [] :
(() J).IsAdjointPair (() J') ((Matrix.toLin b₁ b₂) A) ((Matrix.toLin b₂ b₁) A') J.IsAdjointPair J' A A'
theorem Matrix.isAdjointPair_equiv {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) (A₁ : Matrix n n R) (A₂ : Matrix n n R) [] (P : Matrix n n R) (h : ) :
(P.transpose * J * P).IsAdjointPair (P.transpose * J * P) A₁ A₂ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
def pairSelfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) (J₂ : Matrix n n R) [] :
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
• = Submodule.map (LinearMap.toMatrix') ((Matrix.toLinearMap₂' J).isPairSelfAdjointSubmodule (Matrix.toLinearMap₂' J₂))
Instances For
@[simp]
theorem mem_pairSelfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) (J₂ : Matrix n n R) (A₁ : Matrix n n R) [] :
def selfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) [] :
Submodule R (Matrix n n R)

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

Equations
Instances For
@[simp]
theorem mem_selfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) (A₁ : Matrix n n R) [] :
def skewAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) [] :
Submodule R (Matrix n n R)

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

Equations
Instances For
@[simp]
theorem mem_skewAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [] [] (J : Matrix n n R) (A₁ : Matrix n n R) [] :

### Nondegenerate bilinear forms #

theorem Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [] [Module R₁ M₁] [] [] {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :
(Matrix.toLinearMap₂' M).SeparatingLeft (() M).SeparatingLeft
theorem Matrix.Nondegenerate.toLinearMap₂' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [] [] {M : Matrix ι ι R₁} (h : M.Nondegenerate) :
(Matrix.toLinearMap₂' M).SeparatingLeft
@[simp]
theorem Matrix.separatingLeft_toLinearMap₂'_iff {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [] [] {M : Matrix ι ι R₁} :
(Matrix.toLinearMap₂' M).SeparatingLeft M.Nondegenerate
theorem Matrix.Nondegenerate.toLinearMap₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [] [Module R₁ M₁] [] [] {M : Matrix ι ι R₁} (h : M.Nondegenerate) (b : Basis ι R₁ M₁) :
(() M).SeparatingLeft
@[simp]
theorem Matrix.separatingLeft_toLinearMap₂_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [] [Module R₁ M₁] [] [] {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :
(() M).SeparatingLeft M.Nondegenerate
@[simp]
theorem LinearMap.nondegenerate_toMatrix₂'_iff {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [] [] {B : (ιR₁) →ₗ[R₁] (ιR₁) →ₗ[R₁] R₁} :
(LinearMap.toMatrix₂' B).Nondegenerate B.SeparatingLeft
theorem LinearMap.SeparatingLeft.toMatrix₂' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [] [] {B : (ιR₁) →ₗ[R₁] (ιR₁) →ₗ[R₁] R₁} (h : B.SeparatingLeft) :
(LinearMap.toMatrix₂' B).Nondegenerate
@[simp]
theorem LinearMap.nondegenerate_toMatrix_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [] [Module R₁ M₁] [] [] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) :
(() B).Nondegenerate B.SeparatingLeft
theorem LinearMap.SeparatingLeft.toMatrix₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [] [Module R₁ M₁] [] [] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (h : B.SeparatingLeft) (b : Basis ι R₁ M₁) :
(() B).Nondegenerate
theorem LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [] [] [IsDomain R₁] {M : Matrix ι ι R₁} :
(Matrix.toLinearMap₂' M).SeparatingLeft M.det 0
theorem LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [] [] [IsDomain R₁] (M : Matrix ι ι R₁) (h : M.det 0) :
(Matrix.toLinearMap₂' M).SeparatingLeft
theorem LinearMap.separatingLeft_iff_det_ne_zero {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [] [Module R₁ M₁] [] [] [IsDomain R₁] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) :
B.SeparatingLeft (() B).det 0
theorem LinearMap.separatingLeft_of_det_ne_zero {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [] [Module R₁ M₁] [] [] [IsDomain R₁] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) (h : (() B).det 0) :
B.SeparatingLeft