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 semiring R,
M₁, M₁', ... are modules over the ring R₁,
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} [Semiring R] [AddCommMonoid M] [Module R M] (A : BilinForm R M) (x : M) :

M →ₗ[R] R

Auxiliary definition to define toLinHom; see below.

Equations

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

Instances For

source

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

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

Auxiliary definition to define toLinHom; see below.

Equations

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

Instances For

source

def BilinForm.toLinHom {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (R₂ : Type u_5) [CommSemiring R₂] [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ 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. This is the most general version of the construction; it is R₂-linear for some distinguished commutative subsemiring R₂ of the scalar ring. Over a semiring with no particular distinguished such subsemiring, use toLin', which is ℕ-linear. Over a commutative semiring, use toLin, which is linear.

Equations

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

Instances For

source

@[simp]

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

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

source

@[inline, reducible]

abbrev BilinForm.toLin' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

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

The linear map obtained from a BilinForm by fixing the left co-ordinate and evaluating in the right. Over a commutative semiring, use toLin, which is linear rather than ℕ-linear.

Equations

BilinForm.toLin' = BilinForm.toLinHom ℕ

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

def BilinForm.toLinHomFlip {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (R₂ : Type u_5) [CommSemiring R₂] [Algebra R₂ R] [Module R₂ M] [IsScalarTower R₂ 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. This is the most general version of the construction; it is R₂-linear for some distinguished commutative subsemiring R₂ of the scalar ring. Over semiring with no particular distinguished such subsemiring, use toLin'Flip, which is ℕ-linear. Over a commutative semiring, use toLinFlip, which is linear.

Equations

BilinForm.toLinHomFlip R₂ = LinearMap.comp (BilinForm.toLinHom R₂) ↑(BilinForm.flipHom R₂)

Instances For

source

@[simp]

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

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

source

@[inline, reducible]

abbrev BilinForm.toLin'Flip {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

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

The linear map obtained from a BilinForm by fixing the right co-ordinate and evaluating in the left. Over a commutative semiring, use toLinFlip, which is linear rather than ℕ-linear.

Equations

BilinForm.toLin'Flip = BilinForm.toLinHomFlip ℕ

Instances For

source

def LinearMap.toBilinAux {R₂ : Type u_5} {M₂ : Type u_6} [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

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

Instances For

source

def BilinForm.toLin {R₂ : Type u_5} {M₂ : Type u_6} [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

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

Instances For

source

def LinearMap.toBilin {R₂ : Type u_5} {M₂ : Type u_6} [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

Instances For

source

@[simp]

theorem LinearMap.toBilinAux_eq {R₂ : Type u_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] :

LinearEquiv.symm LinearMap.toBilin = BilinForm.toLin

source

@[simp]

theorem BilinForm.toLin_symm {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] :

LinearEquiv.symm BilinForm.toLin = LinearMap.toBilin

source

@[simp]

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

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

source

@[simp]

theorem BilinForm.toLin_apply {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {B₂ : BilinForm R₂ M₂} (x : M₂) :

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

source

@[simp]

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

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

source

def LinearMap.compBilinForm {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {R' : Type u_11} [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

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

Instances For

source

def BilinForm.comp {R : Type u_1} {M : Type u_2} [Semiring 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

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

Instances For

source

def BilinForm.compLeft {R : Type u_1} {M : Type u_2} [Semiring 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

Instances For

source

def BilinForm.compRight {R : Type u_1} {M : Type u_2} [Semiring 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

Instances For

source

theorem BilinForm.comp_comp {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] {M'' : Type u_11} [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} [Semiring 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} [Semiring 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} [Semiring 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.bilin (BilinForm.comp B l r) v w = BilinForm.bilin B (l v) (r w)

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem BilinForm.comp_id_left {R : Type u_1} {M : Type u_2} [Semiring 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} [Semiring 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} [Semiring 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} [Semiring 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} [Semiring 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} [Semiring 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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} [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.

Instances For

source

@[simp]

theorem BilinForm.congr_apply {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} [AddCommMonoid M₂'] [Module R₂ M₂'] (e : M₂ ≃ₗ[R₂] M₂') (B : BilinForm R₂ M₂) (x : M₂') (y : M₂') :

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

source

@[simp]

theorem BilinForm.congr_symm {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} [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_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} {M₂'' : Type u_12} [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_5} {M₂ : Type u_6} [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

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

Instances For

source

@[simp]

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

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

source

@[simp]

theorem BilinForm.linMulLin_comp {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} [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_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {B₂ : BilinForm R₂ M₂} {F₂ : BilinForm R₂ M₂} {ι : Type u_13} (b : Basis ι R₂ M₂) (h : ∀ (i j : ι), BilinForm.bilin B₂ (b i) (b j) = BilinForm.bilin F₂ (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_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {B₂ : BilinForm R₂ M₂} {ι : Type u_13} (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 • BilinForm.bilin B₂ (b i) (b j)) = BilinForm.bilin B₂ x y

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