Bilinear form #
This file defines the conversion between bilinear forms and matrices.
Main definitions #
Matrix.toBilingiven a basis define a bilinear formMatrix.toBilin'define the bilinear form onn → RBilinForm.toMatrix: calculate the matrix coefficients of a bilinear formBilinForm.toMatrix': calculate the matrix coefficients of a bilinear form onn → R
Notation #
In this file we use the following type variables:
M₁is a module over the commutative semiringR₁,M₂is a module over the commutative ringR₂.
Tags #
bilinear form, bilin form, BilinearForm, matrix, basis
def
Matrix.toBilin'Aux
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
(M : Matrix n n R₁)
:
LinearMap.BilinForm R₁ (n → R₁)
The map from Matrix n n R to bilinear forms on n → R.
This is an auxiliary definition for the equivalence Matrix.toBilin'.
Equations
- M.toBilin'Aux = Matrix.toLinearMap₂'Aux (RingHom.id R₁) (RingHom.id R₁) M
Instances For
theorem
Matrix.toBilin'Aux_single
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₁)
(i j : n)
:
def
BilinForm.toMatrixAux
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
(b : n → M₁)
:
The linear map from bilinear forms to Matrix n n R given an n-indexed basis.
This is an auxiliary definition for the equivalence Matrix.toBilin'.
Equations
- BilinForm.toMatrixAux b = LinearMap.toMatrix₂Aux R₁ b b
Instances For
@[simp]
theorem
LinearMap.BilinForm.toMatrixAux_apply
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
(B : LinearMap.BilinForm R₁ M₁)
(b : n → M₁)
(i j : n)
:
theorem
toBilin'Aux_toMatrixAux
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(B₂ : LinearMap.BilinForm R₁ (n → R₁))
:
ToMatrix' section #
This section deals with the conversion between matrices and bilinear forms on n → R₂.
def
LinearMap.BilinForm.toMatrix'
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
:
The linear equivalence between bilinear forms on n → R and n × n matrices
Equations
Instances For
The linear equivalence between n × n matrices and bilinear forms on n → R
Instances For
@[simp]
theorem
Matrix.toBilin'Aux_eq
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₁)
:
theorem
Matrix.toBilin'_apply
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₁)
(x y : n → R₁)
:
theorem
Matrix.toBilin'_apply'
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₁)
(v w : n → R₁)
:
@[simp]
theorem
Matrix.toBilin'_single
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₁)
(i j : n)
:
@[simp]
theorem
LinearMap.BilinForm.toMatrix'_symm
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
:
@[simp]
theorem
Matrix.toBilin'_symm
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
:
@[simp]
theorem
Matrix.toBilin'_toMatrix'
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(B : LinearMap.BilinForm R₁ (n → R₁))
:
@[simp]
theorem
LinearMap.BilinForm.toMatrix'_toBilin'
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₁)
:
@[simp]
theorem
LinearMap.BilinForm.toMatrix'_apply
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(B : LinearMap.BilinForm R₁ (n → R₁))
(i j : n)
:
@[simp]
theorem
LinearMap.BilinForm.toMatrix'_comp
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
{o : Type u_6}
[Fintype n]
[Fintype o]
[DecidableEq n]
[DecidableEq o]
(B : LinearMap.BilinForm R₁ (n → R₁))
(l r : (o → R₁) →ₗ[R₁] n → R₁)
:
theorem
LinearMap.BilinForm.toMatrix'_compLeft
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(B : LinearMap.BilinForm R₁ (n → R₁))
(f : (n → R₁) →ₗ[R₁] n → R₁)
:
theorem
LinearMap.BilinForm.toMatrix'_compRight
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(B : LinearMap.BilinForm R₁ (n → R₁))
(f : (n → R₁) →ₗ[R₁] n → R₁)
:
theorem
LinearMap.BilinForm.mul_toMatrix'_mul
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
{o : Type u_6}
[Fintype n]
[Fintype o]
[DecidableEq n]
[DecidableEq o]
(B : LinearMap.BilinForm R₁ (n → R₁))
(M : Matrix o n R₁)
(N : Matrix n o R₁)
:
theorem
LinearMap.BilinForm.mul_toMatrix'
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(B : LinearMap.BilinForm R₁ (n → R₁))
(M : Matrix n n R₁)
:
theorem
LinearMap.BilinForm.toMatrix'_mul
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(B : LinearMap.BilinForm R₁ (n → R₁))
(M : Matrix n n R₁)
:
ToMatrix section #
This section deals with the conversion between matrices and bilinear forms on a module with a fixed basis.
noncomputable def
BilinForm.toMatrix
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
:
BilinForm.toMatrix b is the equivalence between R-bilinear forms on M and
n-by-n matrices with entries in R, if b is an R-basis for M.
Equations
Instances For
noncomputable def
Matrix.toBilin
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
:
BilinForm.toMatrix b is the equivalence between R-bilinear forms on M and
n-by-n matrices with entries in R, if b is an R-basis for M.
Equations
Instances For
@[simp]
theorem
BilinForm.toMatrix_apply
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
(i j : n)
:
theorem
BilinForm.dotProduct_toMatrix_mulVec
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
(x y : n → R₁)
:
theorem
BilinForm.apply_eq_dotProduct_toMatrix_mulVec
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
(x y : M₁)
:
@[simp]
theorem
Matrix.toBilin_apply
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(M : Matrix n n R₁)
(x y : M₁)
:
theorem
BilinearForm.toMatrixAux_eq
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
:
@[simp]
theorem
BilinForm.toMatrix_symm
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
:
@[simp]
theorem
Matrix.toBilin_symm
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
:
theorem
Matrix.toBilin_basisFun
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
:
theorem
BilinForm.toMatrix_basisFun
{R₁ : Type u_1}
[CommSemiring R₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
:
@[simp]
theorem
Matrix.toBilin_toMatrix
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
:
@[simp]
theorem
BilinForm.toMatrix_toBilin
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(M : Matrix n n R₁)
:
theorem
BilinForm.toMatrix_comp
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
{o : Type u_6}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
{M₂' : Type u_7}
[AddCommMonoid M₂']
[Module R₁ M₂']
(c : Module.Basis o R₁ M₂')
[DecidableEq o]
(B : LinearMap.BilinForm R₁ M₁)
(l r : M₂' →ₗ[R₁] M₁)
:
(toMatrix c) (B.comp l r) = ((LinearMap.toMatrix c b) l).transpose * (toMatrix b) B * (LinearMap.toMatrix c b) r
theorem
BilinForm.toMatrix_compLeft
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
(f : M₁ →ₗ[R₁] M₁)
:
theorem
BilinForm.toMatrix_compRight
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
(f : M₁ →ₗ[R₁] M₁)
:
@[simp]
theorem
BilinForm.toMatrix_mul_basis_toMatrix
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
{o : Type u_6}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
[DecidableEq o]
(c : Module.Basis o R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
:
theorem
BilinForm.mul_toMatrix_mul
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
{o : Type u_6}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
{M₂' : Type u_7}
[AddCommMonoid M₂']
[Module R₁ M₂']
(c : Module.Basis o R₁ M₂')
[DecidableEq o]
(B : LinearMap.BilinForm R₁ M₁)
(M : Matrix o n R₁)
(N : Matrix n o R₁)
:
M * (toMatrix b) B * N = (toMatrix c) (B.comp ((Matrix.toLin c b) M.transpose) ((Matrix.toLin c b) N))
theorem
BilinForm.mul_toMatrix
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
(M : Matrix n n R₁)
:
theorem
BilinForm.toMatrix_mul
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
[Fintype n]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
(B : LinearMap.BilinForm R₁ M₁)
(M : Matrix n n R₁)
:
theorem
Matrix.toBilin_comp
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{n : Type u_5}
{o : Type u_6}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Module.Basis n R₁ M₁)
{M₂' : Type u_7}
[AddCommMonoid M₂']
[Module R₁ M₂']
(c : Module.Basis o R₁ M₂')
[DecidableEq o]
(M : Matrix n n R₁)
(P Q : Matrix n o R₁)
:
theorem
mem_pairSelfAdjointMatricesSubmodule'
{R₂ : Type u_3}
[CommRing R₂]
{n : Type u_5}
[Fintype n]
(J J₃ A : Matrix n n R₂)
[DecidableEq n]
:
def
selfAdjointMatricesSubmodule'
{R₂ : Type u_3}
[CommRing R₂]
{n : Type u_5}
[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
theorem
mem_selfAdjointMatricesSubmodule'
{R₂ : Type u_3}
[CommRing R₂]
{n : Type u_5}
[Fintype n]
(J A : Matrix n n R₂)
[DecidableEq n]
:
def
skewAdjointMatricesSubmodule'
{R₂ : Type u_3}
[CommRing R₂]
{n : Type u_5}
[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
theorem
mem_skewAdjointMatricesSubmodule'
{R₂ : Type u_3}
[CommRing R₂]
{n : Type u_5}
[Fintype n]
(J A : Matrix n n R₂)
[DecidableEq n]
:
theorem
Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin
{R₁ : Type u_1}
{M₁ : Type u_2}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₁}
(b : Module.Basis ι R₁ M₁)
:
theorem
Matrix.Nondegenerate.toBilin'
{R₂ : Type u_3}
[CommRing R₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₂}
(h : M.Nondegenerate)
:
@[simp]
theorem
Matrix.nondegenerate_toBilin'_iff
{R₂ : Type u_3}
[CommRing R₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₂}
:
theorem
Matrix.Nondegenerate.toBilin
{R₂ : Type u_3}
{M₂ : Type u_4}
[CommRing R₂]
[AddCommGroup M₂]
[Module R₂ M₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₂}
(h : M.Nondegenerate)
(b : Module.Basis ι R₂ M₂)
:
((Matrix.toBilin b) M).Nondegenerate
@[simp]
theorem
Matrix.nondegenerate_toBilin_iff
{R₂ : Type u_3}
{M₂ : Type u_4}
[CommRing R₂]
[AddCommGroup M₂]
[Module R₂ M₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₂}
(b : Module.Basis ι R₂ M₂)
:
Lemmas transferring nondegeneracy between a bilinear form and its associated matrix
@[simp]
theorem
LinearMap.BilinForm.nondegenerate_toMatrix'_iff
{R₂ : Type u_3}
[CommRing R₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{B : LinearMap.BilinForm R₂ (ι → R₂)}
:
theorem
LinearMap.BilinForm.Nondegenerate.toMatrix'
{R₂ : Type u_3}
[CommRing R₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{B : LinearMap.BilinForm R₂ (ι → R₂)}
(h : B.Nondegenerate)
:
@[simp]
theorem
LinearMap.BilinForm.nondegenerate_toMatrix_iff
{R₂ : Type u_3}
{M₂ : Type u_4}
[CommRing R₂]
[AddCommGroup M₂]
[Module R₂ M₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{B : LinearMap.BilinForm R₂ M₂}
(b : Module.Basis ι R₂ M₂)
:
theorem
LinearMap.BilinForm.Nondegenerate.toMatrix
{R₂ : Type u_3}
{M₂ : Type u_4}
[CommRing R₂]
[AddCommGroup M₂]
[Module R₂ M₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{B : LinearMap.BilinForm R₂ M₂}
(h : B.Nondegenerate)
(b : Module.Basis ι R₂ M₂)
:
((BilinForm.toMatrix b) B).Nondegenerate
Some shorthands for combining the above with Matrix.nondegenerate_of_det_ne_zero
theorem
LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero
{A : Type u_5}
[CommRing A]
[IsDomain A]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι A}
:
theorem
LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero'
{A : Type u_5}
[CommRing A]
[IsDomain A]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
(M : Matrix ι ι A)
(h : M.det ≠ 0)
:
theorem
LinearMap.BilinForm.nondegenerate_iff_det_ne_zero
{M₂ : Type u_4}
[AddCommGroup M₂]
{A : Type u_5}
[CommRing A]
[IsDomain A]
[Module A M₂]
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
{B : LinearMap.BilinForm A M₂}
(b : Module.Basis ι A M₂)
:
theorem
LinearMap.BilinForm.nondegenerate_of_det_ne_zero
{M₂ : Type u_4}
[AddCommGroup M₂]
{A : Type u_5}
[CommRing A]
[IsDomain A]
[Module A M₂]
(B₃ : LinearMap.BilinForm A M₂)
{ι : Type u_6}
[DecidableEq ι]
[Fintype ι]
(b : Module.Basis ι A M₂)
(h : ((BilinForm.toMatrix b) B₃).det ≠ 0)
: