Bilinear form #

This file defines orthogonal bilinear forms.

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,

source

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

Equations

B.IsOrtho x y = ((B x) y = 0)

Instances For

source

theorem LinearMap.BilinForm.isOrtho_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {x y : M} :

B.IsOrtho x y ↔ (B x) y = 0

source

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

B.IsOrtho 0 x

source

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

B.IsOrtho x 0

source

theorem LinearMap.BilinForm.ne_zero_of_not_isOrtho_self {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} (x : V) (hx₁ : ¬B.IsOrtho x x) :

x ≠ 0

source

theorem LinearMap.BilinForm.IsRefl.ortho_comm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsRefl) {x y : M} :

B.IsOrtho x y ↔ B.IsOrtho y x

source

theorem LinearMap.BilinForm.IsAlt.ortho_comm {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (H : B₁.IsAlt) {x y : M₁} :

B₁.IsOrtho x y ↔ B₁.IsOrtho y x

source

theorem LinearMap.BilinForm.IsSymm.ortho_comm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsSymm) {x y : M} :

B.IsOrtho x y ↔ B.IsOrtho y x

source

def LinearMap.BilinForm.iIsOrtho {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : Type w} (B : LinearMap.BilinForm 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 BilinForm.IsOrtho

Equations

B.iIsOrtho v = LinearMap.IsOrthoᵢ B v

Instances For

source

theorem LinearMap.BilinForm.iIsOrtho_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : Type w} {B : LinearMap.BilinForm R M} {v : n → M} :

B.iIsOrtho v ↔ ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0

source

@[simp]

theorem LinearMap.BilinForm.isOrtho_smul_left {R₄ : Type u_7} {M₄ : Type u_8} [CommRing R₄] [IsDomain R₄] [AddCommGroup M₄] [Module R₄ M₄] {G : LinearMap.BilinForm R₄ M₄} {x y : M₄} {a : R₄} (ha : a ≠ 0) :

G.IsOrtho (a • x) y ↔ G.IsOrtho x y

source

@[simp]

theorem LinearMap.BilinForm.isOrtho_smul_right {R₄ : Type u_7} {M₄ : Type u_8} [CommRing R₄] [IsDomain R₄] [AddCommGroup M₄] [Module R₄ M₄] {G : LinearMap.BilinForm R₄ M₄} {x y : M₄} {a : R₄} (ha : a ≠ 0) :

G.IsOrtho x (a • y) ↔ G.IsOrtho x y

source

theorem LinearMap.BilinForm.linearIndependent_of_iIsOrtho {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {n : Type w} {B : LinearMap.BilinForm K V} {v : n → V} (hv₁ : B.iIsOrtho v) (hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)) :

LinearIndependent K v

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.

source

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

Equations

B.orthogonal N = { carrier := {m : M | ∀ n ∈ N, B.IsOrtho n m}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.BilinForm.mem_orthogonal_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {N : Submodule R M} {m : M} :

m ∈ B.orthogonal N ↔ ∀ n ∈ N, B.IsOrtho n m

source

@[simp]

theorem LinearMap.BilinForm.orthogonal_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :

B.orthogonal ⊥ = ⊤

source

theorem LinearMap.BilinForm.orthogonal_le {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {N L : Submodule R M} (h : N ≤ L) :

B.orthogonal L ≤ B.orthogonal N

source

theorem LinearMap.BilinForm.le_orthogonal_orthogonal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {N : Submodule R M} (b : B.IsRefl) :

N ≤ B.orthogonal (B.orthogonal N)

source

theorem LinearMap.BilinForm.orthogonal_top_eq_ker {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsRefl) :

B.orthogonal ⊤ = LinearMap.ker B

source

theorem LinearMap.BilinForm.orthogonal_top_eq_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.Nondegenerate) (hB₀ : B.IsRefl) :

B.orthogonal ⊤ = ⊥

source

theorem LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :

Submodule.span K {x} ⊓ B.orthogonal (Submodule.span K {x}) = ⊥

source

theorem LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} (x : V) :

B.orthogonal (Submodule.span K {x}) = LinearMap.ker (B.toLinHomAux₁ x)

source

theorem LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :

Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x}) = ⊤

source

theorem LinearMap.BilinForm.isCompl_span_singleton_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :

IsCompl (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.

source

theorem LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : LinearMap.BilinForm R₁ M₁) (b : B.IsRefl) {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).

source

@[deprecated LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal]

theorem LinearMap.BilinForm.nondegenerateRestrictOfDisjointOrthogonal {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : LinearMap.BilinForm R₁ M₁) (b : B.IsRefl) {W : Submodule R₁ M₁} (hW : Disjoint W (B.orthogonal W)) :

(B.restrict W).Nondegenerate

Alias of LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal.

The restriction of a reflexive bilinear form B onto a submodule W is nondegenerate if Disjoint W (B.orthogonal W).

source

theorem LinearMap.BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : Type w} [Nontrivial R] {B : LinearMap.BilinForm R M} {v : Basis n R M} (h : B.iIsOrtho ⇑v) (hB : B.Nondegenerate) (i : n) :

¬B.IsOrtho (v i) (v i)

An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal elements.

source

theorem LinearMap.BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : Type w} [Nontrivial R] [NoZeroDivisors R] (B : LinearMap.BilinForm R M) (v : Basis n R M) (hO : B.iIsOrtho ⇑v) :

B.Nondegenerate ↔ ∀ (i : n), ¬B.IsOrtho (v i) (v i)

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.

source

theorem LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (W : Subspace K V) (b : B.IsRefl) :

Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict B W)) = W ⊓ B.orthogonal ⊤

source

theorem LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (W : Subspace K V) :

(LinearMap.range (LinearMap.domRestrict B W)).dualCoannihilator = B.orthogonal W

source

theorem LinearMap.BilinForm.ker_restrict_eq_of_codisjoint {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (hpq : Codisjoint p q) {B : LinearMap.BilinForm R M} (hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0) :

LinearMap.ker (B.restrict p) = Submodule.comap p.subtype (LinearMap.ker B)

source

theorem LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {W : Submodule R M} (b₁ : B.IsRefl) :

W ⊓ B.orthogonal W ≤ Submodule.map W.subtype (LinearMap.ker (B.restrict W))

source

theorem LinearMap.BilinForm.finrank_add_finrank_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (b₁ : B.IsRefl) (W : Submodule K V) :

Module.finrank K ↥W + Module.finrank K ↥(B.orthogonal W) = Module.finrank K V + Module.finrank K ↥(W ⊓ B.orthogonal ⊤)

source

theorem LinearMap.BilinForm.finrank_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : Submodule K V) :

Module.finrank K ↥(B.orthogonal W) = Module.finrank K V - Module.finrank K ↥W

source

theorem LinearMap.BilinForm.orthogonal_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : Submodule K V) :

B.orthogonal (B.orthogonal W) = W

source

theorem LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (hB₀ : B.IsRefl) :

IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)

source

theorem LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) :

IsCompl 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.

source

@[deprecated LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate]

theorem LinearMap.BilinForm.restrict_nondegenerate_of_isCompl_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) :

IsCompl W (B.orthogonal W)

Alias of LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate.

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.

source

theorem LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) :

(B.restrict W).Nondegenerate ↔ IsCompl 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.

source

theorem LinearMap.BilinForm.orthogonal_eq_top_iff {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) :

B.orthogonal W = ⊤ ↔ W = ⊥

source

theorem LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.orthogonal W = ⊥) :

W = ⊤

source

theorem LinearMap.BilinForm.orthogonal_eq_bot_iff {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.Nondegenerate) :

B.orthogonal W = ⊥ ↔ W = ⊤

We note that we cannot use BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal for the lemma below since the below lemma does not require V to be finite dimensional. However, BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal does not require B to be nondegenerate on the whole space.

source

theorem LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (b₁ : B.Nondegenerate) (b₂ : B.IsRefl) {x : V} (hx : ¬B.IsOrtho 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.

source

@[deprecated LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton]

theorem LinearMap.BilinForm.restrictNondegenerateOrthogonalSpanSingleton {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (b₁ : B.Nondegenerate) (b₂ : B.IsRefl) {x : V} (hx : ¬B.IsOrtho x x) :

(B.restrict (B.orthogonal (Submodule.span K {x}))).Nondegenerate

Alias of LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton.

The restriction of a reflexive, non-degenerate bilinear form on the orthogonal complement of the span of a singleton is also non-degenerate.

Documentation

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Bilinear form #

Notations #

References #

Tags #