Bilinear form

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

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

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

Notations

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

In this file we use the following type variables:

• M, M', ... are modules over the commutative semiring R,
• M₁, M₁', ... are modules over the commutative ring R₁,
• V, ... is a vector space over the field K.

References

• https://en.wikipedia.org/wiki/Bilinear_form

Tags

Bilinear form,

@[deprecated]

theorem LinearMap.BilinForm.coeFn_congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {x x' y y' : M} : x = x' → y = y' → (B x) y = (B x') y'

theorem LinearMap.BilinForm.add_left {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (x y z : M) : (B (x + y)) z = (B x) z + (B y) z

theorem LinearMap.BilinForm.smul_left {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (a : R) (x y : M) : (B (a • x)) y = a * (B x) y

theorem LinearMap.BilinForm.add_right {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (x y z : M) : (B x) (y + z) = (B x) y + (B x) z

theorem LinearMap.BilinForm.smul_right {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (a : R) (x y : M) : (B x) (a • y) = a * (B x) y

theorem LinearMap.BilinForm.zero_left {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (x : M) : (B 0) x = 0

theorem LinearMap.BilinForm.zero_right {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (x : M) : (B x) 0 = 0

theorem LinearMap.BilinForm.neg_left {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (x y : M₁) : (B₁ (-x)) y = -(B₁ x) y

theorem LinearMap.BilinForm.neg_right {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (x y : M₁) : (B₁ x) (-y) = -(B₁ x) y

theorem LinearMap.BilinForm.sub_left {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (x y z : M₁) : (B₁ (x - y)) z = (B₁ x) z - (B₁ y) z

theorem LinearMap.BilinForm.sub_right {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (x y z : M₁) : (B₁ x) (y - z) = (B₁ x) y - (B₁ x) z

theorem LinearMap.BilinForm.smul_left_of_tower {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] {B : LinearMap.BilinForm R M} (r : S) (x y : M) : (B (r • x)) y = r • (B x) y

theorem LinearMap.BilinForm.smul_right_of_tower {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] {B : LinearMap.BilinForm R M} (r : S) (x y : M) : (B x) (r • y) = r • (B x) y

theorem LinearMap.BilinForm.coe_injective {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.Injective fun (B : LinearMap.BilinForm R M) (x y : M) => (B x) y

theorem LinearMap.BilinForm.ext {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B D : LinearMap.BilinForm R M} (H : ∀ (x y : M), (B x) y = (D x) y) : B = D

theorem LinearMap.BilinForm.congr_fun {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B D : LinearMap.BilinForm R M} (h : B = D) (x y : M) : (B x) y = (D x) y

@[deprecated]

theorem LinearMap.BilinForm.coe_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : ⇑0 = 0

@[simp]

theorem LinearMap.BilinForm.zero_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x y : M) : (0 x) y = 0

@[deprecated]

theorem LinearMap.BilinForm.coe_add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B D : LinearMap.BilinForm R M) : ⇑(B + D) = ⇑B + ⇑D

@[simp]

theorem LinearMap.BilinForm.add_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B D : LinearMap.BilinForm R M) (x y : M) : ((B + D) x) y = (B x) y + (D x) y

@[deprecated]

theorem LinearMap.BilinForm.coe_neg {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : LinearMap.BilinForm R₁ M₁) : ⇑(-B₁) = -⇑B₁

@[simp]

theorem LinearMap.BilinForm.neg_apply {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : LinearMap.BilinForm R₁ M₁) (x y : M₁) : ((-B₁) x) y = -(B₁ x) y

@[deprecated]

theorem LinearMap.BilinForm.coe_sub {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ D₁ : LinearMap.BilinForm R₁ M₁) : ⇑(B₁ - D₁) = ⇑B₁ - ⇑D₁

@[simp]

theorem LinearMap.BilinForm.sub_apply {R₁ : Type u_4} {M₁ : Type u_5} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ D₁ : LinearMap.BilinForm R₁ M₁) (x y : M₁) : ((B₁ - D₁) x) y = (B₁ x) y - (D₁ x) y

def LinearMap.BilinForm.coeFnAddMonoidHom {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm R M →+ M → M → R

coeFn as an AddMonoidHom

Equations

• LinearMap.BilinForm.coeFnAddMonoidHom = { toFun := fun (B : LinearMap.BilinForm R M) (x y : M) => (B x) y, map_zero' := ⋯, map_add' := ⋯ }

def LinearMap.BilinForm.flipHomAux {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm R M →ₗ[R] LinearMap.BilinForm R M

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

Equations

• LinearMap.BilinForm.flipHomAux = { toFun := fun (A : LinearMap.BilinForm R M) => LinearMap.flip A, map_add' := ⋯, map_smul' := ⋯ }

theorem LinearMap.BilinForm.flip_flip_aux {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : LinearMap.BilinForm R M) : LinearMap.BilinForm.flipHomAux (LinearMap.BilinForm.flipHomAux A) = A

def LinearMap.BilinForm.flipHom {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm R M ≃ₗ[R] LinearMap.BilinForm R M

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

Equations

• LinearMap.BilinForm.flipHom = { toLinearMap := LinearMap.BilinForm.flipHomAux, invFun := ⇑LinearMap.BilinForm.flipHomAux, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearMap.BilinForm.flip_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : LinearMap.BilinForm R M) (x y : M) : ((LinearMap.BilinForm.flipHom A) x) y = (A y) x

theorem LinearMap.BilinForm.flip_flip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm.flipHom ≪≫ₗ LinearMap.BilinForm.flipHom = LinearEquiv.refl R (LinearMap.BilinForm R M)

@[reducible, inline]

abbrev LinearMap.BilinForm.flip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : LinearMap.BilinForm R M

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

Equations

• B.flip = LinearMap.BilinForm.flipHom B

def LinearMap.BilinForm.restrict {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (W : Submodule R M) : LinearMap.BilinForm R ↥W

The restriction of a bilinear form on a submodule.

Equations

• B.restrict W = LinearMap.domRestrict₁₂ B W W

@[simp]

theorem LinearMap.BilinForm.restrict_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (W : Submodule R M) (m : ↥W) : (B.restrict W) m = (B ↑m).domRestrict W