mathlib documentation

linear_algebra.sesquilinear_form

Sesquilinear form #

This files provides properties about sesquilinear forms. The maps considered are of the form M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R, where I₁ : R₁ →+* R and I₂ : R₂ →+* R are ring homomorphisms and M₁ is a module over R₁ and M₂ is a module over R₂. Sesquilinear forms are the special case that M₁ = M₂, R₁ = R₂ = R, and I₁ = ring_hom.id R. Taking additionally I₂ = ring_hom.id R, then one obtains bilinear forms.

These forms are a special case of the bilinear maps defined in bilinear_map.lean and all basic lemmas about construction and elementary calculations are found there.

Main declarations #

References #

Tags #

Sesquilinear form,

Orthogonal vectors #

source
def linear_map.is_ortho {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁] [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x : M₁) (y : M₂) :
Prop

The proposition that two elements of a sesquilinear form space are orthogonal

Equations
source
theorem linear_map.is_ortho_def {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁] [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} {x : M₁} {y : M₂} :
B.is_ortho x y ↔ ⇑(⇑B x) y = 0
source
theorem linear_map.is_ortho_zero_left {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁] [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x : M₂) :
B.is_ortho 0 x
source
theorem linear_map.is_ortho_zero_right {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁] [comm_semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x : M₁) :
B.is_ortho x 0
source
def linear_map.is_Ortho {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁] {I₁ I₁' : R₁ →+* R} {n : Type u_3} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R) (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

Equations
source
theorem linear_map.is_Ortho_def {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁] {I₁ I₁' : R₁ →+* R} {n : Type u_3} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R} {v : n → M₁} :
B.is_Ortho v ↔ ∀ (i j : n), i ≠ j → ⇑(⇑B (v i)) (v j) = 0
source
theorem linear_map.ortho_smul_left {K : Type u_8} {K₁ : Type u_9} {K₂ : Type u_10} {V₁ : Type u_12} {V₂ : Type u_13} [field K] [field K₁] [add_comm_group V₁] [module K₁ V₁] [field K₂] [add_comm_group V₂] [module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K} {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K} {x : V₁} {y : V₂} {a : K₁} (ha : a ≠ 0) :
B.is_ortho x y ↔ B.is_ortho (a • x) y
source
theorem linear_map.ortho_smul_right {K : Type u_8} {K₁ : Type u_9} {K₂ : Type u_10} {V₁ : Type u_12} {V₂ : Type u_13} [field K] [field K₁] [add_comm_group V₁] [module K₁ V₁] [field K₂] [add_comm_group V₂] [module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K} {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K} {x : V₁} {y : V₂} {a : K₂} {ha : a ≠ 0} :
B.is_ortho x y ↔ B.is_ortho x (a • y)
source
theorem linear_map.linear_independent_of_is_Ortho {K : Type u_8} {K₁ : Type u_9} {V₁ : Type u_12} {n : Type u_14} [field K] [field K₁] [add_comm_group V₁] [module K₁ V₁] {I₁ I₁' : K₁ →+* K} {B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K} {v : n → V₁} (hv₁ : B.is_Ortho v) (hv₂ : ∀ (i : n), ¬B.is_ortho (v i) (v i)) :
linear_independent K₁ v

A set of orthogonal vectors v with respect to some sesquilinear form B is linearly independent if for all i, B (v i) (v i) ≠ 0.

Reflexive bilinear forms #

source
def linear_map.is_refl {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :
Prop

The proposition that a sesquilinear form is reflexive

Equations
source
theorem linear_map.is_refl.eq_zero {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : B.is_refl) {x y : M₁} :
⇑(⇑B x) y = 0 → ⇑(⇑B y) x = 0
source
theorem linear_map.is_refl.ortho_comm {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : B.is_refl) {x y : M₁} :
B.is_ortho x y ↔ B.is_ortho y x

Symmetric bilinear forms #

source
def linear_map.is_symm {R : Type u_1} {M : Type u_5} [comm_ring R] [add_comm_group M] [module R M] {I : R →+* R} (B : M →ₗ[R] M →ₛₗ[I] R) :
Prop

The proposition that a sesquilinear form is symmetric

Equations
source
@[protected]
theorem linear_map.is_symm.eq {R : Type u_1} {M : Type u_5} [comm_ring R] [add_comm_group M] [module R M] {I : R →+* R} {B' : M →ₗ[R] M →ₛₗ[I] R} (H : B'.is_symm) (x y : M) :
⇑I (⇑(⇑B' x) y) = ⇑(⇑B' y) x
source
theorem linear_map.is_symm.is_refl {R : Type u_1} {M : Type u_5} [comm_ring R] [add_comm_group M] [module R M] {I : R →+* R} {B' : M →ₗ[R] M →ₛₗ[I] R} (H : B'.is_symm) :
B'.is_refl
source
theorem linear_map.is_symm.ortho_comm {R : Type u_1} {M : Type u_5} [comm_ring R] [add_comm_group M] [module R M] {I : R →+* R} {B' : M →ₗ[R] M →ₛₗ[I] R} (H : B'.is_symm) {x y : M} :
B'.is_ortho x y ↔ B'.is_ortho y x

Alternating bilinear forms #

source
def linear_map.is_alt {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :
Prop

The proposition that a sesquilinear form is alternating

Equations
source
theorem linear_map.is_alt.self_eq_zero {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : B.is_alt) (x : M₁) :
⇑(⇑B x) x = 0
source
theorem linear_map.is_alt.neg {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : B.is_alt) (x y : M₁) :
-⇑(⇑B x) y = ⇑(⇑B y) x
source
theorem linear_map.is_alt.is_refl {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : B.is_alt) :
B.is_refl
source
theorem linear_map.is_alt.ortho_comm {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : B.is_alt) {x y : M₁} :
B.is_ortho x y ↔ B.is_ortho y x

The orthogonal complement #

source
def submodule.orthogonal_bilin {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} (N : submodule R₁ M₁) (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :
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.

Equations
source
@[simp]
theorem submodule.mem_orthogonal_bilin_iff {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} {N : submodule R₁ M₁} {m : M₁} :
m ∈ N.orthogonal_bilin B ↔ ∀ (n : M₁), n ∈ N → B.is_ortho n m
source
theorem submodule.orthogonal_bilin_le {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} {N L : submodule R₁ M₁} (h : N ≤ L) :
L.orthogonal_bilin B ≤ N.orthogonal_bilin B
source
theorem submodule.le_orthogonal_bilin_orthogonal_bilin {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [comm_ring R] [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} {N : submodule R₁ M₁} (b : B.is_refl) :
N ≤ (N.orthogonal_bilin B).orthogonal_bilin B
source
theorem linear_map.span_singleton_inf_orthogonal_eq_bot {K : Type u_8} {K₁ : Type u_9} {V₁ : Type u_12} [field K] [field K₁] [add_comm_group V₁] [module K₁ V₁] {J₁ J₁' : K₁ →+* K} (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K) (x : V₁) (hx : ¬B.is_ortho x x) :
submodule.span K₁ {x} ⊓ (submodule.span K₁ {x}).orthogonal_bilin B = ⊥
source
theorem linear_map.orthogonal_span_singleton_eq_to_lin_ker {K : Type u_8} {V : Type u_11} [field K] [add_comm_group V] [module K V] {J : K →+* K} {B : V →ₗ[K] V →ₛₗ[J] K} (x : V) :
(submodule.span K {x}).orthogonal_bilin B = (⇑B x).ker
source
theorem linear_map.span_singleton_sup_orthogonal_eq_top {K : Type u_8} {V : Type u_11} [field K] [add_comm_group V] [module K V] {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.is_ortho x x) :
submodule.span K {x} ⊔ (submodule.span K {x}).orthogonal_bilin B = ⊤
source
theorem linear_map.is_compl_span_singleton_orthogonal {K : Type u_8} {V : Type u_11} [field K] [add_comm_group V] [module K V] {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.is_ortho x x) :
is_compl (submodule.span K {x}) ((submodule.span K {x}).orthogonal_bilin B)

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.