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.

Tags #

Bilinear form,

def LinearMap.BilinForm.IsOrtho {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (x : M) (y : M) :

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
theorem LinearMap.BilinForm.isOrtho_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {x : M} {y : M} :
B.IsOrtho x y (B x) y = 0
theorem LinearMap.BilinForm.isOrtho_zero_left {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) :
B.IsOrtho 0 x
theorem LinearMap.BilinForm.isOrtho_zero_right {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (x : M) :
B.IsOrtho x 0
theorem LinearMap.BilinForm.ne_zero_of_not_isOrtho_self {V : Type u_5} {K : Type u_6} [] [] [Module K V] {B : } (x : V) (hx₁ : ¬B.IsOrtho x x) :
x 0
theorem LinearMap.BilinForm.IsRefl.ortho_comm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : B.IsRefl) {x : M} {y : M} :
B.IsOrtho x y B.IsOrtho y x
theorem LinearMap.BilinForm.IsAlt.ortho_comm {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [] [Module R₁ M₁] {B₁ : } (H : B₁.IsAlt) {x : M₁} {y : M₁} :
B₁.IsOrtho x y B₁.IsOrtho y x
theorem LinearMap.BilinForm.IsSymm.ortho_comm {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (H : B.IsSymm) {x : M} {y : M} :
B.IsOrtho x y B.IsOrtho y x
def LinearMap.BilinForm.iIsOrtho {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} (B : ) (v : nM) :

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 =
Instances For
theorem LinearMap.BilinForm.iIsOrtho_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} {B : } {v : nM} :
B.iIsOrtho 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₄] [] [Module R₄ M₄] {G : } {x : M₄} {y : M₄} {a : R₄} (ha : a 0) :
G.IsOrtho (a x) y G.IsOrtho x y
@[simp]
theorem LinearMap.BilinForm.isOrtho_smul_right {R₄ : Type u_7} {M₄ : Type u_8} [CommRing R₄] [IsDomain R₄] [] [Module R₄ M₄] {G : } {x : M₄} {y : M₄} {a : R₄} (ha : a 0) :
G.IsOrtho x (a y) G.IsOrtho x y
theorem LinearMap.BilinForm.linearIndependent_of_iIsOrtho {V : Type u_5} {K : Type u_6} [] [] [Module K V] {n : Type w} {B : } {v : nV} (hv₁ : B.iIsOrtho v) (hv₂ : ∀ (i : n), ¬B.IsOrtho (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.

def LinearMap.BilinForm.orthogonal {R : Type u_1} {M : Type u_2} [] [] [Module R M] (B : ) (N : ) :

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 | nN, B.IsOrtho n m}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem LinearMap.BilinForm.mem_orthogonal_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {N : } {m : M} :
m B.orthogonal N nN, B.IsOrtho n m
@[simp]
theorem LinearMap.BilinForm.orthogonal_bot {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } :
B.orthogonal =
theorem LinearMap.BilinForm.orthogonal_le {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {N : } {L : } (h : N L) :
B.orthogonal L B.orthogonal N
theorem LinearMap.BilinForm.le_orthogonal_orthogonal {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } {N : } (b : B.IsRefl) :
N B.orthogonal (B.orthogonal N)
theorem LinearMap.BilinForm.orthogonal_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] {B : } (hB : B.Nondegenerate) (hB₀ : B.IsRefl) :
B.orthogonal =
theorem LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot {V : Type u_5} {K : Type u_6} [] [] [Module K V] {B : } {x : V} (hx : ¬B.IsOrtho x x) :
Submodule.span K {x} B.orthogonal (Submodule.span K {x}) =
theorem LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker {V : Type u_5} {K : Type u_6} [] [] [Module K V] {B : } (x : V) :
B.orthogonal (Submodule.span K {x}) = LinearMap.ker (B.toLinHomAux₁ x)
theorem LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top {V : Type u_5} {K : Type u_6} [] [] [Module K V] {B : } {x : V} (hx : ¬B.IsOrtho x x) :
Submodule.span K {x} B.orthogonal (Submodule.span K {x}) =
theorem LinearMap.BilinForm.isCompl_span_singleton_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] {B : } {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.

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

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

theorem LinearMap.BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} [] {B : } {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.

theorem LinearMap.BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : Type w} [] [] (B : ) (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.

theorem LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] (B : ) (W : Subspace K V) (b : B.IsRefl) :
= W B.orthogonal
theorem LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] (B : ) (W : Subspace K V) :
.dualCoannihilator = B.orthogonal W
theorem LinearMap.BilinForm.ker_restrict_eq_of_codisjoint {R : Type u_1} {M : Type u_2} [] [] [Module R M] {p : } {q : } (hpq : ) {B : } (hB : xp, yq, (B x) y = 0) :
LinearMap.ker (B.restrict p) = Submodule.comap p.subtype
theorem LinearMap.BilinForm.finrank_add_finrank_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } (b₁ : B.IsRefl) (W : ) :
+ FiniteDimensional.finrank K (B.orthogonal W) = + FiniteDimensional.finrank K (W B.orthogonal )
theorem LinearMap.BilinForm.finrank_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : ) :
FiniteDimensional.finrank K (B.orthogonal W) =
theorem LinearMap.BilinForm.orthogonal_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : ) :
B.orthogonal (B.orthogonal W) = W
theorem LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } {W : } (hB₀ : B.IsRefl) :
IsCompl W (B.orthogonal W) Disjoint W (B.orthogonal W)
theorem LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } {W : } (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.

@[deprecated LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate]
theorem LinearMap.BilinForm.restrict_nondegenerate_of_isCompl_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } {W : } (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.

theorem LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } {W : } (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.

theorem LinearMap.BilinForm.orthogonal_eq_top_iff {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } {W : } (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) :
B.orthogonal W = W =
theorem LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } {W : } (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.orthogonal W = ) :
W =
theorem LinearMap.BilinForm.orthogonal_eq_bot_iff {V : Type u_5} {K : Type u_6} [] [] [Module K V] [] {B : } {W : } (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.Nondegenerate) :
B.orthogonal W = W =
theorem LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict {V : Type u_5} {K : Type u_6} [] [] [Module K V] {B : } {W : } (b₁ : B.IsRefl) :
W B.orthogonal W Submodule.map W.subtype (LinearMap.ker (B.restrict 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.restrict_nondegenerate_orthogonal_spanSingleton {V : Type u_5} {K : Type u_6} [] [] [Module K V] (B : ) (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.

@[deprecated LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton]
theorem LinearMap.BilinForm.restrictNondegenerateOrthogonalSpanSingleton {V : Type u_5} {K : Type u_6} [] [] [Module K V] (B : ) (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.