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_10}
{n : Type u_11}
{m : Type u_12}
[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
Instances For
theorem
Matrix.toLinearMap₂'Aux_single
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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)
:
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_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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)
:
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_10}
{n : Type u_11}
{m : Type u_12}
[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 σ₁ σ₂ ((toMatrix₂Aux R (fun (i : n) => Pi.single i 1) fun (j : m) => Pi.single 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_10}
{n : Type u_11}
{m : Type u_12}
[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) => Pi.single i 1) fun (j : m) => Pi.single j 1) (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_10}
{n : Type u_11}
{m : Type u_12}
[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
Instances For
def
LinearMap.toMatrix₂'
(R : Type u_1)
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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_10}
{n : Type u_11}
{m : Type u_12}
[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
Instances For
def
Matrix.toLinearMap₂'
(R : Type u_1)
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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
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_10}
{n : Type u_11}
{m : Type u_12}
[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₂)
:
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_10}
{n : Type u_11}
{m : Type u_12}
[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₂)
:
theorem
Matrix.toLinearMap₂'_apply
{R : Type u_1}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₂)
:
theorem
Matrix.toLinearMap₂'_apply'
{n : Type u_11}
{m : Type u_12}
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
{T : Type u_16}
[CommSemiring T]
(M : Matrix n m T)
(v : n → T)
(w : m → T)
:
@[simp]
theorem
Matrix.toLinearMapₛₗ₂'_single
{R : Type u_1}
{R₁ : Type u_2}
{S₁ : Type u_3}
{R₂ : Type u_4}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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)
:
@[simp]
theorem
Matrix.toLinearMap₂'_single
{R : Type u_1}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[Fintype n]
[Fintype m]
[DecidableEq n]
[DecidableEq m]
(M : Matrix n m N₂)
(i : n)
(j : m)
:
@[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_10}
{n : Type u_11}
{m : Type u_12}
[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]
:
@[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_10}
{n : Type u_11}
{m : Type u_12}
[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]
:
@[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_10}
{n : Type u_11}
{m : Type u_12}
[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₂)
:
@[simp]
theorem
Matrix.toLinearMap₂'_toMatrix'
{R : Type u_1}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₂)
:
@[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_10}
{n : Type u_11}
{m : Type u_12}
[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₂)
:
@[simp]
theorem
LinearMap.toMatrix'_toLinearMap₂'
{R : Type u_1}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₂)
:
@[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_10}
{n : Type u_11}
{m : Type u_12}
[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)
:
@[simp]
theorem
LinearMap.toMatrix₂'_apply
{R : Type u_1}
{S₁ : Type u_3}
{S₂ : Type u_5}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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)
:
@[simp]
theorem
LinearMap.toMatrix₂'_compl₁₂
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{m' : Type u_14}
{R : Type u_16}
[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)
:
theorem
LinearMap.toMatrix₂'_comp
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{R : Type u_16}
[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)
:
theorem
LinearMap.toMatrix₂'_compl₂
{n : Type u_11}
{m : Type u_12}
{m' : Type u_14}
{R : Type u_16}
[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)
:
theorem
LinearMap.mul_toMatrix₂'_mul
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{m' : Type u_14}
{R : Type u_16}
[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)
:
theorem
LinearMap.mul_toMatrix'
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{R : Type u_16}
[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)
:
theorem
LinearMap.toMatrix₂'_mul
{n : Type u_11}
{m : Type u_12}
{m' : Type u_14}
{R : Type u_16}
[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)
:
theorem
Matrix.toLinearMap₂'_comp
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{m' : Type u_14}
{R : Type u_16}
[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)
:
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_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.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
Instances For
noncomputable def
Matrix.toLinearMap₂
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.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
Instances For
@[simp]
theorem
LinearMap.toMatrix₂_apply
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] N₂)
(i : n)
(j : m)
:
@[simp]
theorem
Matrix.toLinearMap₂_apply
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
(M : Matrix n m N₂)
(x : M₁)
(y : M₂)
:
theorem
LinearMap.toMatrix₂Aux_eq
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] N₂)
:
@[simp]
theorem
LinearMap.toMatrix₂_symm
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
:
@[simp]
theorem
Matrix.toLinearMap₂_symm
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
:
theorem
Matrix.toLinearMap₂_basisFun
{R : Type u_1}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
:
theorem
LinearMap.toMatrix₂_basisFun
{R : Type u_1}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[CommSemiring R]
[AddCommMonoid N₂]
[Module R N₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
:
@[simp]
theorem
Matrix.toLinearMap₂_toMatrix₂
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] N₂)
:
@[simp]
theorem
LinearMap.toMatrix₂_toLinearMap₂
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_10}
{n : Type u_11}
{m : Type u_12}
[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₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
(M : Matrix n m N₂)
:
theorem
LinearMap.toMatrix₂_compl₁₂
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{M₁' : Type u_8}
{M₂' : Type u_9}
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{m' : Type u_14}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[AddCommMonoid M₁']
[Module R M₁']
[AddCommMonoid M₂']
[Module R M₂']
(b₁' : Module.Basis n' R M₁')
(b₂' : Module.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₂)
:
theorem
LinearMap.toMatrix₂_comp
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{M₁' : Type u_8}
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[AddCommMonoid M₁']
[Module R M₁']
(b₁' : Module.Basis n' R M₁')
[Fintype n']
[DecidableEq n']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(f : M₁' →ₗ[R] M₁)
:
theorem
LinearMap.toMatrix₂_compl₂
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{M₂' : Type u_9}
{n : Type u_11}
{m : Type u_12}
{m' : Type u_14}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[AddCommMonoid M₂']
[Module R M₂']
(b₂' : Module.Basis m' R M₂')
[Fintype m']
[DecidableEq m']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(f : M₂' →ₗ[R] M₂)
:
@[simp]
theorem
LinearMap.toMatrix₂_mul_basis_toMatrix
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{m' : Type u_14}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[Fintype n']
[Fintype m']
[DecidableEq n']
[DecidableEq m']
(c₁ : Module.Basis n' R M₁)
(c₂ : Module.Basis m' R M₂)
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
:
theorem
LinearMap.mul_toMatrix₂_mul
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{M₁' : Type u_8}
{M₂' : Type u_9}
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{m' : Type u_14}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[AddCommMonoid M₁']
[Module R M₁']
[AddCommMonoid M₂']
[Module R M₂']
(b₁' : Module.Basis n' R M₁')
(b₂' : Module.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 * (toMatrix₂ b₁ b₂) B * N = (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_6}
{M₂ : Type u_7}
{M₁' : Type u_8}
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[AddCommMonoid M₁']
[Module R M₁']
(b₁' : Module.Basis n' R M₁')
[Fintype n']
[DecidableEq n']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(M : Matrix n' n R)
:
theorem
LinearMap.toMatrix₂_mul
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{M₂' : Type u_9}
{n : Type u_11}
{m : Type u_12}
{m' : Type u_14}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[AddCommMonoid M₂']
[Module R M₂']
(b₂' : Module.Basis m' R M₂')
[Fintype m']
[DecidableEq m']
(B : M₁ →ₗ[R] M₂ →ₗ[R] R)
(M : Matrix m m' R)
:
theorem
Matrix.toLinearMap₂_compl₁₂
{R : Type u_1}
{M₁ : Type u_6}
{M₂ : Type u_7}
{M₁' : Type u_8}
{M₂' : Type u_9}
{n : Type u_11}
{m : Type u_12}
{n' : Type u_13}
{m' : Type u_14}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
(b₁ : Module.Basis n R M₁)
(b₂ : Module.Basis m R M₂)
[AddCommMonoid M₁']
[Module R M₁']
[AddCommMonoid M₂']
[Module R M₂']
(b₁' : Module.Basis n' R M₁')
(b₂' : Module.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)
:
((toLinearMap₂ b₁ b₂) M).compl₁₂ ((toLin b₁' b₁) P) ((toLin b₂' b₂) Q) = (toLinearMap₂ b₁' b₂') (P.transpose * M * Q)
Adjoint pairs #
def
Matrix.IsAdjointPair
{R : Type u_1}
{n : Type u_11}
{n' : Type u_13}
[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
Instances For
@[simp]
theorem
isAdjointPair_toLinearMap₂'
{R : Type u_1}
{n : Type u_11}
{n' : Type u_13}
[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_6}
{M₂ : Type u_7}
{n : Type u_11}
{n' : Type u_13}
[CommRing R]
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[Fintype n]
[Fintype n']
(b₁ : Module.Basis n R M₁)
(b₂ : Module.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_11}
[CommRing R]
[Fintype n]
(J 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
Instances For
@[simp]
theorem
mem_pairSelfAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_11}
[CommRing R]
[Fintype n]
(J J₂ A₁ : Matrix n n R)
[DecidableEq n]
:
def
selfAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_11}
[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_11}
[CommRing R]
[Fintype n]
(J A₁ : Matrix n n R)
[DecidableEq n]
:
def
skewAdjointMatricesSubmodule
{R : Type u_1}
{n : Type u_11}
[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_11}
[CommRing R]
[Fintype n]
(J A₁ : Matrix n n R)
[DecidableEq n]
:
Nondegenerate bilinear forms #
theorem
Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂
{R₁ : Type u_2}
{M₁ : Type u_6}
{ι : Type u_15}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(b : Module.Basis ι R₁ M₁)
:
theorem
Matrix.Nondegenerate.toLinearMap₂'
{R₁ : Type u_2}
{ι : Type u_15}
[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_15}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
:
theorem
Matrix.Nondegenerate.toLinearMap₂
{R₁ : Type u_2}
{M₁ : Type u_6}
{ι : Type u_15}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(h : M.Nondegenerate)
(b : Module.Basis ι R₁ M₁)
:
((Matrix.toLinearMap₂ b b) M).SeparatingLeft
@[simp]
theorem
Matrix.separatingLeft_toLinearMap₂_iff
{R₁ : Type u_2}
{M₁ : Type u_6}
{ι : Type u_15}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(b : Module.Basis ι R₁ M₁)
:
@[simp]
theorem
LinearMap.nondegenerate_toMatrix₂'_iff
{R₁ : Type u_2}
{ι : Type u_15}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
{B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁}
:
theorem
LinearMap.SeparatingLeft.toMatrix₂'
{R₁ : Type u_2}
{ι : Type u_15}
[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_6}
{ι : Type u_15}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : Module.Basis ι R₁ M₁)
:
theorem
LinearMap.SeparatingLeft.toMatrix₂
{R₁ : Type u_2}
{M₁ : Type u_6}
{ι : Type u_15}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(h : B.SeparatingLeft)
(b : Module.Basis ι R₁ M₁)
:
((LinearMap.toMatrix₂ b b) B).Nondegenerate
theorem
LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero
{R₁ : Type u_2}
{ι : Type u_15}
[CommRing R₁]
[DecidableEq ι]
[Fintype ι]
[IsDomain R₁]
{M : Matrix ι ι R₁}
:
theorem
LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero'
{R₁ : Type u_2}
{ι : Type u_15}
[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_6}
{ι : Type u_15}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
[IsDomain R₁]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : Module.Basis ι R₁ M₁)
:
theorem
LinearMap.separatingLeft_of_det_ne_zero
{R₁ : Type u_2}
{M₁ : Type u_6}
{ι : Type u_15}
[CommRing R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[DecidableEq ι]
[Fintype ι]
[IsDomain R₁]
{B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁}
(b : Module.Basis ι R₁ M₁)
(h : ((toMatrix₂ b b) B).det ≠ 0)
: