Bilinear form and linear maps #

This file describes the relation between bilinear forms and linear maps.

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 #

Tags #

Bilinear form,

source

def BilinForm.toLinHomAux₁ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : BilinForm R M) (x : M) :

M →ₗ[R] R

Auxiliary definition to define toLinHom; see below.

Equations

BilinForm.toLinHomAux₁ A x = { toAddHom := { toFun := fun (y : M) => A.bilin x y, map_add' := ⋯ }, map_smul' := ⋯ }

source

def BilinForm.toLinHomAux₂ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : BilinForm R M) :

M →ₗ[R] M →ₗ[R] R

Auxiliary definition to define toLinHom; see below.

Equations

BilinForm.toLinHomAux₂ A = { toAddHom := { toFun := BilinForm.toLinHomAux₁ A, map_add' := ⋯ }, map_smul' := ⋯ }

source

def BilinForm.toLinHom {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R

The linear map obtained from a BilinForm by fixing the left co-ordinate and evaluating in the right.

Equations

BilinForm.toLinHom = { toAddHom := { toFun := BilinForm.toLinHomAux₂, map_add' := ⋯ }, map_smul' := ⋯ }

source

@[simp]

theorem BilinForm.toLin'_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : BilinForm R M) (x : M) :

⇑((BilinForm.toLinHom A) x) = A.bilin x

source

@[simp]

theorem BilinForm.sum_left {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) {α : Type u_7} (t : Finset α) (g : α → M) (w : M) :

B.bilin (Finset.sum t fun (i : α) => g i) w = Finset.sum t fun (i : α) => B.bilin (g i) w

source

@[simp]

theorem BilinForm.sum_right {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) {α : Type u_7} (t : Finset α) (w : M) (g : α → M) :

B.bilin w (Finset.sum t fun (i : α) => g i) = Finset.sum t fun (i : α) => B.bilin w (g i)

source

@[simp]

theorem BilinForm.sum_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} (t : Finset α) (B : α → BilinForm R M) (v : M) (w : M) :

(Finset.sum t fun (i : α) => B i).bilin v w = Finset.sum t fun (i : α) => (B i).bilin v w

source

def BilinForm.toLinHomFlip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R

The linear map obtained from a BilinForm by fixing the right co-ordinate and evaluating in the left.

Equations

BilinForm.toLinHomFlip = LinearMap.comp BilinForm.toLinHom ↑BilinForm.flipHom

source

@[simp]

theorem BilinForm.toLin'Flip_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : BilinForm R M) (x : M) :

⇑((BilinForm.toLinHomFlip A) x) = fun (y : M) => A.bilin y x

source

def LinearMap.toBilinAux {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M →ₗ[R] R) :

BilinForm 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 LinearMap.toBilin.

Equations

LinearMap.toBilinAux f = { bilin := fun (x y : M) => (f x) y, bilin_add_left := ⋯, bilin_smul_left := ⋯, bilin_add_right := ⋯, bilin_smul_right := ⋯ }

source

def BilinForm.toLin {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R

Bilinear forms are linearly equivalent to maps with two arguments that are linear in both.

Equations

BilinForm.toLin = let __src := BilinForm.toLinHom; { toLinearMap := __src, invFun := LinearMap.toBilinAux, left_inv := ⋯, right_inv := ⋯ }

source

def LinearMap.toBilin {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

(M →ₗ[R] M →ₗ[R] R) ≃ₗ[R] BilinForm R M

A map with two arguments that is linear in both is linearly equivalent to bilinear form.

Equations

LinearMap.toBilin = LinearEquiv.symm BilinForm.toLin

source

@[simp]

theorem LinearMap.toBilinAux_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M →ₗ[R] R) :

LinearMap.toBilinAux f = LinearMap.toBilin f

source

@[simp]

theorem LinearMap.toBilin_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

LinearEquiv.symm LinearMap.toBilin = BilinForm.toLin

source

@[simp]

theorem BilinForm.toLin_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

LinearEquiv.symm BilinForm.toLin = LinearMap.toBilin

source

@[simp]

theorem LinearMap.toBilin_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M →ₗ[R] R) (x : M) (y : M) :

(LinearMap.toBilin f).bilin x y = (f x) y

source

@[simp]

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

⇑((BilinForm.toLin B) x) = B.bilin x

source

@[simp]

theorem LinearMap.compBilinForm_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {R' : Type u_7} [CommSemiring R'] [Algebra R' R] [Module R' M] [IsScalarTower R' R M] (f : R →ₗ[R'] R') (B : BilinForm R M) (x : M) (y : M) :

(LinearMap.compBilinForm f B).bilin x y = f (B.bilin x y)

source

def LinearMap.compBilinForm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {R' : Type u_7} [CommSemiring R'] [Algebra R' R] [Module R' M] [IsScalarTower R' R M] (f : R →ₗ[R'] R') (B : BilinForm R M) :

BilinForm R' M

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

Equations

LinearMap.compBilinForm f B = { bilin := fun (x y : M) => f (B.bilin x y), bilin_add_left := ⋯, bilin_smul_left := ⋯, bilin_add_right := ⋯, bilin_smul_right := ⋯ }

source

def BilinForm.comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (B : BilinForm R M') (l : M →ₗ[R] M') (r : M →ₗ[R] M') :

BilinForm R M

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

Equations

BilinForm.comp B l r = { bilin := fun (x y : M) => B.bilin (l x) (r y), bilin_add_left := ⋯, bilin_smul_left := ⋯, bilin_add_right := ⋯, bilin_smul_right := ⋯ }

source

def BilinForm.compLeft {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (f : M →ₗ[R] M) :

BilinForm R M

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

Equations

BilinForm.compLeft B f = BilinForm.comp B f LinearMap.id

source

def BilinForm.compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (f : M →ₗ[R] M) :

BilinForm R M

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

Equations

BilinForm.compRight B f = BilinForm.comp B LinearMap.id f

source

theorem BilinForm.comp_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] {M'' : Type u_7} [AddCommMonoid M''] [Module R M''] (B : BilinForm R M'') (l : M →ₗ[R] M') (r : M →ₗ[R] M') (l' : M' →ₗ[R] M'') (r' : M' →ₗ[R] M'') :

BilinForm.comp (BilinForm.comp B l' r') l r = BilinForm.comp B (l' ∘ₗ l) (r' ∘ₗ r)

source

@[simp]

theorem BilinForm.compLeft_compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (l : M →ₗ[R] M) (r : M →ₗ[R] M) :

BilinForm.compRight (BilinForm.compLeft B l) r = BilinForm.comp B l r

source

@[simp]

theorem BilinForm.compRight_compLeft {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (l : M →ₗ[R] M) (r : M →ₗ[R] M) :

BilinForm.compLeft (BilinForm.compRight B r) l = BilinForm.comp B l r

source

@[simp]

theorem BilinForm.comp_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (B : BilinForm R M') (l : M →ₗ[R] M') (r : M →ₗ[R] M') (v : M) (w : M) :

(BilinForm.comp B l r).bilin v w = B.bilin (l v) (r w)

source

@[simp]

theorem BilinForm.compLeft_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (f : M →ₗ[R] M) (v : M) (w : M) :

(BilinForm.compLeft B f).bilin v w = B.bilin (f v) w

source

@[simp]

theorem BilinForm.compRight_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (f : M →ₗ[R] M) (v : M) (w : M) :

(BilinForm.compRight B f).bilin v w = B.bilin v (f w)

source

@[simp]

theorem BilinForm.comp_id_left {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (r : M →ₗ[R] M) :

BilinForm.comp B LinearMap.id r = BilinForm.compRight B r

source

@[simp]

theorem BilinForm.comp_id_right {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (l : M →ₗ[R] M) :

BilinForm.comp B l LinearMap.id = BilinForm.compLeft B l

source

@[simp]

theorem BilinForm.compLeft_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) :

BilinForm.compLeft B LinearMap.id = B

source

@[simp]

theorem BilinForm.compRight_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) :

BilinForm.compRight B LinearMap.id = B

source

@[simp]

theorem BilinForm.comp_id_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) :

BilinForm.comp B LinearMap.id LinearMap.id = B

source

theorem BilinForm.comp_inj {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (B₁ : BilinForm R M') (B₂ : BilinForm R M') {l : M →ₗ[R] M'} {r : M →ₗ[R] M'} (hₗ : Function.Surjective ⇑l) (hᵣ : Function.Surjective ⇑r) :

BilinForm.comp B₁ l r = BilinForm.comp B₂ l r ↔ B₁ = B₂

source

def BilinForm.congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') :

BilinForm R M ≃ₗ[R] BilinForm R M'

Apply a linear equivalence on the arguments of a bilinear form.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem BilinForm.congr_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') (B : BilinForm R M) (x : M') (y : M') :

((BilinForm.congr e) B).bilin x y = B.bilin ((LinearEquiv.symm e) x) ((LinearEquiv.symm e) y)

source

@[simp]

theorem BilinForm.congr_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') :

LinearEquiv.symm (BilinForm.congr e) = BilinForm.congr (LinearEquiv.symm e)

source

@[simp]

theorem BilinForm.congr_refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

BilinForm.congr (LinearEquiv.refl R M) = LinearEquiv.refl R (BilinForm R M)

source

theorem BilinForm.congr_trans {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M ≃ₗ[R] M') (f : M' ≃ₗ[R] M'') :

BilinForm.congr e ≪≫ₗ BilinForm.congr f = BilinForm.congr (e ≪≫ₗ f)

source

theorem BilinForm.congr_congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M' ≃ₗ[R] M'') (f : M ≃ₗ[R] M') (B : BilinForm R M) :

(BilinForm.congr e) ((BilinForm.congr f) B) = (BilinForm.congr (f ≪≫ₗ e)) B

source

theorem BilinForm.congr_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M ≃ₗ[R] M') (B : BilinForm R M) (l : M'' →ₗ[R] M') (r : M'' →ₗ[R] M') :

BilinForm.comp ((BilinForm.congr e) B) l r = BilinForm.comp B (↑(LinearEquiv.symm e) ∘ₗ l) (↑(LinearEquiv.symm e) ∘ₗ r)

source

theorem BilinForm.comp_congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l : M' →ₗ[R] M) (r : M' →ₗ[R] M) :

(BilinForm.congr e) (BilinForm.comp B l r) = BilinForm.comp B (l ∘ₗ ↑(LinearEquiv.symm e)) (r ∘ₗ ↑(LinearEquiv.symm e))

source

def BilinForm.linMulLin {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) (g : M →ₗ[R] R) :

BilinForm R M

linMulLin f g is the bilinear form mapping x and y to f x * g y

Equations

BilinForm.linMulLin f g = { bilin := fun (x y : M) => f x * g y, bilin_add_left := ⋯, bilin_smul_left := ⋯, bilin_add_right := ⋯, bilin_smul_right := ⋯ }

source

@[simp]

theorem BilinForm.linMulLin_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (x : M) (y : M) :

(BilinForm.linMulLin f g).bilin x y = f x * g y

source

@[simp]

theorem BilinForm.linMulLin_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (l : M' →ₗ[R] M) (r : M' →ₗ[R] M) :

BilinForm.comp (BilinForm.linMulLin f g) l r = BilinForm.linMulLin (f ∘ₗ l) (g ∘ₗ r)

source

@[simp]

theorem BilinForm.linMulLin_compLeft {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (l : M →ₗ[R] M) :

BilinForm.compLeft (BilinForm.linMulLin f g) l = BilinForm.linMulLin (f ∘ₗ l) g

source

@[simp]

theorem BilinForm.linMulLin_compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (r : M →ₗ[R] M) :

BilinForm.compRight (BilinForm.linMulLin f g) r = BilinForm.linMulLin f (g ∘ₗ r)

source

theorem BilinForm.ext_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {F₂ : BilinForm R M} {ι : Type u_9} (b : Basis ι R M) (h : ∀ (i j : ι), B.bilin (b i) (b j) = F₂.bilin (b i) (b j)) :

B = F₂

Two bilinear forms are equal when they are equal on all basis vectors.

source

theorem BilinForm.sum_repr_mul_repr_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {ι : Type u_9} (b : Basis ι R M) (x : M) (y : M) :

(Finsupp.sum (b.repr x) fun (i : ι) (xi : R) => Finsupp.sum (b.repr y) fun (j : ι) (yj : R) => xi • yj • B.bilin (b i) (b j)) = B.bilin x y

Write out B x y as a sum over B (b i) (b j) if b is a basis.

Documentation

Mathlib.LinearAlgebra.BilinearForm.Hom

Bilinear form and linear maps #

Notations #

References #

Tags #