Bilinear form #
This file defines a bilinear form over a module. Basic ideas such as orthogonality are also introduced, as well as reflexivive, 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 x 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 quadratic_form.lean with
exists_orthogonal_basis.
Notations #
Given any term B of type bilin_form, 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 semiringR,M₁,M₁', ... are modules over the ringR₁,M₂,M₂', ... are modules over the commutative semiringR₂,M₃,M₃', ... are modules over the commutative ringR₃,V, ... is a vector space over the fieldK.
References #
Tags #
Bilinear form,
structure
bilin_form
(R : Type u_1)
(M : Type u_2)
[semiring R]
[add_comm_monoid M]
[module R M] :
Type (max u_1 u_2)
- bilin : M → M → R
- bilin_add_left : ∀ (x y z : M), self.bilin (x + y) z = self.bilin x z + self.bilin y z
- bilin_smul_left : ∀ (a : R) (x y : M), self.bilin (a • x) y = a * self.bilin x y
- bilin_add_right : ∀ (x y z : M), self.bilin x (y + z) = self.bilin x y + self.bilin x z
- bilin_smul_right : ∀ (a : R) (x y : M), self.bilin x (a • y) = a * self.bilin x y
bilin_form R M is the type of R-bilinear functions M → M → R.
@[protected, instance]
def
bilin_form.has_coe_to_fun
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
has_coe_to_fun (bilin_form R M) (λ (_x : bilin_form R M), M → M → R)
Equations
- bilin_form.has_coe_to_fun = {coe := bilin_form.bilin _inst_3}
@[simp]
theorem
bilin_form.coe_fn_mk
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : M → M → R)
(h₁ : ∀ (x y z : M), f (x + y) z = f x z + f y z)
(h₂ : ∀ (a : R) (x y : M), f (a • x) y = a * f x y)
(h₃ : ∀ (x y z : M), f x (y + z) = f x y + f x z)
(h₄ : ∀ (a : R) (x y : M), f x (a • y) = a * f x y) :
⇑{bilin := f, bilin_add_left := h₁, bilin_smul_left := h₂, bilin_add_right := h₃, bilin_smul_right := h₄} = f
theorem
bilin_form.coe_fn_congr
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{x x' y y' : M} :
@[simp]
theorem
bilin_form.add_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(x y z : M) :
@[simp]
theorem
bilin_form.smul_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(a : R)
(x y : M) :
@[simp]
theorem
bilin_form.add_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(x y z : M) :
@[simp]
theorem
bilin_form.smul_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(a : R)
(x y : M) :
@[simp]
theorem
bilin_form.zero_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(x : M) :
@[simp]
theorem
bilin_form.zero_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(x : M) :
@[simp]
theorem
bilin_form.neg_left
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(x y : M₁) :
@[simp]
theorem
bilin_form.neg_right
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(x y : M₁) :
@[simp]
theorem
bilin_form.sub_left
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(x y z : M₁) :
@[simp]
theorem
bilin_form.sub_right
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(x y z : M₁) :
@[ext]
theorem
bilin_form.ext
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B D : bilin_form R M}
(H : ∀ (x y : M), ⇑B x y = ⇑D x y) :
B = D
theorem
bilin_form.congr_fun
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B D : bilin_form R M}
(h : B = D)
(x y : M) :
theorem
bilin_form.ext_iff
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B D : bilin_form R M} :
@[protected, instance]
def
bilin_form.add_comm_monoid
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
add_comm_monoid (bilin_form R M)
Equations
- bilin_form.add_comm_monoid = {add := λ (B D : bilin_form R M), {bilin := λ (x y : M), ⇑B x y + ⇑D x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, add_assoc := _, zero := {bilin := λ (x y : M), 0, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default {bilin := λ (x y : M), 0, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _} (λ (B D : bilin_form R M), {bilin := λ (x y : M), ⇑B x y + ⇑D x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}) bilin_form.add_comm_monoid._proof_12 bilin_form.add_comm_monoid._proof_13, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
def
bilin_form.add_comm_group
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁] :
add_comm_group (bilin_form R₁ M₁)
Equations
- bilin_form.add_comm_group = {add := add_comm_monoid.add bilin_form.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero bilin_form.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul bilin_form.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := λ (B : bilin_form R₁ M₁), {bilin := λ (x y : M₁), -B.bilin x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, sub := add_group.sub._default add_comm_monoid.add bilin_form.add_comm_group._proof_10 add_comm_monoid.zero bilin_form.add_comm_group._proof_11 bilin_form.add_comm_group._proof_12 add_comm_monoid.nsmul bilin_form.add_comm_group._proof_13 bilin_form.add_comm_group._proof_14 (λ (B : bilin_form R₁ M₁), {bilin := λ (x y : M₁), -B.bilin x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}), sub_eq_add_neg := _, zsmul := add_group.zsmul._default add_comm_monoid.add bilin_form.add_comm_group._proof_16 add_comm_monoid.zero bilin_form.add_comm_group._proof_17 bilin_form.add_comm_group._proof_18 add_comm_monoid.nsmul bilin_form.add_comm_group._proof_19 bilin_form.add_comm_group._proof_20 (λ (B : bilin_form R₁ M₁), {bilin := λ (x y : M₁), -B.bilin x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[simp]
theorem
bilin_form.add_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B D : bilin_form R M}
(x y : M) :
@[simp]
theorem
bilin_form.zero_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(x y : M) :
@[simp]
theorem
bilin_form.neg_apply
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(x y : M₁) :
@[protected, instance]
def
bilin_form.inhabited
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
inhabited (bilin_form R M)
Equations
- bilin_form.inhabited = {default := 0}
@[protected, instance]
def
bilin_form.module
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R] :
module R₂ (bilin_form R M)
bilin_form R M inherits the scalar action from any commutative subalgebra R₂ of R.
When R itself is commutative, this provides an R-action via algebra.id.
Equations
- bilin_form.module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (c : R₂) (B : bilin_form R M), {bilin := λ (x y : M), c • ⇑B x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
bilin_form.smul_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R]
(B : bilin_form R M)
(a : R₂)
(x y : M) :
def
bilin_form.flip_hom_aux
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(R₂ : Type u_5)
[comm_semiring R₂]
[algebra R₂ R] :
bilin_form R M →ₗ[R₂] bilin_form R M
Auxiliary construction for the flip of a bilinear form, obtained by exchanging the left and
right arguments. This version is a linear_map; it is later upgraded to a linear_equiv
in flip_hom.
Equations
- bilin_form.flip_hom_aux R₂ = {to_fun := λ (A : bilin_form R M), {bilin := λ (i j : M), ⇑A j i, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, map_add' := _, map_smul' := _}
theorem
bilin_form.flip_flip_aux
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R]
(A : bilin_form R M) :
⇑(bilin_form.flip_hom_aux R₂) (⇑(bilin_form.flip_hom_aux R₂) A) = A
def
bilin_form.flip_hom
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(R₂ : Type u_5)
[comm_semiring R₂]
[algebra R₂ R] :
bilin_form R M ≃ₗ[R₂] bilin_form R M
The flip of a bilinear form, obtained by exchanging the left and right arguments. This is a
less structured version of the equiv which applies to general (noncommutative) rings R with a
distinguished commutative subring R₂; over a commutative ring use flip.
Equations
- bilin_form.flip_hom R₂ = {to_fun := (bilin_form.flip_hom_aux R₂).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(bilin_form.flip_hom_aux R₂), left_inv := _, right_inv := _}
@[simp]
theorem
bilin_form.flip_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R]
(A : bilin_form R M)
(x y : M) :
⇑(⇑(bilin_form.flip_hom R₂) A) x y = ⇑A y x
theorem
bilin_form.flip_flip
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R] :
(bilin_form.flip_hom R₂).trans (bilin_form.flip_hom R₂) = linear_equiv.refl R₂ (bilin_form R M)
def
bilin_form.flip'
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
bilin_form R M ≃ₗ[ℕ] bilin_form R M
The flip of a bilinear form over a ring, obtained by exchanging the left and right arguments,
here considered as an ℕ-linear equivalence, i.e. an additive equivalence.
def
bilin_form.flip
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂] :
bilin_form R₂ M₂ ≃ₗ[R₂] bilin_form R₂ M₂
The flip of a bilinear form over a commutative ring, obtained by exchanging the left and
right arguments.
def
bilin_form.to_lin_hom_aux₁
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(A : bilin_form R M)
(x : M) :
Auxiliary definition to define to_lin_hom; see below.
def
bilin_form.to_lin_hom_aux₂
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R]
[module R₂ M]
[is_scalar_tower R₂ R M]
(A : bilin_form R M) :
Auxiliary definition to define to_lin_hom; see below.
Equations
- A.to_lin_hom_aux₂ = {to_fun := A.to_lin_hom_aux₁, map_add' := _, map_smul' := _}
def
bilin_form.to_lin_hom
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(R₂ : Type u_5)
[comm_semiring R₂]
[algebra R₂ R]
[module R₂ M]
[is_scalar_tower R₂ R M] :
The linear map obtained from a bilin_form 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 to_lin', which is ℕ-linear. Over a commutative semiring, use to_lin,
which is linear.
Equations
- bilin_form.to_lin_hom R₂ = {to_fun := bilin_form.to_lin_hom_aux₂ _inst_18, map_add' := _, map_smul' := _}
@[simp]
theorem
bilin_form.to_lin'_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R]
[module R₂ M]
[is_scalar_tower R₂ R M]
(A : bilin_form R M)
(x : M) :
def
bilin_form.to_lin'
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
The linear map obtained from a bilin_form by fixing the left co-ordinate and evaluating in
the right.
Over a commutative semiring, use to_lin, which is linear rather than ℕ-linear.
@[simp]
theorem
bilin_form.sum_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{α : Type u_3}
(t : finset α)
(g : α → M)
(w : M) :
@[simp]
theorem
bilin_form.sum_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{α : Type u_3}
(t : finset α)
(w : M)
(g : α → M) :
def
bilin_form.to_lin_hom_flip
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(R₂ : Type u_5)
[comm_semiring R₂]
[algebra R₂ R]
[module R₂ M]
[is_scalar_tower R₂ R M] :
The linear map obtained from a bilin_form 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 to_lin'_flip, which is ℕ-linear. Over a commutative semiring, use
to_lin_flip, which is linear.
Equations
@[simp]
theorem
bilin_form.to_lin'_flip_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
[algebra R₂ R]
[module R₂ M]
[is_scalar_tower R₂ R M]
(A : bilin_form R M)
(x : M) :
def
bilin_form.to_lin'_flip
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
The linear map obtained from a bilin_form by fixing the right co-ordinate and evaluating in
the left.
Over a commutative semiring, use to_lin_flip, which is linear rather than ℕ-linear.
def
linear_map.to_bilin_aux
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) :
bilin_form 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 linear_map.to_bilin.
Equations
- f.to_bilin_aux = {bilin := λ (x y : M₂), ⇑(⇑f x) y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
def
bilin_form.to_lin
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂] :
Bilinear forms are linearly equivalent to maps with two arguments that are linear in both.
Equations
- bilin_form.to_lin = {to_fun := (bilin_form.to_lin_hom R₂).to_fun, map_add' := _, map_smul' := _, inv_fun := linear_map.to_bilin_aux _inst_9, left_inv := _, right_inv := _}
def
linear_map.to_bilin
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂] :
A map with two arguments that is linear in both is linearly equivalent to bilinear form.
Equations
@[simp]
theorem
linear_map.to_bilin_aux_eq
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(f : M₂ →ₗ[R₂] M₂ →ₗ[R₂] R₂) :
@[simp]
theorem
linear_map.to_bilin_symm
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂] :
@[simp]
theorem
bilin_form.to_lin_symm
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂] :
@[simp, norm_cast]
theorem
bilin_form.to_lin_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{B₂ : bilin_form R₂ M₂}
(x : M₂) :
def
bilin_form.comp
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{M' : Type w}
[add_comm_monoid M']
[module R M']
(B : bilin_form R M')
(l r : M →ₗ[R] M') :
bilin_form R M
Apply a linear map on the left and right argument of a bilinear form.
Equations
- B.comp l r = {bilin := λ (x y : M), ⇑B (⇑l x) (⇑r y), bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
def
bilin_form.comp_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(f : M →ₗ[R] M) :
bilin_form R M
Apply a linear map to the left argument of a bilinear form.
Equations
- B.comp_left f = B.comp f linear_map.id
def
bilin_form.comp_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(f : M →ₗ[R] M) :
bilin_form R M
Apply a linear map to the right argument of a bilinear form.
Equations
- B.comp_right f = B.comp linear_map.id f
theorem
bilin_form.comp_comp
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{M' : Type w}
[add_comm_monoid M']
[module R M']
{M'' : Type u_3}
[add_comm_monoid M'']
[module R M'']
(B : bilin_form R M'')
(l r : M →ₗ[R] M')
(l' r' : M' →ₗ[R] M'') :
@[simp]
theorem
bilin_form.comp_left_comp_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(l r : M →ₗ[R] M) :
(B.comp_left l).comp_right r = B.comp l r
@[simp]
theorem
bilin_form.comp_right_comp_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(l r : M →ₗ[R] M) :
(B.comp_right r).comp_left l = B.comp l r
@[simp]
theorem
bilin_form.comp_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{M' : Type w}
[add_comm_monoid M']
[module R M']
(B : bilin_form R M')
(l r : M →ₗ[R] M')
(v w : M) :
@[simp]
theorem
bilin_form.comp_left_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(f : M →ₗ[R] M)
(v w : M) :
@[simp]
theorem
bilin_form.comp_right_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(f : M →ₗ[R] M)
(v w : M) :
⇑(B.comp_right f) v w = ⇑B v (⇑f w)
@[simp]
theorem
bilin_form.comp_id_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(r : M →ₗ[R] M) :
B.comp linear_map.id r = B.comp_right r
@[simp]
theorem
bilin_form.comp_id_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(l : M →ₗ[R] M) :
B.comp l linear_map.id = B.comp_left l
@[simp]
theorem
bilin_form.comp_left_id
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M) :
B.comp_left linear_map.id = B
@[simp]
theorem
bilin_form.comp_right_id
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M) :
B.comp_right linear_map.id = B
@[simp]
theorem
bilin_form.comp_id_id
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M) :
theorem
bilin_form.comp_inj
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{M' : Type w}
[add_comm_monoid M']
[module R M']
(B₁ B₂ : bilin_form R M')
{l r : M →ₗ[R] M'}
(hₗ : function.surjective ⇑l)
(hᵣ : function.surjective ⇑r) :
def
bilin_form.congr
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
[add_comm_monoid M₂']
[module R₂ M₂']
(e : M₂ ≃ₗ[R₂] M₂') :
bilin_form R₂ M₂ ≃ₗ[R₂] bilin_form R₂ M₂'
Apply a linear equivalence on the arguments of a bilinear form.
@[simp]
theorem
bilin_form.congr_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
[add_comm_monoid M₂']
[module R₂ M₂']
(e : M₂ ≃ₗ[R₂] M₂')
(B : bilin_form R₂ M₂)
(x y : M₂') :
@[simp]
theorem
bilin_form.congr_symm
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
[add_comm_monoid M₂']
[module R₂ M₂']
(e : M₂ ≃ₗ[R₂] M₂') :
@[simp]
theorem
bilin_form.congr_refl
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂] :
bilin_form.congr (linear_equiv.refl R₂ M₂) = linear_equiv.refl R₂ (bilin_form R₂ M₂)
theorem
bilin_form.congr_trans
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
{M₂'' : Type u_12}
[add_comm_monoid M₂']
[add_comm_monoid M₂'']
[module R₂ M₂']
[module R₂ M₂'']
(e : M₂ ≃ₗ[R₂] M₂')
(f : M₂' ≃ₗ[R₂] M₂'') :
(bilin_form.congr e).trans (bilin_form.congr f) = bilin_form.congr (e.trans f)
theorem
bilin_form.congr_congr
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
{M₂'' : Type u_12}
[add_comm_monoid M₂']
[add_comm_monoid M₂'']
[module R₂ M₂']
[module R₂ M₂'']
(e : M₂' ≃ₗ[R₂] M₂'')
(f : M₂ ≃ₗ[R₂] M₂')
(B : bilin_form R₂ M₂) :
⇑(bilin_form.congr e) (⇑(bilin_form.congr f) B) = ⇑(bilin_form.congr (f.trans e)) B
theorem
bilin_form.congr_comp
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
{M₂'' : Type u_12}
[add_comm_monoid M₂']
[add_comm_monoid M₂'']
[module R₂ M₂']
[module R₂ M₂'']
(e : M₂ ≃ₗ[R₂] M₂')
(B : bilin_form R₂ M₂)
(l r : M₂'' →ₗ[R₂] M₂') :
theorem
bilin_form.comp_congr
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
{M₂'' : Type u_12}
[add_comm_monoid M₂']
[add_comm_monoid M₂'']
[module R₂ M₂']
[module R₂ M₂'']
(e : M₂' ≃ₗ[R₂] M₂'')
(B : bilin_form R₂ M₂)
(l r : M₂' →ₗ[R₂] M₂) :
def
bilin_form.lin_mul_lin
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(f g : M₂ →ₗ[R₂] R₂) :
bilin_form R₂ M₂
lin_mul_lin f g is the bilinear form mapping x and y to f x * g y
Equations
- bilin_form.lin_mul_lin f g = {bilin := λ (x y : M₂), (⇑f x) * ⇑g y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
@[simp]
theorem
bilin_form.lin_mul_lin_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{f g : M₂ →ₗ[R₂] R₂}
(x y : M₂) :
@[simp]
theorem
bilin_form.lin_mul_lin_comp
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
[add_comm_monoid M₂']
[module R₂ M₂']
{f g : M₂ →ₗ[R₂] R₂}
(l r : M₂' →ₗ[R₂] M₂) :
(bilin_form.lin_mul_lin f g).comp l r = bilin_form.lin_mul_lin (f.comp l) (g.comp r)
@[simp]
theorem
bilin_form.lin_mul_lin_comp_left
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{f g : M₂ →ₗ[R₂] R₂}
(l : M₂ →ₗ[R₂] M₂) :
(bilin_form.lin_mul_lin f g).comp_left l = bilin_form.lin_mul_lin (f.comp l) g
@[simp]
theorem
bilin_form.lin_mul_lin_comp_right
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{f g : M₂ →ₗ[R₂] R₂}
(r : M₂ →ₗ[R₂] M₂) :
(bilin_form.lin_mul_lin f g).comp_right r = bilin_form.lin_mul_lin f (g.comp r)
def
bilin_form.is_ortho
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(x y : M) :
Prop
The proposition that two elements of a bilinear form space are orthogonal. For orthogonality
of an indexed set of elements, use bilin_form.is_Ortho.
theorem
bilin_form.is_ortho_def
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{x y : M} :
theorem
bilin_form.is_ortho_zero_left
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(x : M) :
B.is_ortho 0 x
theorem
bilin_form.is_ortho_zero_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(x : M) :
B.is_ortho x 0
theorem
bilin_form.ne_zero_of_not_is_ortho_self
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
{B : bilin_form K V}
(x : V)
(hx₁ : ¬B.is_ortho x x) :
x ≠ 0
def
bilin_form.is_Ortho
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{n : Type w}
(B : bilin_form R M)
(v : n → M) :
Prop
A set of vectors v is orthogonal with respect to some bilinear form B if and only
if for all i ≠ j, B (v i) (v j) = 0. For orthogonality between two elements, use
bilin_form.is_ortho
theorem
bilin_form.is_Ortho_def
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{n : Type w}
{B : bilin_form R M}
{v : n → M} :
@[simp]
theorem
bilin_form.is_ortho_smul_left
{R₄ : Type u_13}
{M₄ : Type u_14}
[ring R₄]
[is_domain R₄]
[add_comm_group M₄]
[module R₄ M₄]
{G : bilin_form R₄ M₄}
{x y : M₄}
{a : R₄}
(ha : a ≠ 0) :
@[simp]
theorem
bilin_form.is_ortho_smul_right
{R₄ : Type u_13}
{M₄ : Type u_14}
[ring R₄]
[is_domain R₄]
[add_comm_group M₄]
[module R₄ M₄]
{G : bilin_form R₄ M₄}
{x y : M₄}
{a : R₄}
(ha : a ≠ 0) :
theorem
bilin_form.linear_independent_of_is_Ortho
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
{n : Type w}
{B : bilin_form K V}
{v : n → V}
(hv₁ : B.is_Ortho v)
(hv₂ : ∀ (i : n), ¬B.is_ortho (v i) (v i)) :
A set of orthogonal vectors v with respect to some bilinear form B is linearly independent
if for all i, B (v i) (v i) ≠ 0.
theorem
bilin_form.ext_basis
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{B₃ F₃ : bilin_form R₃ M₃}
{ι : Type u_13}
(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
bilin_form.sum_repr_mul_repr_mul
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{B₃ : bilin_form R₃ M₃}
{ι : Type u_13}
(b : basis ι R₃ M₃)
(x y : M₃) :
Write out B x y as a sum over B (b i) (b j) if b is a basis.
def
bilin_form.is_refl
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M) :
Prop
The proposition that a bilinear form is reflexive
theorem
bilin_form.is_refl.eq_zero
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(H : B.is_refl)
{x y : M} :
theorem
bilin_form.is_refl.ortho_comm
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(H : B.is_refl)
{x y : M} :
def
bilin_form.is_symm
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M) :
Prop
The proposition that a bilinear form is symmetric
@[protected]
theorem
bilin_form.is_symm.eq
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(H : B.is_symm)
(x y : M) :
theorem
bilin_form.is_symm.is_refl
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(H : B.is_symm) :
B.is_refl
theorem
bilin_form.is_symm.ortho_comm
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(H : B.is_symm)
{x y : M} :
theorem
bilin_form.is_symm_iff_flip'
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{R₂ : Type u_5}
[comm_semiring R₂]
{B : bilin_form R M}
[algebra R₂ R] :
B.is_symm ↔ ⇑(bilin_form.flip_hom R₂) B = B
def
bilin_form.is_alt
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M) :
Prop
The proposition that a bilinear form is alternating
theorem
bilin_form.is_alt.self_eq_zero
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(H : B.is_alt)
(x : M) :
theorem
bilin_form.is_alt.neg
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(H : B₁.is_alt)
(x y : M₁) :
theorem
bilin_form.is_alt.is_refl
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(H : B₁.is_alt) :
B₁.is_refl
theorem
bilin_form.is_alt.ortho_comm
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
(H : B₁.is_alt)
{x y : M₁} :
def
bilin_form.is_adjoint_pair
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
{M' : Type u_13}
[add_comm_monoid M']
[module R M']
(B' : bilin_form R M')
(f : M →ₗ[R] M')
(g : M' →ₗ[R] M) :
Prop
Given a pair of modules equipped with bilinear forms, this is the condition for a pair of maps between them to be mutually adjoint.
theorem
bilin_form.is_adjoint_pair.eq
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{M' : Type u_13}
[add_comm_monoid M']
[module R M']
{B' : bilin_form R M'}
{f : M →ₗ[R] M'}
{g : M' →ₗ[R] M}
(h : B.is_adjoint_pair B' f g)
{x : M}
{y : M'} :
theorem
bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
(F : bilin_form R M)
(f g : module.End R M) :
B.is_adjoint_pair F f g ↔ F.comp_left f = B.comp_right g
theorem
bilin_form.is_adjoint_pair_zero
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{M' : Type u_13}
[add_comm_monoid M']
[module R M']
{B' : bilin_form R M'} :
B.is_adjoint_pair B' 0 0
theorem
bilin_form.is_adjoint_pair_id
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M} :
B.is_adjoint_pair B 1 1
theorem
bilin_form.is_adjoint_pair.add
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{M' : Type u_13}
[add_comm_monoid M']
[module R M']
{B' : bilin_form R M'}
{f f' : M →ₗ[R] M'}
{g g' : M' →ₗ[R] M}
(h : B.is_adjoint_pair B' f g)
(h' : B.is_adjoint_pair B' f' g') :
B.is_adjoint_pair B' (f + f') (g + g')
theorem
bilin_form.is_adjoint_pair.sub
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{B₁ : bilin_form R₁ M₁}
{M₁' : Type u_14}
[add_comm_group M₁']
[module R₁ M₁']
{B₁' : bilin_form R₁ M₁'}
{f₁ f₁' : M₁ →ₗ[R₁] M₁'}
{g₁ g₁' : M₁' →ₗ[R₁] M₁}
(h : B₁.is_adjoint_pair B₁' f₁ g₁)
(h' : B₁.is_adjoint_pair B₁' f₁' g₁') :
B₁.is_adjoint_pair B₁' (f₁ - f₁') (g₁ - g₁')
theorem
bilin_form.is_adjoint_pair.smul
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{B₂ : bilin_form R₂ M₂}
{M₂' : Type u_11}
[add_comm_monoid M₂']
[module R₂ M₂']
{B₂' : bilin_form R₂ M₂'}
{f₂ : M₂ →ₗ[R₂] M₂'}
{g₂ : M₂' →ₗ[R₂] M₂}
(c : R₂)
(h : B₂.is_adjoint_pair B₂' f₂ g₂) :
B₂.is_adjoint_pair B₂' (c • f₂) (c • g₂)
theorem
bilin_form.is_adjoint_pair.comp
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{M' : Type u_13}
[add_comm_monoid M']
[module R M']
{B' : bilin_form R M'}
{f : M →ₗ[R] M'}
{g : M' →ₗ[R] M}
{M'' : Type u_15}
[add_comm_monoid M'']
[module R M'']
(B'' : bilin_form R M'')
{f' : M' →ₗ[R] M''}
{g' : M'' →ₗ[R] M'}
(h : B.is_adjoint_pair B' f g)
(h' : B'.is_adjoint_pair B'' f' g') :
B.is_adjoint_pair B'' (f'.comp f) (g.comp g')
theorem
bilin_form.is_adjoint_pair.mul
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{f g f' g' : module.End R M}
(h : B.is_adjoint_pair B f g)
(h' : B.is_adjoint_pair B f' g') :
B.is_adjoint_pair B (f * f') (g' * g)
def
bilin_form.is_pair_self_adjoint
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B F : bilin_form R M)
(f : module.End R M) :
Prop
The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept of self adjointness. In the case that one of the forms is the negation of the other, this is the usual concept of skew adjointness.
Equations
- B.is_pair_self_adjoint F f = B.is_adjoint_pair F f f
def
bilin_form.is_pair_self_adjoint_submodule
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(B₂ F₂ : bilin_form R₂ M₂) :
submodule R₂ (module.End R₂ M₂)
The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms.
Equations
- B₂.is_pair_self_adjoint_submodule F₂ = {carrier := {f : module.End R₂ M₂ | B₂.is_pair_self_adjoint F₂ f}, add_mem' := _, zero_mem' := _, smul_mem' := _}
@[simp]
theorem
bilin_form.mem_is_pair_self_adjoint_submodule
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(B₂ F₂ : bilin_form R₂ M₂)
(f : module.End R₂ M₂) :
f ∈ B₂.is_pair_self_adjoint_submodule F₂ ↔ B₂.is_pair_self_adjoint F₂ f
theorem
bilin_form.is_pair_self_adjoint_equiv
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{M₃' : Type u_16}
[add_comm_group M₃']
[module R₃ M₃']
(B₃ F₃ : bilin_form R₃ M₃)
(e : M₃' ≃ₗ[R₃] M₃)
(f : module.End R₃ M₃) :
def
bilin_form.is_self_adjoint
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(f : module.End R M) :
Prop
An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an adjoint for itself.
Equations
- B.is_self_adjoint f = B.is_adjoint_pair B f f
def
bilin_form.is_skew_adjoint
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
(B₁ : bilin_form R₁ M₁)
(f : module.End R₁ M₁) :
Prop
An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation serves as an adjoint.
Equations
- B₁.is_skew_adjoint f = B₁.is_adjoint_pair B₁ f (-f)
theorem
bilin_form.is_skew_adjoint_iff_neg_self_adjoint
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
(B₁ : bilin_form R₁ M₁)
(f : module.End R₁ M₁) :
B₁.is_skew_adjoint f ↔ (-B₁).is_adjoint_pair B₁ f f
def
bilin_form.self_adjoint_submodule
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(B₂ : bilin_form R₂ M₂) :
submodule R₂ (module.End R₂ M₂)
The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Jordan subalgebra.)
Equations
@[simp]
theorem
bilin_form.mem_self_adjoint_submodule
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(B₂ : bilin_form R₂ M₂)
(f : module.End R₂ M₂) :
f ∈ B₂.self_adjoint_submodule ↔ B₂.is_self_adjoint f
def
bilin_form.skew_adjoint_submodule
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
(B₃ : bilin_form R₃ M₃) :
submodule R₃ (module.End R₃ M₃)
The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Lie subalgebra.)
Equations
@[simp]
theorem
bilin_form.mem_skew_adjoint_submodule
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
(B₃ : bilin_form R₃ M₃)
(f : module.End R₃ M₃) :
f ∈ B₃.skew_adjoint_submodule ↔ B₃.is_skew_adjoint f
def
bilin_form.orthogonal
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(N : submodule R M) :
submodule R M
The orthogonal complement of a submodule N with respect to some bilinear form is the set of
elements x which are orthogonal to all elements of N; i.e., for all y in N, B x y = 0.
Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal
complement for which, for all y in N, B y x = 0. This variant definition is not currently
provided in mathlib.
@[simp]
theorem
bilin_form.mem_orthogonal_iff
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{N : submodule R M}
{m : M} :
m ∈ B.orthogonal N ↔ ∀ (n : M), n ∈ N → B.is_ortho n m
theorem
bilin_form.orthogonal_le
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{N L : submodule R M}
(h : N ≤ L) :
B.orthogonal L ≤ B.orthogonal N
theorem
bilin_form.le_orthogonal_orthogonal
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{B : bilin_form R M}
{N : submodule R M}
(b : B.is_refl) :
N ≤ B.orthogonal (B.orthogonal N)
theorem
bilin_form.span_singleton_inf_orthogonal_eq_bot
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
{B : bilin_form K V}
{x : V}
(hx : ¬B.is_ortho x x) :
submodule.span K {x} ⊓ B.orthogonal (submodule.span K {x}) = ⊥
theorem
bilin_form.orthogonal_span_singleton_eq_to_lin_ker
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
{B : bilin_form K V}
(x : V) :
B.orthogonal (submodule.span K {x}) = (⇑(⇑bilin_form.to_lin B) x).ker
theorem
bilin_form.span_singleton_sup_orthogonal_eq_top
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
{B : bilin_form K V}
{x : V}
(hx : ¬B.is_ortho x x) :
submodule.span K {x} ⊔ B.orthogonal (submodule.span K {x}) = ⊤
theorem
bilin_form.is_compl_span_singleton_orthogonal
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
{B : bilin_form K V}
{x : V}
(hx : ¬B.is_ortho x x) :
is_compl (submodule.span K {x}) (B.orthogonal (submodule.span K {x}))
Given a bilinear form B and some x such that B x x ≠ 0, the span of the singleton of x
is complement to its orthogonal complement.
def
bilin_form.restrict
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(W : submodule R M) :
bilin_form R ↥W
The restriction of a bilinear form on a submodule.
Equations
- B.restrict W = {bilin := λ (a b : ↥W), ⇑B ↑a ↑b, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
@[simp]
theorem
bilin_form.restrict_apply
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(W : submodule R M)
(a b : ↥W) :
theorem
bilin_form.restrict_symm
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M)
(b : B.is_symm)
(W : submodule R M) :
The restriction of a symmetric bilinear form on a submodule is also symmetric.
def
bilin_form.nondegenerate
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(B : bilin_form R M) :
Prop
A nondegenerate bilinear form is a bilinear form such that the only element that is orthogonal
to every other element is 0; i.e., for all nonzero m in M, there exists n in M with
B m n ≠ 0.
Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
chirality; in addition to this "left" nondegeneracy condition one could define a "right"
nondegeneracy condition that in the situation described, B n m ≠ 0. This variant definition is
not currently provided in mathlib. In finite dimension either definition implies the other.
Equations
- B.nondegenerate = ∀ (m : M), (∀ (n : M), ⇑B m n = 0) → m = 0
theorem
bilin_form.not_nondegenerate_zero
(R : Type u_1)
(M : Type u_2)
[semiring R]
[add_comm_monoid M]
[module R M]
[nontrivial M] :
In a non-trivial module, zero is not non-degenerate.
theorem
bilin_form.nondegenerate.ne_zero
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
[nontrivial M]
{B : bilin_form R M}
(h : B.nondegenerate) :
B ≠ 0
theorem
bilin_form.nondegenerate.congr
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
[add_comm_monoid M₂']
[module R₂ M₂']
{B : bilin_form R₂ M₂}
(e : M₂ ≃ₗ[R₂] M₂')
(h : B.nondegenerate) :
(⇑(bilin_form.congr e) B).nondegenerate
@[simp]
theorem
bilin_form.nondegenerate_congr_iff
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₂' : Type u_11}
[add_comm_monoid M₂']
[module R₂ M₂']
{B : bilin_form R₂ M₂}
(e : M₂ ≃ₗ[R₂] M₂') :
(⇑(bilin_form.congr e) B).nondegenerate ↔ B.nondegenerate
theorem
bilin_form.nondegenerate_iff_ker_eq_bot
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{B : bilin_form R₂ M₂} :
B.nondegenerate ↔ (⇑bilin_form.to_lin B).ker = ⊥
A bilinear form is nondegenerate if and only if it has a trivial kernel.
theorem
bilin_form.nondegenerate.ker_eq_bot
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{B : bilin_form R₂ M₂}
(h : B.nondegenerate) :
(⇑bilin_form.to_lin B).ker = ⊥
theorem
bilin_form.nondegenerate_restrict_of_disjoint_orthogonal
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
(B : bilin_form R₁ M₁)
(b : B.is_refl)
{W : submodule R₁ M₁}
(hW : disjoint W (B.orthogonal W)) :
(B.restrict W).nondegenerate
The restriction of a reflexive bilinear form B onto a submodule W is
nondegenerate if disjoint W (B.orthogonal W).
theorem
bilin_form.is_Ortho.not_is_ortho_basis_self_of_nondegenerate
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{n : Type w}
[nontrivial R]
{B : bilin_form R M}
{v : basis n R M}
(h : B.is_Ortho ⇑v)
(hB : B.nondegenerate)
(i : n) :
An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal elements.
theorem
bilin_form.is_Ortho.nondegenerate_iff_not_is_ortho_basis_self
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{n : Type w}
[nontrivial R]
[no_zero_divisors R]
(B : bilin_form R M)
(v : basis n R M)
(hO : B.is_Ortho ⇑v) :
Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate iff the basis has no elements which are self-orthogonal.
theorem
bilin_form.to_lin_restrict_ker_eq_inf_orthogonal
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
(B : bilin_form K V)
(W : subspace K V)
(b : B.is_refl) :
submodule.map (submodule.subtype W) ((⇑bilin_form.to_lin B).dom_restrict W).ker = W ⊓ B.orthogonal ⊤
theorem
bilin_form.to_lin_restrict_range_dual_annihilator_comap_eq_orthogonal
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
(B : bilin_form K V)
(W : subspace K V) :
((⇑bilin_form.to_lin B).dom_restrict W).range.dual_annihilator_comap = B.orthogonal W
theorem
bilin_form.finrank_add_finrank_orthogonal
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{B : bilin_form K V}
{W : subspace K V}
(b₁ : B.is_refl) :
finite_dimensional.finrank K ↥W + finite_dimensional.finrank K ↥(B.orthogonal W) = finite_dimensional.finrank K V + finite_dimensional.finrank K ↥(W ⊓ B.orthogonal ⊤)
theorem
bilin_form.restrict_nondegenerate_of_is_compl_orthogonal
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{B : bilin_form K V}
{W : subspace K V}
(b₁ : B.is_refl)
(b₂ : (B.restrict W).nondegenerate) :
is_compl W (B.orthogonal W)
A subspace is complement to its orthogonal complement with respect to some reflexive bilinear form if that bilinear form restricted on to the subspace is nondegenerate.
theorem
bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{B : bilin_form K V}
{W : subspace K V}
(b₁ : B.is_refl) :
(B.restrict W).nondegenerate ↔ is_compl W (B.orthogonal W)
A subspace is complement to its orthogonal complement with respect to some reflexive bilinear form if and only if that bilinear form restricted on to the subspace is nondegenerate.
noncomputable
def
bilin_form.to_dual
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(B : bilin_form K V)
(b : B.nondegenerate) :
V ≃ₗ[K] module.dual K V
Given a nondegenerate bilinear form B on a finite-dimensional vector space, B.to_dual is
the linear equivalence between a vector space and its dual with the underlying linear map
B.to_lin.
Equations
- B.to_dual b = (⇑bilin_form.to_lin B).linear_equiv_of_injective _ bilin_form.to_dual._proof_11
theorem
bilin_form.to_dual_def
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{B : bilin_form K V}
(b : B.nondegenerate)
{m n : V} :
noncomputable
def
bilin_form.dual_basis
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
(B : bilin_form K V)
(hB : B.nondegenerate)
(b : basis ι K V) :
basis ι K V
The B-dual basis B.dual_basis hB b to a finite basis b satisfies
B (B.dual_basis hB b i) (b j) = B (b i) (B.dual_basis hB b j) = if i = j then 1 else 0,
where B is a nondegenerate (symmetric) bilinear form and b is a finite basis.
Equations
- B.dual_basis hB b = b.dual_basis.map (B.to_dual hB).symm
@[simp]
theorem
bilin_form.dual_basis_repr_apply
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
(B : bilin_form K V)
(hB : B.nondegenerate)
(b : basis ι K V)
(x : V)
(i : ι) :
theorem
bilin_form.apply_dual_basis_left
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
(B : bilin_form K V)
(hB : B.nondegenerate)
(b : basis ι K V)
(i j : ι) :
theorem
bilin_form.apply_dual_basis_right
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
(B : bilin_form K V)
(hB : B.nondegenerate)
(sym : B.is_symm)
(b : basis ι K V)
(i j : ι) :
We note that we cannot use bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal for the
lemma below since the below lemma does not require V to be finite dimensional. However,
bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal does not require B to be nondegenerate
on the whole space.
theorem
bilin_form.restrict_orthogonal_span_singleton_nondegenerate
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
(B : bilin_form K V)
(b₁ : B.nondegenerate)
(b₂ : B.is_refl)
{x : V}
(hx : ¬B.is_ortho x x) :
(B.restrict (B.orthogonal (submodule.span K {x}))).nondegenerate
The restriction of a reflexive, non-degenerate bilinear form on the orthogonal complement of the span of a singleton is also non-degenerate.
theorem
bilin_form.comp_left_injective
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
(B : bilin_form R₁ M₁)
(b : B.nondegenerate) :
theorem
bilin_form.is_adjoint_pair_unique_of_nondegenerate
{R₁ : Type u_3}
{M₁ : Type u_4}
[ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
(B : bilin_form R₁ M₁)
(b : B.nondegenerate)
(φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁)
(hψ₁ : B.is_adjoint_pair B ψ₁ φ)
(hψ₂ : B.is_adjoint_pair B ψ₂ φ) :
ψ₁ = ψ₂
noncomputable
def
bilin_form.symm_comp_of_nondegenerate
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(B₁ B₂ : bilin_form K V)
(b₂ : B₂.nondegenerate) :
Given bilinear forms B₁, B₂ where B₂ is nondegenerate, symm_comp_of_nondegenerate
is the linear map B₂.to_lin⁻¹ ∘ B₁.to_lin.
Equations
- B₁.symm_comp_of_nondegenerate B₂ b₂ = (B₂.to_dual b₂).symm.to_linear_map.comp (⇑bilin_form.to_lin B₁)
theorem
bilin_form.comp_symm_comp_of_nondegenerate_apply
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(B₁ : bilin_form K V)
{B₂ : bilin_form K V}
(b₂ : B₂.nondegenerate)
(v : V) :
⇑(⇑bilin_form.to_lin B₂) (⇑(B₁.symm_comp_of_nondegenerate B₂ b₂) v) = ⇑(⇑bilin_form.to_lin B₁) v
@[simp]
theorem
bilin_form.symm_comp_of_nondegenerate_left_apply
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(B₁ : bilin_form K V)
{B₂ : bilin_form K V}
(b₂ : B₂.nondegenerate)
(v w : V) :
⇑B₂ (⇑(B₁.symm_comp_of_nondegenerate B₂ b₂) w) v = ⇑B₁ w v
noncomputable
def
bilin_form.left_adjoint_of_nondegenerate
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(B : bilin_form K V)
(b : B.nondegenerate)
(φ : V →ₗ[K] V) :
Given the nondegenerate bilinear form B and the linear map φ,
left_adjoint_of_nondegenerate provides the left adjoint of φ with respect to B.
The lemma proving this property is bilin_form.is_adjoint_pair_left_adjoint_of_nondegenerate.
Equations
- B.left_adjoint_of_nondegenerate b φ = (B.comp_right φ).symm_comp_of_nondegenerate B b
theorem
bilin_form.is_adjoint_pair_left_adjoint_of_nondegenerate
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(B : bilin_form K V)
(b : B.nondegenerate)
(φ : V →ₗ[K] V) :
B.is_adjoint_pair B (B.left_adjoint_of_nondegenerate b φ) φ
theorem
bilin_form.is_adjoint_pair_iff_eq_of_nondegenerate
{V : Type u_9}
{K : Type u_10}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(B : bilin_form K V)
(b : B.nondegenerate)
(ψ φ : V →ₗ[K] V) :
B.is_adjoint_pair B ψ φ ↔ ψ = B.left_adjoint_of_nondegenerate b φ
Given the nondegenerate bilinear form B, the linear map φ has a unique left adjoint given by
bilin_form.left_adjoint_of_nondegenerate.