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] [semimodule R M] :
Type (max u_1 u_2)
  • 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_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] :
Equations
@[simp]
theorem bilin_form.coe_fn_mk {R : Type u_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_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] [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_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] :
Equations
@[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] [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.zero_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule 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
@[instance]
def bilin_form.inhabited {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] :
Equations
@[instance]
def bilin_form.semimodule {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] :

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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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₂] [semimodule 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 {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (R₂ : Type u_5) [comm_semiring R₂] [algebra R₂ R] [semimodule 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] [semimodule R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] (R₂ : Type u_5) [comm_semiring R₂] [algebra R₂ R] [semimodule 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] [semimodule R M] {R₂ : Type u_5} [comm_semiring R₂] [algebra R₂ R] [semimodule 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] [semimodule 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₂] [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 bilin_form.to_lin {R₂ : Type u_5} {M₂ : Type u_6} [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
def linear_map.to_bilin {R₂ : Type u_5} {M₂ : Type u_6} [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
@[simp]
theorem linear_map.to_bilin_aux_eq {R₂ : Type u_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] :
@[simp]
theorem bilin_form.to_lin_symm {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] :
@[simp]
theorem bilin_form.to_lin_apply {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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] [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type w} [add_comm_monoid M'] [semimodule R M'] {M'' : Type u_3} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_11} [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_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_11} [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_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_11} [add_comm_monoid M₂'] [semimodule R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') :
theorem bilin_form.congr_comp {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_11} [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₂) (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₂] [semimodule R₂ M₂] {M₂' : Type u_11} [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₂) (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₂] [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_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {M₂' : Type u_11} [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_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [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_1} {M : Type u_2} [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. 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] [semimodule 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] [semimodule 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] [semimodule 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] [vector_space 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] [semimodule 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] [semimodule R M] {n : Type w} {B : bilin_form R M} {v : n → M} :
B.is_Ortho v ∀ (i j : n), i jB (v j) (v i) = 0
@[simp]
theorem bilin_form.is_ortho_smul_left {R₄ : Type u_12} {M₄ : Type u_13} [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_12} {M₄ : Type u_13} [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] [vector_space 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_12} {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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {B₃ : bilin_form R₃ M₃} {ι : Type u_12} {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_5} [comm_semiring R₂] {n : Type u_11} [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_5} [comm_semiring R₂] {n : Type u_11} [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_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] (M : matrix n n R₃) :
theorem matrix.to_bilin'_apply {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [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
theorem matrix.to_bilin'_apply' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] (M : matrix n n R₃) (v w : n → R₃) :
@[simp]
theorem matrix.to_bilin'_std_basis {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_bilin'_symm {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_bilin'_to_matrix' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) :
@[simp]
theorem bilin_form.to_matrix'_to_bilin' {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] (M : matrix n n R₃) :
@[simp]
theorem bilin_form.to_matrix'_apply {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} {o : Type u_12} [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_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} {o : Type u_12} [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_7} [comm_ring R₃] {n : Type u_11} [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_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] (B : bilin_form R₃ (n → R₃)) (M : matrix n n R₃) :
theorem matrix.to_bilin'_comp {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} {o : Type u_12} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) :
@[simp]
theorem matrix.to_bilin_symm {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [fintype n] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) :
theorem matrix.to_bilin_is_basis_fun {R₃ : Type u_7} [comm_ring R₃] {n : Type u_11} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_bilin_to_matrix {R₃ : Type u_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) {M₃' : Type u_13} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) {M₃' : Type u_13} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {n : Type u_11} {o : Type u_12} [fintype n] [fintype o] [decidable_eq n] {b : n → M₃} (hb : is_basis R₃ b) {M₃' : Type u_13} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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
theorem sym_bilin_form.is_sym_iff_flip' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {R₂ : Type u_5} [comm_semiring R₂] {B : bilin_form R M} [algebra R₂ R] :
def alt_bilin_form.is_alt {R : Type u_1} {M : Type u_2} [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_1} {M : Type u_2} [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_3} {M₁ : Type u_4} [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_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) {M' : Type u_11} [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_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} {M' : Type u_11} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} {M' : Type u_11} [add_comm_monoid M'] [semimodule 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] [semimodule 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] [semimodule R M] {B : bilin_form R M} {M' : Type u_11} [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_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ : bilin_form R₁ M₁} {M₁' : Type u_12} [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₂] [semimodule R₂ M₂] {B₂ : bilin_form R₂ M₂} {M₂' : Type u_13} [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_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {B : bilin_form R M} {M' : Type u_11} [add_comm_monoid M'] [semimodule R M'] {B' : bilin_form R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} {M'' : Type u_14} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [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_7} {M₃ : Type u_8} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃] {M₃' : Type u_15} [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] [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_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₂] [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_5} {M₂ : Type u_6} [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_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 matrix.is_adjoint_pair {R₃ : Type u_7} [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_7} [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_7} [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_7} [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_7} {M₃ : Type u_8} [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_7} [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_7} [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_7} [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_7} [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_7} [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_7} [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_7} [comm_ring R₃] {n : Type w} [fintype n] (J A : matrix n n R₃) [decidable_eq n] :
def bilin_form.orthogonal {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] {B : bilin_form R M} {N : submodule R M} (hB : refl_bilin_form.is_refl B) :
theorem bilin_form.span_singleton_inf_orthogonal_eq_bot {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [vector_space 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] [vector_space 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] [vector_space 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] [vector_space 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] [semimodule 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] [semimodule 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_sym {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (B : bilin_form R M) (hB : sym_bilin_form.is_sym B) (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] [semimodule 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.nondegenerate_iff_ker_eq_bot {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule 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_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₁) (hB : sym_bilin_form.is_sym B) {W : submodule R₁ M₁} (hW : disjoint W (B.orthogonal W)) :

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

theorem bilin_form.restrict_nondegenerate_of_is_compl_orthogonal {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {B : bilin_form K V} {W : subspace K V} (hB₁ : sym_bilin_form.is_sym B) (hB₂ : (B.restrict W).nondegenerate) :

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

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

def bilin_form.to_dual {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (B : bilin_form K V) (hB : 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] [vector_space K V] [finite_dimensional K V] {B : bilin_form K V} (hB : B.nondegenerate) {m n : V} :
((B.to_dual hB) m) n = B m n

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] [vector_space K V] (B : bilin_form K V) (hB₁ : B.nondegenerate) (hB₂ : sym_bilin_form.is_sym B) {x : V} (hx : ¬B.is_ortho x x) :

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