Documentation

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

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:

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

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} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {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} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (x : M) :
    B.IsOrtho 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) :
    B.IsOrtho 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₁ : ¬B.IsOrtho 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 : 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₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (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} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (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} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : Type w} (B : LinearMap.BilinForm R M) (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
    Instances For
      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 : 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₄] [AddCommGroup M₄] [Module R₄ M₄] {G : LinearMap.BilinForm R₄ M₄} {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₄] [AddCommGroup M₄] [Module R₄ M₄] {G : LinearMap.BilinForm R₄ M₄} {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} [Field K] [AddCommGroup V] [Module K V] {n : Type w} {B : LinearMap.BilinForm K V} {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} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (N : 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 | 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} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {N : Submodule R M} {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} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :
        B.orthogonal =
        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) :
        B.orthogonal L B.orthogonal 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 : B.IsRefl) :
        N B.orthogonal (B.orthogonal N)
        theorem LinearMap.BilinForm.orthogonal_top {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 =
        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}) =
        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)
        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}) =
        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.

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

        @[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).

        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.

        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.

        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 : xp, yq, (B x) y = 0) :
        LinearMap.ker (B.restrict p) = Submodule.comap p.subtype (LinearMap.ker B)
        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) :
        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
        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)
        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.

        @[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.

        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.

        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 =
        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 =
        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 =
        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 : Submodule K V} (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} [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.

        @[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.