Documentation

Mathlib.LinearAlgebra.BilinearForm.Basic

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:

References #

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 : M} {x' : M} {y : M} {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 : M) (y : M) (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 : M) (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 : M) (y : M) (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 : M) (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 : M₁) (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 : M₁) (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 : M₁) (y : M₁) (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 : M₁) (y : M₁) (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 : M) (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 : M) (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_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {D : LinearMap.BilinForm R M} :
B = D ∀ (x y : M), (B x) y = (D x) y
theorem LinearMap.BilinForm.ext {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {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 : LinearMap.BilinForm R M} {D : LinearMap.BilinForm R M} (h : B = D) (x : M) (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 : M) (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 : LinearMap.BilinForm R M) (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 : LinearMap.BilinForm R M) (D : LinearMap.BilinForm R M) (x : M) (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 : M₁) (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₁ : LinearMap.BilinForm R₁ M₁) (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₁ : LinearMap.BilinForm R₁ M₁) (D₁ : LinearMap.BilinForm R₁ M₁) (x : M₁) (y : M₁) :
((B₁ - D₁) x) y = (B₁ x) y - (D₁ x) y

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

    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
    Instances For
      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

      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 := }
      Instances For
        @[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 : M) (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]

        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
          @[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

          The restriction of a bilinear form on a submodule.

          Equations
          Instances For