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

Tags

Bilinear form,

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 : M) (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

• LinearMap.BilinForm.IsOrtho B x y = ((B x) y = 0)

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 : M} {y : M} : LinearMap.BilinForm.IsOrtho B x y ↔ (B x) y = 0

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) : LinearMap.BilinForm.IsOrtho B 0 x

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) : LinearMap.BilinForm.IsOrtho B x 0

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₁ : ¬LinearMap.BilinForm.IsOrtho B x x) : x ≠ 0

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 : LinearMap.BilinForm.IsRefl B) {x : M} {y : M} : LinearMap.BilinForm.IsOrtho B x y ↔ LinearMap.BilinForm.IsOrtho B y x

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 : LinearMap.BilinForm.IsAlt B₁) {x : M₁} {y : M₁} : LinearMap.BilinForm.IsOrtho B₁ x y ↔ LinearMap.BilinForm.IsOrtho B₁ y x

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 : LinearMap.BilinForm.IsSymm B) {x : M} {y : M} : LinearMap.BilinForm.IsOrtho B x y ↔ LinearMap.BilinForm.IsOrtho B y x

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

• LinearMap.BilinForm.iIsOrtho B v = Pairwise (LinearMap.BilinForm.IsOrtho B on v)

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} : LinearMap.BilinForm.iIsOrtho B v ↔ ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0

@[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 : M₄} {y : M₄} {a : R₄} (ha : a ≠ 0) : LinearMap.BilinForm.IsOrtho G (a • x) y ↔ LinearMap.BilinForm.IsOrtho G x y

@[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 : M₄} {y : M₄} {a : R₄} (ha : a ≠ 0) : LinearMap.BilinForm.IsOrtho G x (a • y) ↔ LinearMap.BilinForm.IsOrtho G x y

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₁ : LinearMap.BilinForm.iIsOrtho B v) (hv₂ : ∀ (i : n), ¬LinearMap.BilinForm.IsOrtho B (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.

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

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

@[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 ∈ LinearMap.BilinForm.orthogonal B N ↔ ∀ n ∈ N, LinearMap.BilinForm.IsOrtho B n m

@[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} : LinearMap.BilinForm.orthogonal B ⊥ = ⊤

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 : Submodule R M} {L : Submodule R M} (h : N ≤ L) : LinearMap.BilinForm.orthogonal B L ≤ LinearMap.BilinForm.orthogonal B N

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 : LinearMap.BilinForm.IsRefl B) : N ≤ LinearMap.BilinForm.orthogonal B (LinearMap.BilinForm.orthogonal B N)

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 : ¬LinearMap.BilinForm.IsOrtho B x x) : Submodule.span K {x} ⊓ LinearMap.BilinForm.orthogonal B (Submodule.span K {x}) = ⊥

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) : LinearMap.BilinForm.orthogonal B (Submodule.span K {x}) = LinearMap.ker (LinearMap.BilinForm.toLinHomAux₁ B x)

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 : ¬LinearMap.BilinForm.IsOrtho B x x) : Submodule.span K {x} ⊔ LinearMap.BilinForm.orthogonal B (Submodule.span K {x}) = ⊤

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 : ¬LinearMap.BilinForm.IsOrtho B x x) : IsCompl (Submodule.span K {x}) (LinearMap.BilinForm.orthogonal B (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.

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 : LinearMap.BilinForm.IsRefl B) {W : Submodule R₁ M₁} (hW : Disjoint W (LinearMap.BilinForm.orthogonal B W)) : LinearMap.BilinForm.Nondegenerate (LinearMap.BilinForm.restrict B W)

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

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 : LinearMap.BilinForm.iIsOrtho B ⇑v) (hB : LinearMap.BilinForm.Nondegenerate B) (i : n) : ¬LinearMap.BilinForm.IsOrtho B (v i) (v i)

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

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 : LinearMap.BilinForm.iIsOrtho B ⇑v) : LinearMap.BilinForm.Nondegenerate B ↔ ∀ (i : n), ¬LinearMap.BilinForm.IsOrtho B (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.

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 : LinearMap.BilinForm.IsRefl B) : Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict B W)) = W ⊓ LinearMap.BilinForm.orthogonal B ⊤

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) : Submodule.dualCoannihilator (LinearMap.range (LinearMap.domRestrict B W)) = LinearMap.BilinForm.orthogonal B W

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

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} {W : Subspace K V} (b₁ : LinearMap.BilinForm.IsRefl B) : FiniteDimensional.finrank K ↥W + FiniteDimensional.finrank K ↥(LinearMap.BilinForm.orthogonal B W) = FiniteDimensional.finrank K V + FiniteDimensional.finrank K ↥(W ⊓ LinearMap.BilinForm.orthogonal B ⊤)

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 : Subspace K V} (b₁ : LinearMap.BilinForm.IsRefl B) (b₂ : LinearMap.BilinForm.Nondegenerate (LinearMap.BilinForm.restrict B W)) : IsCompl W (LinearMap.BilinForm.orthogonal B 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 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 : Subspace K V} (b₁ : LinearMap.BilinForm.IsRefl B) : LinearMap.BilinForm.Nondegenerate (LinearMap.BilinForm.restrict B W) ↔ IsCompl W (LinearMap.BilinForm.orthogonal B 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.

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 : Subspace K V} (b₁ : LinearMap.BilinForm.IsRefl B) (b₂ : LinearMap.BilinForm.Nondegenerate (LinearMap.BilinForm.restrict B W)) : LinearMap.BilinForm.orthogonal B W = ⊤ ↔ W = ⊥

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 : Subspace K V} (b₁ : LinearMap.BilinForm.IsRefl B) (b₂ : LinearMap.BilinForm.Nondegenerate (LinearMap.BilinForm.restrict B W)) (b₃ : LinearMap.BilinForm.orthogonal B W = ⊥) : W = ⊤

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 : Subspace K V} (b₁ : LinearMap.BilinForm.IsRefl B) (b₂ : LinearMap.BilinForm.Nondegenerate (LinearMap.BilinForm.restrict B W)) (b₃ : LinearMap.BilinForm.Nondegenerate B) : LinearMap.BilinForm.orthogonal B W = ⊥ ↔ W = ⊤

theorem LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict {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₁ : LinearMap.BilinForm.IsRefl B) : W ⊓ LinearMap.BilinForm.orthogonal B W ≤ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.BilinForm.restrict B 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.

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

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