mathlib3 documentation

linear_algebra.bilinear_form

Bilinear form #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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,

source
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_form R M is the type of R-bilinear functions M → M → R.

Instances for bilin_form
source
@[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
source
@[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
source
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'
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem bilin_form.coe_injective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
function.injective coe_fn
source
@[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
source
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
source
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
source
@[protected, instance]
def bilin_form.has_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
has_zero (bilin_form R M)
Equations
source
@[simp]
theorem bilin_form.coe_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
⇑0 = 0
source
@[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
source
@[protected, instance]
def bilin_form.has_add {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
has_add (bilin_form R M)
Equations
source
@[simp]
theorem bilin_form.coe_add {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) = ⇑B + ⇑D
source
@[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
source
@[protected, instance]
def bilin_form.has_smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [monoid α] [distrib_mul_action α R] [smul_comm_class α R R] :
has_smul α (bilin_form R M)

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

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

Equations
source
@[simp]
theorem bilin_form.coe_smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [monoid α] [distrib_mul_action α R] [smul_comm_class α R R] (a : α) (B : bilin_form R M) :
⇑(a • B) = a • ⇑B
source
@[simp]
theorem bilin_form.smul_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [monoid α] [distrib_mul_action α R] [smul_comm_class α R R] (a : α) (B : bilin_form R M) (x y : M) :
⇑(a • B) x y = a • ⇑B x y
source
@[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] :
add_comm_monoid (bilin_form R M)
Equations
source
@[protected, instance]
def bilin_form.has_neg {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] :
has_neg (bilin_form R₁ M₁)
Equations
source
@[simp]
theorem bilin_form.coe_neg {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B₁ : bilin_form R₁ M₁) :
⇑-B₁ = -⇑B₁
source
@[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
source
@[protected, instance]
def bilin_form.has_sub {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] :
has_sub (bilin_form R₁ M₁)
Equations
source
@[simp]
theorem bilin_form.coe_sub {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B₁ D₁ : bilin_form R₁ M₁) :
⇑(B₁ - D₁) = ⇑B₁ - ⇑D₁
source
@[simp]
theorem bilin_form.sub_apply {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] (B₁ D₁ : bilin_form R₁ M₁) (x y : M₁) :
⇑(B₁ - D₁) x y = ⇑B₁ x y - ⇑D₁ x y
source
@[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₁] :
add_comm_group (bilin_form R₁ M₁)
Equations
source
@[protected, instance]
def bilin_form.inhabited {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
inhabited (bilin_form R M)
Equations
source
def bilin_form.coe_fn_add_monoid_hom {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
bilin_form R M →+ M → M → R

coe_fn as an add_monoid_hom

Equations
source
@[protected, instance]
def bilin_form.distrib_mul_action {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [monoid α] [distrib_mul_action α R] [smul_comm_class α R R] :
distrib_mul_action α (bilin_form R M)
Equations
source
@[protected, instance]
def bilin_form.module {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [semiring α] [module α R] [smul_comm_class α R R] :
module α (bilin_form R M)
Equations
source
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] :
bilin_form R M →ₗ[R₂] bilin_form R M

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
source
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) :
⇑(bilin_form.flip_hom_aux R₂) (⇑(bilin_form.flip_hom_aux R₂) A) = A
source
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] :
bilin_form R M ≃ₗ[R₂] bilin_form R M

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
source
@[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
source
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] :
(bilin_form.flip_hom R₂).trans (bilin_form.flip_hom R₂) = linear_equiv.refl R₂ (bilin_form R M)
source
@[reducible]
def bilin_form.flip' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
bilin_form R M ≃ₗ[ℕ] bilin_form 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.

source
@[reducible]
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.

source
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) :
M →ₗ[R] R

Auxiliary definition to define to_lin_hom; see below.

Equations
source
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
source
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] :
bilin_form R M →ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R

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
source
@[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) :
⇑(⇑(⇑(bilin_form.to_lin_hom R₂) A) x) = ⇑A x
source
@[reducible]
def bilin_form.to_lin' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
bilin_form R M →ₗ[ℕ] M →ₗ[ℕ] M →ₗ[R] R

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.

source
@[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 (t.sum (λ (i : α), g i)) w = t.sum (λ (i : α), ⇑B (g i) w)
source
@[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 (t.sum (λ (i : α), g i)) = t.sum (λ (i : α), ⇑B w (g i))
source
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] :
bilin_form R M →ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R

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
source
@[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
source
@[reducible]
def bilin_form.to_lin'_flip {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
bilin_form R M →ₗ[ℕ] M →ₗ[ℕ] M →ₗ[R] R

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.

source
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
source
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
source
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
source
@[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₂) :
f.to_bilin_aux = ⇑linear_map.to_bilin f
source
@[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₂] :
linear_map.to_bilin.symm = bilin_form.to_lin
source
@[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₂] :
bilin_form.to_lin.symm = linear_map.to_bilin
source
@[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₂) :
⇑(⇑(⇑bilin_form.to_lin B₂) x) = ⇑B₂ x
source
def linear_map.comp_bilin_form {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R' : Type u_11} [comm_semiring R'] [algebra R' R] [module R' M] [is_scalar_tower R' R M] (f : R →ₗ[R'] R') (B : bilin_form R M) :
bilin_form R' M

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

Equations
source
@[simp]
theorem linear_map.comp_bilin_form_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {R' : Type u_11} [comm_semiring R'] [algebra R' R] [module R' M] [is_scalar_tower R' R M] (f : R →ₗ[R'] R') (B : bilin_form R M) (x y : M) :
⇑(f.comp_bilin_form B) x y = ⇑f (⇑B x y)
source
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') :
bilin_form R M

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

Equations
source
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) :
bilin_form R M

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

Equations
source
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) :
bilin_form R M

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

Equations
source
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)
source
@[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
source
@[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
source
@[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)
source
@[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
source
@[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)
source
@[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) :
B.comp linear_map.id r = B.comp_right r
source
@[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) :
B.comp l linear_map.id = B.comp_left l
source
@[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) :
B.comp_left linear_map.id = B
source
@[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) :
B.comp_right linear_map.id = B
source
@[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) :
B.comp linear_map.id linear_map.id = B
source
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₂
source
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
source
@[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)
source
@[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₂') :
(bilin_form.congr e).symm = bilin_form.congr e.symm
source
@[simp]
theorem bilin_form.congr_refl {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] :
bilin_form.congr (linear_equiv.refl R₂ M₂) = linear_equiv.refl R₂ (bilin_form R₂ M₂)
source
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₂'') :
(bilin_form.congr e).trans (bilin_form.congr f) = bilin_form.congr (e.trans f)
source
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₂) :
⇑(bilin_form.congr e) (⇑(bilin_form.congr f) B) = ⇑(bilin_form.congr (f.trans e)) B
source
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)
source
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))
source
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
source
@[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
source
@[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₂) :
(bilin_form.lin_mul_lin f g).comp l r = bilin_form.lin_mul_lin (f.comp l) (g.comp r)
source
@[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₂) :
(bilin_form.lin_mul_lin f g).comp_left l = bilin_form.lin_mul_lin (f.comp l) g
source
@[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₂) :
(bilin_form.lin_mul_lin f g).comp_right r = bilin_form.lin_mul_lin f (g.comp r)
source
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
source
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
source
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
source
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
source
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
source
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
source
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 ≠ j → ⇑B (v i) (v j) = 0
source
@[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
source
@[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
source
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)) :
linear_independent K v

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.

source
theorem bilin_form.ext_basis {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid 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.

source
theorem bilin_form.sum_repr_mul_repr_mul {R₂ : Type u_5} {M₂ : Type u_6} [comm_semiring R₂] [add_comm_monoid 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.

Reflexivity, symmetry, and alternativity #

source
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
source
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 = 0 → ⇑B y x = 0
source
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
source
@[protected]
theorem bilin_form.is_refl.neg {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B : bilin_form R₁ M₁} (hB : B.is_refl) :
(-B).is_refl
source
@[protected]
theorem bilin_form.is_refl.smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [semiring α] [module α R] [smul_comm_class α R R] [no_zero_smul_divisors α R] (a : α) {B : bilin_form R M} (hB : B.is_refl) :
(a • B).is_refl
source
@[protected]
theorem bilin_form.is_refl.group_smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [group α] [distrib_mul_action α R] [smul_comm_class α R R] (a : α) {B : bilin_form R M} (hB : B.is_refl) :
(a • B).is_refl
source
@[simp]
theorem bilin_form.is_refl_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
0.is_refl
source
@[simp]
theorem bilin_form.is_refl_neg {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B : bilin_form R₁ M₁} :
(-B).is_refl ↔ B.is_refl
source
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
Instances for bilin_form.is_symm
source
@[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
source
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) :
B.is_refl
source
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
source
@[protected]
theorem bilin_form.is_symm.add {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B₁ B₂ : bilin_form R M} (hB₁ : B₁.is_symm) (hB₂ : B₂.is_symm) :
(B₁ + B₂).is_symm
source
@[protected]
theorem bilin_form.is_symm.sub {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ B₂ : bilin_form R₁ M₁} (hB₁ : B₁.is_symm) (hB₂ : B₂.is_symm) :
(B₁ - B₂).is_symm
source
@[protected]
theorem bilin_form.is_symm.neg {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B : bilin_form R₁ M₁} (hB : B.is_symm) :
(-B).is_symm
source
@[protected]
theorem bilin_form.is_symm.smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [monoid α] [distrib_mul_action α R] [smul_comm_class α R R] (a : α) {B : bilin_form R M} (hB : B.is_symm) :
(a • B).is_symm
source
@[simp]
theorem bilin_form.is_symm_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
0.is_symm
source
@[simp]
theorem bilin_form.is_symm_neg {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B : bilin_form R₁ M₁} :
(-B).is_symm ↔ B.is_symm
source
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] :
B.is_symm ↔ ⇑(bilin_form.flip_hom R₂) B = B
source
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
source
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
source
theorem bilin_form.is_alt.neg_eq {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
source
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
source
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
source
@[protected]
theorem bilin_form.is_alt.add {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {B₁ B₂ : bilin_form R M} (hB₁ : B₁.is_alt) (hB₂ : B₂.is_alt) :
(B₁ + B₂).is_alt
source
@[protected]
theorem bilin_form.is_alt.sub {R₁ : Type u_3} {M₁ : Type u_4} [ring R₁] [add_comm_group M₁] [module R₁ M₁] {B₁ B₂ : bilin_form R₁ M₁} (hB₁ : B₁.is_alt) (hB₂ : B₂.is_alt) :
(B₁ - B₂).is_alt
source
@[protected]
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₁} (hB : B.is_alt) :
(-B).is_alt
source
@[protected]
theorem bilin_form.is_alt.smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_3} [monoid α] [distrib_mul_action α R] [smul_comm_class α R R] (a : α) {B : bilin_form R M} (hB : B.is_alt) :
(a • B).is_alt
source
@[simp]
theorem bilin_form.is_alt_zero {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
0.is_alt
source
@[simp]
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₁} :
(-B).is_alt ↔ B.is_alt

Linear adjoints #

source
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
source
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)
source
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) :
B.is_adjoint_pair F f g ↔ F.comp_left f = B.comp_right g
source
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'} :
B.is_adjoint_pair B' 0 0
source
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} :
B.is_adjoint_pair B 1 1
source
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')
source
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₁')
source
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₂)
source
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')
source
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)
source
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
source
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
source
@[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₂) :
f ∈ B₂.is_pair_self_adjoint_submodule F₂ ↔ B₂.is_pair_self_adjoint F₂ f
source
theorem bilin_form.is_pair_self_adjoint_equiv {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₂'] (F₂ : bilin_form R₂ M₂) (e : M₂' ≃ₗ[R₂] M₂) (f : module.End R₂ M₂) :
B₂.is_pair_self_adjoint F₂ f ↔ (B₂.comp ↑e ↑e).is_pair_self_adjoint (F₂.comp ↑e ↑e) (⇑(e.symm.conj) f)
source
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
source
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
source
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
source
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
source
@[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₂) :
f ∈ B₂.self_adjoint_submodule ↔ B₂.is_self_adjoint f
source
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
source
@[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₃) :
f ∈ B₃.skew_adjoint_submodule ↔ B₃.is_skew_adjoint f
source
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) :
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
source
@[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 ∈ N → B.is_ortho n m
source
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) :
B.orthogonal L ≤ B.orthogonal N
source
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) :
N ≤ B.orthogonal (B.orthogonal N)
source
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) :
submodule.span K {x} ⊓ B.orthogonal (submodule.span K {x}) = ⊥
source
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) :
B.orthogonal (submodule.span K {x}) = linear_map.ker (⇑(⇑bilin_form.to_lin B) x)
source
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) :
submodule.span K {x} ⊔ B.orthogonal (submodule.span K {x}) = ⊤
source
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) :
is_compl (submodule.span K {x}) (B.orthogonal (submodule.span K {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.

source
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) :
bilin_form R ↥W

The restriction of a bilinear form on a submodule.

Equations
source
@[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
source
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) :
(B.restrict W).is_symm

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

source
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
source
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] :
¬0.nondegenerate

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

source
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
source
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) :
(⇑(bilin_form.congr e) B).nondegenerate
source
@[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₂') :
(⇑(bilin_form.congr e) B).nondegenerate ↔ B.nondegenerate
source
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₂} :
B.nondegenerate ↔ linear_map.ker (⇑bilin_form.to_lin B) = ⊥

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

source
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) :
linear_map.ker (⇑bilin_form.to_lin B) = ⊥
source
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)) :
(B.restrict W).nondegenerate

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

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

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

source
theorem bilin_form.to_lin_restrict_ker_eq_inf_orthogonal {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] (B : bilin_form K V) (W : subspace K V) (b : B.is_refl) :
submodule.map (submodule.subtype W) (linear_map.ker ((⇑bilin_form.to_lin B).dom_restrict W)) = W ⊓ B.orthogonal ⊤
source
theorem bilin_form.to_lin_restrict_range_dual_coannihilator_eq_orthogonal {V : Type u_9} {K : Type u_10} [field K] [add_comm_group V] [module K V] (B : bilin_form K V) (W : subspace K V) :
(linear_map.range ((⇑bilin_form.to_lin B).dom_restrict W)).dual_coannihilator = B.orthogonal W
source
theorem bilin_form.finrank_add_finrank_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) :
finite_dimensional.finrank K ↥W + finite_dimensional.finrank K ↥(B.orthogonal W) = finite_dimensional.finrank K V + finite_dimensional.finrank K ↥(W ⊓ B.orthogonal ⊤)
source
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) :
is_compl W (B.orthogonal W)

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

source
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) :
(B.restrict W).nondegenerate ↔ is_compl W (B.orthogonal W)

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.

source
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) :
V ≃ₗ[K] module.dual K V

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

source
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) :
(B.restrict (B.orthogonal (submodule.span K {x}))).nondegenerate

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

source
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) :
function.injective B.comp_left
source
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 ψ₂ φ) :
ψ₁ = ψ₂
source
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) :
V →ₗ[K] V

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

Equations
source
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) :
⇑(⇑bilin_form.to_lin B₂) (⇑(B₁.symm_comp_of_nondegenerate B₂ b₂) v) = ⇑(⇑bilin_form.to_lin B₁) v
source
@[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
source
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) :
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
source
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) :
B.is_adjoint_pair B (B.left_adjoint_of_nondegenerate b φ) φ
source
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) :
B.is_adjoint_pair B ψ φ ↔ ψ = B.left_adjoint_of_nondegenerate b φ

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