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] [CommSemiring R₁] [CommSemiring 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] [CommSemiring R₁] [CommSemiring 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 => R₁) i) 1)) (↑(LinearMap.stdBasis R₂ (fun x => 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] [CommSemiring R₁] [CommSemiring 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

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

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] [CommSemiring R₁] [CommSemiring 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} [CommRing R] [CommRing R₁] [CommRing 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 => ↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j => ↑(LinearMap.stdBasis R₂ (fun x => 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} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : Matrix n m R) :

↑(LinearMap.toMatrix₂Aux (fun i => ↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j => ↑(LinearMap.stdBasis R₂ (fun x => 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} [CommRing R] [CommRing R₁] [CommRing 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} [CommRing 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} [CommRing R] [CommRing R₁] [CommRing 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ₛₗ₂' σ₁ σ₂ = LinearEquiv.symm LinearMap.toMatrixₛₗ₂'

Instances For

source

def Matrix.toLinearMap₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing 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₂' = LinearEquiv.symm LinearMap.toMatrix₂'

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} [CommRing R] [CommRing R₁] [CommRing 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} [CommRing R] [CommRing R₁] [CommRing 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.sum Finset.univ fun i => Finset.sum Finset.univ fun j => ↑σ₁ (x i) * M i j * ↑σ₂ (y j)

source

theorem Matrix.toLinearMap₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing 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.sum Finset.univ fun i => Finset.sum Finset.univ fun j => x i * M i j * y j

source

theorem Matrix.toLinearMap₂'_apply' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing 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 (Matrix.mulVec M 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} [CommRing R] [CommRing R₁] [CommRing 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 => R₁) i) 1)) (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = M i j

source

@[simp]

theorem Matrix.toLinearMap₂'_stdBasis {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing 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 => R) i) 1)) (↑(LinearMap.stdBasis R (fun x => 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} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :

LinearEquiv.symm LinearMap.toMatrixₛₗ₂' = 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} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :

LinearEquiv.symm (Matrix.toLinearMapₛₗ₂' σ₁ σ₂) = 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} [CommRing R] [CommRing R₁] [CommRing 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} [CommRing 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} [CommRing R] [CommRing R₁] [CommRing 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} [CommRing 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} [CommRing R] [CommRing R₁] [CommRing 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 => R₁) i) 1)) (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1)

source

@[simp]

theorem LinearMap.toMatrix₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing 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 => R) i) 1)) (↑(LinearMap.stdBasis R (fun x => 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} [CommRing 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₂' (LinearMap.compl₁₂ B l r) = Matrix.transpose (↑LinearMap.toMatrix' l) * ↑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} [CommRing 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₂' (LinearMap.comp B f) = Matrix.transpose (↑LinearMap.toMatrix' f) * ↑LinearMap.toMatrix₂' B

source

theorem LinearMap.toMatrix₂'_compl₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommRing 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₂' (LinearMap.compl₂ B 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} [CommRing 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₂' (LinearMap.compl₁₂ B (↑Matrix.toLin' (Matrix.transpose M)) (↑Matrix.toLin' N))

source

theorem LinearMap.mul_toMatrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [CommRing 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₂' (LinearMap.comp B (↑Matrix.toLin' (Matrix.transpose M)))

source

theorem LinearMap.toMatrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommRing 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₂' (LinearMap.compl₂ B (↑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} [CommRing 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) :

LinearMap.compl₁₂ (↑Matrix.toLinearMap₂' M) (↑Matrix.toLin' P) (↑Matrix.toLin' Q) = ↑Matrix.toLinearMap₂' (Matrix.transpose P * 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} [CommRing 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₂ = LinearEquiv.trans (LinearEquiv.arrowCongr (Basis.equivFun b₁) (LinearEquiv.arrowCongr (Basis.equivFun b₂) (LinearEquiv.refl R R))) 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} [CommRing 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₂ = LinearEquiv.symm (LinearMap.toMatrix₂ b₁ b₂)

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} [CommRing 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} [CommRing 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.sum Finset.univ fun i => Finset.sum Finset.univ fun j => ↑(↑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} [CommRing 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} [CommRing 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₂) :

LinearEquiv.symm (LinearMap.toMatrix₂ b₁ b₂) = 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} [CommRing 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₂) :

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

source

theorem Matrix.toLinearMap₂_basisFun {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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₂') (LinearMap.compl₁₂ B l r) = Matrix.transpose (↑(LinearMap.toMatrix b₁' b₁) l) * ↑(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} [CommRing 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₂) (LinearMap.comp B f) = Matrix.transpose (↑(LinearMap.toMatrix b₁' b₁) f) * ↑(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} [CommRing 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₂') (LinearMap.compl₂ B 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} [CommRing 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) :

Matrix.transpose (Basis.toMatrix b₁ ↑c₁) * ↑(LinearMap.toMatrix₂ b₁ b₂) B * Basis.toMatrix b₂ ↑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} [CommRing 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₂') (LinearMap.compl₁₂ B (↑(Matrix.toLin b₁' b₁) (Matrix.transpose M)) (↑(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} [CommRing 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₂) (LinearMap.comp B (↑(Matrix.toLin b₁' b₁) (Matrix.transpose M)))

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} [CommRing 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₂') (LinearMap.compl₂ B (↑(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} [CommRing 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) :

LinearMap.compl₁₂ (↑(Matrix.toLinearMap₂ b₁ b₂) M) (↑(Matrix.toLin b₁' b₁) P) (↑(Matrix.toLin b₂' b₂) Q) = ↑(Matrix.toLinearMap₂ b₁' b₂') (Matrix.transpose P * 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

Matrix.IsAdjointPair J J' A A' = (Matrix.transpose A * 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

Matrix.IsSelfAdjoint J A₁ = Matrix.IsAdjointPair J 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

Matrix.IsSkewAdjoint J A₁ = Matrix.IsAdjointPair J 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'] :

LinearMap.IsAdjointPair (↑Matrix.toLinearMap₂' J) (↑Matrix.toLinearMap₂' J') (↑Matrix.toLin' A) (↑Matrix.toLin' A') ↔ Matrix.IsAdjointPair J 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'] :

LinearMap.IsAdjointPair (↑(Matrix.toLinearMap₂ b₁ b₁) J) (↑(Matrix.toLinearMap₂ b₂ b₂) J') (↑(Matrix.toLin b₁ b₂) A) (↑(Matrix.toLin b₂ b₁) A') ↔ Matrix.IsAdjointPair J 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) [DecidableEq n] (P : Matrix n n R) (h : IsUnit P) :

Matrix.IsAdjointPair (Matrix.transpose P * J * P) (Matrix.transpose P * J * P) A₁ A₁ ↔ Matrix.IsAdjointPair J 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') (LinearMap.isPairSelfAdjointSubmodule (↑Matrix.toLinearMap₂' J) (↑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₂ ↔ Matrix.IsAdjointPair J 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 ↔ Matrix.IsSelfAdjoint J 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 ↔ Matrix.IsSkewAdjoint J 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₁) :

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

source

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

LinearMap.SeparatingLeft (↑Matrix.toLinearMap₂' M)

source

@[simp]

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

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

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 : Matrix.Nondegenerate M) (b : Basis ι R₁ M₁) :

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

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₁) :

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

source

@[simp]

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

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

source

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

Matrix.Nondegenerate (↑LinearMap.toMatrix₂' B)

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₁) :

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

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 : LinearMap.SeparatingLeft B) (b : Basis ι R₁ M₁) :

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

source

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

LinearMap.SeparatingLeft (↑Matrix.toLinearMap₂' M) ↔ Matrix.det M ≠ 0

source

theorem LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] [IsDomain R₁] (M : Matrix ι ι R₁) (h : Matrix.det M ≠ 0) :

LinearMap.SeparatingLeft (↑Matrix.toLinearMap₂' M)

source

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

LinearMap.SeparatingLeft B ↔ Matrix.det (↑(LinearMap.toMatrix₂ b b) B) ≠ 0

source

theorem LinearMap.separatingLeft_of_det_ne_zero {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] [IsDomain R₁] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) (h : Matrix.det (↑(LinearMap.toMatrix₂ b b) B) ≠ 0) :

LinearMap.SeparatingLeft B

Sesquilinear form #

Main definitions #

Todos #

Tags #

Bilinear forms over n → R #

Bilinear forms over arbitrary vector spaces #

Adjoint pairs #

Nondegenerate bilinear forms #

Bilinear forms over `n → R` #