mathlib documentation

linear_algebra.bilinear_form

Bilinear form #

This file defines a bilinear form over a module. Basic ideas such as orthogonality are also introduced, as well as reflexivive, 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 x 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 quadratic_form.lean with exists_orthogonal_basis.

Notations #

Given any term B of type bilin_form, 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:

References #

Tags #

Bilinear form,

structure bilin_form (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] :
Type (max u_1 u_2)
  • bilin : M → M → R
  • bilin_add_left : ∀ (x y z : M), self.bilin (x + y) z = self.bilin x z + self.bilin y z
  • bilin_smul_left : ∀ (a : R) (x y : M), self.bilin (a x) y = a * self.bilin x y
  • bilin_add_right : ∀ (x y z : M), self.bilin x (y + z) = self.bilin x y + self.bilin x z
  • bilin_smul_right : ∀ (a : R) (x y : M), self.bilin x (a y) = a * self.bilin x y

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

@[protected, instance]
def bilin_form.has_coe_to_fun {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
has_coe_to_fun (bilin_form R M) (λ (_x : bilin_form R M), M → M → R)
Equations
@[simp]
theorem bilin_form.coe_fn_mk {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (f : M → M → R) (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₄} = f
theorem bilin_form.coe_fn_congr {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {x x' y y' : M} :
x = x'y = y'B x y = B x' y'
@[simp]
theorem bilin_form.add_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (x y z : M) :
B (x + y) z = B x z + B y z
@[simp]
theorem bilin_form.smul_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (a : R) (x y : M) :
B (a x) y = a * B x y
@[simp]
theorem bilin_form.add_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (x y z : M) :
B x (y + z) = B x y + B x z
@[simp]
theorem bilin_form.smul_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (a : R) (x y : M) :
B x (a y) = a * B x y
@[simp]
theorem bilin_form.zero_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (x : M) :
B 0 x = 0
@[simp]
theorem bilin_form.zero_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (x : M) :
B x 0 = 0
@[simp]
theorem bilin_form.neg_left {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (x y : M₁) :
B₁ (-x) y = -B₁ x y
@[simp]
theorem bilin_form.neg_right {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (x y : M₁) :
B₁ x (-y) = -B₁ x y
@[simp]
theorem bilin_form.sub_left {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (x y z : M₁) :
B₁ (x - y) z = B₁ x z - B₁ y z
@[simp]
theorem bilin_form.sub_right {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (x y z : M₁) :
B₁ x (y - z) = B₁ x y - B₁ x z
@[ext]
theorem bilin_form.ext {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B D : bilin_form R M} (H : ∀ (x y : M), B x y = D x y) :
B = D
theorem bilin_form.congr_fun {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B D : bilin_form R M} (h : B = D) (x y : M) :
B x y = D x y
theorem bilin_form.ext_iff {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B D : bilin_form R M} :
B = D ∀ (x y : M), B x y = D x y
@[protected, instance]
def bilin_form.add_comm_monoid {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[protected, instance]
def bilin_form.add_comm_group {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] :
Equations
@[simp]
theorem bilin_form.add_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B D : bilin_form R M} (x y : M) :
(B + D) x y = B x y + D x y
@[simp]
theorem bilin_form.zero_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (x y : M) :
0 x y = 0
@[simp]
theorem bilin_form.neg_apply {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (x y : M₁) :
(-B₁) x y = -B₁ x y
@[protected, instance]
def bilin_form.inhabited {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[protected, instance]
def bilin_form.module {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] :
module R₂ (bilin_form R M)

bilin_form R M inherits the scalar action from any commutative subalgebra R₂ of R.

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

Equations
@[simp]
theorem bilin_form.smul_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] (B : bilin_form R M) (a : R₂) (x y : M) :
(a B) x y = a B x y
def bilin_form.flip_hom_aux {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (R₂ : Type u_5) [comm_semiring R₂] [algebra R₂ R] :

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

Equations
theorem bilin_form.flip_flip_aux {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] (A : bilin_form R M) :
def bilin_form.flip_hom {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (R₂ : Type u_5) [comm_semiring R₂] [algebra 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.

Equations
@[simp]
theorem bilin_form.flip_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] (A : bilin_form R M) (x y : M) :
((bilin_form.flip_hom R₂) A) x y = A y x
theorem bilin_form.flip_flip {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] :
def bilin_form.flip' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [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.

def bilin_form.flip {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] :
bilin_form R₂ M₂ ≃ₗ[R₂] bilin_form R₂ M₂

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

def bilin_form.to_lin_hom_aux₁ {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (A : bilin_form R M) (x : M) :

Auxiliary definition to define to_lin_hom; see below.

Equations
def bilin_form.to_lin_hom_aux₂ {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] [module R₂ M] [is_scalar_tower R₂ R M] (A : bilin_form R M) :
M →ₗ[R₂] M →ₗ[R] R

Auxiliary definition to define to_lin_hom; see below.

Equations
def bilin_form.to_lin_hom {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (R₂ : Type u_5) [comm_semiring R₂] [algebra R₂ R] [module R₂ M] [is_scalar_tower R₂ R M] :

The linear map obtained from a bilin_form 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 to_lin', which is -linear. Over a commutative semiring, use to_lin, which is linear.

Equations
@[simp]
theorem bilin_form.to_lin'_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] [module R₂ M] [is_scalar_tower R₂ R M] (A : bilin_form R M) (x : M) :
def bilin_form.to_lin' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :

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

@[simp]
theorem bilin_form.sum_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {α : Type u_3} (t : finset α) (g : α → M) (w : M) :
B (∑ (i : α) in t, g i) w = ∑ (i : α) in t, B (g i) w
@[simp]
theorem bilin_form.sum_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {α : Type u_3} (t : finset α) (w : M) (g : α → M) :
B w (∑ (i : α) in t, g i) = ∑ (i : α) in t, B w (g i)
def bilin_form.to_lin_hom_flip {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (R₂ : Type u_5) [comm_semiring R₂] [algebra R₂ R] [module R₂ M] [is_scalar_tower R₂ R M] :

The linear map obtained from a bilin_form 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 to_lin'_flip, which is -linear. Over a commutative semiring, use to_lin_flip, which is linear.

Equations
@[simp]
theorem bilin_form.to_lin'_flip_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] [module R₂ M] [is_scalar_tower R₂ R M] (A : bilin_form R M) (x : M) :
(((bilin_form.to_lin_hom_flip R₂) A) x) = λ (y : M), A y x
def bilin_form.to_lin'_flip {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :

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

def linear_map.to_bilin_aux {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) :
bilin_form 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 linear_map.to_bilin.

Equations
def bilin_form.to_lin {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] :
bilin_form R₂ M₂ ≃ₗ[R₂] M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂

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

Equations
def linear_map.to_bilin {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] :
(M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) ≃ₗ[R₂] bilin_form R₂ M₂

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

Equations
@[simp]
theorem linear_map.to_bilin_aux_eq {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) :
@[simp]
theorem linear_map.to_bilin_symm {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] :
@[simp]
theorem bilin_form.to_lin_symm {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] :
@[simp, norm_cast]
theorem bilin_form.to_lin_apply {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {B₂ : bilin_form R₂ M₂} (x : M₂) :
def bilin_form.comp {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {M' : Type w} [add_comm_monoid M'] [module R M'] (B : bilin_form R M') (l r : M →ₗ[R] M') :

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

Equations
def bilin_form.comp_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (f : M →ₗ[R] M) :

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

Equations
def bilin_form.comp_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (f : M →ₗ[R] M) :

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

Equations
theorem bilin_form.comp_comp {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {M' : Type w} [add_comm_monoid M'] [module R M'] {M'' : Type u_3} [add_comm_monoid M''] [module R M''] (B : bilin_form R M'') (l r : M →ₗ[R] M') (l' r' : M' →ₗ[R] M'') :
(B.comp l' r').comp l r = B.comp (l'.comp l) (r'.comp r)
@[simp]
theorem bilin_form.comp_left_comp_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (l r : M →ₗ[R] M) :
(B.comp_left l).comp_right r = B.comp l r
@[simp]
theorem bilin_form.comp_right_comp_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (l r : M →ₗ[R] M) :
(B.comp_right r).comp_left l = B.comp l r
@[simp]
theorem bilin_form.comp_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {M' : Type w} [add_comm_monoid M'] [module R M'] (B : bilin_form R M') (l r : M →ₗ[R] M') (v w : M) :
(B.comp l r) v w = B (l v) (r w)
@[simp]
theorem bilin_form.comp_left_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (f : M →ₗ[R] M) (v w : M) :
(B.comp_left f) v w = B (f v) w
@[simp]
theorem bilin_form.comp_right_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (f : M →ₗ[R] M) (v w : M) :
(B.comp_right f) v w = B v (f w)
@[simp]
theorem bilin_form.comp_id_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (r : M →ₗ[R] M) :
@[simp]
theorem bilin_form.comp_id_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (l : M →ₗ[R] M) :
@[simp]
theorem bilin_form.comp_left_id {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :
@[simp]
theorem bilin_form.comp_right_id {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :
@[simp]
theorem bilin_form.comp_id_id {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :
theorem bilin_form.comp_inj {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {M' : Type w} [add_comm_monoid M'] [module R M'] (B₁ B₂ : bilin_form R M') {l r : M →ₗ[R] M'} (hₗ : function.surjective l) (hᵣ : function.surjective r) :
B₁.comp l r = B₂.comp l r B₁ = B₂
def bilin_form.congr {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} [add_comm_monoid M₂'] [module R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') :
bilin_form R₂ M₂ ≃ₗ[R₂] bilin_form R₂ M₂'

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

Equations
@[simp]
theorem bilin_form.congr_apply {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} [add_comm_monoid M₂'] [module R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') (B : bilin_form R₂ M₂) (x y : M₂') :
((bilin_form.congr e) B) x y = B ((e.symm) x) ((e.symm) y)
@[simp]
theorem bilin_form.congr_symm {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} [add_comm_monoid M₂'] [module R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') :
@[simp]
theorem bilin_form.congr_refl {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] :
theorem bilin_form.congr_trans {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [add_comm_monoid M₂'] [add_comm_monoid M₂''] [module R₂ M₂'] [module R₂ M₂''] (e : M₂ ≃ₗ[R₂] M₂') (f : M₂' ≃ₗ[R₂] M₂'') :
theorem bilin_form.congr_congr {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [add_comm_monoid M₂'] [add_comm_monoid M₂''] [module R₂ M₂'] [module R₂ M₂''] (e : M₂' ≃ₗ[R₂] M₂'') (f : M₂ ≃ₗ[R₂] M₂') (B : bilin_form R₂ M₂) :
theorem bilin_form.congr_comp {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [add_comm_monoid M₂'] [add_comm_monoid M₂''] [module R₂ M₂'] [module R₂ M₂''] (e : M₂ ≃ₗ[R₂] M₂') (B : bilin_form R₂ M₂) (l r : M₂'' →ₗ[R₂] M₂') :
((bilin_form.congr e) B).comp l r = B.comp ((e.symm).comp l) ((e.symm).comp r)
theorem bilin_form.comp_congr {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [add_comm_monoid M₂'] [add_comm_monoid M₂''] [module R₂ M₂'] [module R₂ M₂''] (e : M₂' ≃ₗ[R₂] M₂'') (B : bilin_form R₂ M₂) (l r : M₂' →ₗ[R₂] M₂) :
(bilin_form.congr e) (B.comp l r) = B.comp (l.comp (e.symm)) (r.comp (e.symm))
def bilin_form.lin_mul_lin {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] (f g : M₂ →ₗ[R₂] R₂) :
bilin_form R₂ M₂

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

Equations
@[simp]
theorem bilin_form.lin_mul_lin_apply {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {f g : M₂ →ₗ[R₂] R₂} (x y : M₂) :
(bilin_form.lin_mul_lin f g) x y = (f x) * g y
@[simp]
theorem bilin_form.lin_mul_lin_comp {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} [add_comm_monoid M₂'] [module R₂ M₂'] {f g : M₂ →ₗ[R₂] R₂} (l r : M₂' →ₗ[R₂] M₂) :
@[simp]
theorem bilin_form.lin_mul_lin_comp_left {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {f g : M₂ →ₗ[R₂] R₂} (l : M₂ →ₗ[R₂] M₂) :
@[simp]
theorem bilin_form.lin_mul_lin_comp_right {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {f g : M₂ →ₗ[R₂] R₂} (r : M₂ →ₗ[R₂] M₂) :
def bilin_form.is_ortho {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (x y : M) :
Prop

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

Equations
theorem bilin_form.is_ortho_def {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {x y : M} :
B.is_ortho x y B x y = 0
theorem bilin_form.is_ortho_zero_left {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (x : M) :
B.is_ortho 0 x
theorem bilin_form.is_ortho_zero_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (x : M) :
B.is_ortho x 0
theorem bilin_form.ne_zero_of_not_is_ortho_self {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] {B : bilin_form K V} (x : V) (hx₁ : ¬B.is_ortho x x) :
x 0
def bilin_form.is_Ortho {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {n : Type w} (B : bilin_form R M) (v : n → M) :
Prop

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 bilin_form.is_ortho

Equations
theorem bilin_form.is_Ortho_def {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {n : Type w} {B : bilin_form R M} {v : n → M} :
B.is_Ortho v ∀ (i j : n), i jB (v i) (v j) = 0
@[simp]
theorem bilin_form.is_ortho_smul_left {R₄ : Type u_13} {M₄ : Type u_14} [ring R₄] [is_domain R₄] [add_comm_group M₄] [module R₄ M₄] {G : bilin_form R₄ M₄} {x y : M₄} {a : R₄} (ha : a 0) :
G.is_ortho (a x) y G.is_ortho x y
@[simp]
theorem bilin_form.is_ortho_smul_right {R₄ : Type u_13} {M₄ : Type u_14} [ring R₄] [is_domain R₄] [add_comm_group M₄] [module R₄ M₄] {G : bilin_form R₄ M₄} {x y : M₄} {a : R₄} (ha : a 0) :
G.is_ortho x (a y) G.is_ortho x y
theorem bilin_form.linear_independent_of_is_Ortho {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] {n : Type w} {B : bilin_form K V} {v : n → V} (hv₁ : B.is_Ortho v) (hv₂ : ∀ (i : n), ¬B.is_ortho (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 bilin_form.ext_basis {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {B₃ F₃ : bilin_form R₃ M₃} {ι : Type u_13} (b : basis ι R₃ M₃) (h : ∀ (i j : ι), B₃ (b i) (b j) = F₃ (b i) (b j)) :
B₃ = F₃

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

theorem bilin_form.sum_repr_mul_repr_mul {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {B₃ : bilin_form R₃ M₃} {ι : Type u_13} (b : basis ι R₃ M₃) (x y : M₃) :
((b.repr) x).sum (λ (i : ι) (xi : R₃), ((b.repr) y).sum (λ (j : ι) (yj : R₃), xi yj B₃ (b i) (b j))) = B₃ x y

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

def bilin_form.is_refl {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :
Prop

The proposition that a bilinear form is reflexive

Equations
theorem bilin_form.is_refl.eq_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (H : B.is_refl) {x y : M} :
B x y = 0B y x = 0
theorem bilin_form.is_refl.ortho_comm {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (H : B.is_refl) {x y : M} :
B.is_ortho x y B.is_ortho y x
def bilin_form.is_symm {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :
Prop

The proposition that a bilinear form is symmetric

Equations
@[protected]
theorem bilin_form.is_symm.eq {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (H : B.is_symm) (x y : M) :
B x y = B y x
theorem bilin_form.is_symm.is_refl {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (H : B.is_symm) :
theorem bilin_form.is_symm.ortho_comm {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (H : B.is_symm) {x y : M} :
B.is_ortho x y B.is_ortho y x
theorem bilin_form.is_symm_iff_flip' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R₂ : Type u_5} [comm_semiring R₂] {B : bilin_form R M} [algebra R₂ R] :
def bilin_form.is_alt {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :
Prop

The proposition that a bilinear form is alternating

Equations
theorem bilin_form.is_alt.self_eq_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (H : B.is_alt) (x : M) :
B x x = 0
theorem bilin_form.is_alt.neg {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (H : B₁.is_alt) (x y : M₁) :
-B₁ x y = B₁ y x
theorem bilin_form.is_alt.is_refl {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (H : B₁.is_alt) :
B₁.is_refl
theorem bilin_form.is_alt.ortho_comm {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (H : B₁.is_alt) {x y : M₁} :
B₁.is_ortho x y B₁.is_ortho y x
def bilin_form.is_adjoint_pair {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) {M' : Type u_13} [add_comm_monoid M'] [module R M'] (B' : bilin_form R M') (f : M →ₗ[R] M') (g : M' →ₗ[R] M) :
Prop

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

Equations
theorem bilin_form.is_adjoint_pair.eq {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {M' : Type u_13} [add_comm_monoid M'] [module R M'] {B' : bilin_form R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} (h : B.is_adjoint_pair B' f g) {x : M} {y : M'} :
B' (f x) y = B x (g y)
theorem bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (F : bilin_form R M) (f g : module.End R M) :
theorem bilin_form.is_adjoint_pair_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {M' : Type u_13} [add_comm_monoid M'] [module R M'] {B' : bilin_form R M'} :
theorem bilin_form.is_adjoint_pair_id {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} :
theorem bilin_form.is_adjoint_pair.add {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {M' : Type u_13} [add_comm_monoid M'] [module R M'] {B' : bilin_form R M'} {f f' : M →ₗ[R] M'} {g g' : M' →ₗ[R] M} (h : B.is_adjoint_pair B' f g) (h' : B.is_adjoint_pair B' f' g') :
B.is_adjoint_pair B' (f + f') (g + g')
theorem bilin_form.is_adjoint_pair.sub {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} {M₁' : Type u_14} [add_comm_group M₁'] [module R₁ M₁'] {B₁' : bilin_form R₁ M₁'} {f₁ f₁' : M₁ →ₗ[R₁] M₁'} {g₁ g₁' : M₁' →ₗ[R₁] M₁} (h : B₁.is_adjoint_pair B₁' f₁ g₁) (h' : B₁.is_adjoint_pair B₁' f₁' g₁') :
B₁.is_adjoint_pair B₁' (f₁ - f₁') (g₁ - g₁')
theorem bilin_form.is_adjoint_pair.smul {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {B₂ : bilin_form R₂ M₂} {M₂' : Type u_11} [add_comm_monoid M₂'] [module R₂ M₂'] {B₂' : bilin_form R₂ M₂'} {f₂ : M₂ →ₗ[R₂] M₂'} {g₂ : M₂' →ₗ[R₂] M₂} (c : R₂) (h : B₂.is_adjoint_pair B₂' f₂ g₂) :
B₂.is_adjoint_pair B₂' (c f₂) (c g₂)
theorem bilin_form.is_adjoint_pair.comp {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {M' : Type u_13} [add_comm_monoid M'] [module R M'] {B' : bilin_form R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} {M'' : Type u_15} [add_comm_monoid M''] [module R M''] (B'' : bilin_form R M'') {f' : M' →ₗ[R] M''} {g' : M'' →ₗ[R] M'} (h : B.is_adjoint_pair B' f g) (h' : B'.is_adjoint_pair B'' f' g') :
B.is_adjoint_pair B'' (f'.comp f) (g.comp g')
theorem bilin_form.is_adjoint_pair.mul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {f g f' g' : module.End R M} (h : B.is_adjoint_pair B f g) (h' : B.is_adjoint_pair B f' g') :
B.is_adjoint_pair B (f * f') (g' * g)
def bilin_form.is_pair_self_adjoint {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B F : bilin_form R M) (f : module.End R M) :
Prop

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.

Equations
def bilin_form.is_pair_self_adjoint_submodule {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] (B₂ F₂ : bilin_form R₂ M₂) :
submodule R₂ (module.End R₂ M₂)

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

Equations
@[simp]
theorem bilin_form.mem_is_pair_self_adjoint_submodule {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] (B₂ F₂ : bilin_form R₂ M₂) (f : module.End R₂ M₂) :
theorem bilin_form.is_pair_self_adjoint_equiv {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {M₃' : Type u_16} [add_comm_group M₃'] [module R₃ M₃'] (B₃ F₃ : bilin_form R₃ M₃) (e : M₃' ≃ₗ[R₃] M₃) (f : module.End R₃ M₃) :
def bilin_form.is_self_adjoint {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (f : module.End R M) :
Prop

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

Equations
def bilin_form.is_skew_adjoint {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B₁ : bilin_form R₁ M₁) (f : module.End R₁ M₁) :
Prop

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

Equations
theorem bilin_form.is_skew_adjoint_iff_neg_self_adjoint {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B₁ : bilin_form R₁ M₁) (f : module.End R₁ M₁) :
B₁.is_skew_adjoint f (-B₁).is_adjoint_pair B₁ f f
def bilin_form.self_adjoint_submodule {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] (B₂ : bilin_form 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.)

Equations
@[simp]
theorem bilin_form.mem_self_adjoint_submodule {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] (B₂ : bilin_form R₂ M₂) (f : module.End R₂ M₂) :
def bilin_form.skew_adjoint_submodule {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] (B₃ : bilin_form 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.)

Equations
@[simp]
theorem bilin_form.mem_skew_adjoint_submodule {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] (B₃ : bilin_form R₃ M₃) (f : module.End R₃ M₃) :
def bilin_form.orthogonal {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (N : submodule R M) :

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.

Equations
@[simp]
theorem bilin_form.mem_orthogonal_iff {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {N : submodule R M} {m : M} :
m B.orthogonal N ∀ (n : M), n NB.is_ortho n m
theorem bilin_form.orthogonal_le {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {N L : submodule R M} (h : N L) :
theorem bilin_form.le_orthogonal_orthogonal {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} {N : submodule R M} (b : B.is_refl) :
theorem bilin_form.span_singleton_inf_orthogonal_eq_bot {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] {B : bilin_form K V} {x : V} (hx : ¬B.is_ortho x x) :
theorem bilin_form.orthogonal_span_singleton_eq_to_lin_ker {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] {B : bilin_form K V} (x : V) :
theorem bilin_form.span_singleton_sup_orthogonal_eq_top {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] {B : bilin_form K V} {x : V} (hx : ¬B.is_ortho x x) :
theorem bilin_form.is_compl_span_singleton_orthogonal {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] {B : bilin_form K V} {x : V} (hx : ¬B.is_ortho x x) :

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.

def bilin_form.restrict {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (W : submodule R M) :

The restriction of a bilinear form on a submodule.

Equations
@[simp]
theorem bilin_form.restrict_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (W : submodule R M) (a b : W) :
(B.restrict W) a b = B a b
theorem bilin_form.restrict_symm {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (b : B.is_symm) (W : submodule R M) :

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

def bilin_form.nondegenerate {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :
Prop

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.

Equations
theorem bilin_form.not_nondegenerate_zero (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] [nontrivial M] :

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

theorem bilin_form.nondegenerate.ne_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] [nontrivial M] {B : bilin_form R M} (h : B.nondegenerate) :
B 0
theorem bilin_form.nondegenerate.congr {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} [add_comm_monoid M₂'] [module R₂ M₂'] {B : bilin_form R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') (h : B.nondegenerate) :
@[simp]
theorem bilin_form.nondegenerate_congr_iff {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {M₂' : Type u_11} [add_comm_monoid M₂'] [module R₂ M₂'] {B : bilin_form R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') :
theorem bilin_form.nondegenerate_iff_ker_eq_bot {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {B : bilin_form R₂ M₂} :

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

theorem bilin_form.nondegenerate.ker_eq_bot {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {B : bilin_form R₂ M₂} (h : B.nondegenerate) :
theorem bilin_form.nondegenerate_restrict_of_disjoint_orthogonal {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B : bilin_form R₁ M₁) (b : B.is_refl) {W : submodule R₁ M₁} (hW : disjoint W (B.orthogonal W)) :

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

theorem bilin_form.is_Ortho.not_is_ortho_basis_self_of_nondegenerate {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {n : Type w} [nontrivial R] {B : bilin_form R M} {v : basis n R M} (h : B.is_Ortho v) (hB : B.nondegenerate) (i : n) :
¬B.is_ortho (v i) (v i)

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

theorem bilin_form.is_Ortho.nondegenerate_iff_not_is_ortho_basis_self {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {n : Type w} [nontrivial R] [no_zero_divisors R] (B : bilin_form R M) (v : basis n R M) (hO : B.is_Ortho v) :
B.nondegenerate ∀ (i : n), ¬B.is_ortho (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 bilin_form.restrict_nondegenerate_of_is_compl_orthogonal {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {B : bilin_form K V} {W : subspace K V} (b₁ : B.is_refl) (b₂ : (B.restrict W).nondegenerate) :

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 bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {B : bilin_form K V} {W : subspace K V} (b₁ : B.is_refl) :

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 bilin_form.to_dual {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (B : bilin_form K V) (b : B.nondegenerate) :

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

Equations
theorem bilin_form.to_dual_def {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {B : bilin_form K V} (b : B.nondegenerate) {m n : V} :
((B.to_dual b) m) n = B m n
noncomputable def bilin_form.dual_basis {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {ι : Type u_12} [decidable_eq ι] [fintype ι] (B : bilin_form K V) (hB : B.nondegenerate) (b : basis ι K V) :
basis ι K V

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

Equations
@[simp]
theorem bilin_form.dual_basis_repr_apply {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {ι : Type u_12} [decidable_eq ι] [fintype ι] (B : bilin_form K V) (hB : B.nondegenerate) (b : basis ι K V) (x : V) (i : ι) :
(((B.dual_basis hB b).repr) x) i = B x (b i)
theorem bilin_form.apply_dual_basis_left {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {ι : Type u_12} [decidable_eq ι] [fintype ι] (B : bilin_form K V) (hB : B.nondegenerate) (b : basis ι K V) (i j : ι) :
B ((B.dual_basis hB b) i) (b j) = ite (j = i) 1 0
theorem bilin_form.apply_dual_basis_right {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {ι : Type u_12} [decidable_eq ι] [fintype ι] (B : bilin_form K V) (hB : B.nondegenerate) (sym : B.is_symm) (b : basis ι K V) (i j : ι) :
B (b i) ((B.dual_basis hB b) j) = ite (i = j) 1 0

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

theorem bilin_form.restrict_orthogonal_span_singleton_nondegenerate {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] (B : bilin_form K V) (b₁ : B.nondegenerate) (b₂ : B.is_refl) {x : V} (hx : ¬B.is_ortho x x) :

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

theorem bilin_form.comp_left_injective {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B : bilin_form R₁ M₁) (b : B.nondegenerate) :
theorem bilin_form.is_adjoint_pair_unique_of_nondegenerate {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B : bilin_form R₁ M₁) (b : B.nondegenerate) (φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁) (hψ₁ : B.is_adjoint_pair B ψ₁ φ) (hψ₂ : B.is_adjoint_pair B ψ₂ φ) :
ψ₁ = ψ₂
noncomputable def bilin_form.symm_comp_of_nondegenerate {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (B₁ B₂ : bilin_form K V) (b₂ : B₂.nondegenerate) :

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

Equations
theorem bilin_form.comp_symm_comp_of_nondegenerate_apply {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (B₁ : bilin_form K V) {B₂ : bilin_form K V} (b₂ : B₂.nondegenerate) (v : V) :
@[simp]
theorem bilin_form.symm_comp_of_nondegenerate_left_apply {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (B₁ : bilin_form K V) {B₂ : bilin_form K V} (b₂ : B₂.nondegenerate) (v w : V) :
B₂ ((B₁.symm_comp_of_nondegenerate B₂ b₂) w) v = B₁ w v
noncomputable def bilin_form.left_adjoint_of_nondegenerate {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (B : bilin_form K V) (b : B.nondegenerate) (φ : V →ₗ[K] V) :

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

Equations
theorem bilin_form.is_adjoint_pair_left_adjoint_of_nondegenerate {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (B : bilin_form K V) (b : B.nondegenerate) (φ : V →ₗ[K] V) :
theorem bilin_form.is_adjoint_pair_iff_eq_of_nondegenerate {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (B : bilin_form K V) (b : B.nondegenerate) (ψ φ : V →ₗ[K] V) :

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