Nondegeneracy of the real inner product

The real inner product innerₗ E is a nondegenerate bilinear form on E (TauCeti.nondegenerate_inner): a vector orthogonal to every vector is orthogonal to itself, hence zero. This is the hypothesis under which Mathlib's bilinear-form constructions, such as the dual basis LinearMap.BilinForm.dualBasis, apply to the inner product. In finite dimension it is moreover a perfect pairing (TauCeti.bijective_innerₗ), as Mathlib's exteriorPower.hodgeStar requires of its bilinear form. Its pullback along an injective linear map, such as the metric induced by an immersion, is again nondegenerate (TauCeti.nondegenerate_inner_comp), so a vector is determined by its pairings with it (TauCeti.eq_of_forall_inner_comp).

The dual basis of a basis b for the inner product pairs with a vector to give its coordinates in b (Module.Basis.inner_dualBasis_left), and it is obtained from b by the inverse of the Gram matrix (Module.Basis.dualBasis_innerₗ_eq_sum). In a coordinate frame of a Riemannian metric, these are the coordinate covectors dxⁱ with their musical isomorphism gⁱʲ ∂ⱼ.

theorem TauCeti.nondegenerate_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : (innerₗ E).Nondegenerate

The real inner product is a nondegenerate bilinear form.

theorem TauCeti.bijective_innerₗ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : Function.Bijective ⇑(innerₗ E)

In finite dimension the real inner product is a perfect pairing: v ↦ ⟪v, ·⟫ is a bijection onto the dual.

theorem TauCeti.nondegenerate_inner_comp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {V : Type u_2} [AddCommGroup V] [Module ℝ V] {L : V →ₗ[ℝ] E} (hL : Function.Injective ⇑L) : (LinearMap.BilinForm.comp (innerₗ E) L L).Nondegenerate

The real inner product pulled back along an injective linear map is nondegenerate: a vector v with ⟪L v, L w⟫ = 0 for every w has ⟪L v, L v⟫ = 0, so L v = 0.

theorem TauCeti.eq_of_forall_inner_comp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {V : Type u_2} [AddCommGroup V] [Module ℝ V] {L : V →ₗ[ℝ] E} (hL : Function.Injective ⇑L) {u u' : V} (H : ∀ (w : V), inner ℝ (L u) (L w) = inner ℝ (L u') (L w)) : u = u'

For an injective linear map L, a vector u is determined by the pairings ⟪L u, L w⟫ of the pulled-back inner product.

theorem Module.Basis.inner_dualBasis_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] [Finite ι] (b : Basis ι ℝ E) (i : ι) (v : E) : inner ℝ ((LinearMap.BilinForm.dualBasis (innerₗ E) ⋯ b) i) v = (b.repr v) i

The inner product with the i-th vector of the dual basis of b is the i-th coordinate in b.

theorem Module.Basis.dualBasis_innerₗ_eq_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ E) (i : ι) : (LinearMap.BilinForm.dualBasis (innerₗ E) ⋯ b) i = ∑ j : ι, (Matrix.gram ℝ ⇑b)⁻¹ i j • b j

The dual basis through the inverse Gram matrix: the i-th vector of the dual basis of b is ∑ⱼ (G⁻¹)ᵢⱼ bⱼ, where G = (⟪bᵢ, bⱼ⟫) is the Gram matrix of b.