Bilinear form #

This file defines the conversion between bilinear forms and matrices.

Main definitions #

Matrix.toBilin given a basis define a bilinear form
Matrix.toBilin' define the bilinear form on n → R
BilinForm.toMatrix: calculate the matrix coefficients of a bilinear form
BilinForm.toMatrix': calculate the matrix coefficients of a bilinear form on n → R

Notations #

In this file we use the following type variables:

M, M', ... are modules over the commutative semiring R,
M₁, M₁', ... are modules over the commutative ring R₁,
M₂, M₂', ... are modules over the commutative semiring R₂,
M₃, M₃', ... are modules over the commutative ring R₃,
V, ... is a vector space over the field K.

Tags #

bilinear form, bilin form, BilinearForm, matrix, basis

source

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)

Instances For

source

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

source

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₂) :

BilinForm R₂ M₂ →ₗ[R₂] Matrix n n R₂

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

Instances For

source

@[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)

source

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₂.

source

def BilinForm.toMatrix' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :

BilinForm R₂ (n → R₂) ≃ₗ[R₂] Matrix n n R₂

The linear equivalence between bilinear forms on n → R and n × n matrices

Equations

BilinForm.toMatrix' = LinearEquiv.trans BilinForm.toLin LinearMap.toMatrix₂'

Instances For

source

@[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

source

def Matrix.toBilin' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :

Matrix n n R₂ ≃ₗ[R₂] BilinForm R₂ (n → R₂)

The linear equivalence between n × n matrices and bilinear forms on n → R

Equations

Matrix.toBilin' = LinearEquiv.symm BilinForm.toMatrix'

Instances For

source

@[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

source

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

source

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)

source

@[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

source

@[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'

source

@[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'

source

@[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

source

@[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

source

@[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)

source

@[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

source

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

source

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

source

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))

source

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)))

source

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))

source

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.

source

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 R₂ M₂ ≃ₗ[R₂] Matrix n n R₂

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)

Instances For

source

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₂) :

Matrix n n R₂ ≃ₗ[R₂] BilinForm 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

Matrix.toBilin b = LinearEquiv.symm (BilinForm.toMatrix b)

Instances For

source

@[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)

source

@[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

source

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

source

@[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₂) :

LinearEquiv.symm (BilinForm.toMatrix b) = Matrix.toBilin b

source

@[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₂) :

LinearEquiv.symm (Matrix.toBilin b) = BilinForm.toMatrix b

source

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'

source

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'

source

@[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

source

@[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

source

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

source

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

source

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

source

@[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

source

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))

source

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)))

source

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))

source

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)

source

@[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'

source

@[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'

source

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⁻¹)

source

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] :

Submodule R₃ (Matrix n n R₃)

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₃))

Instances For

source

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

source

def selfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [Fintype n] (J : Matrix n n R₃) [DecidableEq n] :

Submodule R₃ (Matrix n n R₃)

The submodule of self-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations

selfAdjointMatricesSubmodule' J = pairSelfAdjointMatricesSubmodule J J

Instances For

source

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] :

A ∈ selfAdjointMatricesSubmodule J ↔ Matrix.IsSelfAdjoint J A

source

def skewAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [Fintype n] (J : Matrix n n R₃) [DecidableEq n] :

Submodule R₃ (Matrix n n R₃)

The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations

skewAdjointMatricesSubmodule' J = pairSelfAdjointMatricesSubmodule (-J) J

Instances For

source

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] :

A ∈ skewAdjointMatricesSubmodule J ↔ Matrix.IsSkewAdjoint J A

source

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)

source

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)

source

@[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

source

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₃) :

BilinForm.Nondegenerate ((Matrix.toBilin b) M)

source

@[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₃) :

BilinForm.Nondegenerate ((Matrix.toBilin b) M) ↔ Matrix.Nondegenerate M

Lemmas transferring nondegeneracy between a bilinear form and its associated matrix

source

@[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

source

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)

source

@[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₃) :

Matrix.Nondegenerate ((BilinForm.toMatrix b) B) ↔ BilinForm.Nondegenerate B

source

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₃) :

Matrix.Nondegenerate ((BilinForm.toMatrix b) B)

Some shorthands for combining the above with Matrix.nondegenerate_of_det_ne_zero

source

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

source

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)

source

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

source

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) :

BilinForm.Nondegenerate B₃

Documentation

Mathlib.LinearAlgebra.Matrix.BilinearForm

Bilinear form #

Main definitions #

Notations #

Tags #

`ToMatrix'` section #

`ToMatrix` section #

Bilinear form #

Main definitions #

Notations #

Tags #

ToMatrix' section #

ToMatrix section #

`ToMatrix'` section #

`ToMatrix` section #