# Bilinear form #

This file defines the conversion between bilinear forms and matrices.

## Main definitions #

• Matrix.toBilin given a basis define a bilinear form
• Matrix.toBilin' define the bilinear form on n → R
• BilinForm.toMatrix: calculate the matrix coefficients of a bilinear form
• BilinForm.toMatrix': calculate the matrix coefficients of a bilinear form on n → R

## Notations #

In this file we use the following type variables:

• M, M', ... are modules over the commutative semiring R,
• M₁, M₁', ... are modules over the commutative ring R₁,
• M₂, M₂', ... are modules over the commutative semiring R₂,
• M₃, M₃', ... are modules over the commutative ring R₃,
• V, ... is a vector space over the field K.

## Tags #

bilinear form, bilin form, BilinearForm, matrix, basis

def Matrix.toBilin'Aux {R₂ : Type u_5} [] {n : Type u_11} [] (M : Matrix n n R₂) :
LinearMap.BilinForm R₂ (nR₂)

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

This is an auxiliary definition for the equivalence Matrix.toBilin'.

Equations
Instances For
theorem Matrix.toBilin'Aux_stdBasis {R₂ : Type u_5} [] {n : Type u_11} [] [] (M : Matrix n n R₂) (i : n) (j : n) :
( ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) = M i j
def BilinForm.toMatrixAux {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} (b : nM₂) :
→ₗ[R₂] Matrix n n R₂

The linear map from bilinear forms to Matrix n n R given an n-indexed basis.

This is an auxiliary definition for the equivalence Matrix.toBilin'.

Equations
Instances For
@[simp]
theorem LinearMap.BilinForm.toMatrixAux_apply {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} (B : ) (b : nM₂) (i : n) (j : n) :
B i j = (B (b i)) (b j)
theorem toBilin'Aux_toMatrixAux {R₂ : Type u_5} [] {n : Type u_11} [] [] (B₂ : LinearMap.BilinForm R₂ (nR₂)) :
Matrix.toBilin'Aux ((BilinForm.toMatrixAux fun (j : n) => (LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) B₂) = B₂

### ToMatrix' section #

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

def LinearMap.BilinForm.toMatrix' {R₂ : Type u_5} [] {n : Type u_11} [] [] :
LinearMap.BilinForm R₂ (nR₂) ≃ₗ[R₂] Matrix n n R₂

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

Equations
• LinearMap.BilinForm.toMatrix' = LinearMap.toMatrix₂'
Instances For
@[simp]
theorem LinearMap.BilinForm.toMatrixAux_stdBasis {R₂ : Type u_5} [] {n : Type u_11} [] [] (B : LinearMap.BilinForm R₂ (nR₂)) :
(BilinForm.toMatrixAux fun (j : n) => (LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) B = LinearMap.BilinForm.toMatrix' B
def Matrix.toBilin' {R₂ : Type u_5} [] {n : Type u_11} [] [] :
Matrix n n R₂ ≃ₗ[R₂] LinearMap.BilinForm R₂ (nR₂)

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

Equations
Instances For
@[simp]
theorem Matrix.toBilin'Aux_eq {R₂ : Type u_5} [] {n : Type u_11} [] [] (M : Matrix n n R₂) :
= Matrix.toBilin' M
theorem Matrix.toBilin'_apply {R₂ : Type u_5} [] {n : Type u_11} [] [] (M : Matrix n n R₂) (x : nR₂) (y : nR₂) :
((Matrix.toBilin' M) x) y = Finset.sum Finset.univ fun (i : n) => Finset.sum Finset.univ fun (j : n) => x i * M i j * y j
theorem Matrix.toBilin'_apply' {R₂ : Type u_5} [] {n : Type u_11} [] [] (M : Matrix n n R₂) (v : nR₂) (w : nR₂) :
((Matrix.toBilin' M) v) w =
@[simp]
theorem Matrix.toBilin'_stdBasis {R₂ : Type u_5} [] {n : Type u_11} [] [] (M : Matrix n n R₂) (i : n) (j : n) :
((Matrix.toBilin' M) ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) = M i j
@[simp]
theorem LinearMap.BilinForm.toMatrix'_symm {R₂ : Type u_5} [] {n : Type u_11} [] [] :
LinearEquiv.symm LinearMap.BilinForm.toMatrix' = Matrix.toBilin'
@[simp]
theorem Matrix.toBilin'_symm {R₂ : Type u_5} [] {n : Type u_11} [] [] :
LinearEquiv.symm Matrix.toBilin' = LinearMap.BilinForm.toMatrix'
@[simp]
theorem Matrix.toBilin'_toMatrix' {R₂ : Type u_5} [] {n : Type u_11} [] [] (B : LinearMap.BilinForm R₂ (nR₂)) :
Matrix.toBilin' (LinearMap.BilinForm.toMatrix' B) = B
@[simp]
theorem LinearMap.BilinForm.toMatrix'_toBilin' {R₂ : Type u_5} [] {n : Type u_11} [] [] (M : Matrix n n R₂) :
LinearMap.BilinForm.toMatrix' (Matrix.toBilin' M) = M
@[simp]
theorem LinearMap.BilinForm.toMatrix'_apply {R₂ : Type u_5} [] {n : Type u_11} [] [] (B : LinearMap.BilinForm R₂ (nR₂)) (i : n) (j : n) :
LinearMap.BilinForm.toMatrix' B i j = (B ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1)
@[simp]
theorem LinearMap.BilinForm.toMatrix'_comp {R₂ : Type u_5} [] {n : Type u_11} {o : Type u_12} [] [] [] [] (B : LinearMap.BilinForm R₂ (nR₂)) (l : (oR₂) →ₗ[R₂] nR₂) (r : (oR₂) →ₗ[R₂] nR₂) :
LinearMap.BilinForm.toMatrix' () = Matrix.transpose (LinearMap.toMatrix' l) * LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' r
theorem LinearMap.BilinForm.toMatrix'_compLeft {R₂ : Type u_5} [] {n : Type u_11} [] [] (B : LinearMap.BilinForm R₂ (nR₂)) (f : (nR₂) →ₗ[R₂] nR₂) :
LinearMap.BilinForm.toMatrix' = Matrix.transpose (LinearMap.toMatrix' f) * LinearMap.BilinForm.toMatrix' B
theorem LinearMap.BilinForm.toMatrix'_compRight {R₂ : Type u_5} [] {n : Type u_11} [] [] (B : LinearMap.BilinForm R₂ (nR₂)) (f : (nR₂) →ₗ[R₂] nR₂) :
LinearMap.BilinForm.toMatrix' = LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' f
theorem LinearMap.BilinForm.mul_toMatrix'_mul {R₂ : Type u_5} [] {n : Type u_11} {o : Type u_12} [] [] [] [] (B : LinearMap.BilinForm R₂ (nR₂)) (M : Matrix o n R₂) (N : Matrix n o R₂) :
M * LinearMap.BilinForm.toMatrix' B * N = LinearMap.BilinForm.toMatrix' (LinearMap.BilinForm.comp B (Matrix.toLin' ()) (Matrix.toLin' N))
theorem LinearMap.BilinForm.mul_toMatrix' {R₂ : Type u_5} [] {n : Type u_11} [] [] (B : LinearMap.BilinForm R₂ (nR₂)) (M : Matrix n n R₂) :
M * LinearMap.BilinForm.toMatrix' B = LinearMap.BilinForm.toMatrix' (LinearMap.BilinForm.compLeft B (Matrix.toLin' ()))
theorem LinearMap.BilinForm.toMatrix'_mul {R₂ : Type u_5} [] {n : Type u_11} [] [] (B : LinearMap.BilinForm R₂ (nR₂)) (M : Matrix n n R₂) :
LinearMap.BilinForm.toMatrix' B * M = LinearMap.BilinForm.toMatrix' (LinearMap.BilinForm.compRight B (Matrix.toLin' M))
theorem Matrix.toBilin'_comp {R₂ : Type u_5} [] {n : Type u_11} {o : Type u_12} [] [] [] [] (M : Matrix n n R₂) (P : Matrix n o R₂) (Q : Matrix n o R₂) :
LinearMap.BilinForm.comp (Matrix.toBilin' M) (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toBilin' ( * Q)

### ToMatrix section #

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

noncomputable def BilinForm.toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) :
≃ₗ[R₂] Matrix n n R₂

BilinForm.toMatrix b is the equivalence between R-bilinear forms on M and n-by-n matrices with entries in R, if b is an R-basis for M.

Equations
Instances For
noncomputable def Matrix.toBilin {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) :
Matrix n n R₂ ≃ₗ[R₂]

BilinForm.toMatrix b is the equivalence between R-bilinear forms on M and n-by-n matrices with entries in R, if b is an R-basis for M.

Equations
Instances For
@[simp]
theorem BilinForm.toMatrix_apply {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (B : ) (i : n) (j : n) :
B i j = (B (b i)) (b j)
@[simp]
theorem Matrix.toBilin_apply {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (M : Matrix n n R₂) (x : M₂) (y : M₂) :
((() M) x) y = Finset.sum Finset.univ fun (i : n) => Finset.sum Finset.univ fun (j : n) => (b.repr x) i * M i j * (b.repr y) j
theorem BilinearForm.toMatrixAux_eq {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (B : ) :
B = B
@[simp]
theorem BilinForm.toMatrix_symm {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) :
@[simp]
theorem Matrix.toBilin_symm {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) :
theorem Matrix.toBilin_basisFun {R₂ : Type u_5} [] {n : Type u_11} [] [] :
Matrix.toBilin (Pi.basisFun R₂ n) = Matrix.toBilin'
theorem BilinForm.toMatrix_basisFun {R₂ : Type u_5} [] {n : Type u_11} [] [] :
= LinearMap.BilinForm.toMatrix'
@[simp]
theorem Matrix.toBilin_toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (B : ) :
() ( B) = B
@[simp]
theorem BilinForm.toMatrix_toBilin {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (M : Matrix n n R₂) :
(() M) = M
theorem BilinForm.toMatrix_comp {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [] [] [] (b : Basis n R₂ M₂) {M₂' : Type u_13} [] [Module R₂ M₂'] (c : Basis o R₂ M₂') [] (B : ) (l : M₂' →ₗ[R₂] M₂) (r : M₂' →ₗ[R₂] M₂) :
() = Matrix.transpose (() l) * B * () r
theorem BilinForm.toMatrix_compLeft {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (B : ) (f : M₂ →ₗ[R₂] M₂) :
= Matrix.transpose (() f) * B
theorem BilinForm.toMatrix_compRight {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (B : ) (f : M₂ →ₗ[R₂] M₂) :
= B * () f
@[simp]
theorem BilinForm.toMatrix_mul_basis_toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [] [] [] (b : Basis n R₂ M₂) [] (c : Basis o R₂ M₂) (B : ) :
* B * = B
theorem BilinForm.mul_toMatrix_mul {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [] [] [] (b : Basis n R₂ M₂) {M₂' : Type u_13} [] [Module R₂ M₂'] (c : Basis o R₂ M₂') [] (B : ) (M : Matrix o n R₂) (N : Matrix n o R₂) :
M * B * N = (LinearMap.BilinForm.comp B (() ()) (() N))
theorem BilinForm.mul_toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (B : ) (M : Matrix n n R₂) :
theorem BilinForm.toMatrix_mul {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} [] [] (b : Basis n R₂ M₂) (B : ) (M : Matrix n n R₂) :
theorem Matrix.toBilin_comp {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [] [] [] (b : Basis n R₂ M₂) {M₂' : Type u_13} [] [Module R₂ M₂'] (c : Basis o R₂ M₂') [] (M : Matrix n n R₂) (P : Matrix n o R₂) (Q : Matrix n o R₂) :
LinearMap.BilinForm.comp (() M) (() P) (() Q) = () ( * Q)
@[simp]
theorem isAdjointPair_toBilin' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (J : Matrix n n R₃) (J₃ : Matrix n n R₃) (A : Matrix n n R₃) (A' : Matrix n n R₃) [] :
LinearMap.BilinForm.IsAdjointPair (Matrix.toBilin' J) (Matrix.toBilin' J₃) (Matrix.toLin' A) (Matrix.toLin' A') Matrix.IsAdjointPair J J₃ A A'
@[simp]
theorem isAdjointPair_toBilin {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [] [Module R₃ M₃] {n : Type u_11} [] (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₃) [] :
LinearMap.BilinForm.IsAdjointPair (() J) (() J₃) (() A) (() A') Matrix.IsAdjointPair J J₃ A A'
theorem Matrix.isAdjointPair_equiv' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (J : Matrix n n R₃) (A : Matrix n n R₃) (A' : Matrix n n R₃) [] (P : Matrix n n R₃) (h : ) :
Matrix.IsAdjointPair ( * P) ( * P) A A' Matrix.IsAdjointPair J J (P * A * P⁻¹) (P * A' * P⁻¹)
def pairSelfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (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
Instances For
theorem mem_pairSelfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (J : Matrix n n R₃) (J₃ : Matrix n n R₃) (A : Matrix n n R₃) [] :
def selfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (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
theorem mem_selfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (J : Matrix n n R₃) (A : Matrix n n R₃) [] :
def skewAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (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
theorem mem_skewAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [] (J : Matrix n n R₃) (A : Matrix n n R₃) [] :
theorem Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {ι : Type u_12} [] [] {M : Matrix ι ι R₂} (b : Basis ι R₂ M₂) :
theorem Matrix.Nondegenerate.toBilin' {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [] [] {M : Matrix ι ι R₃} (h : ) :
@[simp]
theorem Matrix.nondegenerate_toBilin'_iff {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [] [] {M : Matrix ι ι R₃} :
theorem Matrix.Nondegenerate.toBilin {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [] [Module R₃ M₃] {ι : Type u_12} [] [] {M : Matrix ι ι R₃} (h : ) (b : Basis ι R₃ M₃) :
@[simp]
theorem Matrix.nondegenerate_toBilin_iff {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [] [Module R₃ M₃] {ι : Type u_12} [] [] {M : Matrix ι ι R₃} (b : Basis ι R₃ M₃) :

Lemmas transferring nondegeneracy between a bilinear form and its associated matrix

@[simp]
theorem LinearMap.BilinForm.nondegenerate_toMatrix'_iff {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [] [] {B : LinearMap.BilinForm R₃ (ιR₃)} :
Matrix.Nondegenerate (LinearMap.BilinForm.toMatrix' B)
theorem LinearMap.BilinForm.Nondegenerate.toMatrix' {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [] [] {B : LinearMap.BilinForm R₃ (ιR₃)} :
Matrix.Nondegenerate (LinearMap.BilinForm.toMatrix' B)
@[simp]
theorem LinearMap.BilinForm.nondegenerate_toMatrix_iff {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [] [Module R₃ M₃] {ι : Type u_12} [] [] {B : } (b : Basis ι R₃ M₃) :
theorem LinearMap.BilinForm.Nondegenerate.toMatrix {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [] [Module R₃ M₃] {ι : Type u_12} [] [] {B : } (b : Basis ι R₃ M₃) :

Some shorthands for combining the above with Matrix.nondegenerate_of_det_ne_zero

theorem LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero {A : Type u_11} [] [] {ι : Type u_12} [] [] {M : Matrix ι ι A} :
theorem LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero' {A : Type u_11} [] [] {ι : Type u_12} [] [] (M : Matrix ι ι A) (h : 0) :
theorem LinearMap.BilinForm.nondegenerate_iff_det_ne_zero {M₃ : Type u_8} [] {A : Type u_11} [] [] [Module A M₃] {ι : Type u_12} [] [] {B : } (b : Basis ι A M₃) :
theorem LinearMap.BilinForm.nondegenerate_of_det_ne_zero {M₃ : Type u_8} [] {A : Type u_11} [] [] [Module A M₃] (B₃ : ) {ι : Type u_12} [] [] (b : Basis ι A M₃) (h : Matrix.det ( B₃) 0) :