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 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,

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

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

theorem BilinForm.isOrtho_def {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {x : M} {y : M} : BilinForm.IsOrtho B x y ↔ B.bilin x y = 0

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

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

theorem BilinForm.ne_zero_of_not_isOrtho_self {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {B : BilinForm K V} (x : V) (hx₁ : ¬BilinForm.IsOrtho B x x) : x ≠ 0

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

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

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

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

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

theorem BilinForm.iIsOrtho_def {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : Type w} {B : BilinForm R M} {v : n → M} : BilinForm.iIsOrtho B v ↔ ∀ (i j : n), i ≠ j → B.bilin (v i) (v j) = 0

@[simp]

theorem BilinForm.isOrtho_smul_left {R₄ : Type u_13} {M₄ : Type u_14} [Ring R₄] [IsDomain R₄] [AddCommGroup M₄] [Module R₄ M₄] {G : BilinForm R₄ M₄} {x : M₄} {y : M₄} {a : R₄} (ha : a ≠ 0) : BilinForm.IsOrtho G (a • x) y ↔ BilinForm.IsOrtho G x y

@[simp]

theorem BilinForm.isOrtho_smul_right {R₄ : Type u_13} {M₄ : Type u_14} [Ring R₄] [IsDomain R₄] [AddCommGroup M₄] [Module R₄ M₄] {G : BilinForm R₄ M₄} {x : M₄} {y : M₄} {a : R₄} (ha : a ≠ 0) : BilinForm.IsOrtho G x (a • y) ↔ BilinForm.IsOrtho G x y

theorem BilinForm.linearIndependent_of_iIsOrtho {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {n : Type w} {B : BilinForm K V} {v : n → V} (hv₁ : BilinForm.iIsOrtho B v) (hv₂ : ∀ (i : n), ¬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 BilinForm.orthogonal {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (B : 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 BilinForm.mem_orthogonal_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {N : Submodule R M} {m : M} : m ∈ BilinForm.orthogonal B N ↔ ∀ n ∈ N, BilinForm.IsOrtho B n m

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

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

theorem BilinForm.span_singleton_inf_orthogonal_eq_bot {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {B : BilinForm K V} {x : V} (hx : ¬BilinForm.IsOrtho B x x) : Submodule.span K {x} ⊓ BilinForm.orthogonal B (Submodule.span K {x}) = ⊥

theorem BilinForm.orthogonal_span_singleton_eq_toLin_ker {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {B : BilinForm K V} (x : V) : BilinForm.orthogonal B (Submodule.span K {x}) = LinearMap.ker ((BilinForm.toLin B) x)

theorem BilinForm.span_singleton_sup_orthogonal_eq_top {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {B : BilinForm K V} {x : V} (hx : ¬BilinForm.IsOrtho B x x) : Submodule.span K {x} ⊔ BilinForm.orthogonal B (Submodule.span K {x}) = ⊤

theorem BilinForm.isCompl_span_singleton_orthogonal {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {B : BilinForm K V} {x : V} (hx : ¬BilinForm.IsOrtho B x x) : IsCompl (Submodule.span K {x}) (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 BilinForm.nondegenerateRestrictOfDisjointOrthogonal {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : BilinForm R₁ M₁) (b : BilinForm.IsRefl B) {W : Submodule R₁ M₁} (hW : Disjoint W (BilinForm.orthogonal B W)) : BilinForm.Nondegenerate (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 BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : Type w} [Nontrivial R] {B : BilinForm R M} {v : Basis n R M} (h : BilinForm.iIsOrtho B ⇑v) (hB : BilinForm.Nondegenerate B) (i : n) : ¬BilinForm.IsOrtho B (v i) (v i)

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

theorem BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : Type w} [Nontrivial R] [NoZeroDivisors R] (B : BilinForm R M) (v : Basis n R M) (hO : BilinForm.iIsOrtho B ⇑v) : BilinForm.Nondegenerate B ↔ ∀ (i : n), ¬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 BilinForm.toLin_restrict_ker_eq_inf_orthogonal {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] (B : BilinForm K V) (W : Subspace K V) (b : BilinForm.IsRefl B) : Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (BilinForm.toLin B) W)) = W ⊓ BilinForm.orthogonal B ⊤

theorem BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] (B : BilinForm K V) (W : Subspace K V) : Submodule.dualCoannihilator (LinearMap.range (LinearMap.domRestrict (BilinForm.toLin B) W)) = BilinForm.orthogonal B W

theorem BilinForm.finrank_add_finrank_orthogonal {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : BilinForm K V} {W : Subspace K V} (b₁ : BilinForm.IsRefl B) : FiniteDimensional.finrank K ↥W + FiniteDimensional.finrank K ↥(BilinForm.orthogonal B W) = FiniteDimensional.finrank K V + FiniteDimensional.finrank K ↥(W ⊓ BilinForm.orthogonal B ⊤)

theorem BilinForm.restrict_nondegenerate_of_isCompl_orthogonal {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : BilinForm K V} {W : Subspace K V} (b₁ : BilinForm.IsRefl B) (b₂ : BilinForm.Nondegenerate (BilinForm.restrict B W)) : IsCompl W (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 BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : BilinForm K V} {W : Subspace K V} (b₁ : BilinForm.IsRefl B) : BilinForm.Nondegenerate (BilinForm.restrict B W) ↔ IsCompl W (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.

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 BilinForm.restrictOrthogonalSpanSingletonNondegenerate {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] (B : BilinForm K V) (b₁ : BilinForm.Nondegenerate B) (b₂ : BilinForm.IsRefl B) {x : V} (hx : ¬BilinForm.IsOrtho B x x) : BilinForm.Nondegenerate (BilinForm.restrict B (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.