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
Notations #
In this file we use the following type variables:
M,M', ... are modules over the commutative semiringR,M₁,M₁', ... are modules over the commutative ringR₁,M₂,M₂', ... are modules over the commutative semiringR₂,M₃,M₃', ... are modules over the commutative ringR₃,V, ... is a vector space over the fieldK.
Tags #
bilinear form, bilin form, BilinearForm, matrix, basis
def
Matrix.toBilin'Aux
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
(M : Matrix n n R₂)
:
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
- Matrix.toBilin'Aux M = LinearMap.toBilin (Matrix.toLinearMap₂'Aux (RingHom.id R₂) (RingHom.id R₂) M)
theorem
Matrix.toBilin'Aux_stdBasis
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₂)
(i : n)
(j : n)
:
(Matrix.toBilin'Aux M).bilin ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1)
((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) = M i j
def
BilinForm.toMatrixAux
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
(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.comp (LinearMap.toMatrix₂Aux b b) BilinForm.toLinHom
@[simp]
theorem
BilinForm.toMatrixAux_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
(B : BilinForm R₂ M₂)
(b : n → M₂)
(i : n)
(j : n)
:
(BilinForm.toMatrixAux b) B i j = B.bilin (b i) (b j)
theorem
toBilin'Aux_toMatrixAux
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B₂ : BilinForm R₂ (n → R₂))
:
Matrix.toBilin'Aux ((BilinForm.toMatrixAux fun (j : n) => (LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) B₂) = B₂
ToMatrix' section #
This section deals with the conversion between matrices and bilinear forms on n → R₂.
def
BilinForm.toMatrix'
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
:
The linear equivalence between bilinear forms on n → R and n × n matrices
Equations
- BilinForm.toMatrix' = LinearEquiv.trans BilinForm.toLin LinearMap.toMatrix₂'
@[simp]
theorem
BilinForm.toMatrixAux_stdBasis
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B : BilinForm R₂ (n → R₂))
:
(BilinForm.toMatrixAux fun (j : n) => (LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) B = BilinForm.toMatrix' B
The linear equivalence between n × n matrices and bilinear forms on n → R
Equations
- Matrix.toBilin' = LinearEquiv.symm BilinForm.toMatrix'
@[simp]
theorem
Matrix.toBilin'Aux_eq
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₂)
:
Matrix.toBilin'Aux M = Matrix.toBilin' M
theorem
Matrix.toBilin'_apply
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₂)
(x : n → R₂)
(y : n → R₂)
:
(Matrix.toBilin' M).bilin x y = Finset.sum Finset.univ fun (i : n) => Finset.sum Finset.univ fun (j : n) => x i * M i j * y j
theorem
Matrix.toBilin'_apply'
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₂)
(v : n → R₂)
(w : n → R₂)
:
(Matrix.toBilin' M).bilin v w = Matrix.dotProduct v (Matrix.mulVec M w)
@[simp]
theorem
Matrix.toBilin'_stdBasis
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₂)
(i : n)
(j : n)
:
(Matrix.toBilin' M).bilin ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1)
((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) = M i j
@[simp]
theorem
BilinForm.toMatrix'_symm
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
:
LinearEquiv.symm BilinForm.toMatrix' = Matrix.toBilin'
@[simp]
theorem
Matrix.toBilin'_symm
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
:
LinearEquiv.symm Matrix.toBilin' = BilinForm.toMatrix'
@[simp]
theorem
Matrix.toBilin'_toMatrix'
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B : BilinForm R₂ (n → R₂))
:
Matrix.toBilin' (BilinForm.toMatrix' B) = B
@[simp]
theorem
BilinForm.toMatrix'_toBilin'
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(M : Matrix n n R₂)
:
BilinForm.toMatrix' (Matrix.toBilin' M) = M
@[simp]
theorem
BilinForm.toMatrix'_apply
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B : BilinForm R₂ (n → R₂))
(i : n)
(j : n)
:
BilinForm.toMatrix' B i j = B.bilin ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1) ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1)
@[simp]
theorem
BilinForm.toMatrix'_comp
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
{o : Type u_12}
[Fintype n]
[Fintype o]
[DecidableEq n]
[DecidableEq o]
(B : BilinForm R₂ (n → R₂))
(l : (o → R₂) →ₗ[R₂] n → R₂)
(r : (o → R₂) →ₗ[R₂] n → R₂)
:
BilinForm.toMatrix' (BilinForm.comp B l r) = Matrix.transpose (LinearMap.toMatrix' l) * BilinForm.toMatrix' B * LinearMap.toMatrix' r
theorem
BilinForm.toMatrix'_compLeft
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B : BilinForm R₂ (n → R₂))
(f : (n → R₂) →ₗ[R₂] n → R₂)
:
BilinForm.toMatrix' (BilinForm.compLeft B f) = Matrix.transpose (LinearMap.toMatrix' f) * BilinForm.toMatrix' B
theorem
BilinForm.toMatrix'_compRight
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B : BilinForm R₂ (n → R₂))
(f : (n → R₂) →ₗ[R₂] n → R₂)
:
BilinForm.toMatrix' (BilinForm.compRight B f) = BilinForm.toMatrix' B * LinearMap.toMatrix' f
theorem
BilinForm.mul_toMatrix'_mul
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
{o : Type u_12}
[Fintype n]
[Fintype o]
[DecidableEq n]
[DecidableEq o]
(B : BilinForm R₂ (n → R₂))
(M : Matrix o n R₂)
(N : Matrix n o R₂)
:
M * BilinForm.toMatrix' B * N = BilinForm.toMatrix' (BilinForm.comp B (Matrix.toLin' (Matrix.transpose M)) (Matrix.toLin' N))
theorem
BilinForm.mul_toMatrix'
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B : BilinForm R₂ (n → R₂))
(M : Matrix n n R₂)
:
M * BilinForm.toMatrix' B = BilinForm.toMatrix' (BilinForm.compLeft B (Matrix.toLin' (Matrix.transpose M)))
theorem
BilinForm.toMatrix'_mul
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(B : BilinForm R₂ (n → R₂))
(M : Matrix n n R₂)
:
BilinForm.toMatrix' B * M = BilinForm.toMatrix' (BilinForm.compRight B (Matrix.toLin' M))
theorem
Matrix.toBilin'_comp
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
{o : Type u_12}
[Fintype n]
[Fintype o]
[DecidableEq n]
[DecidableEq o]
(M : Matrix n n R₂)
(P : Matrix n o R₂)
(Q : Matrix n o R₂)
:
BilinForm.comp (Matrix.toBilin' M) (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toBilin' (Matrix.transpose P * M * Q)
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_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : 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
- BilinForm.toMatrix b = LinearEquiv.trans BilinForm.toLin (LinearMap.toMatrix₂ b b)
noncomputable def
Matrix.toBilin
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : 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
@[simp]
theorem
BilinForm.toMatrix_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(B : BilinForm R₂ M₂)
(i : n)
(j : n)
:
(BilinForm.toMatrix b) B i j = B.bilin (b i) (b j)
@[simp]
theorem
Matrix.toBilin_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(M : Matrix n n R₂)
(x : M₂)
(y : M₂)
:
((Matrix.toBilin b) M).bilin x y = Finset.sum Finset.univ fun (i : n) => Finset.sum Finset.univ fun (j : n) => (b.repr x) i * M i j * (b.repr y) j
theorem
BilinearForm.toMatrixAux_eq
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(B : BilinForm R₂ M₂)
:
(BilinForm.toMatrixAux ⇑b) B = (BilinForm.toMatrix b) B
@[simp]
theorem
BilinForm.toMatrix_symm
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
:
@[simp]
theorem
Matrix.toBilin_symm
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
:
theorem
Matrix.toBilin_basisFun
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
:
Matrix.toBilin (Pi.basisFun R₂ n) = Matrix.toBilin'
theorem
BilinForm.toMatrix_basisFun
{R₂ : Type u_5}
[CommSemiring R₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
:
BilinForm.toMatrix (Pi.basisFun R₂ n) = BilinForm.toMatrix'
@[simp]
theorem
Matrix.toBilin_toMatrix
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(B : BilinForm R₂ M₂)
:
(Matrix.toBilin b) ((BilinForm.toMatrix b) B) = B
@[simp]
theorem
BilinForm.toMatrix_toBilin
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(M : Matrix n n R₂)
:
(BilinForm.toMatrix b) ((Matrix.toBilin b) M) = M
theorem
BilinForm.toMatrix_comp
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
{o : Type u_12}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Basis n R₂ M₂)
{M₂' : Type u_13}
[AddCommMonoid M₂']
[Module R₂ M₂']
(c : Basis o R₂ M₂')
[DecidableEq o]
(B : BilinForm R₂ M₂)
(l : M₂' →ₗ[R₂] M₂)
(r : M₂' →ₗ[R₂] M₂)
:
(BilinForm.toMatrix c) (BilinForm.comp B l r) = Matrix.transpose ((LinearMap.toMatrix c b) l) * (BilinForm.toMatrix b) B * (LinearMap.toMatrix c b) r
theorem
BilinForm.toMatrix_compLeft
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(B : BilinForm R₂ M₂)
(f : M₂ →ₗ[R₂] M₂)
:
(BilinForm.toMatrix b) (BilinForm.compLeft B f) = Matrix.transpose ((LinearMap.toMatrix b b) f) * (BilinForm.toMatrix b) B
theorem
BilinForm.toMatrix_compRight
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(B : BilinForm R₂ M₂)
(f : M₂ →ₗ[R₂] M₂)
:
(BilinForm.toMatrix b) (BilinForm.compRight B f) = (BilinForm.toMatrix b) B * (LinearMap.toMatrix b b) f
@[simp]
theorem
BilinForm.toMatrix_mul_basis_toMatrix
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
{o : Type u_12}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Basis n R₂ M₂)
[DecidableEq o]
(c : Basis o R₂ M₂)
(B : BilinForm R₂ M₂)
:
Matrix.transpose (Basis.toMatrix b ⇑c) * (BilinForm.toMatrix b) B * Basis.toMatrix b ⇑c = (BilinForm.toMatrix c) B
theorem
BilinForm.mul_toMatrix_mul
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
{o : Type u_12}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Basis n R₂ M₂)
{M₂' : Type u_13}
[AddCommMonoid M₂']
[Module R₂ M₂']
(c : Basis o R₂ M₂')
[DecidableEq o]
(B : BilinForm R₂ M₂)
(M : Matrix o n R₂)
(N : Matrix n o R₂)
:
M * (BilinForm.toMatrix b) B * N = (BilinForm.toMatrix c) (BilinForm.comp B ((Matrix.toLin c b) (Matrix.transpose M)) ((Matrix.toLin c b) N))
theorem
BilinForm.mul_toMatrix
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(B : BilinForm R₂ M₂)
(M : Matrix n n R₂)
:
M * (BilinForm.toMatrix b) B = (BilinForm.toMatrix b) (BilinForm.compLeft B ((Matrix.toLin b b) (Matrix.transpose M)))
theorem
BilinForm.toMatrix_mul
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
[Fintype n]
[DecidableEq n]
(b : Basis n R₂ M₂)
(B : BilinForm R₂ M₂)
(M : Matrix n n R₂)
:
(BilinForm.toMatrix b) B * M = (BilinForm.toMatrix b) (BilinForm.compRight B ((Matrix.toLin b b) M))
theorem
Matrix.toBilin_comp
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{n : Type u_11}
{o : Type u_12}
[Fintype n]
[Fintype o]
[DecidableEq n]
(b : Basis n R₂ M₂)
{M₂' : Type u_13}
[AddCommMonoid M₂']
[Module R₂ M₂']
(c : Basis o R₂ M₂')
[DecidableEq o]
(M : Matrix n n R₂)
(P : Matrix n o R₂)
(Q : Matrix n o R₂)
:
BilinForm.comp ((Matrix.toBilin b) M) ((Matrix.toLin c b) P) ((Matrix.toLin c b) Q) = (Matrix.toBilin c) (Matrix.transpose P * M * Q)
@[simp]
theorem
isAdjointPair_toBilin'
{R₃ : Type u_7}
[CommRing R₃]
{n : Type u_11}
[Fintype n]
(J : Matrix n n R₃)
(J₃ : Matrix n n R₃)
(A : Matrix n n R₃)
(A' : Matrix n n R₃)
[DecidableEq n]
:
BilinForm.IsAdjointPair (Matrix.toBilin' J) (Matrix.toBilin' J₃) (Matrix.toLin' A) (Matrix.toLin' A') ↔ Matrix.IsAdjointPair J J₃ A A'
@[simp]
theorem
isAdjointPair_toBilin
{R₃ : Type u_7}
{M₃ : Type u_8}
[CommRing R₃]
[AddCommGroup M₃]
[Module R₃ M₃]
{n : Type u_11}
[Fintype n]
(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]
:
BilinForm.IsAdjointPair ((Matrix.toBilin b) J) ((Matrix.toBilin 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_7}
[CommRing R₃]
{n : Type u_11}
[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_7}
[CommRing R₃]
{n : Type u_11}
[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') (BilinForm.isPairSelfAdjointSubmodule (Matrix.toBilin' J) (Matrix.toBilin' J₃))
theorem
mem_pairSelfAdjointMatricesSubmodule'
{R₃ : Type u_7}
[CommRing R₃]
{n : Type u_11}
[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_7}
[CommRing R₃]
{n : Type u_11}
[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
theorem
mem_selfAdjointMatricesSubmodule'
{R₃ : Type u_7}
[CommRing R₃]
{n : Type u_11}
[Fintype n]
(J : Matrix n n R₃)
(A : Matrix n n R₃)
[DecidableEq n]
:
def
skewAdjointMatricesSubmodule'
{R₃ : Type u_7}
[CommRing R₃]
{n : Type u_11}
[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
theorem
mem_skewAdjointMatricesSubmodule'
{R₃ : Type u_7}
[CommRing R₃]
{n : Type u_11}
[Fintype n]
(J : Matrix n n R₃)
(A : Matrix n n R₃)
[DecidableEq n]
:
theorem
Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin
{R₂ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₂}
(b : Basis ι R₂ M₂)
:
BilinForm.Nondegenerate (Matrix.toBilin' M) ↔ BilinForm.Nondegenerate ((Matrix.toBilin b) M)
theorem
Matrix.Nondegenerate.toBilin'
{R₃ : Type u_7}
[CommRing R₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₃}
(h : Matrix.Nondegenerate M)
:
BilinForm.Nondegenerate (Matrix.toBilin' M)
@[simp]
theorem
Matrix.nondegenerate_toBilin'_iff
{R₃ : Type u_7}
[CommRing R₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₃}
:
BilinForm.Nondegenerate (Matrix.toBilin' M) ↔ Matrix.Nondegenerate M
theorem
Matrix.Nondegenerate.toBilin
{R₃ : Type u_7}
{M₃ : Type u_8}
[CommRing R₃]
[AddCommGroup M₃]
[Module R₃ M₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₃}
(h : Matrix.Nondegenerate M)
(b : Basis ι R₃ M₃)
:
@[simp]
theorem
Matrix.nondegenerate_toBilin_iff
{R₃ : Type u_7}
{M₃ : Type u_8}
[CommRing R₃]
[AddCommGroup M₃]
[Module R₃ M₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι R₃}
(b : Basis ι R₃ M₃)
:
Lemmas transferring nondegeneracy between a bilinear form and its associated matrix
@[simp]
theorem
BilinForm.nondegenerate_toMatrix'_iff
{R₃ : Type u_7}
[CommRing R₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{B : BilinForm R₃ (ι → R₃)}
:
Matrix.Nondegenerate (BilinForm.toMatrix' B) ↔ BilinForm.Nondegenerate B
theorem
BilinForm.Nondegenerate.toMatrix'
{R₃ : Type u_7}
[CommRing R₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{B : BilinForm R₃ (ι → R₃)}
(h : BilinForm.Nondegenerate B)
:
Matrix.Nondegenerate (BilinForm.toMatrix' B)
@[simp]
theorem
BilinForm.nondegenerate_toMatrix_iff
{R₃ : Type u_7}
{M₃ : Type u_8}
[CommRing R₃]
[AddCommGroup M₃]
[Module R₃ M₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{B : BilinForm R₃ M₃}
(b : Basis ι R₃ M₃)
:
theorem
BilinForm.Nondegenerate.toMatrix
{R₃ : Type u_7}
{M₃ : Type u_8}
[CommRing R₃]
[AddCommGroup M₃]
[Module R₃ M₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{B : BilinForm R₃ M₃}
(h : BilinForm.Nondegenerate B)
(b : Basis ι R₃ M₃)
:
Some shorthands for combining the above with Matrix.nondegenerate_of_det_ne_zero
theorem
BilinForm.nondegenerate_toBilin'_iff_det_ne_zero
{A : Type u_11}
[CommRing A]
[IsDomain A]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{M : Matrix ι ι A}
:
BilinForm.Nondegenerate (Matrix.toBilin' M) ↔ Matrix.det M ≠ 0
theorem
BilinForm.nondegenerate_toBilin'_of_det_ne_zero'
{A : Type u_11}
[CommRing A]
[IsDomain A]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
(M : Matrix ι ι A)
(h : Matrix.det M ≠ 0)
:
BilinForm.Nondegenerate (Matrix.toBilin' M)
theorem
BilinForm.nondegenerate_iff_det_ne_zero
{M₃ : Type u_8}
[AddCommGroup M₃]
{A : Type u_11}
[CommRing A]
[IsDomain A]
[Module A M₃]
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
{B : BilinForm A M₃}
(b : Basis ι A M₃)
:
BilinForm.Nondegenerate B ↔ Matrix.det ((BilinForm.toMatrix b) B) ≠ 0
theorem
BilinForm.nondegenerate_of_det_ne_zero
{M₃ : Type u_8}
[AddCommGroup M₃]
{A : Type u_11}
[CommRing A]
[IsDomain A]
[Module A M₃]
(B₃ : BilinForm A M₃)
{ι : Type u_12}
[DecidableEq ι]
[Fintype ι]
(b : Basis ι A M₃)
(h : Matrix.det ((BilinForm.toMatrix b) B₃) ≠ 0)
: