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

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) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] :
Type (max u v)
  • bilin : M → M → R
  • bilin_add_left : ∀ (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z
  • bilin_smul_left : ∀ (a : R) (x y : M), c.bilin (a x) y = a * c.bilin x y
  • bilin_add_right : ∀ (x y z : M), c.bilin x (y + z) = c.bilin x y + c.bilin x z
  • bilin_smul_right : ∀ (a : R) (x y : M), c.bilin x (a y) = a * c.bilin x y

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

@[instance]
def bilin_form.has_coe_to_fun {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[simp]
theorem bilin_form.coe_fn_mk {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (x : M) :
B 0 x = 0

@[simp]
theorem bilin_form.zero_right {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (x : M) :
B x 0 = 0

@[simp]
theorem bilin_form.neg_left {R₁ : Type u} {M₁ : Type v} [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} {M₁ : Type v} [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} {M₁ : Type v} [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} {M₁ : Type v} [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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B D : bilin_form R M} (H : ∀ (x y : M), B x y = D x y) :
B = D

@[instance]
def bilin_form.add_comm_monoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def bilin_form.add_comm_group {R₁ : Type u} {M₁ : Type v} [ring R₁] [add_comm_group M₁] [module R₁ M₁] :

Equations
@[simp]
theorem bilin_form.add_apply {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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.neg_apply {R₁ : Type u} {M₁ : Type v} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (x y : M₁) :
(-B₁) x y = -B₁ x y

@[instance]
def bilin_form.inhabited {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def bilin_form.semimodule {M : Type v} [add_comm_monoid M] {R : Type u_1} [comm_semiring R] [semimodule R M] :

Equations
@[simp]
theorem bilin_form.smul_apply {M : Type v} [add_comm_monoid M] {R : Type u_1} [comm_semiring R] [semimodule R M] (B : bilin_form R M) (a : R) (x y : M) :
(a B) x y = a B x y

def linear_map.to_bilin_aux {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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 linear_map.to_bilin {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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
def bilin_form.to_lin {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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
@[simp]
theorem linear_map.to_bilin_aux_eq {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] (f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) :

@[simp]
theorem linear_map.to_bilin_symm {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] :

@[simp]
theorem bilin_form.to_lin_symm {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] :

@[simp]
theorem to_linear_map_apply {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {B₂ : bilin_form R₂ M₂} (x : M₂) :

@[simp]
theorem map_sum_left {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {B₂ : bilin_form R₂ M₂} {α : Type u_1} (t : finset α) (g : α → M₂) (w : M₂) :
B₂ (∑ (i : α) in t, g i) w = ∑ (i : α) in t, B₂ (g i) w

@[simp]
theorem map_sum_right {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {B₂ : bilin_form R₂ M₂} {α : Type u_1} (t : finset α) (w : M₂) (g : α → M₂) :
B₂ w (∑ (i : α) in t, g i) = ∑ (i : α) in t, B₂ w (g i)

def bilin_form.comp {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type w} [add_comm_monoid M'] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type w} [add_comm_monoid M'] [semimodule R M'] {M'' : Type u_1} [add_comm_monoid M''] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type w} [add_comm_monoid M'] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) (f : M →ₗ[R] M) (v w : M) :
(B.comp_right f) v w = B v (f w)

theorem bilin_form.comp_injective {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type w} [add_comm_monoid M'] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_1} [add_comm_monoid M₂'] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_1} [add_comm_monoid M₂'] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_1} [add_comm_monoid M₂'] [semimodule R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') :

theorem bilin_form.congr_comp {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_1} [add_comm_monoid M₂'] [semimodule R₂ M₂'] {M₂'' : Type u_2} [add_comm_monoid M₂''] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_1} [add_comm_monoid M₂'] [semimodule R₂ M₂'] {M₂'' : Type u_2} [add_comm_monoid M₂''] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_1} [add_comm_monoid M₂'] [semimodule R₂ M₂'] {f g : M₂ →ₗ[R₂] R₂} (l r : M₂' →ₗ[R₂] M₂) :

@[simp]
theorem bilin_form.lin_mul_lin_comp_left {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {f g : M₂ →ₗ[R₂] R₂} (l : M₂ →ₗ[R₂] M₂) :

@[simp]
theorem bilin_form.lin_mul_lin_comp_right {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {f g : M₂ →ₗ[R₂] R₂} (r : M₂ →ₗ[R₂] M₂) :

def bilin_form.is_ortho {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) (x y : M) :
Prop

The proposition that two elements of a bilinear form space are orthogonal

Equations
theorem bilin_form.ortho_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (x : M) :
B.is_ortho 0 x

@[simp]
theorem bilin_form.is_ortho_smul_left {R₄ : Type u_2} {M₄ : Type u_3} [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_2} {M₄ : Type u_3} [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.ext_basis {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {B₃ F₃ : bilin_form R₃ M₃} {ι : Type u_2} {b : ι → M₃} (hb : is_basis R₃ b) (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} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {B₃ : bilin_form R₃ M₃} {ι : Type u_2} {b : ι → M₃} (hb : is_basis R₃ b) (x y : M₃) :
((hb.repr) x).sum (λ (i : ι) (xi : R₃), ((hb.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 matrix.to_bilin'_aux {R₂ : Type u} [comm_semiring R₂] {n : Type u_1} [fintype n] (M : matrix n n R₂) :
bilin_form 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.to_bilin_form'.

Equations
theorem matrix.to_bilin'_aux_std_basis {R₂ : Type u} [comm_semiring R₂] {n : Type u_1} [fintype n] [decidable_eq n] (M : matrix n n R₂) (i j : n) :
(M.to_bilin'_aux) ((linear_map.std_basis R₂ (λ (_x : n), R₂) i) 1) ((linear_map.std_basis R₂ (λ (_x : n), R₂) j) 1) = M i j

def bilin_form.to_matrix_aux {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {n : Type u_1} [fintype n] (b : n → M₂) :
bilin_form 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.to_bilin_form'.

Equations
theorem to_bilin'_aux_to_matrix_aux {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B₃ : bilin_form R₃ (n → R₃)) :
((bilin_form.to_matrix_aux (λ (j : n), (linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1)) B₃).to_bilin'_aux = B₃

### to_matrix' section

This section deals with the conversion between matrices and bilinear forms on n → R₃.

def bilin_form.to_matrix' {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] :
bilin_form R₃ (n → R₃) ≃ₗ[R₃] matrix n n R₃

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

Equations
@[simp]
theorem bilin_form.to_matrix_aux_std_basis {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) :
(bilin_form.to_matrix_aux (λ (j : n), (linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1)) B = bilin_form.to_matrix' B

def matrix.to_bilin' {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] :
matrix n n R₃ ≃ₗ[R₃] bilin_form R₃ (n → R₃)

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

Equations
@[simp]
theorem matrix.to_bilin'_aux_eq {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (M : matrix n n R₃) :

theorem matrix.to_bilin'_apply {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (M : matrix n n R₃) (x y : n → R₃) :
(matrix.to_bilin' M) x y = ∑ (i j : n), ((x i) * M i j) * y j

@[simp]
theorem matrix.to_bilin'_std_basis {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (M : matrix n n R₃) (i j : n) :
(matrix.to_bilin' M) ((linear_map.std_basis R₃ (λ (_x : n), R₃) i) 1) ((linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1) = M i j

@[simp]
theorem bilin_form.to_matrix'_symm {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] :

@[simp]
theorem matrix.to_bilin'_symm {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] :

@[simp]
theorem matrix.to_bilin'_to_matrix' {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) :

@[simp]
theorem bilin_form.to_matrix'_to_bilin' {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (M : matrix n n R₃) :

@[simp]
theorem bilin_form.to_matrix'_apply {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) (i j : n) :
bilin_form.to_matrix' B i j = B ((linear_map.std_basis R₃ (λ (_x : n), R₃) i) 1) ((linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1)

@[simp]
theorem bilin_form.to_matrix'_comp {R₃ : Type u} [comm_ring R₃] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (B : bilin_form R₃ (n → R₃)) (l r : (o → R₃) →ₗ[R₃] n → R₃) :

theorem bilin_form.to_matrix'_comp_left {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) (f : (n → R₃) →ₗ[R₃] n → R₃) :

theorem bilin_form.to_matrix'_comp_right {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) (f : (n → R₃) →ₗ[R₃] n → R₃) :

theorem bilin_form.mul_to_matrix'_mul {R₃ : Type u} [comm_ring R₃] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (B : bilin_form R₃ (n → R₃)) (M : matrix o n R₃) (N : matrix n o R₃) :

theorem bilin_form.mul_to_matrix' {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) (M : matrix n n R₃) :

theorem bilin_form.to_matrix'_mul {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) (M : matrix n n R₃) :

theorem matrix.to_bilin'_comp {R₃ : Type u} [comm_ring R₃] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (M : matrix n n R₃) (P Q : matrix n o R₃) :

### to_matrix section

This section deals with the conversion between matrices and bilinear forms on a module with a fixed basis.

def bilin_form.to_matrix {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) :
bilin_form R₃ M₃ ≃ₗ[R₃] matrix n n R₃

bilin_form.to_matrix hb is the equivalence between R-bilinear forms on M and n-by-n matrices with entries in R, if hb is an R-basis for M.

Equations
def matrix.to_bilin {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) :
matrix n n R₃ ≃ₗ[R₃] bilin_form R₃ M₃

bilin_form.to_matrix hb is the equivalence between R-bilinear forms on M and n-by-n matrices with entries in R, if hb is an R-basis for M.

Equations
@[simp]
theorem is_basis.equiv_fun_symm_std_basis {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (i : n) :
(hb.equiv_fun.symm) ((linear_map.std_basis R₃ (λ (_x : n), R₃) i) 1) = b i

@[simp]
theorem bilin_form.to_matrix_apply {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (B : bilin_form R₃ M₃) (i j : n) :
(bilin_form.to_matrix hb) B i j = B (b i) (b j)

@[simp]
theorem matrix.to_bilin_apply {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (M : matrix n n R₃) (x y : M₃) :
((matrix.to_bilin hb) M) x y = ∑ (i j : n), ((((hb.repr) x) i) * M i j) * ((hb.repr) y) j

theorem bilinear_form.to_matrix_aux_eq {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (B : bilin_form R₃ M₃) :

@[simp]
theorem bilin_form.to_matrix_symm {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) :

@[simp]
theorem matrix.to_bilin_symm {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) :

theorem matrix.to_bilin_is_basis_fun {R₃ : Type u} [comm_ring R₃] {n : Type u_1} [fintype n] [decidable_eq n] :

@[simp]
theorem matrix.to_bilin_to_matrix {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (B : bilin_form R₃ M₃) :

@[simp]
theorem bilin_form.to_matrix_to_bilin {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (M : matrix n n R₃) :

theorem bilin_form.to_matrix_comp {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) {M₃' : Type u_3} [add_comm_group M₃'] [module R₃ M₃'] {c : o → M₃'} (hc : is_basis R₃ c) [decidable_eq o] (B : bilin_form R₃ M₃) (l r : M₃' →ₗ[R₃] M₃) :

theorem bilin_form.to_matrix_comp_left {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (B : bilin_form R₃ M₃) (f : M₃ →ₗ[R₃] M₃) :

theorem bilin_form.to_matrix_comp_right {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (B : bilin_form R₃ M₃) (f : M₃ →ₗ[R₃] M₃) :

theorem bilin_form.mul_to_matrix_mul {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) {M₃' : Type u_3} [add_comm_group M₃'] [module R₃ M₃'] {c : o → M₃'} (hc : is_basis R₃ c) [decidable_eq o] (B : bilin_form R₃ M₃) (M : matrix o n R₃) (N : matrix n o R₃) :

theorem bilin_form.mul_to_matrix {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (B : bilin_form R₃ M₃) (M : matrix n n R₃) :

theorem bilin_form.to_matrix_mul {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) (B : bilin_form R₃ M₃) (M : matrix n n R₃) :

theorem matrix.to_bilin_comp {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) {M₃' : Type u_3} [add_comm_group M₃'] [module R₃ M₃'] {c : o → M₃'} (hc : is_basis R₃ c) [decidable_eq o] (M : matrix n n R₃) (P Q : matrix n o R₃) :

def refl_bilin_form.is_refl {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) :
Prop

The proposition that a bilinear form is reflexive

Equations
theorem refl_bilin_form.eq_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (H : refl_bilin_form.is_refl B) {x y : M} :
B x y = 0B y x = 0

theorem refl_bilin_form.ortho_sym {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (H : refl_bilin_form.is_refl B) {x y : M} :
B.is_ortho x y B.is_ortho y x

def sym_bilin_form.is_sym {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) :
Prop

The proposition that a bilinear form is symmetric

Equations
theorem sym_bilin_form.sym {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (H : sym_bilin_form.is_sym B) (x y : M) :
B x y = B y x

theorem sym_bilin_form.is_refl {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (H : sym_bilin_form.is_sym B) :

theorem sym_bilin_form.ortho_sym {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (H : sym_bilin_form.is_sym B) {x y : M} :
B.is_ortho x y B.is_ortho y x

def alt_bilin_form.is_alt {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) :
Prop

The proposition that a bilinear form is alternating

Equations
theorem alt_bilin_form.self_eq_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} (H : alt_bilin_form.is_alt B) (x : M) :
B x x = 0

theorem alt_bilin_form.neg {R₁ : Type u} {M₁ : Type v} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} (H : alt_bilin_form.is_alt B₁) (x y : M₁) :
-B₁ x y = B₁ y x

def bilin_form.is_adjoint_pair {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) {M' : Type u_1} [add_comm_monoid M'] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} {M' : Type u_1} [add_comm_monoid M'] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} {M' : Type u_1} [add_comm_monoid M'] [semimodule R M'] {B' : bilin_form R M'} :

theorem bilin_form.is_adjoint_pair_id {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} :

theorem bilin_form.is_adjoint_pair.add {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} {M' : Type u_1} [add_comm_monoid M'] [semimodule 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} {M₁ : Type v} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} {M₁' : Type u_2} [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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {B₂ : bilin_form R₂ M₂} {M₂' : Type u_3} [add_comm_monoid M₂'] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} {M' : Type u_1} [add_comm_monoid M'] [semimodule R M'] {B' : bilin_form R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} {M'' : Type u_4} [add_comm_monoid M''] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] (B₂ F₂ : bilin_form R₂ M₂) (f : module.End R₂ M₂) :

theorem bilin_form.is_pair_self_adjoint_equiv {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {M₃' : Type u_5} [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} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule 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} {M₁ : Type v} [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} {M₁ : Type v} [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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] (B₂ : bilin_form R₂ M₂) (f : module.End R₂ M₂) :

def bilin_form.skew_adjoint_submodule {R₃ : Type u} {M₃ : Type v} [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} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] (B₃ : bilin_form R₃ M₃) (f : module.End R₃ M₃) :

def matrix.is_adjoint_pair {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J J₃ A A' : matrix n n R₃) :
Prop

The condition for the square matrices A, A' to be an adjoint pair with respect to the square matrices J, J₃.

Equations
def matrix.is_self_adjoint {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J A : matrix n n R₃) :
Prop

The condition for a square matrix A to be self-adjoint with respect to the square matrix J.

Equations
def matrix.is_skew_adjoint {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J A : matrix n n R₃) :
Prop

The condition for a square matrix A to be skew-adjoint with respect to the square matrix J.

Equations
@[simp]
theorem is_adjoint_pair_to_bilin' {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J J₃ A A' : matrix n n R₃) [decidable_eq n] :

@[simp]
theorem is_adjoint_pair_to_bilin {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type w} [fintype n] {b : n → M₃} (hb : is_basis R₃ b) (J J₃ A A' : matrix n n R₃) [decidable_eq n] :

theorem matrix.is_adjoint_pair_equiv {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J A A' : matrix n n R₃) [decidable_eq n] (P : matrix n n R₃) (h : is_unit P) :
(P J P).is_adjoint_pair (P J P) A A' J.is_adjoint_pair J (P A P⁻¹) (P A' P⁻¹)

def pair_self_adjoint_matrices_submodule {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J J₃ : matrix n n R₃) [decidable_eq 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
@[simp]
theorem mem_pair_self_adjoint_matrices_submodule {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J J₃ A : matrix n n R₃) [decidable_eq n] :

def self_adjoint_matrices_submodule {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J : matrix n n R₃) [decidable_eq 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
@[simp]
theorem mem_self_adjoint_matrices_submodule {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J A : matrix n n R₃) [decidable_eq n] :

def skew_adjoint_matrices_submodule {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J : matrix n n R₃) [decidable_eq 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
@[simp]
theorem mem_skew_adjoint_matrices_submodule {R₃ : Type u} [comm_ring R₃] {n : Type w} [fintype n] (J A : matrix n n R₃) [decidable_eq n] :