Symmetric bilinear forms in real vector spaces

Content created by Egbert Rijke, Fredrik Bakke and Louis Wasserman.

Created on 2025-11-26.
Last modified on 2026-05-02.

module linear-algebra.symmetric-bilinear-forms-real-vector-spaces where
Imports 
open import foundation.dependent-products-propositions
open import foundation.propositions
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

Idea

A bilinear form B on a real vector space V is symmetric if B u v ＝ B v u for all u and v in V.

Definition

Symmetry of a bilinear form

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

  is-symmetric-prop-bilinear-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
  is-symmetric-prop-bilinear-form-ℝ-Vector-Space =
    Π-Prop
      ( type-ℝ-Vector-Space V)
      ( λ x →
        Π-Prop
          ( type-ℝ-Vector-Space V)
          ( λ y →
            Id-Prop
              ( ℝ-Set l1)
              ( map-bilinear-form-ℝ-Vector-Space V B x y)
              ( map-bilinear-form-ℝ-Vector-Space V B y x)))

  is-symmetric-bilinear-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
  is-symmetric-bilinear-form-ℝ-Vector-Space =
    type-Prop is-symmetric-prop-bilinear-form-ℝ-Vector-Space

Recent changes