Orthogonality relative to a bilinear form in a real vector space

Content created by Louis Wasserman.

Created on 2025-11-26.
Last modified on 2025-11-26.

module linear-algebra.orthogonality-bilinear-forms-real-vector-spaces where
Imports 
open import foundation.binary-relations
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import linear-algebra.bilinear-forms-real-vector-spaces
open import linear-algebra.real-vector-spaces

open import real-numbers.dedekind-real-numbers
open import real-numbers.rational-real-numbers

Idea

Two elements u and v of a real vector space V are orthogonal relative to a bilinear form B : V → V → ℝ if B u v = 0.

Definition

module _
  {l1 l2 : Level}
  (V : ℝ-Vector-Space l1 l2)
  (B : bilinear-form-ℝ-Vector-Space V)
  where

  is-orthogonal-prop-bilinear-form-ℝ-Vector-Space :
    Relation-Prop (lsuc l1) (type-ℝ-Vector-Space V)
  is-orthogonal-prop-bilinear-form-ℝ-Vector-Space v w =
    Id-Prop
      ( ℝ-Set l1)
      ( map-bilinear-form-ℝ-Vector-Space V B v w)
      ( raise-zero-ℝ l1)

  is-orthogonal-bilinear-form-ℝ-Vector-Space :
    Relation (lsuc l1) (type-ℝ-Vector-Space V)
  is-orthogonal-bilinear-form-ℝ-Vector-Space =
    type-Relation-Prop is-orthogonal-prop-bilinear-form-ℝ-Vector-Space

Recent changes