# mathlib3documentation

linear_algebra.matrix.bilinear_form

# Bilinear form #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the conversion between bilinear forms and matrices.

## Main definitions #

• matrix.to_bilin given a basis define a bilinear form
• matrix.to_bilin' define the bilinear form on n → R
• bilin_form.to_matrix: calculate the matrix coefficients of a bilinear form
• bilin_form.to_matrix': 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 semiring R,
• M₁, M₁', ... are modules over the 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, matrix, basis

def matrix.to_bilin'_aux {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] (M : n R₂) :
(n R₂)

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

This is an auxiliary definition for the equivalence matrix.to_bilin_form'.

Equations
theorem matrix.to_bilin'_aux_std_basis {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : n R₂) (i j : n) :
(M.to_bilin'_aux) ( (λ (_x : n), R₂) i) 1) ( (λ (_x : n), R₂) j) 1) = M i j
def bilin_form.to_matrix_aux {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} (b : n M₂) :
M₂ →ₗ[R₂] 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.to_bilin_form'.

Equations
@[simp]
theorem bilin_form.to_matrix_aux_apply {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} (B : M₂) (b : n M₂) (i j : n) :
i j = B (b i) (b j)
theorem to_bilin'_aux_to_matrix_aux {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B₂ : (n R₂)) :
((bilin_form.to_matrix_aux (λ (j : n), (λ (_x : n), R₂) j) 1)) B₂).to_bilin'_aux = B₂

### to_matrix' section #

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

def bilin_form.to_matrix' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] :
(n R₂) ≃ₗ[R₂] n R₂

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

Equations
@[simp]
theorem bilin_form.to_matrix_aux_std_basis {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : (n R₂)) :
(bilin_form.to_matrix_aux (λ (j : n), (λ (_x : n), R₂) j) 1)) B =
def matrix.to_bilin' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] :
n R₂ ≃ₗ[R₂] (n R₂)

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

Equations
@[simp]
theorem matrix.to_bilin'_aux_eq {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : n R₂) :
theorem matrix.to_bilin'_apply {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : n R₂) (x y : n R₂) :
x y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), x i * M i j * y j))
theorem matrix.to_bilin'_apply' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : n R₂) (v w : n R₂) :
v w = (M.mul_vec w)
@[simp]
theorem matrix.to_bilin'_std_basis {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : n R₂) (i j : n) :
( (λ (_x : n), R₂) i) 1) ( (λ (_x : n), R₂) j) 1) = M i j
@[simp]
theorem bilin_form.to_matrix'_symm {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_bilin'_symm {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_bilin'_to_matrix' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : (n R₂)) :
@[simp]
theorem bilin_form.to_matrix'_to_bilin' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : n R₂) :
@[simp]
theorem bilin_form.to_matrix'_apply {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : (n R₂)) (i j : n) :
= B ( (λ (_x : n), R₂) i) 1) ( (λ (_x : n), R₂) j) 1)
@[simp]
theorem bilin_form.to_matrix'_comp {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (B : (n R₂)) (l r : (o R₂) →ₗ[R₂] n R₂) :
theorem bilin_form.to_matrix'_comp_left {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : (n R₂)) (f : (n R₂) →ₗ[R₂] n R₂) :
theorem bilin_form.to_matrix'_comp_right {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : (n R₂)) (f : (n R₂) →ₗ[R₂] n R₂) :
theorem bilin_form.mul_to_matrix'_mul {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (B : (n R₂)) (M : n R₂) (N : o R₂) :
(M.mul .mul N =
theorem bilin_form.mul_to_matrix' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : (n R₂)) (M : n R₂) :
theorem bilin_form.to_matrix'_mul {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : (n R₂)) (M : n R₂) :
theorem matrix.to_bilin'_comp {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (M : n R₂) (P Q : o R₂) :

### to_matrix section #

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

noncomputable def bilin_form.to_matrix {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) :
M₂ ≃ₗ[R₂] n R₂

bilin_form.to_matrix 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
noncomputable def matrix.to_bilin {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) :
n R₂ ≃ₗ[R₂] M₂

bilin_form.to_matrix 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
@[simp]
theorem bilin_form.to_matrix_apply {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (B : M₂) (i j : n) :
i j = B (b i) (b j)
@[simp]
theorem matrix.to_bilin_apply {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (M : n R₂) (x y : M₂) :
( M) x y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), ((b.repr) x) i * M i j * ((b.repr) y) j))
theorem bilinear_form.to_matrix_aux_eq {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (B : M₂) :
=
@[simp]
theorem bilin_form.to_matrix_symm {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) :
@[simp]
theorem matrix.to_bilin_symm {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) :
theorem matrix.to_bilin_basis_fun {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] :
theorem bilin_form.to_matrix_basis_fun {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_bilin_to_matrix {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (B : M₂) :
B) = B
@[simp]
theorem bilin_form.to_matrix_to_bilin {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (M : n R₂) :
( M) = M
theorem bilin_form.to_matrix_comp {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] (b : R₂ M₂) {M₂' : Type u_13} [add_comm_monoid M₂'] [module R₂ M₂'] (c : R₂ M₂') [decidable_eq o] (B : M₂) (l r : M₂' →ₗ[R₂] M₂) :
(B.comp l r) = (( b) l).transpose.mul B)).mul ( b) r)
theorem bilin_form.to_matrix_comp_left {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (B : M₂) (f : M₂ →ₗ[R₂] M₂) :
(B.comp_left f) = ( b) f).transpose.mul B)
theorem bilin_form.to_matrix_comp_right {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (B : M₂) (f : M₂ →ₗ[R₂] M₂) :
(B.comp_right f) = B).mul ( b) f)
@[simp]
theorem bilin_form.to_matrix_mul_basis_to_matrix {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] (b : R₂ M₂) [decidable_eq o] (c : R₂ M₂) (B : M₂) :
theorem bilin_form.mul_to_matrix_mul {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] (b : R₂ M₂) {M₂' : Type u_13} [add_comm_monoid M₂'] [module R₂ M₂'] (c : R₂ M₂') [decidable_eq o] (B : M₂) (M : n R₂) (N : o R₂) :
(M.mul B)).mul N = (B.comp ( b) M.transpose) ( b) N))
theorem bilin_form.mul_to_matrix {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (B : M₂) (M : n R₂) :
M.mul B) = (B.comp_left ( b) M.transpose))
theorem bilin_form.to_matrix_mul {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} [fintype n] [decidable_eq n] (b : R₂ M₂) (B : M₂) (M : n R₂) :
B).mul M = (B.comp_right ( b) M))
theorem matrix.to_bilin_comp {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] (b : R₂ M₂) {M₂' : Type u_13} [add_comm_monoid M₂'] [module R₂ M₂'] (c : R₂ M₂') [decidable_eq o] (M : n R₂) (P Q : o R₂) :
( M).comp ( b) P) ( b) Q) = ((P.transpose.mul M).mul Q)
@[simp]
theorem is_adjoint_pair_to_bilin' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J J₃ A A' : n R₃) [decidable_eq n] :
@[simp]
theorem is_adjoint_pair_to_bilin {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [fintype n] (b : R₃ M₃) (J J₃ A A' : n R₃) [decidable_eq n] :
( J).is_adjoint_pair ( J₃) ( b) A) ( b) A') J.is_adjoint_pair J₃ A A'
theorem matrix.is_adjoint_pair_equiv' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J A A' : n R₃) [decidable_eq n] (P : n R₃) (h : is_unit P) :
((P.transpose.mul J).mul P).is_adjoint_pair ((P.transpose.mul J).mul P) A A' ((P.mul A).mul P⁻¹) ((P.mul A').mul P⁻¹)
def pair_self_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J J₃ : n R₃) [decidable_eq n] :
(matrix n n R₃)

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

Equations
theorem mem_pair_self_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J J₃ A : n R₃) [decidable_eq n] :
def self_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J : n R₃) [decidable_eq n] :
(matrix n n R₃)

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

Equations
theorem mem_self_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J A : n R₃) [decidable_eq n] :
def skew_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J : n R₃) [decidable_eq n] :
(matrix n n R₃)

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

Equations
theorem mem_skew_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J A : n R₃) [decidable_eq n] :
theorem matrix.nondegenerate_to_bilin'_iff_nondegenerate_to_bilin {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {ι : Type u_12} [decidable_eq ι] [fintype ι] {M : ι R₂} (b : R₂ M₂) :
theorem matrix.nondegenerate.to_bilin' {R₃ : Type u_7} [comm_ring R₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {M : ι R₃} (h : M.nondegenerate) :
@[simp]
theorem matrix.nondegenerate_to_bilin'_iff {R₃ : Type u_7} [comm_ring R₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {M : ι R₃} :
theorem matrix.nondegenerate.to_bilin {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {M : ι R₃} (h : M.nondegenerate) (b : R₃ M₃) :
@[simp]
theorem matrix.nondegenerate_to_bilin_iff {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {M : ι R₃} (b : R₃ M₃) :
@[simp]
theorem bilin_form.nondegenerate_to_matrix'_iff {R₃ : Type u_7} [comm_ring R₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {B : R₃)} :
theorem bilin_form.nondegenerate.to_matrix' {R₃ : Type u_7} [comm_ring R₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {B : R₃)} (h : B.nondegenerate) :
@[simp]
theorem bilin_form.nondegenerate_to_matrix_iff {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {B : M₃} (b : R₃ M₃) :
theorem bilin_form.nondegenerate.to_matrix {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {B : M₃} (h : B.nondegenerate) (b : R₃ M₃) :
theorem bilin_form.nondegenerate_to_bilin'_iff_det_ne_zero {A : Type u_11} [comm_ring A] [is_domain A] {ι : Type u_12} [decidable_eq ι] [fintype ι] {M : ι A} :
M.det 0
theorem bilin_form.nondegenerate_to_bilin'_of_det_ne_zero' {A : Type u_11} [comm_ring A] [is_domain A] {ι : Type u_12} [decidable_eq ι] [fintype ι] (M : ι A) (h : M.det 0) :
theorem bilin_form.nondegenerate_iff_det_ne_zero {M₃ : Type u_8} [add_comm_group M₃] {A : Type u_11} [comm_ring A] [is_domain A] [ M₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {B : M₃} (b : A M₃) :
theorem bilin_form.nondegenerate_of_det_ne_zero {M₃ : Type u_8} [add_comm_group M₃] {A : Type u_11} [comm_ring A] [is_domain A] [ M₃] (B₃ : M₃) {ι : Type u_12} [decidable_eq ι] [fintype ι] (b : A M₃) (h : B₃).det 0) :