Forms definite off the origin separate vectors

A semilinear map of two arguments B that is definite off the origin, B x x ≠ 0 for x ≠ 0, separates vectors: two vectors pairing identically against every vector are equal, because their difference pairs to zero with itself. On a finite-dimensional space, a separating form represents every pairing by a linear map.

Main results

• LinearMap.eq_of_forall_sesq_eq: a form definite off the origin separates vectors.
• LinearMap.exists_linearMap_forall_apply_eq_apply: every pairing factors through a separating form on a finite-dimensional space.

theorem LinearMap.eq_of_forall_sesq_eq {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [Semiring R] [CommSemiring S] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module S P] {I₁ I₂ : R →+* S} {B : M →ₛₗ[I₁] M →ₛₗ[I₂] P} (hdef : ∀ (x : M), x ≠ 0 → (B x) x ≠ 0) {u v : M} (h : ∀ (y : M), (B u) y = (B v) y) : u = v

A form definite off the origin separates vectors: two vectors pairing identically against every vector are equal, because their difference pairs to zero with itself. Mathlib's LinearMap.SeparatingLeft is the same separation stated as a property of the form; definiteness off the origin is what supplies it here, and is the shape the callers carry it in.

theorem LinearMap.exists_linearMap_forall_apply_eq_apply {K : Type u_5} {V : Type u_6} {W : Type u_7} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K V] {I : K →+* K} {B : V →ₛₗ[I] V →ₗ[K] K} (hB : B.SeparatingRight) (S : V →ₛₗ[I] W →ₗ[K] K) : ∃ (T : W →ₗ[K] V), ∀ (x : V) (y : W), (S x) y = (B x) (T y)

Representing a pairing through a separating form. Let B be a form on a finite-dimensional space V, semilinear in the first variable and separating in the second, for instance a nondegenerate sesquilinear form. Every pairing S of V with W of the same type has the form S x y = B x (T y) for a linear map T : W → V.