Skip to content

Rank of a bilinear form

4 fully proved

Bilin Form

TheoremThe Gram matrices of a bilinear form in two bases have the same rank#✓fully proved

Let \(V\) be a vector space over a field \(K\), let \(B\) be a bilinear form on \(V\), and let \(b = (b_i)_{i \in n_1}\) and \(c = (c_j)_{j \in n_2}\) be bases of \(V\) indexed by finite types \(n_1\) and \(n_2\). Then the Gram matrices \((B(b_i, b_j))_{i, j \in n_1}\) and \((B(c_i, c_j))_{i, j \in n_2}\) have the same rank.

theorem rank_toMatrix_eq_rank_toMatrix {n₁ n₂ : Type*} [Fintype n₁] [DecidableEq n₁]
    [Fintype n₂] [DecidableEq n₂] (b₁ : Module.Basis n₁ K V) (b₂ : Module.Basis n₂ K V)
    (B : LinearMap.BilinForm K V) : (toMatrix b₁ B).rank = (toMatrix b₂ B).rank
Used by 1
Used byBasis independence of the rank of a bilinear form

Rank of a bilinear form

DefinitionRank of a bilinear form#✓fully proved

Let \(V\) be a vector space over a field \(K\), let \(B\) be a bilinear form on \(V\), and let \(b = (b_i)_{i \in n}\) be a basis of \(V\) indexed by a finite type \(n\). The rank of \(B\) with respect to \(b\) is the rank of the Gram matrix \((B(b_i, b_j))_{i, j \in n}\) of \(B\) in \(b\).

By the basis independence theorem, this number does not depend on the choice of \(b\).

noncomputable def bilinFormRank {n : Type*} [Fintype n] [DecidableEq n]
    (b : Module.Basis n K V) (B : LinearMap.BilinForm K V) : ℕ :=
  (LinearMap.BilinForm.toMatrix b B).rank
Sources
  • N. Bourbaki, Algebra I, Chapters 1-3, Springer (1989), Chapter III.
Used by 2
Used byBasis independence of the rank of a bilinear form · Rank of a bilinear form via its Gram matrix

TheoremRank of a bilinear form via its Gram matrix#✓fully proved

Let \(V\) be a vector space over a field \(K\), let \(B\) be a bilinear form on \(V\), and let \(b = (b_i)_{i \in n}\) be a basis of \(V\) indexed by a finite type \(n\). Then the rank of \(B\) with respect to \(b\) equals the rank of the Gram matrix \((B(b_i, b_j))_{i, j \in n}\). This holds by definition.

theorem bilinFormRank_eq_matrix_rank {n : Type*} [Fintype n] [DecidableEq n]
    (b : Module.Basis n K V) (B : LinearMap.BilinForm K V) :
    bilinFormRank b B = (LinearMap.BilinForm.toMatrix b B).rank
Sources
  • N. Bourbaki, Algebra I, Chapters 1-3, Springer (1989), Chapter III.
Uses 1 · Used by 1
Statement usesRank of a bilinear form
Used byBasis independence of the rank of a bilinear form

TheoremBasis independence of the rank of a bilinear form#✓fully proved

Let \(V\) be a vector space over a field \(K\), let \(B\) be a bilinear form on \(V\), and let \(b = (b_i)_{i \in n_1}\) and \(c = (c_j)_{j \in n_2}\) be bases of \(V\) indexed by finite types \(n_1\) and \(n_2\). Then the rank of \(B\) with respect to \(b\) equals the rank of the Gram matrix \((B(c_i, c_j))_{i, j \in n_2}\) of \(B\) in \(c\).

Proof: The Gram matrix in one basis is the Gram matrix in the other multiplied on both sides by change-of-basis matrices. Since the rank of a product is at most the rank of each factor, each rank is at most the other, hence they are equal.

theorem bilinFormRank_basis_independent {n₁ n₂ : Type*} [Fintype n₁] [DecidableEq n₁]
    [Fintype n₂] [DecidableEq n₂]
    (b₁ : Module.Basis n₁ K V) (b₂ : Module.Basis n₂ K V) (B : LinearMap.BilinForm K V) :
    bilinFormRank b₁ B = (LinearMap.BilinForm.toMatrix b₂ B).rank
Sources
  • N. Bourbaki, Algebra I, Chapters 1-3, Springer (1989), Chapter III.
Uses 3
Statement usesRank of a bilinear form
Proof usesThe Gram matrices of a bilinear form in two bases have the same rank · Rank of a bilinear form via its Gram matrix

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.