# Documentation

Mathlib.LinearAlgebra.BilinearForm

# Bilinear form #

This file defines a bilinear form over a module. Basic ideas such as orthogonality are also introduced, as well as reflexive, symmetric, non-degenerate and alternating bilinear forms. Adjoints of linear maps with respect to a bilinear form are also introduced.

A bilinear form on an R-(semi)module M, is a function from M × M to R, that is linear in both arguments. Comments will typically abbreviate "(semi)module" as just "module", but the definitions should be as general as possible.

The result that there exists an orthogonal basis with respect to a symmetric, nondegenerate bilinear form can be found in QuadraticForm.lean with exists_orthogonal_basis.

## Notations #

Given any term B of type BilinForm, due to a coercion, can use the notation B x y to refer to the function field, ie. B x y = B.bilin x y.

In this file we use the following type variables:

• M, M', ... are modules over the semiring R,
• M₁, M₁', ... are modules over the 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,

structure BilinForm (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
Type (max u_1 u_2)

BilinForm R M is the type of R-bilinear functions M → M → R.

Instances For
instance BilinForm.instCoeFunBilinFormForAll {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
CoeFun () fun x => MMR
theorem BilinForm.coeFn_mk {R : Type u_1} {M : Type u_2} [] [] [Module R M] (f : MMR) (h₁ : ∀ (x y z : M), f (x + y) z = f x z + f y z) (h₂ : ∀ (a : R) (x y : M), f (a x) y = a * f x y) (h₃ : ∀ (x y z : M), f x (y + z) = f x y + f x z) (h₄ : ∀ (a : R) (x y : M), f x (a y) = a * f x y) :
{ bilin := f, bilin_add_left := h₁, bilin_smul_left := h₂, bilin_add_right := h₃, bilin_smul_right := h₄ }.bilin = f
theorem BilinForm.coeFn_congr {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {x : M} {x' : M} {y : M} {y' : M} :
x = x'y = y' = BilinForm.bilin B x' y'
@[simp]
theorem BilinForm.add_left {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) (y : M) (z : M) :
BilinForm.bilin B (x + y) z = +
@[simp]
theorem BilinForm.smul_left {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (a : R) (x : M) (y : M) :
BilinForm.bilin B (a x) y = a *
@[simp]
theorem BilinForm.add_right {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) (y : M) (z : M) :
BilinForm.bilin B x (y + z) = +
@[simp]
theorem BilinForm.smul_right {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (a : R) (x : M) (y : M) :
BilinForm.bilin B x (a y) = a *
@[simp]
theorem BilinForm.zero_left {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) :
= 0
@[simp]
theorem BilinForm.zero_right {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) :
= 0
@[simp]
theorem BilinForm.neg_left {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} (x : M₁) (y : M₁) :
BilinForm.bilin B₁ (-x) y = -BilinForm.bilin B₁ x y
@[simp]
theorem BilinForm.neg_right {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} (x : M₁) (y : M₁) :
BilinForm.bilin B₁ x (-y) = -BilinForm.bilin B₁ x y
@[simp]
theorem BilinForm.sub_left {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} (x : M₁) (y : M₁) (z : M₁) :
BilinForm.bilin B₁ (x - y) z = BilinForm.bilin B₁ x z - BilinForm.bilin B₁ y z
@[simp]
theorem BilinForm.sub_right {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} (x : M₁) (y : M₁) (z : M₁) :
BilinForm.bilin B₁ x (y - z) = BilinForm.bilin B₁ x y - BilinForm.bilin B₁ x z
theorem BilinForm.coe_injective {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
Function.Injective BilinForm.bilin
theorem BilinForm.ext {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {D : } (H : ∀ (x y : M), = ) :
B = D
theorem BilinForm.congr_fun {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {D : } (h : B = D) (x : M) (y : M) :
=
theorem BilinForm.ext_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {D : } :
B = D ∀ (x y : M), =
instance BilinForm.instZeroBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
Zero ()
@[simp]
theorem BilinForm.coe_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
0.bilin = 0
@[simp]
theorem BilinForm.zero_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (x : M) (y : M) :
= 0
instance BilinForm.instAddBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
@[simp]
theorem BilinForm.coe_add {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (D : ) :
(B + D).bilin = B.bilin + D.bilin
@[simp]
theorem BilinForm.add_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (D : ) (x : M) (y : M) :
BilinForm.bilin (B + D) x y = +
instance BilinForm.instSMulBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_11} [] [] [] :
SMul α ()

BilinForm R M inherits the scalar action by α on R if this is compatible with multiplication.

When R itself is commutative, this provides an R-action via Algebra.id.

@[simp]
theorem BilinForm.coe_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_11} [] [] [] (a : α) (B : ) :
(a B).bilin = a B.bilin
@[simp]
theorem BilinForm.smul_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_11} [] [] [] (a : α) (B : ) (x : M) (y : M) :
BilinForm.bilin (a B) x y = a
instance BilinForm.instSMulCommClassBilinFormInstSMulBilinFormInstSMulBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_11} {β : Type u_12} [] [] [] [] [] [] [] :
SMulCommClass α β ()
instance BilinForm.instIsScalarTowerBilinFormInstSMulBilinFormInstSMulBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_11} {β : Type u_12} [] [] [SMul α β] [] [] [] [] [] :
IsScalarTower α β ()
instance BilinForm.instAddCommMonoidBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
instance BilinForm.instNegBilinFormToSemiringToAddCommMonoid {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] :
Neg (BilinForm R₁ M₁)
@[simp]
theorem BilinForm.coe_neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) :
(-B₁).bilin = -B₁.bilin
@[simp]
theorem BilinForm.neg_apply {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (x : M₁) (y : M₁) :
BilinForm.bilin (-B₁) x y = -BilinForm.bilin B₁ x y
instance BilinForm.instSubBilinFormToSemiringToAddCommMonoid {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] :
Sub (BilinForm R₁ M₁)
@[simp]
theorem BilinForm.coe_sub {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (D₁ : BilinForm R₁ M₁) :
(B₁ - D₁).bilin = B₁.bilin - D₁.bilin
@[simp]
theorem BilinForm.sub_apply {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (D₁ : BilinForm R₁ M₁) (x : M₁) (y : M₁) :
BilinForm.bilin (B₁ - D₁) x y = BilinForm.bilin B₁ x y - BilinForm.bilin D₁ x y
instance BilinForm.instAddCommGroupBilinFormToSemiringToAddCommMonoid {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] :
instance BilinForm.instInhabitedBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
def BilinForm.coeFnAddMonoidHom {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
→+ MMR

coeFn as an AddMonoidHom

Instances For
instance BilinForm.instModuleBilinFormInstAddCommMonoidBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_11} [] [Module α R] [] :
Module α ()
def BilinForm.flipHomAux {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R₂ : Type u_5) [] [Algebra R₂ R] :
→ₗ[R₂]

Auxiliary construction for the flip of a bilinear form, obtained by exchanging the left and right arguments. This version is a LinearMap; it is later upgraded to a LinearEquiv in flipHom.

Instances For
theorem BilinForm.flip_flip_aux {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R₂ : Type u_5} [] [Algebra R₂ R] (A : ) :
↑() (↑() A) = A
def BilinForm.flipHom {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R₂ : Type u_5) [] [Algebra R₂ R] :
≃ₗ[R₂]

The flip of a bilinear form, obtained by exchanging the left and right arguments. This is a less structured version of the equiv which applies to general (noncommutative) rings R with a distinguished commutative subring R₂; over a commutative ring use flip.

Instances For
@[simp]
theorem BilinForm.flip_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R₂ : Type u_5} [] [Algebra R₂ R] (A : ) (x : M) (y : M) :
BilinForm.bilin (↑() A) x y =
theorem BilinForm.flip_flip {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R₂ : Type u_5} [] [Algebra R₂ R] :
@[inline, reducible]
abbrev BilinForm.flip' {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

The flip of a bilinear form over a ring, obtained by exchanging the left and right arguments, here considered as an ℕ-linear equivalence, i.e. an additive equivalence.

Instances For
@[inline, reducible]
abbrev BilinForm.flip {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] :
BilinForm R₂ M₂ ≃ₗ[R₂] BilinForm R₂ M₂

The flip of a bilinear form over a commutative ring, obtained by exchanging the left and right arguments.

Instances For
def BilinForm.toLinHomAux₁ {R : Type u_1} {M : Type u_2} [] [] [Module R M] (A : ) (x : M) :

Auxiliary definition to define toLinHom; see below.

Instances For
def BilinForm.toLinHomAux₂ {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R₂ : Type u_5} [] [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ R M] (A : ) :
M →ₗ[R₂] M →ₗ[R] R

Auxiliary definition to define toLinHom; see below.

Instances For
def BilinForm.toLinHom {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R₂ : Type u_5) [] [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ R M] :
→ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R

The linear map obtained from a BilinForm by fixing the left co-ordinate and evaluating in the right. This is the most general version of the construction; it is R₂-linear for some distinguished commutative subsemiring R₂ of the scalar ring. Over a semiring with no particular distinguished such subsemiring, use toLin', which is ℕ-linear. Over a commutative semiring, use toLin, which is linear.

Instances For
@[simp]
theorem BilinForm.toLin'_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R₂ : Type u_5} [] [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ R M] (A : ) (x : M) :
↑(↑(↑() A) x) =
@[inline, reducible]
abbrev BilinForm.toLin' {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

The linear map obtained from a BilinForm by fixing the left co-ordinate and evaluating in the right. Over a commutative semiring, use toLin, which is linear rather than ℕ-linear.

Instances For
@[simp]
theorem BilinForm.sum_left {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) {α : Type u_11} (t : ) (g : αM) (w : M) :
BilinForm.bilin B (Finset.sum t fun i => g i) w = Finset.sum t fun i => BilinForm.bilin B (g i) w
@[simp]
theorem BilinForm.sum_right {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) {α : Type u_11} (t : ) (w : M) (g : αM) :
BilinForm.bilin B w (Finset.sum t fun i => g i) = Finset.sum t fun i => BilinForm.bilin B w (g i)
def BilinForm.toLinHomFlip {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R₂ : Type u_5) [] [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ R M] :
→ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R

The linear map obtained from a BilinForm by fixing the right co-ordinate and evaluating in the left. This is the most general version of the construction; it is R₂-linear for some distinguished commutative subsemiring R₂ of the scalar ring. Over semiring with no particular distinguished such subsemiring, use toLin'Flip, which is ℕ-linear. Over a commutative semiring, use toLinFlip, which is linear.

Instances For
@[simp]
theorem BilinForm.toLin'Flip_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R₂ : Type u_5} [] [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ R M] (A : ) (x : M) :
↑(↑(↑() A) x) = fun y =>
@[inline, reducible]
abbrev BilinForm.toLin'Flip {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

The linear map obtained from a BilinForm by fixing the right co-ordinate and evaluating in the left. Over a commutative semiring, use toLinFlip, which is linear rather than ℕ-linear.

Instances For
def LinearMap.toBilinAux {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) :
BilinForm R₂ M₂

A map with two arguments that is linear in both is a bilinear form.

This is an auxiliary definition for the full linear equivalence LinearMap.toBilin.

Instances For
def BilinForm.toLin {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] :
BilinForm R₂ M₂ ≃ₗ[R₂] M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂

Bilinear forms are linearly equivalent to maps with two arguments that are linear in both.

Instances For
def LinearMap.toBilin {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] :
(M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) ≃ₗ[R₂] BilinForm R₂ M₂

A map with two arguments that is linear in both is linearly equivalent to bilinear form.

Instances For
@[simp]
theorem LinearMap.toBilinAux_eq {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) :
= LinearMap.toBilin f
@[simp]
theorem LinearMap.toBilin_symm {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] :
LinearEquiv.symm LinearMap.toBilin = BilinForm.toLin
@[simp]
theorem BilinForm.toLin_symm {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] :
LinearEquiv.symm BilinForm.toLin = LinearMap.toBilin
@[simp]
theorem LinearMap.toBilin_apply {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) (x : M₂) (y : M₂) :
BilinForm.bilin (LinearMap.toBilin f) x y = ↑(f x) y
@[simp]
theorem BilinForm.toLin_apply {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {B₂ : BilinForm R₂ M₂} (x : M₂) :
↑(↑(BilinForm.toLin B₂) x) =
@[simp]
theorem LinearMap.compBilinForm_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R' : Type u_11} [] [Algebra R' R] [Module R' M] [IsScalarTower R' R M] (f : R →ₗ[R'] R') (B : ) (x : M) (y : M) :
= f ()
def LinearMap.compBilinForm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {R' : Type u_11} [] [Algebra R' R] [Module R' M] [IsScalarTower R' R M] (f : R →ₗ[R'] R') (B : ) :

Apply a linear map on the output of a bilinear form.

Instances For
def BilinForm.comp {R : Type u_1} {M : Type u_2} [] [] [Module R M] {M' : Type w} [] [Module R M'] (B : BilinForm R M') (l : M →ₗ[R] M') (r : M →ₗ[R] M') :

Apply a linear map on the left and right argument of a bilinear form.

Instances For
def BilinForm.compLeft {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (f : M →ₗ[R] M) :

Apply a linear map to the left argument of a bilinear form.

Instances For
def BilinForm.compRight {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (f : M →ₗ[R] M) :

Apply a linear map to the right argument of a bilinear form.

Instances For
theorem BilinForm.comp_comp {R : Type u_1} {M : Type u_2} [] [] [Module R M] {M' : Type w} [] [Module R M'] {M'' : Type u_11} [] [Module R M''] (B : BilinForm R M'') (l : M →ₗ[R] M') (r : M →ₗ[R] M') (l' : M' →ₗ[R] M'') (r' : M' →ₗ[R] M'') :
@[simp]
theorem BilinForm.compLeft_compRight {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (l : M →ₗ[R] M) (r : M →ₗ[R] M) :
=
@[simp]
theorem BilinForm.compRight_compLeft {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (l : M →ₗ[R] M) (r : M →ₗ[R] M) :
=
@[simp]
theorem BilinForm.comp_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {M' : Type w} [] [Module R M'] (B : BilinForm R M') (l : M →ₗ[R] M') (r : M →ₗ[R] M') (v : M) (w : M) :
BilinForm.bilin () v w = BilinForm.bilin B (l v) (r w)
@[simp]
theorem BilinForm.compLeft_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (f : M →ₗ[R] M) (v : M) (w : M) :
= BilinForm.bilin B (f v) w
@[simp]
theorem BilinForm.compRight_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (f : M →ₗ[R] M) (v : M) (w : M) :
= BilinForm.bilin B v (f w)
@[simp]
theorem BilinForm.comp_id_left {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (r : M →ₗ[R] M) :
BilinForm.comp B LinearMap.id r =
@[simp]
theorem BilinForm.comp_id_right {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (l : M →ₗ[R] M) :
BilinForm.comp B l LinearMap.id =
@[simp]
theorem BilinForm.compLeft_id {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) :
BilinForm.compLeft B LinearMap.id = B
@[simp]
theorem BilinForm.compRight_id {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) :
BilinForm.compRight B LinearMap.id = B
@[simp]
theorem BilinForm.comp_id_id {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) :
BilinForm.comp B LinearMap.id LinearMap.id = B
theorem BilinForm.comp_inj {R : Type u_1} {M : Type u_2} [] [] [Module R M] {M' : Type w} [] [Module R M'] (B₁ : BilinForm R M') (B₂ : BilinForm R M') {l : M →ₗ[R] M'} {r : M →ₗ[R] M'} (hₗ : ) (hᵣ : ) :
BilinForm.comp B₁ l r = BilinForm.comp B₂ l r B₁ = B₂
def BilinForm.congr {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} [] [Module R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') :
BilinForm R₂ M₂ ≃ₗ[R₂] BilinForm R₂ M₂'

Apply a linear equivalence on the arguments of a bilinear form.

Instances For
@[simp]
theorem BilinForm.congr_apply {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} [] [Module R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') (B : BilinForm R₂ M₂) (x : M₂') (y : M₂') :
BilinForm.bilin (↑() B) x y = BilinForm.bilin B (↑() x) (↑() y)
@[simp]
theorem BilinForm.congr_symm {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} [] [Module R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') :
@[simp]
theorem BilinForm.congr_refl {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] :
theorem BilinForm.congr_trans {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [] [AddCommMonoid M₂''] [Module R₂ M₂'] [Module R₂ M₂''] (e : M₂ ≃ₗ[R₂] M₂') (f : M₂' ≃ₗ[R₂] M₂'') :
theorem BilinForm.congr_congr {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [] [AddCommMonoid M₂''] [Module R₂ M₂'] [Module R₂ M₂''] (e : M₂' ≃ₗ[R₂] M₂'') (f : M₂ ≃ₗ[R₂] M₂') (B : BilinForm R₂ M₂) :
↑() (↑() B) = ↑() B
theorem BilinForm.congr_comp {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [] [AddCommMonoid M₂''] [Module R₂ M₂'] [Module R₂ M₂''] (e : M₂ ≃ₗ[R₂] M₂') (B : BilinForm R₂ M₂) (l : M₂'' →ₗ[R₂] M₂') (r : M₂'' →ₗ[R₂] M₂') :
BilinForm.comp (↑() B) l r = BilinForm.comp B (LinearMap.comp (↑()) l) (LinearMap.comp (↑()) r)
theorem BilinForm.comp_congr {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [] [AddCommMonoid M₂''] [Module R₂ M₂'] [Module R₂ M₂''] (e : M₂' ≃ₗ[R₂] M₂'') (B : BilinForm R₂ M₂) (l : M₂' →ₗ[R₂] M₂) (r : M₂' →ₗ[R₂] M₂) :
↑() () = BilinForm.comp B () ()
def BilinForm.linMulLin {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (f : M₂ →ₗ[R₂] R₂) (g : M₂ →ₗ[R₂] R₂) :
BilinForm R₂ M₂

linMulLin f g is the bilinear form mapping x and y to f x * g y

Instances For
@[simp]
theorem BilinForm.linMulLin_apply {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {f : M₂ →ₗ[R₂] R₂} {g : M₂ →ₗ[R₂] R₂} (x : M₂) (y : M₂) :
= f x * g y
@[simp]
theorem BilinForm.linMulLin_comp {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} [] [Module R₂ M₂'] {f : M₂ →ₗ[R₂] R₂} {g : M₂ →ₗ[R₂] R₂} (l : M₂' →ₗ[R₂] M₂) (r : M₂' →ₗ[R₂] M₂) :
@[simp]
theorem BilinForm.linMulLin_compLeft {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {f : M₂ →ₗ[R₂] R₂} {g : M₂ →ₗ[R₂] R₂} (l : M₂ →ₗ[R₂] M₂) :
=
@[simp]
theorem BilinForm.linMulLin_compRight {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {f : M₂ →ₗ[R₂] R₂} {g : M₂ →ₗ[R₂] R₂} (r : M₂ →ₗ[R₂] M₂) :
=
def BilinForm.IsOrtho {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (x : M) (y : M) :

The proposition that two elements of a bilinear form space are orthogonal. For orthogonality of an indexed set of elements, use BilinForm.iIsOrtho.

Instances For
theorem BilinForm.isOrtho_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {x : M} {y : M} :
= 0
theorem BilinForm.isOrtho_zero_left {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) :
theorem BilinForm.isOrtho_zero_right {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) :
theorem BilinForm.ne_zero_of_not_isOrtho_self {V : Type u_9} {K : Type u_10} [] [] [Module K V] {B : } (x : V) (hx₁ : ¬) :
x 0
def BilinForm.iIsOrtho {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} (B : ) (v : nM) :

A set of vectors v is orthogonal with respect to some bilinear form B if and only if for all i ≠ j, B (v i) (v j) = 0. For orthogonality between two elements, use BilinForm.IsOrtho

Instances For
theorem BilinForm.iIsOrtho_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} {B : } {v : nM} :
∀ (i j : n), i jBilinForm.bilin B (v i) (v j) = 0
@[simp]
theorem BilinForm.isOrtho_smul_left {R₄ : Type u_13} {M₄ : Type u_14} [Ring R₄] [IsDomain R₄] [] [Module R₄ M₄] {G : BilinForm R₄ M₄} {x : M₄} {y : M₄} {a : R₄} (ha : a 0) :
@[simp]
theorem BilinForm.isOrtho_smul_right {R₄ : Type u_13} {M₄ : Type u_14} [Ring R₄] [IsDomain R₄] [] [Module R₄ M₄] {G : BilinForm R₄ M₄} {x : M₄} {y : M₄} {a : R₄} (ha : a 0) :
theorem BilinForm.linearIndependent_of_iIsOrtho {V : Type u_9} {K : Type u_10} [] [] [Module K V] {n : Type w} {B : } {v : nV} (hv₁ : ) (hv₂ : ∀ (i : n), ¬BilinForm.IsOrtho B (v i) (v i)) :

A set of orthogonal vectors v with respect to some bilinear form B is linearly independent if for all i, B (v i) (v i) ≠ 0.

theorem BilinForm.ext_basis {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {B₂ : BilinForm R₂ M₂} {F₂ : BilinForm R₂ M₂} {ι : Type u_13} (b : Basis ι R₂ M₂) (h : ∀ (i j : ι), BilinForm.bilin B₂ (b i) (b j) = BilinForm.bilin F₂ (b i) (b j)) :
B₂ = F₂

Two bilinear forms are equal when they are equal on all basis vectors.

theorem BilinForm.sum_repr_mul_repr_mul {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {B₂ : BilinForm R₂ M₂} {ι : Type u_13} (b : Basis ι R₂ M₂) (x : M₂) (y : M₂) :
(Finsupp.sum (b.repr x) fun i xi => Finsupp.sum (b.repr y) fun j yj => xi yj BilinForm.bilin B₂ (b i) (b j)) = BilinForm.bilin B₂ x y

Write out B x y as a sum over B (b i) (b j) if b is a basis.

### Reflexivity, symmetry, and alternativity #

def BilinForm.IsRefl {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) :

The proposition that a bilinear form is reflexive

Instances For
theorem BilinForm.IsRefl.eq_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : ) {x : M} {y : M} :
= 0 = 0
theorem BilinForm.IsRefl.ortho_comm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : ) {x : M} {y : M} :
theorem BilinForm.IsRefl.neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B : BilinForm R₁ M₁} (hB : ) :
theorem BilinForm.IsRefl.smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_13} [] [Module α R] [] [] (a : α) {B : } (hB : ) :
theorem BilinForm.IsRefl.groupSMul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_13} [] [] [] (a : α) {B : } (hB : ) :
@[simp]
theorem BilinForm.isRefl_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
@[simp]
theorem BilinForm.isRefl_neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B : BilinForm R₁ M₁} :
def BilinForm.IsSymm {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) :

The proposition that a bilinear form is symmetric

Instances For
theorem BilinForm.IsSymm.eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : ) (x : M) (y : M) :
=
theorem BilinForm.IsSymm.isRefl {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : ) :
theorem BilinForm.IsSymm.ortho_comm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : ) {x : M} {y : M} :
theorem BilinForm.IsSymm.add {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B₁ : } {B₂ : } (hB₁ : ) (hB₂ : ) :
BilinForm.IsSymm (B₁ + B₂)
theorem BilinForm.IsSymm.sub {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} {B₂ : BilinForm R₁ M₁} (hB₁ : ) (hB₂ : ) :
BilinForm.IsSymm (B₁ - B₂)
theorem BilinForm.IsSymm.neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B : BilinForm R₁ M₁} (hB : ) :
theorem BilinForm.IsSymm.smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_13} [] [] [] (a : α) {B : } (hB : ) :
@[simp]
theorem BilinForm.isSymm_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
@[simp]
theorem BilinForm.isSymm_neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B : BilinForm R₁ M₁} :
theorem BilinForm.isSymm_iff_flip {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R₂ : Type u_5) [] {B : } [Algebra R₂ R] :
↑() B = B
def BilinForm.IsAlt {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) :

The proposition that a bilinear form is alternating

Instances For
theorem BilinForm.IsAlt.self_eq_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : ) (x : M) :
= 0
theorem BilinForm.IsAlt.neg_eq {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} (H : ) (x : M₁) (y : M₁) :
theorem BilinForm.IsAlt.isRefl {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} (H : ) :
theorem BilinForm.IsAlt.ortho_comm {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} (H : ) {x : M₁} {y : M₁} :
theorem BilinForm.IsAlt.add {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B₁ : } {B₂ : } (hB₁ : ) (hB₂ : ) :
BilinForm.IsAlt (B₁ + B₂)
theorem BilinForm.IsAlt.sub {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} {B₂ : BilinForm R₁ M₁} (hB₁ : ) (hB₂ : ) :
BilinForm.IsAlt (B₁ - B₂)
theorem BilinForm.IsAlt.neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B : BilinForm R₁ M₁} (hB : ) :
theorem BilinForm.IsAlt.smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_13} [] [] [] (a : α) {B : } (hB : ) :
@[simp]
theorem BilinForm.isAlt_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
@[simp]
theorem BilinForm.isAlt_neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B : BilinForm R₁ M₁} :

def BilinForm.IsAdjointPair {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) {M' : Type u_13} [] [Module R M'] (B' : BilinForm R M') (f : M →ₗ[R] M') (g : M' →ₗ[R] M) :

Given a pair of modules equipped with bilinear forms, this is the condition for a pair of maps between them to be mutually adjoint.

Instances For
theorem BilinForm.IsAdjointPair.eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {M' : Type u_13} [] [Module R M'] {B' : BilinForm R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} (h : ) {x : M} {y : M'} :
BilinForm.bilin B' (f x) y = BilinForm.bilin B x (g y)
theorem BilinForm.isAdjointPair_iff_compLeft_eq_compRight {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (F : ) (f : ) (g : ) :
theorem BilinForm.isAdjointPair_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {M' : Type u_13} [] [Module R M'] {B' : BilinForm R M'} :
theorem BilinForm.isAdjointPair_id {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } :
theorem BilinForm.IsAdjointPair.add {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {M' : Type u_13} [] [Module R M'] {B' : BilinForm R M'} {f : M →ₗ[R] M'} {f' : M →ₗ[R] M'} {g : M' →ₗ[R] M} {g' : M' →ₗ[R] M} (h : ) (h' : BilinForm.IsAdjointPair B B' f' g') :
BilinForm.IsAdjointPair B B' (f + f') (g + g')
theorem BilinForm.IsAdjointPair.sub {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} {M₁' : Type u_14} [AddCommGroup M₁'] [Module R₁ M₁'] {B₁' : BilinForm R₁ M₁'} {f₁ : M₁ →ₗ[R₁] M₁'} {f₁' : M₁ →ₗ[R₁] M₁'} {g₁ : M₁' →ₗ[R₁] M₁} {g₁' : M₁' →ₗ[R₁] M₁} (h : BilinForm.IsAdjointPair B₁ B₁' f₁ g₁) (h' : BilinForm.IsAdjointPair B₁ B₁' f₁' g₁') :
BilinForm.IsAdjointPair B₁ B₁' (f₁ - f₁') (g₁ - g₁')
theorem BilinForm.IsAdjointPair.smul {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {B₂ : BilinForm R₂ M₂} {M₂' : Type u_11} [] [Module R₂ M₂'] {B₂' : BilinForm R₂ M₂'} {f₂ : M₂ →ₗ[R₂] M₂'} {g₂ : M₂' →ₗ[R₂] M₂} (c : R₂) (h : BilinForm.IsAdjointPair B₂ B₂' f₂ g₂) :
BilinForm.IsAdjointPair B₂ B₂' (c f₂) (c g₂)
theorem BilinForm.IsAdjointPair.comp {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {M' : Type u_13} [] [Module R M'] {B' : BilinForm R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} {M'' : Type u_15} [] [Module R M''] (B'' : BilinForm R M'') {f' : M' →ₗ[R] M''} {g' : M'' →ₗ[R] M'} (h : ) (h' : BilinForm.IsAdjointPair B' B'' f' g') :
theorem BilinForm.IsAdjointPair.mul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {f : } {g : } {f' : } {g' : } (h : ) (h' : BilinForm.IsAdjointPair B B f' g') :
BilinForm.IsAdjointPair B B (f * f') (g' * g)
def BilinForm.IsPairSelfAdjoint {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (F : ) (f : ) :

The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept of self adjointness. In the case that one of the forms is the negation of the other, this is the usual concept of skew adjointness.

Instances For
def BilinForm.isPairSelfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) (F₂ : BilinForm R₂ M₂) :
Submodule R₂ (Module.End R₂ M₂)

The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms.

Instances For
@[simp]
theorem BilinForm.mem_isPairSelfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) (F₂ : BilinForm R₂ M₂) (f : Module.End R₂ M₂) :
theorem BilinForm.isPairSelfAdjoint_equiv {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) {M₂' : Type u_11} [] [Module R₂ M₂'] (F₂ : BilinForm R₂ M₂) (e : M₂' ≃ₗ[R₂] M₂) (f : Module.End R₂ M₂) :
BilinForm.IsPairSelfAdjoint (BilinForm.comp B₂ e e) (BilinForm.comp F₂ e e) (↑() f)
def BilinForm.IsSelfAdjoint {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (f : ) :

An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an adjoint for itself.

Instances For
def BilinForm.IsSkewAdjoint {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (f : Module.End R₁ M₁) :

An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation serves as an adjoint.

Instances For
theorem BilinForm.isSkewAdjoint_iff_neg_self_adjoint {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (f : Module.End R₁ M₁) :
def BilinForm.selfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) :
Submodule R₂ (Module.End R₂ M₂)

The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Jordan subalgebra.)

Instances For
@[simp]
theorem BilinForm.mem_selfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) (f : Module.End R₂ M₂) :
def BilinForm.skewAdjointSubmodule {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [] [Module R₃ M₃] (B₃ : BilinForm R₃ M₃) :
Submodule R₃ (Module.End R₃ M₃)

The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Lie subalgebra.)

Instances For
@[simp]
theorem BilinForm.mem_skewAdjointSubmodule {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [] [Module R₃ M₃] (B₃ : BilinForm R₃ M₃) (f : Module.End R₃ M₃) :
def BilinForm.orthogonal {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (N : ) :

The orthogonal complement of a submodule N with respect to some bilinear form is the set of elements x which are orthogonal to all elements of N; i.e., for all y in N, B x y = 0.

Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal complement for which, for all y in N, B y x = 0. This variant definition is not currently provided in mathlib.

Instances For
@[simp]
theorem BilinForm.mem_orthogonal_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {N : } {m : M} :
∀ (n : M), n N
theorem BilinForm.orthogonal_le {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {N : } {L : } (h : N L) :
theorem BilinForm.le_orthogonal_orthogonal {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {N : } (b : ) :
theorem BilinForm.span_singleton_inf_orthogonal_eq_bot {V : Type u_9} {K : Type u_10} [] [] [Module K V] {B : } {x : V} (hx : ¬) :
theorem BilinForm.orthogonal_span_singleton_eq_toLin_ker {V : Type u_9} {K : Type u_10} [] [] [Module K V] {B : } (x : V) :
BilinForm.orthogonal B (Submodule.span K {x}) = LinearMap.ker (↑(BilinForm.toLin B) x)
theorem BilinForm.span_singleton_sup_orthogonal_eq_top {V : Type u_9} {K : Type u_10} [] [] [Module K V] {B : } {x : V} (hx : ¬) :
theorem BilinForm.isCompl_span_singleton_orthogonal {V : Type u_9} {K : Type u_10} [] [] [Module K V] {B : } {x : V} (hx : ¬) :

Given a bilinear form B and some x such that B x x ≠ 0, the span of the singleton of x is complement to its orthogonal complement.

@[simp]
theorem BilinForm.restrict_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (W : ) (a : { x // x W }) (b : { x // x W }) :
= BilinForm.bilin B a b
def BilinForm.restrict {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (W : ) :
BilinForm R { x // x W }

The restriction of a bilinear form on a submodule.

Instances For
theorem BilinForm.restrictSymm {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (b : ) (W : ) :

The restriction of a symmetric bilinear form on a submodule is also symmetric.

def BilinForm.Nondegenerate {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) :

A nondegenerate bilinear form is a bilinear form such that the only element that is orthogonal to every other element is 0; i.e., for all nonzero m in M, there exists n in M with B m n ≠ 0.

Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a chirality; in addition to this "left" nondegeneracy condition one could define a "right" nondegeneracy condition that in the situation described, B n m ≠ 0. This variant definition is not currently provided in mathlib. In finite dimension either definition implies the other.

Instances For
theorem BilinForm.not_nondegenerate_zero (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :

In a non-trivial module, zero is not non-degenerate.

theorem BilinForm.Nondegenerate.ne_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] {B : } (h : ) :
B 0
theorem BilinForm.Nondegenerate.congr {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} [] [Module R₂ M₂'] {B : BilinForm R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') (h : ) :
@[simp]
theorem BilinForm.nondegenerate_congr_iff {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {M₂' : Type u_11} [] [Module R₂ M₂'] {B : BilinForm R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') :
theorem BilinForm.nondegenerate_iff_ker_eq_bot {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {B : BilinForm R₂ M₂} :
LinearMap.ker (BilinForm.toLin B) =

A bilinear form is nondegenerate if and only if it has a trivial kernel.

theorem BilinForm.Nondegenerate.ker_eq_bot {R₂ : Type u_5} {M₂ : Type u_6} [] [] [Module R₂ M₂] {B : BilinForm R₂ M₂} (h : ) :
LinearMap.ker (BilinForm.toLin B) =
theorem BilinForm.nondegenerateRestrictOfDisjointOrthogonal {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B : BilinForm R₁ M₁) (b : ) {W : Submodule R₁ M₁} (hW : Disjoint W ()) :

The restriction of a reflexive bilinear form B onto a submodule W is nondegenerate if Disjoint W (B.orthogonal W).

theorem BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} [] {B : } {v : Basis n R M} (h : ) (hB : ) (i : n) :
¬BilinForm.IsOrtho B (v i) (v i)

An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal elements.

theorem BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} [] [] (B : ) (v : Basis n R M) (hO : ) :
∀ (i : n), ¬BilinForm.IsOrtho B (v i) (v i)

Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate iff the basis has no elements which are self-orthogonal.

theorem BilinForm.toLin_restrict_ker_eq_inf_orthogonal {V : Type u_9} {K : Type u_10} [] [] [Module K V] (B : ) (W : Subspace K V) (b : ) :
Submodule.map () (LinearMap.ker (LinearMap.domRestrict (BilinForm.toLin B) W)) =
theorem BilinForm.finrank_add_finrank_orthogonal {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {B : } {W : Subspace K V} (b₁ : ) :
theorem BilinForm.restrict_nondegenerate_of_isCompl_orthogonal {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {B : } {W : Subspace K V} (b₁ : ) (b₂ : ) :
IsCompl W ()

A subspace is complement to its orthogonal complement with respect to some reflexive bilinear form if that bilinear form restricted on to the subspace is nondegenerate.

theorem BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {B : } {W : Subspace K V} (b₁ : ) :

A subspace is complement to its orthogonal complement with respect to some reflexive bilinear form if and only if that bilinear form restricted on to the subspace is nondegenerate.

noncomputable def BilinForm.toDual {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] (B : ) (b : ) :

Given a nondegenerate bilinear form B on a finite-dimensional vector space, B.toDual is the linear equivalence between a vector space and its dual with the underlying linear map B.toLin.

Instances For
theorem BilinForm.toDual_def {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {B : } (b : ) {m : V} {n : V} :
↑(↑() m) n =
noncomputable def BilinForm.dualBasis {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {ι : Type u_12} [] [] (B : ) (hB : ) (b : Basis ι K V) :
Basis ι K V

The B-dual basis B.dualBasis hB b to a finite basis b satisfies B (B.dualBasis hB b i) (b j) = B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0, where B is a nondegenerate (symmetric) bilinear form and b is a finite basis.

Instances For
@[simp]
theorem BilinForm.dualBasis_repr_apply {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {ι : Type u_12} [] [] (B : ) (hB : ) (b : Basis ι K V) (x : V) (i : ι) :
↑(().repr x) i = BilinForm.bilin B x (b i)
theorem BilinForm.apply_dualBasis_left {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {ι : Type u_12} [] [] (B : ) (hB : ) (b : Basis ι K V) (i : ι) (j : ι) :
BilinForm.bilin B (↑() i) (b j) = if j = i then 1 else 0
theorem BilinForm.apply_dualBasis_right {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] {ι : Type u_12} [] [] (B : ) (hB : ) (sym : ) (b : Basis ι K V) (i : ι) (j : ι) :
BilinForm.bilin B (b i) (↑() j) = if i = j then 1 else 0

We note that we cannot use BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal for the lemma below since the below lemma does not require V to be finite dimensional. However, BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal does not require B to be nondegenerate on the whole space.

theorem BilinForm.restrictOrthogonalSpanSingletonNondegenerate {V : Type u_9} {K : Type u_10} [] [] [Module K V] (B : ) (b₁ : ) (b₂ : ) {x : V} (hx : ¬) :

The restriction of a reflexive, non-degenerate bilinear form on the orthogonal complement of the span of a singleton is also non-degenerate.

theorem BilinForm.compLeft_injective {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B : BilinForm R₁ M₁) (b : ) :
theorem BilinForm.isAdjointPair_unique_of_nondegenerate {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [] [Module R₁ M₁] (B : BilinForm R₁ M₁) (b : ) (φ : M₁ →ₗ[R₁] M₁) (ψ₁ : M₁ →ₗ[R₁] M₁) (ψ₂ : M₁ →ₗ[R₁] M₁) (hψ₁ : ) (hψ₂ : ) :
ψ₁ = ψ₂
noncomputable def BilinForm.symmCompOfNondegenerate {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] (B₁ : ) (B₂ : ) (b₂ : ) :

Given bilinear forms B₁, B₂ where B₂ is nondegenerate, symmCompOfNondegenerate is the linear map B₂.toLin⁻¹ ∘ B₁.toLin.

Instances For
theorem BilinForm.comp_symmCompOfNondegenerate_apply {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] (B₁ : ) {B₂ : } (b₂ : ) (v : V) :
↑(BilinForm.toLin B₂) (↑() v) = ↑(BilinForm.toLin B₁) v
@[simp]
theorem BilinForm.symmCompOfNondegenerate_left_apply {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] (B₁ : ) {B₂ : } (b₂ : ) (v : V) (w : V) :
BilinForm.bilin B₂ (↑() w) v = BilinForm.bilin B₁ w v
noncomputable def BilinForm.leftAdjointOfNondegenerate {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] (B : ) (b : ) (φ : V →ₗ[K] V) :

Given the nondegenerate bilinear form B and the linear map φ, leftAdjointOfNondegenerate provides the left adjoint of φ with respect to B. The lemma proving this property is BilinForm.isAdjointPairLeftAdjointOfNondegenerate.

Instances For
theorem BilinForm.isAdjointPairLeftAdjointOfNondegenerate {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] (B : ) (b : ) (φ : V →ₗ[K] V) :
theorem BilinForm.isAdjointPair_iff_eq_of_nondegenerate {V : Type u_9} {K : Type u_10} [] [] [Module K V] [] (B : ) (b : ) (ψ : V →ₗ[K] V) (φ : V →ₗ[K] V) :

Given the nondegenerate bilinear form B, the linear map φ has a unique left adjoint given by BilinForm.leftAdjointOfNondegenerate.