mathlib3 documentation

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 #

Notations #

In this file we use the following type variables:

Tags #

bilinear_form, matrix, basis

def matrix.to_bilin'_aux {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] (M : matrix n n R₂) :
bilin_form 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 : matrix n n R₂) (i j : n) :
(M.to_bilin'_aux) ((linear_map.std_basis R₂ (λ (_x : n), R₂) i) 1) ((linear_map.std_basis R₂ (λ (_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₂) :
bilin_form R₂ M₂ →ₗ[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.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 : bilin_form R₂ M₂) (b : n M₂) (i j : n) :
(bilin_form.to_matrix_aux b) B 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₂ : bilin_form R₂ (n R₂)) :
((bilin_form.to_matrix_aux (λ (j : n), (linear_map.std_basis R₂ (λ (_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] :
bilin_form R₂ (n R₂) ≃ₗ[R₂] matrix n 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 : bilin_form R₂ (n R₂)) :
(bilin_form.to_matrix_aux (λ (j : n), (linear_map.std_basis R₂ (λ (_x : n), R₂) j) 1)) B = bilin_form.to_matrix' B
def matrix.to_bilin' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] :
matrix n n R₂ ≃ₗ[R₂] bilin_form 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 : matrix n n R₂) :
theorem matrix.to_bilin'_apply {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : matrix n n R₂) (x y : n R₂) :
(matrix.to_bilin' M) 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 : matrix n n R₂) (v w : n R₂) :
@[simp]
theorem matrix.to_bilin'_std_basis {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (M : matrix n n R₂) (i j : n) :
(matrix.to_bilin' M) ((linear_map.std_basis R₂ (λ (_x : n), R₂) i) 1) ((linear_map.std_basis R₂ (λ (_x : n), R₂) j) 1) = M i j
@[simp]
theorem matrix.to_bilin'_to_matrix' {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : bilin_form R₂ (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 : matrix n 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 : bilin_form R₂ (n R₂)) (i j : n) :
bilin_form.to_matrix' B i j = B ((linear_map.std_basis R₂ (λ (_x : n), R₂) i) 1) ((linear_map.std_basis R₂ (λ (_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 : bilin_form R₂ (n R₂)) (l r : (o 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 : bilin_form R₂ (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 : bilin_form R₂ (n R₂)) (M : matrix o n R₂) (N : matrix n o R₂) :
theorem bilin_form.to_matrix'_mul {R₂ : Type u_5} [comm_semiring R₂] {n : Type u_11} [fintype n] [decidable_eq n] (B : bilin_form R₂ (n R₂)) (M : matrix n 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 : matrix n n R₂) (P Q : matrix n 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 : basis n R₂ M₂) :
bilin_form R₂ M₂ ≃ₗ[R₂] matrix n 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 : basis n R₂ M₂) :
matrix n n R₂ ≃ₗ[R₂] bilin_form 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 : basis n R₂ M₂) (B : bilin_form R₂ M₂) (i j : n) :
(bilin_form.to_matrix b) B 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 : basis n R₂ M₂) (M : matrix n n R₂) (x y : M₂) :
((matrix.to_bilin b) 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 : basis n R₂ M₂) (B : bilin_form R₂ 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 : basis n 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 : basis n R₂ M₂) :
@[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 : basis n R₂ M₂) (B : bilin_form R₂ M₂) :
@[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 : basis n R₂ M₂) (M : matrix n n R₂) :
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 : basis n R₂ M₂) {M₂' : Type u_13} [add_comm_monoid M₂'] [module R₂ M₂'] (c : basis o R₂ M₂') [decidable_eq o] (B : bilin_form R₂ M₂) (l r : M₂' →ₗ[R₂] M₂) :
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 : basis n R₂ M₂) (B : bilin_form R₂ M₂) (f : M₂ →ₗ[R₂] M₂) :
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 : basis n R₂ M₂) (B : bilin_form R₂ M₂) (f : M₂ →ₗ[R₂] M₂) :
@[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 : basis n R₂ M₂) [decidable_eq o] (c : basis o R₂ M₂) (B : bilin_form R₂ 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 : basis n R₂ M₂) {M₂' : Type u_13} [add_comm_monoid M₂'] [module R₂ M₂'] (c : basis o R₂ M₂') [decidable_eq o] (B : bilin_form R₂ M₂) (M : matrix o n R₂) (N : matrix n o R₂) :
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 : basis n R₂ M₂) (B : bilin_form R₂ M₂) (M : matrix n n R₂) :
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 : basis n R₂ M₂) (B : bilin_form R₂ M₂) (M : matrix n n R₂) :
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 : basis n R₂ M₂) {M₂' : Type u_13} [add_comm_monoid M₂'] [module R₂ M₂'] (c : basis o R₂ M₂') [decidable_eq o] (M : matrix n n R₂) (P Q : matrix n o R₂) :
@[simp]
theorem is_adjoint_pair_to_bilin' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J J₃ A A' : matrix n 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 : basis n R₃ M₃) (J J₃ A A' : matrix n n R₃) [decidable_eq n] :
theorem matrix.is_adjoint_pair_equiv' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J A A' : matrix n n R₃) [decidable_eq n] (P : matrix n n R₃) (h : is_unit P) :
((P.transpose.mul J).mul P).is_adjoint_pair ((P.transpose.mul J).mul P) A A' J.is_adjoint_pair J ((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₃ : matrix n n R₃) [decidable_eq 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
theorem mem_pair_self_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J J₃ A : matrix n n R₃) [decidable_eq n] :
def self_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J : matrix n n R₃) [decidable_eq 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
def skew_adjoint_matrices_submodule' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] (J : matrix n n R₃) [decidable_eq 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
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 : matrix ι ι R₂} (b : basis ι R₂ M₂) :
theorem matrix.nondegenerate.to_bilin' {R₃ : Type u_7} [comm_ring R₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {M : matrix ι ι 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 : matrix ι ι 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 : matrix ι ι R₃} (h : M.nondegenerate) (b : basis ι 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 : matrix ι ι R₃} (b : basis ι R₃ M₃) :
@[simp]
theorem bilin_form.nondegenerate.to_matrix' {R₃ : Type u_7} [comm_ring R₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {B : bilin_form R₃ 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 : bilin_form R₃ M₃} (b : basis ι 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 : bilin_form R₃ M₃} (h : B.nondegenerate) (b : basis ι R₃ M₃) :
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] [module A M₃] {ι : Type u_12} [decidable_eq ι] [fintype ι] {B : bilin_form A M₃} (b : basis ι 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] [module A M₃] (B₃ : bilin_form A M₃) {ι : Type u_12} [decidable_eq ι] [fintype ι] (b : basis ι A M₃) (h : ((bilin_form.to_matrix b) B₃).det 0) :