Sesquilinear form #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the conversion between sesquilinear forms and matrices.
Main definitions #
matrix.to_linear_map₂given a basis define a bilinear formmatrix.to_linear_map₂'define the bilinear form onn → Rlinear_map.to_matrix₂: calculate the matrix coefficients of a bilinear formlinear_map.to_matrix₂': calculate the matrix coefficients of a bilinear form onn → R
Todos #
At the moment this is quite a literal port from matrix.bilinear_form. Everything should be
generalized to fully semibilinear forms.
Tags #
sesquilinear_form, matrix, basis
def
matrix.to_linear_map₂'_aux
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_semiring R]
[comm_semiring R₁]
[comm_semiring R₂]
[fintype n]
[fintype m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(f : matrix n m R) :
The map from matrix n n R to bilinear forms on n → R.
This is an auxiliary definition for the equivalence matrix.to_linear_map₂'.
Equations
- matrix.to_linear_map₂'_aux σ₁ σ₂ f = linear_map.mk₂'ₛₗ σ₁ σ₂ (λ (v : n → R₁) (w : m → R₂), finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : m), ⇑σ₁ (v i) * f i j * ⇑σ₂ (w j)))) _ _ _ _
theorem
matrix.to_linear_map₂'_aux_std_basis
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_semiring R]
[comm_semiring R₁]
[comm_semiring R₂]
[fintype n]
[fintype m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
[decidable_eq n]
[decidable_eq m]
(f : matrix n m R)
(i : n)
(j : m) :
⇑(⇑(matrix.to_linear_map₂'_aux σ₁ σ₂ f) (⇑(linear_map.std_basis R₁ (λ (_x : n), R₁) i) 1)) (⇑(linear_map.std_basis R₂ (λ (_x : m), R₂) j) 1) = f i j
def
linear_map.to_matrix₂_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}
[comm_semiring R]
[comm_semiring R₁]
[comm_semiring R₂]
[add_comm_monoid M₁]
[module R₁ M₁]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁ : R₁ →+* R}
{σ₂ : R₂ →+* R}
(b₁ : n → M₁)
(b₂ : m → M₂) :
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.to_linear_mapₛₗ₂'.
@[simp]
theorem
linear_map.to_matrix₂_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}
[comm_semiring R]
[comm_semiring R₁]
[comm_semiring R₂]
[add_comm_monoid M₁]
[module R₁ M₁]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁ : R₁ →+* R}
{σ₂ : R₂ →+* R}
(f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R)
(b₁ : n → M₁)
(b₂ : m → M₂)
(i : n)
(j : m) :
⇑(linear_map.to_matrix₂_aux b₁ b₂) f i j = ⇑(⇑f (b₁ i)) (b₂ j)
theorem
linear_map.to_linear_map₂'_aux_to_matrix₂_aux
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
{σ₁ : R₁ →+* R}
{σ₂ : R₂ →+* R}
(f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R) :
matrix.to_linear_map₂'_aux σ₁ σ₂ (⇑(linear_map.to_matrix₂_aux (λ (i : n), ⇑(linear_map.std_basis R₁ (λ (_x : n), R₁) i) 1) (λ (j : m), ⇑(linear_map.std_basis R₂ (λ (_x : m), R₂) j) 1)) f) = f
theorem
matrix.to_matrix₂_aux_to_linear_map₂'_aux
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
{σ₁ : R₁ →+* R}
{σ₂ : R₂ →+* R}
(f : matrix n m R) :
⇑(linear_map.to_matrix₂_aux (λ (i : n), ⇑(linear_map.std_basis R₁ (λ (_x : n), R₁) i) 1) (λ (j : m), ⇑(linear_map.std_basis R₂ (λ (_x : m), R₂) j) 1)) (matrix.to_linear_map₂'_aux σ₁ σ₂ f) = f
Bilinear forms over n → R #
This section deals with the conversion between matrices and sesquilinear forms on n → R.
def
linear_map.to_matrixₛₗ₂'
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
{σ₁ : R₁ →+* R}
{σ₂ : R₂ →+* R} :
The linear equivalence between sesquilinear forms and n × m matrices
Equations
- linear_map.to_matrixₛₗ₂' = {to_fun := ⇑(linear_map.to_matrix₂_aux (λ (i : n), (λ (i : n), ⇑(linear_map.std_basis R₁ (λ (_x : n), R₁) i) 1) i) (λ (j : m), (λ (j : m), ⇑(linear_map.std_basis R₂ (λ (_x : m), R₂) j) 1) j)), map_add' := _, map_smul' := _, inv_fun := matrix.to_linear_map₂'_aux σ₁ σ₂, left_inv := _, right_inv := _}
def
linear_map.to_matrix₂'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m] :
The linear equivalence between bilinear forms and n × m matrices
Equations
def
matrix.to_linear_mapₛₗ₂'
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R) :
The linear equivalence between n × n matrices and sesquilinear forms on n → R
Equations
def
matrix.to_linear_map₂'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m] :
The linear equivalence between n × n matrices and bilinear forms on n → R
Equations
theorem
matrix.to_linear_mapₛₗ₂'_aux_eq
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(M : matrix n m R) :
matrix.to_linear_map₂'_aux σ₁ σ₂ M = ⇑(matrix.to_linear_mapₛₗ₂' σ₁ σ₂) M
theorem
matrix.to_linear_mapₛₗ₂'_apply
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(M : matrix n m R)
(x : n → R₁)
(y : m → R₂) :
⇑(⇑(⇑(matrix.to_linear_mapₛₗ₂' σ₁ σ₂) M) x) y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : m), ⇑σ₁ (x i) * M i j * ⇑σ₂ (y j)))
theorem
matrix.to_linear_map₂'_apply
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(M : matrix n m R)
(x : n → R)
(y : m → R) :
⇑(⇑(⇑matrix.to_linear_map₂' M) x) y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : m), x i * M i j * y j))
theorem
matrix.to_linear_map₂'_apply'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(M : matrix n m R)
(v : n → R)
(w : m → R) :
⇑(⇑(⇑matrix.to_linear_map₂' M) v) w = matrix.dot_product v (M.mul_vec w)
@[simp]
theorem
matrix.to_linear_mapₛₗ₂'_std_basis
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(M : matrix n m R)
(i : n)
(j : m) :
⇑(⇑(⇑(matrix.to_linear_mapₛₗ₂' σ₁ σ₂) M) (⇑(linear_map.std_basis R₁ (λ (_x : n), R₁) i) 1)) (⇑(linear_map.std_basis R₂ (λ (_x : m), R₂) j) 1) = M i j
@[simp]
theorem
matrix.to_linear_map₂'_std_basis
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(M : matrix n m R)
(i : n)
(j : m) :
⇑(⇑(⇑matrix.to_linear_map₂' M) (⇑(linear_map.std_basis R (λ (_x : n), R) i) 1)) (⇑(linear_map.std_basis R (λ (_x : m), R) j) 1) = M i j
@[simp]
theorem
linear_map.to_matrixₛₗ₂'_symm
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R) :
@[simp]
theorem
matrix.to_linear_mapₛₗ₂'_symm
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R) :
@[simp]
theorem
matrix.to_linear_mapₛₗ₂'_to_matrix'
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R) :
⇑(matrix.to_linear_mapₛₗ₂' σ₁ σ₂) (⇑linear_map.to_matrixₛₗ₂' B) = B
@[simp]
theorem
matrix.to_linear_map₂'_to_matrix'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) :
@[simp]
theorem
linear_map.to_matrix'_to_linear_mapₛₗ₂'
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(M : matrix n m R) :
⇑linear_map.to_matrixₛₗ₂' (⇑(matrix.to_linear_mapₛₗ₂' σ₁ σ₂) M) = M
@[simp]
theorem
linear_map.to_matrix'_to_linear_map₂'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(M : matrix n m R) :
@[simp]
theorem
linear_map.to_matrixₛₗ₂'_apply
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[comm_ring R₁]
[comm_ring R₂]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R)
(i : n)
(j : m) :
⇑linear_map.to_matrixₛₗ₂' B i j = ⇑(⇑B (⇑(linear_map.std_basis R₁ (λ (_x : n), R₁) i) 1)) (⇑(linear_map.std_basis R₂ (λ (_x : m), R₂) j) 1)
@[simp]
theorem
linear_map.to_matrix₂'_apply
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
(B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
(i : n)
(j : m) :
⇑linear_map.to_matrix₂' B i j = ⇑(⇑B (⇑(linear_map.std_basis R (λ (_x : n), R) i) 1)) (⇑(linear_map.std_basis R (λ (_x : m), R) j) 1)
@[simp]
theorem
linear_map.to_matrix₂'_compl₁₂
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{n' : Type u_11}
{m' : Type u_12}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
[fintype n']
[fintype m']
[decidable_eq n']
[decidable_eq m']
(B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
(l : (n' → R) →ₗ[R] n → R)
(r : (m' → R) →ₗ[R] m → R) :
⇑linear_map.to_matrix₂' (B.compl₁₂ l r) = ((⇑linear_map.to_matrix' l).transpose.mul (⇑linear_map.to_matrix₂' B)).mul (⇑linear_map.to_matrix' r)
theorem
linear_map.mul_to_matrix₂'_mul
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{n' : Type u_11}
{m' : Type u_12}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
[fintype n']
[fintype m']
[decidable_eq n']
[decidable_eq m']
(B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
(M : matrix n' n R)
(N : matrix m m' R) :
(M.mul (⇑linear_map.to_matrix₂' B)).mul N = ⇑linear_map.to_matrix₂' (B.compl₁₂ (⇑matrix.to_lin' M.transpose) (⇑matrix.to_lin' N))
theorem
linear_map.mul_to_matrix'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{n' : Type u_11}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
[fintype n']
[decidable_eq n']
(B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
(M : matrix n' n R) :
M.mul (⇑linear_map.to_matrix₂' B) = ⇑linear_map.to_matrix₂' (B.comp (⇑matrix.to_lin' M.transpose))
theorem
linear_map.to_matrix₂'_mul
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{m' : Type u_12}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
[fintype m']
[decidable_eq m']
(B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
(M : matrix m m' R) :
(⇑linear_map.to_matrix₂' B).mul M = ⇑linear_map.to_matrix₂' (B.compl₂ (⇑matrix.to_lin' M))
theorem
matrix.to_linear_map₂'_comp
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{n' : Type u_11}
{m' : Type u_12}
[comm_ring R]
[fintype n]
[fintype m]
[decidable_eq n]
[decidable_eq m]
[fintype n']
[fintype m']
[decidable_eq n']
[decidable_eq m']
(M : matrix n m R)
(P : matrix n n' R)
(Q : matrix m m' R) :
(⇑matrix.to_linear_map₂' M).compl₁₂ (⇑matrix.to_lin' P) (⇑matrix.to_lin' Q) = ⇑matrix.to_linear_map₂' ((P.transpose.mul M).mul 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
linear_map.to_matrix₂
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂) :
linear_map.to_matrix₂ b₁ 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
- linear_map.to_matrix₂ b₁ b₂ = (b₁.equiv_fun.arrow_congr (b₂.equiv_fun.arrow_congr (linear_equiv.refl R R))).trans linear_map.to_matrix₂'
noncomputable
def
matrix.to_linear_map₂
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m 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
- matrix.to_linear_map₂ b₁ b₂ = (linear_map.to_matrix₂ b₁ b₂).symm
@[simp]
theorem
linear_map.to_matrix₂_apply
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(i : n)
(j : m) :
@[simp]
theorem
matrix.to_linear_map₂_apply
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
(M : matrix n m R)
(x : M₁)
(y : M₂) :
theorem
linear_map.to_matrix₂_aux_eq
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
⇑(linear_map.to_matrix₂_aux ⇑b₁ ⇑b₂) B = ⇑(linear_map.to_matrix₂ b₁ b₂) B
@[simp]
theorem
linear_map.to_matrix₂_symm
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂) :
(linear_map.to_matrix₂ b₁ b₂).symm = matrix.to_linear_map₂ b₁ b₂
@[simp]
theorem
matrix.to_linear_map₂_symm
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂) :
(matrix.to_linear_map₂ b₁ b₂).symm = linear_map.to_matrix₂ b₁ b₂
theorem
matrix.to_linear_map₂_basis_fun
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m] :
theorem
linear_map.to_matrix₂_basis_fun
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m] :
@[simp]
theorem
matrix.to_linear_map₂_to_matrix₂
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
⇑(matrix.to_linear_map₂ b₁ b₂) (⇑(linear_map.to_matrix₂ b₁ b₂) B) = B
@[simp]
theorem
linear_map.to_matrix₂_to_linear_map₂
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
(M : matrix n m R) :
⇑(linear_map.to_matrix₂ b₁ b₂) (⇑(matrix.to_linear_map₂ b₁ b₂) M) = M
theorem
linear_map.to_matrix₂_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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[add_comm_monoid M₁']
[module R M₁']
[add_comm_monoid M₂']
[module R M₂']
(b₁' : basis n' R M₁')
(b₂' : basis m' R M₂')
[fintype n']
[fintype m']
[decidable_eq n']
[decidable_eq m']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(l : M₁' →ₗ[R] M₁)
(r : M₂' →ₗ[R] M₂) :
⇑(linear_map.to_matrix₂ b₁' b₂') (B.compl₁₂ l r) = ((⇑(linear_map.to_matrix b₁' b₁) l).transpose.mul (⇑(linear_map.to_matrix₂ b₁ b₂) B)).mul (⇑(linear_map.to_matrix b₂' b₂) r)
theorem
linear_map.to_matrix₂_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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[add_comm_monoid M₁']
[module R M₁']
(b₁' : basis n' R M₁')
[fintype n']
[decidable_eq n']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(f : M₁' →ₗ[R] M₁) :
⇑(linear_map.to_matrix₂ b₁' b₂) (B.comp f) = (⇑(linear_map.to_matrix b₁' b₁) f).transpose.mul (⇑(linear_map.to_matrix₂ b₁ b₂) B)
theorem
linear_map.to_matrix₂_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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[add_comm_monoid M₂']
[module R M₂']
(b₂' : basis m' R M₂')
[fintype m']
[decidable_eq m']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(f : M₂' →ₗ[R] M₂) :
⇑(linear_map.to_matrix₂ b₁ b₂') (B.compl₂ f) = (⇑(linear_map.to_matrix₂ b₁ b₂) B).mul (⇑(linear_map.to_matrix b₂' b₂) f)
@[simp]
theorem
linear_map.to_matrix₂_mul_basis_to_matrix
{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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[fintype n']
[fintype m']
[decidable_eq n']
[decidable_eq m']
(c₁ : basis n' R M₁)
(c₂ : basis m' R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
theorem
linear_map.mul_to_matrix₂_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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[add_comm_monoid M₁']
[module R M₁']
[add_comm_monoid M₂']
[module R M₂']
(b₁' : basis n' R M₁')
(b₂' : basis m' R M₂')
[fintype n']
[fintype m']
[decidable_eq n']
[decidable_eq m']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(M : matrix n' n R)
(N : matrix m m' R) :
(M.mul (⇑(linear_map.to_matrix₂ b₁ b₂) B)).mul N = ⇑(linear_map.to_matrix₂ b₁' b₂') (B.compl₁₂ (⇑(matrix.to_lin b₁' b₁) M.transpose) (⇑(matrix.to_lin b₂' b₂) N))
theorem
linear_map.mul_to_matrix₂
{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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[add_comm_monoid M₁']
[module R M₁']
(b₁' : basis n' R M₁')
[fintype n']
[decidable_eq n']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(M : matrix n' n R) :
M.mul (⇑(linear_map.to_matrix₂ b₁ b₂) B) = ⇑(linear_map.to_matrix₂ b₁' b₂) (B.comp (⇑(matrix.to_lin b₁' b₁) M.transpose))
theorem
linear_map.to_matrix₂_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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[add_comm_monoid M₂']
[module R M₂']
(b₂' : basis m' R M₂')
[fintype m']
[decidable_eq m']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(M : matrix m m' R) :
(⇑(linear_map.to_matrix₂ b₁ b₂) B).mul M = ⇑(linear_map.to_matrix₂ b₁ b₂') (B.compl₂ (⇑(matrix.to_lin b₂' b₂) M))
theorem
matrix.to_linear_map₂_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}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
(b₁ : basis n R M₁)
(b₂ : basis m R M₂)
[add_comm_monoid M₁']
[module R M₁']
[add_comm_monoid M₂']
[module R M₂']
(b₁' : basis n' R M₁')
(b₂' : basis m' R M₂')
[fintype n']
[fintype m']
[decidable_eq n']
[decidable_eq m']
(M : matrix n m R)
(P : matrix n n' R)
(Q : matrix m m' R) :
(⇑(matrix.to_linear_map₂ b₁ b₂) M).compl₁₂ (⇑(matrix.to_lin b₁' b₁) P) (⇑(matrix.to_lin b₂' b₂) Q) = ⇑(matrix.to_linear_map₂ b₁' b₂') ((P.transpose.mul M).mul Q)
Adjoint pairs #
def
matrix.is_adjoint_pair
{R : Type u_1}
{n : Type u_9}
{n' : Type u_11}
[comm_ring 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₃.
def
matrix.is_self_adjoint
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J 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
- J.is_self_adjoint A₁ = J.is_adjoint_pair J A₁ A₁
def
matrix.is_skew_adjoint
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J 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
- J.is_skew_adjoint A₁ = J.is_adjoint_pair J A₁ (-A₁)
@[simp]
theorem
is_adjoint_pair_to_linear_map₂'
{R : Type u_1}
{n : Type u_9}
{n' : Type u_11}
[comm_ring 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)
[decidable_eq n]
[decidable_eq n'] :
(⇑matrix.to_linear_map₂' J).is_adjoint_pair (⇑matrix.to_linear_map₂' J') (⇑matrix.to_lin' A) (⇑matrix.to_lin' A') ↔ J.is_adjoint_pair J' A A'
@[simp]
theorem
is_adjoint_pair_to_linear_map₂
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{n' : Type u_11}
[comm_ring R]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid 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)
[decidable_eq n]
[decidable_eq n'] :
(⇑(matrix.to_linear_map₂ b₁ b₁) J).is_adjoint_pair (⇑(matrix.to_linear_map₂ b₂ b₂) J') (⇑(matrix.to_lin b₁ b₂) A) (⇑(matrix.to_lin b₂ b₁) A') ↔ J.is_adjoint_pair J' A A'
theorem
matrix.is_adjoint_pair_equiv
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J A₁ : matrix n n R)
[decidable_eq n]
(P : matrix n n R)
(h : is_unit P) :
def
pair_self_adjoint_matrices_submodule
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J J₂ : matrix n n R)
[decidable_eq n] :
The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to
given matrices J, J₂.
@[simp]
theorem
mem_pair_self_adjoint_matrices_submodule
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J J₂ A₁ : matrix n n R)
[decidable_eq n] :
A₁ ∈ pair_self_adjoint_matrices_submodule J J₂ ↔ J.is_adjoint_pair J₂ A₁ A₁
def
self_adjoint_matrices_submodule
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J : matrix n n R)
[decidable_eq n] :
The submodule of self-adjoint matrices with respect to the bilinear form corresponding to
the matrix J.
Equations
@[simp]
theorem
mem_self_adjoint_matrices_submodule
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J A₁ : matrix n n R)
[decidable_eq n] :
A₁ ∈ self_adjoint_matrices_submodule J ↔ J.is_self_adjoint A₁
def
skew_adjoint_matrices_submodule
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J : matrix n n R)
[decidable_eq n] :
The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to
the matrix J.
Equations
@[simp]
theorem
mem_skew_adjoint_matrices_submodule
{R : Type u_1}
{n : Type u_9}
[comm_ring R]
[fintype n]
(J A₁ : matrix n n R)
[decidable_eq n] :
A₁ ∈ skew_adjoint_matrices_submodule J ↔ J.is_skew_adjoint A₁
Nondegenerate bilinear forms #
theorem
matrix.separating_left_to_linear_map₂'_iff_separating_left_to_linear_map₂
{R₁ : Type u_2}
{M₁ : Type u_5}
{ι : Type u_13}
[comm_ring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₁}
(b : basis ι R₁ M₁) :
theorem
matrix.nondegenerate.to_linear_map₂'
{R₁ : Type u_2}
{ι : Type u_13}
[comm_ring R₁]
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₁}
(h : M.nondegenerate) :
@[simp]
theorem
matrix.separating_left_to_linear_map₂'_iff
{R₁ : Type u_2}
{ι : Type u_13}
[comm_ring R₁]
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₁} :
theorem
matrix.nondegenerate.to_linear_map₂
{R₁ : Type u_2}
{M₁ : Type u_5}
{ι : Type u_13}
[comm_ring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₁}
(h : M.nondegenerate)
(b : basis ι R₁ M₁) :
(⇑(matrix.to_linear_map₂ b b) M).separating_left
@[simp]
theorem
matrix.separating_left_to_linear_map₂_iff
{R₁ : Type u_2}
{M₁ : Type u_5}
{ι : Type u_13}
[comm_ring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₁}
(b : basis ι R₁ M₁) :
(⇑(matrix.to_linear_map₂ b b) M).separating_left ↔ M.nondegenerate
theorem
linear_map.separating_left.to_matrix₂'
{R₁ : Type u_2}
{ι : Type u_13}
[comm_ring R₁]
[decidable_eq ι]
[fintype ι]
{B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁}
(h : B.separating_left) :
@[simp]
theorem
linear_map.nondegenerate_to_matrix_iff
{R₁ : Type u_2}
{M₁ : Type u_5}
{ι : Type u_13}
[comm_ring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[decidable_eq ι]
[fintype ι]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : basis ι R₁ M₁) :
(⇑(linear_map.to_matrix₂ b b) B).nondegenerate ↔ B.separating_left
theorem
linear_map.separating_left.to_matrix₂
{R₁ : Type u_2}
{M₁ : Type u_5}
{ι : Type u_13}
[comm_ring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[decidable_eq ι]
[fintype ι]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(h : B.separating_left)
(b : basis ι R₁ M₁) :
(⇑(linear_map.to_matrix₂ b b) B).nondegenerate
theorem
linear_map.separating_left_to_linear_map₂'_iff_det_ne_zero
{R₁ : Type u_2}
{ι : Type u_13}
[comm_ring R₁]
[decidable_eq ι]
[fintype ι]
[is_domain R₁]
{M : matrix ι ι R₁} :
(⇑matrix.to_linear_map₂' M).separating_left ↔ M.det ≠ 0
theorem
linear_map.separating_left_to_linear_map₂'_of_det_ne_zero'
{R₁ : Type u_2}
{ι : Type u_13}
[comm_ring R₁]
[decidable_eq ι]
[fintype ι]
[is_domain R₁]
(M : matrix ι ι R₁)
(h : M.det ≠ 0) :
theorem
linear_map.separating_left_iff_det_ne_zero
{R₁ : Type u_2}
{M₁ : Type u_5}
{ι : Type u_13}
[comm_ring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[decidable_eq ι]
[fintype ι]
[is_domain R₁]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : basis ι R₁ M₁) :
B.separating_left ↔ (⇑(linear_map.to_matrix₂ b b) B).det ≠ 0
theorem
linear_map.separating_left_of_det_ne_zero
{R₁ : Type u_2}
{M₁ : Type u_5}
{ι : Type u_13}
[comm_ring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[decidable_eq ι]
[fintype ι]
[is_domain R₁]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : basis ι R₁ M₁)
(h : (⇑(linear_map.to_matrix₂ b b) B).det ≠ 0) :