Bilinear form and linear maps

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

TODO

A lot of this file is now redundant following the replacement of the dedicated _root_.BilinForm structure with LinearMap.BilinForm, which is just an alias for M →ₗ[R] M →ₗ[R] R. For example LinearMap.BilinForm.toLinHom is now just the identity map. This redundant code should be removed.

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,

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

Auxiliary definition to define toLinHom; see below.

Equations

• A.toLinHomAux₁ x = A x

@[deprecated]

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

Auxiliary definition to define toLinHom; see below.

Equations

• A.toLinHomAux₂ = A

@[deprecated]

def LinearMap.BilinForm.toLinHom {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.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

• LinearMap.BilinForm.toLinHom = LinearMap.id

@[deprecated]

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

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

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

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

def LinearMap.BilinForm.toLinHomFlip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.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

• LinearMap.BilinForm.toLinHomFlip = ↑LinearMap.BilinForm.flipHom

theorem LinearMap.BilinForm.toLin'Flip_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : LinearMap.BilinForm R M) (x : M) : ⇑((LinearMap.BilinForm.toLinHomFlip A) x) = fun (y : M) => (A y) x

def LinearMap.toBilinAux {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M →ₗ[R] R) : LinearMap.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

• f.toBilinAux = f

@[deprecated]

def LinearMap.BilinForm.toLin {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.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

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

@[deprecated]

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

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

Equations

• LinearMap.toBilin = LinearMap.BilinForm.toLin.symm

@[deprecated]

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) : f.toBilinAux = f

@[deprecated]

theorem LinearMap.toBilin_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.toBilin.symm = LinearMap.BilinForm.toLin

@[deprecated]

theorem BilinForm.toLin_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm.toLin.symm = LinearMap.toBilin

@[deprecated]

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 y : M) : ((LinearMap.toBilin f) x) y = (f x) y

@[deprecated]

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

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 : LinearMap.BilinForm R M) : LinearMap.BilinForm R' M

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

Equations

• f.compBilinForm B = (LinearMap.restrictScalars₁₂ R' R' B).compr₂ f

@[simp]

theorem LinearMap.compBilinForm_apply_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 : LinearMap.BilinForm R M) (a✝ m : M) : ((f.compBilinForm B) a✝) m = f ((B a✝) m)

def LinearMap.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 : LinearMap.BilinForm R M') (l r : M →ₗ[R] M') : LinearMap.BilinForm R M

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

Equations

• B.comp l r = LinearMap.compl₁₂ B l r

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

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

Equations

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

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

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

Equations

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

theorem LinearMap.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 : LinearMap.BilinForm R M'') (l r : M →ₗ[R] M') (l' r' : M' →ₗ[R] M'') : (B.comp l' r').comp l r = B.comp (l' ∘ₗ l) (r' ∘ₗ r)

@[simp]

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

@[simp]

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

@[simp]

theorem LinearMap.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 : LinearMap.BilinForm R M') (l r : M →ₗ[R] M') (v w : M) : ((B.comp l r) v) w = (B (l v)) (r w)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LinearMap.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₁ B₂ : LinearMap.BilinForm 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₂

def LinearMap.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') : LinearMap.BilinForm R M ≃ₗ[R] LinearMap.BilinForm R M'

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

Equations

• LinearMap.BilinForm.congr e = (LinearEquiv.congrLeft R R e).congrRight.trans (LinearEquiv.congrLeft (M' →ₗ[R] R) R e)

@[simp]

theorem LinearMap.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 : LinearMap.BilinForm R M) (x y : M') : (((LinearMap.BilinForm.congr e) B) x) y = (B (e.symm x)) (e.symm y)

@[simp]

theorem LinearMap.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') : (LinearMap.BilinForm.congr e).symm = LinearMap.BilinForm.congr e.symm

@[simp]

theorem LinearMap.BilinForm.congr_refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearMap.BilinForm.congr (LinearEquiv.refl R M) = LinearEquiv.refl R (LinearMap.BilinForm R M)

theorem LinearMap.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'') : LinearMap.BilinForm.congr e ≪≫ₗ LinearMap.BilinForm.congr f = LinearMap.BilinForm.congr (e ≪≫ₗ f)

theorem LinearMap.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 : LinearMap.BilinForm R M) : (LinearMap.BilinForm.congr e) ((LinearMap.BilinForm.congr f) B) = (LinearMap.BilinForm.congr (f ≪≫ₗ e)) B

theorem LinearMap.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 : LinearMap.BilinForm R M) (l r : M'' →ₗ[R] M') : ((LinearMap.BilinForm.congr e) B).comp l r = B.comp (↑e.symm ∘ₗ l) (↑e.symm ∘ₗ r)

theorem LinearMap.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 : LinearMap.BilinForm R M) (l r : M' →ₗ[R] M) : (LinearMap.BilinForm.congr e) (B.comp l r) = B.comp (l ∘ₗ ↑e.symm) (r ∘ₗ ↑e.symm)

def LinearEquiv.congrRight₂ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] (e : N₁ ≃ₗ[R] N₂) : LinearMap.BilinMap R M N₁ ≃ₗ[R] LinearMap.BilinMap R M N₂

When N₁ and N₂ are equivalent, bilinear maps on M into N₁ are equivalent to bilinear maps into N₂.

Equations

• e.congrRight₂ = e.congrRight.congrRight

@[simp]

theorem LinearEquiv.congrRight₂_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] (e : N₁ ≃ₗ[R] N₂) (B : LinearMap.BilinMap R M N₁) : e.congrRight₂ B = LinearMap.compr₂ B ↑e

@[simp]

theorem LinearEquiv.congrRight₂_refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} [AddCommMonoid N₁] [Module R N₁] : (LinearEquiv.refl R N₁).congrRight₂ = LinearEquiv.refl R (LinearMap.BilinMap R M N₁)

@[simp]

theorem LinearEquiv.congrRight_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] (e : N₁ ≃ₗ[R] N₂) : e.congrRight₂.symm = e.symm.congrRight₂

theorem LinearEquiv.congrRight₂_trans {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N₁] [Module R N₂] [Module R N₃] (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) : (e₁₂ ≪≫ₗ e₂₃).congrRight₂ = e₁₂.congrRight₂ ≪≫ₗ e₂₃.congrRight₂

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

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

Equations

• LinearMap.BilinForm.linMulLin f g = (LinearMap.mul R R).compl₁₂ f g

@[simp]

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

@[simp]

theorem LinearMap.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 g : M →ₗ[R] R} (l r : M' →ₗ[R] M) : (LinearMap.BilinForm.linMulLin f g).comp l r = LinearMap.BilinForm.linMulLin (f ∘ₗ l) (g ∘ₗ r)

@[simp]

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

@[simp]

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

theorem LinearMap.BilinForm.ext_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B F₂ : LinearMap.BilinForm R M} {ι : Type u_9} (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.

theorem LinearMap.BilinForm.sum_repr_mul_repr_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_9} (b : Basis ι R M) (x y : M) : ((b.repr x).sum fun (i : ι) (xi : R) => (b.repr y).sum fun (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.