Sesquilinear form #
This file defines the conversion between sesquilinear maps and matrices.
Main definitions #
Matrix.toLinearMap₂given a basis define a bilinear mapMatrix.toLinearMap₂'define the bilinear map onn → RLinearMap.toMatrix₂: calculate the matrix coefficients of a bilinear mapLinearMap.toMatrix₂': calculate the matrix coefficients of a bilinear map onn → R
TODO #
At the moment this is quite a literal port from Matrix.BilinearForm. Everything should be
generalized to fully semibilinear forms.
Tags #
Sesquilinear form, Sesquilinear map, matrix, basis
def
Matrix.toLinearMap₂'Aux
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[Semiring R₁]
[Semiring S₁]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid N₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
(f : Matrix n m N₂)
:
The map from Matrix n n R to bilinear maps on n → R.
This is an auxiliary definition for the equivalence Matrix.toLinearMap₂'.
Equations
- Matrix.toLinearMap₂'Aux σ₁ σ₂ f = LinearMap.mk₂'ₛₗ σ₁ σ₂ (fun (v : n → R₁) (w : m → R₂) => ∑ i : n, ∑ j : m, σ₂ (w j) • σ₁ (v i) • f i j) ⋯ ⋯ ⋯ ⋯
Instances For
theorem
Matrix.toLinearMap₂'Aux_stdBasis
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[Semiring R₁]
[Semiring S₁]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid N₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[DecidableEq n]
[DecidableEq m]
(f : Matrix n m N₂)
(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}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[Semiring R₁]
[Semiring S₁]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid M₁]
[Module R₁ M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
[AddCommMonoid N₂]
[Module R N₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
{σ₁ : R₁ →+* S₁}
{σ₂ : R₂ →+* S₂}
(b₁ : n → M₁)
(b₂ : m → M₂)
:
The linear map from sesquilinear maps to Matrix n m N₂ 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
Instances For
@[simp]
theorem
LinearMap.toMatrix₂Aux_apply
(R : Type u_1)
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[Semiring R₁]
[Semiring S₁]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid M₁]
[Module R₁ M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
[AddCommMonoid N₂]
[Module R N₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
{σ₁ : R₁ →+* S₁}
{σ₂ : R₂ →+* S₂}
(f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂)
(b₁ : n → M₁)
(b₂ : m → M₂)
(i : n)
(j : m)
:
(LinearMap.toMatrix₂Aux R b₁ b₂) f i j = (f (b₁ i)) (b₂ j)
theorem
LinearMap.toLinearMap₂'Aux_toMatrix₂Aux
(R : Type u_1)
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[Semiring R₁]
[Semiring S₁]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid N₂]
[Module R N₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
{σ₁ : R₁ →+* S₁}
{σ₂ : R₂ →+* S₂}
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
:
Matrix.toLinearMap₂'Aux σ₁ σ₂
((LinearMap.toMatrix₂Aux R (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}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[Semiring R₁]
[Semiring S₁]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid N₂]
[Module R N₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
{σ₁ : R₁ →+* S₁}
{σ₂ : R₂ →+* S₂}
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(f : Matrix n m N₂)
:
(LinearMap.toMatrix₂Aux R (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 maps over n → R #
This section deals with the conversion between matrices and sesquilinear maps on n → R.
def
LinearMap.toMatrixₛₗ₂'
(R : Type u_1)
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
{σ₁ : R₁ →+* S₁}
{σ₂ : R₂ →+* S₂}
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
The linear equivalence between sesquilinear maps 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)
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
The linear equivalence between bilinear maps and n × m matrices
Equations
Instances For
def
Matrix.toLinearMapₛₗ₂'
(R : Type u_1)
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
The linear equivalence between n × n matrices and sesquilinear maps on n → R
Equations
- Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ = (LinearMap.toMatrixₛₗ₂' R).symm
Instances For
def
Matrix.toLinearMap₂'
(R : Type u_1)
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
The linear equivalence between n × n matrices and bilinear maps on n → R
Equations
- Matrix.toLinearMap₂' R = (LinearMap.toMatrix₂' R).symm
Instances For
theorem
Matrix.toLinearMapₛₗ₂'_aux_eq
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
:
Matrix.toLinearMap₂'Aux σ₁ σ₂ M = (Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M
theorem
Matrix.toLinearMapₛₗ₂'_apply
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
(x : n → R₁)
(y : m → R₂)
:
(((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) x) y = ∑ i : n, ∑ j : m, σ₁ (x i) • σ₂ (y j) • M i j
theorem
Matrix.toLinearMap₂'_apply
{R : Type u_1}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
(x : n → S₁)
(y : m → S₂)
:
(((Matrix.toLinearMap₂' R) M) x) y = ∑ i : n, ∑ j : m, x i • y j • M i j
theorem
Matrix.toLinearMap₂'_apply'
{n : Type u_12}
{m : Type u_13}
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
{T : Type u_17}
[CommSemiring T]
(M : Matrix n m T)
(v : n → T)
(w : m → T)
:
(((Matrix.toLinearMap₂' T) M) v) w = Matrix.dotProduct v (M.mulVec w)
@[simp]
theorem
Matrix.toLinearMapₛₗ₂'_stdBasis
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
(i : n)
(j : m)
:
(((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) 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_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[SMulCommClass R R N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
(i : n)
(j : m)
:
(((Matrix.toLinearMap₂' R) 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}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
(LinearMap.toMatrixₛₗ₂' R).symm = Matrix.toLinearMapₛₗ₂' R σ₁ σ₂
@[simp]
theorem
Matrix.toLinearMapₛₗ₂'_symm
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
:
(Matrix.toLinearMapₛₗ₂' R σ₁ σ₂).symm = LinearMap.toMatrixₛₗ₂' R
@[simp]
theorem
Matrix.toLinearMapₛₗ₂'_toMatrix'
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
:
(Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) ((LinearMap.toMatrixₛₗ₂' R) B) = B
@[simp]
theorem
Matrix.toLinearMap₂'_toMatrix'
{R : Type u_1}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂)
:
(Matrix.toLinearMap₂' R) ((LinearMap.toMatrix₂' R) B) = B
@[simp]
theorem
LinearMap.toMatrix'_toLinearMapₛₗ₂'
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
:
(LinearMap.toMatrixₛₗ₂' R) ((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) = M
@[simp]
theorem
LinearMap.toMatrix'_toLinearMap₂'
{R : Type u_1}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
:
(LinearMap.toMatrix₂' R) ((Matrix.toLinearMap₂' R) M) = M
@[simp]
theorem
LinearMap.toMatrixₛₗ₂'_apply
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring R₁]
[Semiring R₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
(σ₁ : R₁ →+* S₁)
(σ₂ : R₂ →+* S₂)
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂)
(i : n)
(j : m)
:
(LinearMap.toMatrixₛₗ₂' R) 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}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Semiring S₁]
[Semiring S₂]
[Module S₁ N₂]
[Module S₂ N₂]
[SMulCommClass S₁ R N₂]
[SMulCommClass S₂ R N₂]
[SMulCommClass S₂ S₁ N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂)
(i : n)
(j : m)
:
(LinearMap.toMatrix₂' R) B i j = (B ((LinearMap.stdBasis S₁ (fun (x : n) => S₁) i) 1)) ((LinearMap.stdBasis S₂ (fun (x : m) => S₂) j) 1)
@[simp]
theorem
LinearMap.toMatrix₂'_compl₁₂
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{m' : Type u_15}
{R : Type u_17}
[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₂' R) (B.compl₁₂ l r) = (LinearMap.toMatrix' l).transpose * (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' r
theorem
LinearMap.toMatrix₂'_comp
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{R : Type u_17}
[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₂' R) (B ∘ₗ f) = (LinearMap.toMatrix' f).transpose * (LinearMap.toMatrix₂' R) B
theorem
LinearMap.toMatrix₂'_compl₂
{n : Type u_12}
{m : Type u_13}
{m' : Type u_15}
{R : Type u_17}
[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₂' R) (B.compl₂ f) = (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' f
theorem
LinearMap.mul_toMatrix₂'_mul
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{m' : Type u_15}
{R : Type u_17}
[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₂' R) B * N = (LinearMap.toMatrix₂' R) (B.compl₁₂ (Matrix.toLin' M.transpose) (Matrix.toLin' N))
theorem
LinearMap.mul_toMatrix'
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{R : Type u_17}
[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₂' R) B = (LinearMap.toMatrix₂' R) (B ∘ₗ Matrix.toLin' M.transpose)
theorem
LinearMap.toMatrix₂'_mul
{n : Type u_12}
{m : Type u_13}
{m' : Type u_15}
{R : Type u_17}
[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₂' R) B * M = (LinearMap.toMatrix₂' R) (B.compl₂ (Matrix.toLin' M))
theorem
Matrix.toLinearMap₂'_comp
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{m' : Type u_15}
{R : Type u_17}
[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)
:
((Matrix.toLinearMap₂' R) M).compl₁₂ (Matrix.toLin' P) (Matrix.toLin' Q) = (Matrix.toLinearMap₂' R) (P.transpose * M * Q)
Bilinear maps over arbitrary vector spaces #
This section deals with the conversion between matrices and bilinear maps on a module with a fixed basis.
noncomputable def
LinearMap.toMatrix₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[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 maps 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₂ = (b₁.equivFun.arrowCongr (b₂.equivFun.arrowCongr (LinearEquiv.refl R N₂))).trans (LinearMap.toMatrix₂' R)
Instances For
noncomputable def
Matrix.toLinearMap₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[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 maps 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₂ = (LinearMap.toMatrix₂ b₁ b₂).symm
Instances For
@[simp]
theorem
LinearMap.toMatrix₂_apply
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Basis n R M₁)
(b₂ : Basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] N₂)
(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_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Basis n R M₁)
(b₂ : Basis m R M₂)
(M : Matrix n m N₂)
(x : M₁)
(y : M₂)
:
(((Matrix.toLinearMap₂ b₁ b₂) M) x) y = ∑ i : n, ∑ j : m, (b₁.repr x) i • (b₂.repr y) j • M i j
theorem
LinearMap.toMatrix₂Aux_eq
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Basis n R M₁)
(b₂ : Basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] N₂)
:
(LinearMap.toMatrix₂Aux R ⇑b₁ ⇑b₂) B = (LinearMap.toMatrix₂ b₁ b₂) B
@[simp]
theorem
LinearMap.toMatrix₂_symm
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Basis n R M₁)
(b₂ : Basis m R M₂)
:
(LinearMap.toMatrix₂ b₁ b₂).symm = Matrix.toLinearMap₂ b₁ b₂
@[simp]
theorem
Matrix.toLinearMap₂_symm
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Basis n R M₁)
(b₂ : Basis m R M₂)
:
(Matrix.toLinearMap₂ b₁ b₂).symm = LinearMap.toMatrix₂ b₁ b₂
theorem
Matrix.toLinearMap₂_basisFun
{R : Type u_1}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
:
Matrix.toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLinearMap₂' R
theorem
LinearMap.toMatrix₂_basisFun
{R : Type u_1}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
:
LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = LinearMap.toMatrix₂' R
@[simp]
theorem
Matrix.toLinearMap₂_toMatrix₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Basis n R M₁)
(b₂ : Basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] N₂)
:
(Matrix.toLinearMap₂ b₁ b₂) ((LinearMap.toMatrix₂ b₁ b₂) B) = B
@[simp]
theorem
LinearMap.toMatrix₂_toLinearMap₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{N₂ : Type u_11}
{n : Type u_12}
{m : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Basis n R M₁)
(b₂ : Basis m R M₂)
(M : Matrix n m N₂)
:
(LinearMap.toMatrix₂ b₁ b₂) ((Matrix.toLinearMap₂ b₁ b₂) M) = M
theorem
LinearMap.toMatrix₂_compl₁₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₁' : Type u_9}
{M₂' : Type u_10}
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{m' : Type u_15}
[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₂') (B.compl₁₂ l r) = ((LinearMap.toMatrix b₁' b₁) l).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) r
theorem
LinearMap.toMatrix₂_comp
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₁' : Type u_9}
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
[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) = ((LinearMap.toMatrix b₁' b₁) f).transpose * (LinearMap.toMatrix₂ b₁ b₂) B
theorem
LinearMap.toMatrix₂_compl₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₂' : Type u_10}
{n : Type u_12}
{m : Type u_13}
{m' : Type u_15}
[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₂') (B.compl₂ 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_7}
{M₂ : Type u_8}
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{m' : Type u_15}
[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)
:
(b₁.toMatrix ⇑c₁).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (LinearMap.toMatrix₂ c₁ c₂) B
theorem
LinearMap.mul_toMatrix₂_mul
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₁' : Type u_9}
{M₂' : Type u_10}
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{m' : Type u_15}
[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₂') (B.compl₁₂ ((Matrix.toLin b₁' b₁) M.transpose) ((Matrix.toLin b₂' b₂) N))
theorem
LinearMap.mul_toMatrix₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₁' : Type u_9}
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
[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₁) M.transpose)
theorem
LinearMap.toMatrix₂_mul
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₂' : Type u_10}
{n : Type u_12}
{m : Type u_13}
{m' : Type u_15}
[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₂') (B.compl₂ ((Matrix.toLin b₂' b₂) M))
theorem
Matrix.toLinearMap₂_compl₁₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₁' : Type u_9}
{M₂' : Type u_10}
{n : Type u_12}
{m : Type u_13}
{n' : Type u_14}
{m' : Type u_15}
[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)
:
((Matrix.toLinearMap₂ b₁ b₂) M).compl₁₂ ((Matrix.toLin b₁' b₁) P) ((Matrix.toLin b₂' b₂) Q) = (Matrix.toLinearMap₂ b₁' b₂') (P.transpose * M * Q)
Adjoint pairs #
def
Matrix.IsAdjointPair
{R : Type u_1}
{n : Type u_12}
{n' : Type u_14}
[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₃.
Instances For
@[simp]
theorem
isAdjointPair_toLinearMap₂'
{R : Type u_1}
{n : Type u_12}
{n' : Type u_14}
[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']
:
((Matrix.toLinearMap₂' R) J).IsAdjointPair ((Matrix.toLinearMap₂' R) J') (Matrix.toLin' A) (Matrix.toLin' A') ↔ J.IsAdjointPair J' A A'
@[simp]
theorem
isAdjointPair_toLinearMap₂
{R : Type u_1}
{M₁ : Type u_7}
{M₂ : Type u_8}
{n : Type u_12}
{n' : Type u_14}
[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']
:
((Matrix.toLinearMap₂ b₁ b₁) J).IsAdjointPair ((Matrix.toLinearMap₂ b₂ b₂) J') ((Matrix.toLin b₁ b₂) A)
((Matrix.toLin b₂ b₁) A') ↔ J.IsAdjointPair J' A A'
def
pairSelfAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_12}
[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') (((Matrix.toLinearMap₂' R) J).isPairSelfAdjointSubmodule ((Matrix.toLinearMap₂' R) J₂))
Instances For
@[simp]
theorem
mem_pairSelfAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_12}
[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₂ ↔ J.IsAdjointPair J₂ A₁ A₁
def
selfAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_12}
[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_12}
[CommRing R]
[Fintype n]
(J : Matrix n n R)
(A₁ : Matrix n n R)
[DecidableEq n]
:
A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁
def
skewAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_12}
[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_12}
[CommRing R]
[Fintype n]
(J : Matrix n n R)
(A₁ : Matrix n n R)
[DecidableEq n]
:
A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁
Nondegenerate bilinear forms #
theorem
Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂
{R₁ : Type u_2}
{M₁ : Type u_7}
{ι : Type u_16}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(b : Basis ι R₁ M₁)
:
((Matrix.toLinearMap₂' R₁) M).SeparatingLeft ↔ ((Matrix.toLinearMap₂ b b) M).SeparatingLeft
theorem
Matrix.Nondegenerate.toLinearMap₂'
{R₁ : Type u_2}
{ι : Type u_16}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(h : M.Nondegenerate)
:
((Matrix.toLinearMap₂' R₁) M).SeparatingLeft
@[simp]
theorem
Matrix.separatingLeft_toLinearMap₂'_iff
{R₁ : Type u_2}
{ι : Type u_16}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
:
((Matrix.toLinearMap₂' R₁) M).SeparatingLeft ↔ M.Nondegenerate
theorem
Matrix.Nondegenerate.toLinearMap₂
{R₁ : Type u_2}
{M₁ : Type u_7}
{ι : Type u_16}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(h : M.Nondegenerate)
(b : Basis ι R₁ M₁)
:
((Matrix.toLinearMap₂ b b) M).SeparatingLeft
@[simp]
theorem
Matrix.separatingLeft_toLinearMap₂_iff
{R₁ : Type u_2}
{M₁ : Type u_7}
{ι : Type u_16}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(b : Basis ι R₁ M₁)
:
((Matrix.toLinearMap₂ b b) M).SeparatingLeft ↔ M.Nondegenerate
@[simp]
theorem
LinearMap.nondegenerate_toMatrix₂'_iff
{R₁ : Type u_2}
{ι : Type u_16}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
{B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁}
:
((LinearMap.toMatrix₂' R₁) B).Nondegenerate ↔ B.SeparatingLeft
theorem
LinearMap.SeparatingLeft.toMatrix₂'
{R₁ : Type u_2}
{ι : Type u_16}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
{B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁}
(h : B.SeparatingLeft)
:
((LinearMap.toMatrix₂' R₁) B).Nondegenerate
@[simp]
theorem
LinearMap.nondegenerate_toMatrix_iff
{R₁ : Type u_2}
{M₁ : Type u_7}
{ι : Type u_16}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : Basis ι R₁ M₁)
:
((LinearMap.toMatrix₂ b b) B).Nondegenerate ↔ B.SeparatingLeft
theorem
LinearMap.SeparatingLeft.toMatrix₂
{R₁ : Type u_2}
{M₁ : Type u_7}
{ι : Type u_16}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(h : B.SeparatingLeft)
(b : Basis ι R₁ M₁)
:
((LinearMap.toMatrix₂ b b) B).Nondegenerate
theorem
LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero
{R₁ : Type u_2}
{ι : Type u_16}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
[IsDomain R₁]
{M : Matrix ι ι R₁}
:
((Matrix.toLinearMap₂' R₁) M).SeparatingLeft ↔ M.det ≠ 0
theorem
LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero'
{R₁ : Type u_2}
{ι : Type u_16}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
[IsDomain R₁]
(M : Matrix ι ι R₁)
(h : M.det ≠ 0)
:
((Matrix.toLinearMap₂' R₁) M).SeparatingLeft
theorem
LinearMap.separatingLeft_iff_det_ne_zero
{R₁ : Type u_2}
{M₁ : Type u_7}
{ι : Type u_16}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
[IsDomain R₁]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : Basis ι R₁ M₁)
:
B.SeparatingLeft ↔ ((LinearMap.toMatrix₂ b b) B).det ≠ 0
theorem
LinearMap.separatingLeft_of_det_ne_zero
{R₁ : Type u_2}
{M₁ : Type u_7}
{ι : Type u_16}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
[IsDomain R₁]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : Basis ι R₁ M₁)
(h : ((LinearMap.toMatrix₂ b b) B).det ≠ 0)
:
B.SeparatingLeft