Sesquilinear form #
This file defines the conversion between sesquilinear forms and matrices.
Main definitions #
Matrix.toLinearMap₂given a basis define a bilinear formMatrix.toLinearMap₂'define the bilinear form onn → RLinearMap.toMatrix₂: calculate the matrix coefficients of a bilinear formLinearMap.toMatrix₂': calculate the matrix coefficients of a bilinear form onn → 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
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]
[Semiring R₁]
[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.toLinearMap₂'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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]
[Semiring R₁]
[Semiring 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 : n) => R₁) i) 1))
((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) = f i j
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]
[Semiring R₁]
[Semiring R₂]
[AddCommMonoid M₁]
[Module R₁ M₁]
[AddCommMonoid 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.toLinearMapₛₗ₂'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
[Semiring R₁]
[Semiring 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)
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}
[CommSemiring R]
[Semiring R₁]
[Semiring 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 : n) => (LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1) fun (j : m) =>
(LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1)
f) = f
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}
[CommSemiring R]
[Semiring R₁]
[Semiring R₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
{σ₁ : R₁ →+* R}
{σ₂ : R₂ →+* R}
(f : Matrix n m R)
:
(LinearMap.toMatrix₂Aux (fun (i : n) => (LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1) fun (j : m) =>
(LinearMap.stdBasis R₂ (fun (x : m) => 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.
def
LinearMap.toMatrixₛₗ₂'
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[Semiring R₁]
[Semiring R₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
{σ₁ : R₁ →+* R}
{σ₂ : R₂ →+* 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
def
LinearMap.toMatrix₂'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
The linear equivalence between bilinear forms and n × m matrices
Equations
- LinearMap.toMatrix₂' = LinearMap.toMatrixₛₗ₂'
Instances For
def
Matrix.toLinearMapₛₗ₂'
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[Semiring R₁]
[Semiring R₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
:
The linear equivalence between n × n matrices and sesquilinear forms on n → R
Equations
- Matrix.toLinearMapₛₗ₂' σ₁ σ₂ = LinearEquiv.symm LinearMap.toMatrixₛₗ₂'
Instances For
def
Matrix.toLinearMap₂'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
The linear equivalence between n × n matrices and bilinear forms on n → R
Equations
- Matrix.toLinearMap₂' = LinearEquiv.symm LinearMap.toMatrix₂'
Instances For
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}
[CommSemiring R]
[Semiring R₁]
[Semiring 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
theorem
Matrix.toLinearMapₛₗ₂'_apply
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[Semiring R₁]
[Semiring 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 : n) => Finset.sum Finset.univ fun (j : m) => σ₁ (x i) * M i j * σ₂ (y j)
theorem
Matrix.toLinearMap₂'_apply
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring 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 : n) => Finset.sum Finset.univ fun (j : m) => x i * M i j * y j
theorem
Matrix.toLinearMap₂'_apply'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring 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)
@[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}
[CommSemiring R]
[Semiring R₁]
[Semiring 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 : n) => R₁) i) 1))
((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) = M i j
@[simp]
theorem
Matrix.toLinearMap₂'_stdBasis
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring 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 : n) => R) i) 1))
((LinearMap.stdBasis R (fun (x : m) => R) j) 1) = M i j
@[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}
[CommSemiring R]
[Semiring R₁]
[Semiring R₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
:
LinearEquiv.symm LinearMap.toMatrixₛₗ₂' = Matrix.toLinearMapₛₗ₂' σ₁ σ₂
@[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}
[CommSemiring R]
[Semiring R₁]
[Semiring R₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
:
LinearEquiv.symm (Matrix.toLinearMapₛₗ₂' σ₁ σ₂) = LinearMap.toMatrixₛₗ₂'
@[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}
[CommSemiring R]
[Semiring R₁]
[Semiring 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
@[simp]
theorem
Matrix.toLinearMap₂'_toMatrix'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
:
Matrix.toLinearMap₂' (LinearMap.toMatrix₂' B) = B
@[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}
[CommSemiring R]
[Semiring R₁]
[Semiring R₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(σ₁ : R₁ →+* R)
(σ₂ : R₂ →+* R)
(M : Matrix n m R)
:
LinearMap.toMatrixₛₗ₂' ((Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M) = M
@[simp]
theorem
LinearMap.toMatrix'_toLinearMap₂'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m R)
:
LinearMap.toMatrix₂' (Matrix.toLinearMap₂' M) = M
@[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}
[CommSemiring R]
[Semiring R₁]
[Semiring 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 : n) => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1)
@[simp]
theorem
LinearMap.toMatrix₂'_apply
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring 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 : n) => R) i) 1)) ((LinearMap.stdBasis R (fun (x : m) => R) j) 1)
@[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}
[CommSemiring 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
theorem
LinearMap.toMatrix₂'_comp
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{n' : Type u_11}
[CommSemiring 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₂' (B ∘ₗ f) = Matrix.transpose (LinearMap.toMatrix' f) * LinearMap.toMatrix₂' B
theorem
LinearMap.toMatrix₂'_compl₂
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{m' : Type u_12}
[CommSemiring 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
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}
[CommSemiring 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))
theorem
LinearMap.mul_toMatrix'
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{n' : Type u_11}
[CommSemiring 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₂' (B ∘ₗ Matrix.toLin' (Matrix.transpose M))
theorem
LinearMap.toMatrix₂'_mul
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{m' : Type u_12}
[CommSemiring 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))
theorem
Matrix.toLinearMap₂'_comp
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
{n' : Type u_11}
{m' : Type u_12}
[CommSemiring 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.
noncomputable def
LinearMap.toMatrix₂
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[CommSemiring 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₂)
:
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
noncomputable def
Matrix.toLinearMap₂
{R : Type u_1}
{M₁ : Type u_5}
{M₂ : Type u_6}
{n : Type u_9}
{m : Type u_10}
[CommSemiring 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.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
@[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}
[CommSemiring 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)
@[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}
[CommSemiring 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 : n) => Finset.sum Finset.univ fun (j : m) => (b₁.repr x) i * M i j * (b₂.repr y) j
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}
[CommSemiring 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
@[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}
[CommSemiring 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₂
@[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}
[CommSemiring 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₂
theorem
Matrix.toLinearMap₂_basisFun
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
:
Matrix.toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLinearMap₂'
theorem
LinearMap.toMatrix₂_basisFun
{R : Type u_1}
{n : Type u_9}
{m : Type u_10}
[CommSemiring R]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
:
LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = LinearMap.toMatrix₂'
@[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}
[CommSemiring 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
@[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}
[CommSemiring 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
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}
[CommSemiring 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
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}
[CommSemiring 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₂) (B ∘ₗ f) = Matrix.transpose ((LinearMap.toMatrix b₁' b₁) f) * (LinearMap.toMatrix₂ b₁ b₂) B
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}
[CommSemiring 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
@[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}
[CommSemiring 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
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}
[CommSemiring 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))
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}
[CommSemiring 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₂) (B ∘ₗ (Matrix.toLin b₁' b₁) (Matrix.transpose M))
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}
[CommSemiring 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))
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}
[CommSemiring 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 #
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)
:
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
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)
:
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
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)
:
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
@[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'
@[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'
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)
(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⁻¹)
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]
:
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
@[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₁
def
selfAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_9}
[CommRing R]
[Fintype n]
(J : Matrix n n R)
[DecidableEq n]
:
The submodule of self-adjoint matrices with respect to the bilinear form corresponding to
the matrix J.
Equations
Instances For
@[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₁
def
skewAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_9}
[CommRing R]
[Fintype n]
(J : Matrix n n R)
[DecidableEq n]
:
The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to
the matrix J.
Equations
Instances For
@[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 #
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)
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)
@[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
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)
@[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₁)
:
@[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
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)
@[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₁)
:
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)
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
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)
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
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)
: