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

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

• LinearMap.BilinForm.toLinHomAux₁ A 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

• LinearMap.BilinForm.toLinHomAux₂ A = 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 (Finset.sum t fun (i : α) => g i)) w = Finset.sum t fun (i : α) => (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) (Finset.sum t fun (i : α) => g i) = Finset.sum t fun (i : α) => (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 : M) (w : M) : ((Finset.sum t fun (i : α) => B i) v) w = Finset.sum t fun (i : α) => ((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

• LinearMap.toBilinAux f = 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 = let __src := LinearMap.BilinForm.toLinHom; { toLinearMap := __src, 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 = LinearEquiv.symm LinearMap.BilinForm.toLin

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

@[deprecated]

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

@[deprecated]

theorem BilinForm.toLin_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : LinearEquiv.symm LinearMap.BilinForm.toLin = 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 : M) (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

@[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), ((LinearMap.compBilinForm f B) a) m = f ((B a) m)

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

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

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

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

Equations

• LinearMap.BilinForm.comp B 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

• LinearMap.BilinForm.compLeft B f = LinearMap.BilinForm.comp B 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

• LinearMap.BilinForm.compRight B f = LinearMap.BilinForm.comp B 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 : M →ₗ[R] M') (r : M →ₗ[R] M') (l' : M' →ₗ[R] M'') (r' : M' →ₗ[R] M'') : LinearMap.BilinForm.comp (LinearMap.BilinForm.comp B l' r') l r = LinearMap.BilinForm.comp B (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 : M →ₗ[R] M) (r : M →ₗ[R] M) : LinearMap.BilinForm.compRight (LinearMap.BilinForm.compLeft B l) r = LinearMap.BilinForm.comp B 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 : M →ₗ[R] M) (r : M →ₗ[R] M) : LinearMap.BilinForm.compLeft (LinearMap.BilinForm.compRight B r) l = LinearMap.BilinForm.comp B 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 : M →ₗ[R] M') (r : M →ₗ[R] M') (v : M) (w : M) : ((LinearMap.BilinForm.comp B 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 : M) (w : M) : ((LinearMap.BilinForm.compLeft B 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 : M) (w : M) : ((LinearMap.BilinForm.compRight B 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) : LinearMap.BilinForm.comp B LinearMap.id r = LinearMap.BilinForm.compRight B 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) : LinearMap.BilinForm.comp B l LinearMap.id = LinearMap.BilinForm.compLeft B 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) : LinearMap.BilinForm.compLeft B 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) : LinearMap.BilinForm.compRight B 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) : LinearMap.BilinForm.comp B 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₁ : LinearMap.BilinForm R M') (B₂ : LinearMap.BilinForm R M') {l : M →ₗ[R] M'} {r : M →ₗ[R] M'} (hₗ : Function.Surjective ⇑l) (hᵣ : Function.Surjective ⇑r) : LinearMap.BilinForm.comp B₁ l r = LinearMap.BilinForm.comp B₂ 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

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

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

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

def LinearMap.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) : 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.compl₁₂ (LinearMap.mul R R) f g

@[simp]

theorem LinearMap.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) : ((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 : M →ₗ[R] R} {g : M →ₗ[R] R} (l : M' →ₗ[R] M) (r : M' →ₗ[R] M) : LinearMap.BilinForm.comp (LinearMap.BilinForm.linMulLin f g) 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 : M →ₗ[R] R} {g : M →ₗ[R] R} (l : M →ₗ[R] M) : LinearMap.BilinForm.compLeft (LinearMap.BilinForm.linMulLin f g) 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 : M →ₗ[R] R} {g : M →ₗ[R] R} (r : M →ₗ[R] M) : LinearMap.BilinForm.compRight (LinearMap.BilinForm.linMulLin f g) 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 : LinearMap.BilinForm R M} {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 : M) (y : M) : (Finsupp.sum (b.repr x) fun (i : ι) (xi : R) => Finsupp.sum (b.repr y) 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.