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

## Notation #

Given any term `B` of type `BilinForm`, due to a coercion, can use the notation `B x y` to refer to the function field, i.e. `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,

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem LinearMap.BilinForm.ext_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B D : LinearMap.BilinForm R M} :
B = D ↔ ∀ (x y : M), (B x) y = (D x) y
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
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' := ⋯ }

Instances For

source
@[simp]
theorem LinearMap.BilinForm.coeFnAddMonoidHom_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (x y : M) :
coeFnAddMonoidHom B x y = (B x) y
source
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 = LinearMap.lflip

Instances For

source
@[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) :
((flipHom A) x) y = (A y) x
source
theorem LinearMap.BilinForm.flip_flip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
flipHom ≪≫ₗ flipHom = LinearEquiv.refl R (LinearMap.BilinForm R M)
source
@[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

Instances For

source
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

Instances For

source
@[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
source
@[simp]
theorem LinearMap.lsmul_flip_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) :
(lsmul R M).flip m = toSpanSingleton R M m