Gram rigidity

Equal pullback inner products determine a canonical linear isometric equivalence between the ranges of two linear maps. Applied to the finitely supported linear-combination maps of two families, this gives an isometry between their spans sending corresponding vectors to each other. No independence, finiteness of the index type, or completeness is needed.

For families in a common finite-dimensional inner-product space, the span isometry extends to an ambient isometry. Thus equality of Gram matrices characterizes equivalence under an ambient linear isometric equivalence, including dependent families and zero vectors.

The range construction uses Mathlib's LinearMap.quotKerEquivRange; the ambient extension uses LinearIsometry.extend. The mathematical result is the usual Gram characterization of unitary equivalence, as in T.-Y. Chien and S. Waldron, A characterization of projective unitary equivalence of finite frames and applications, SIAM J. Discrete Math. 30 (2016).

theorem TauCeti.ker_eq_of_inner_self_eq {𝕜 : Type u_1} {M : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [AddCommGroup M] [Module 𝕜 M] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {S : M →ₗ[𝕜] E} {T : M →ₗ[𝕜] F} (h : ∀ (x : M), inner 𝕜 (S x) (S x) = inner 𝕜 (T x) (T x)) : S.ker = T.ker

Linear maps with equal self inner products have equal kernels. The common source need only be a module.

noncomputable def TauCeti.rangeEquivOfInnerEq {𝕜 : Type u_1} {M : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [AddCommGroup M] [Module 𝕜 M] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {S : M →ₗ[𝕜] E} {T : M →ₗ[𝕜] F} (h : ∀ (x y : M), inner 𝕜 (S x) (S y) = inner 𝕜 (T x) (T y)) : ↥S.range ≃ₗᵢ[𝕜] ↥T.range

The canonical range isometry induced by equal pullback inner products, sending S x to T x.

@[simp]

theorem TauCeti.rangeEquivOfInnerEq_apply {𝕜 : Type u_1} {M : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [AddCommGroup M] [Module 𝕜 M] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {S : M →ₗ[𝕜] E} {T : M →ₗ[𝕜] F} (h : ∀ (x y : M), inner 𝕜 (S x) (S y) = inner 𝕜 (T x) (T y)) (x : M) : (rangeEquivOfInnerEq h) ⟨S x, ⋯⟩ = ⟨T x, ⋯⟩

The range isometry sends each image under the first map to the corresponding image under the second map.

theorem TauCeti.eq_rangeEquivOfInnerEq {𝕜 : Type u_1} {M : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [AddCommGroup M] [Module 𝕜 M] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {S : M →ₗ[𝕜] E} {T : M →ₗ[𝕜] F} (h : ∀ (x y : M), inner 𝕜 (S x) (S y) = inner 𝕜 (T x) (T y)) {e : ↥S.range ≃ₗᵢ[𝕜] ↥T.range} (he : ∀ (x : M), ↑(e ⟨S x, ⋯⟩) = T x) : e = rangeEquivOfInnerEq h

A range isometry is uniquely determined by its values on the images of the common source.

noncomputable def TauCeti.spanEquivOfInnerEq {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {ι : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {v : ι → E} {w : ι → F} (h : ∀ (i j : ι), inner 𝕜 (v i) (v j) = inner 𝕜 (w i) (w j)) : ↥(Submodule.span 𝕜 (Set.range v)) ≃ₗᵢ[𝕜] ↥(Submodule.span 𝕜 (Set.range w))

Families with equal pairwise inner products have canonically isometric spans. The isometry sends each vector of the first family to its partner in the second.

@[simp]

theorem TauCeti.spanEquivOfInnerEq_apply {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {ι : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {v : ι → E} {w : ι → F} (h : ∀ (i j : ι), inner 𝕜 (v i) (v j) = inner 𝕜 (w i) (w j)) (i : ι) : (spanEquivOfInnerEq h) ⟨v i, ⋯⟩ = ⟨w i, ⋯⟩

The canonical span isometry sends corresponding family vectors to each other.

theorem TauCeti.eq_spanEquivOfInnerEq {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {ι : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {v : ι → E} {w : ι → F} (h : ∀ (i j : ι), inner 𝕜 (v i) (v j) = inner 𝕜 (w i) (w j)) {e : ↥(Submodule.span 𝕜 (Set.range v)) ≃ₗᵢ[𝕜] ↥(Submodule.span 𝕜 (Set.range w))} (he : ∀ (i : ι), ↑(e ⟨v i, ⋯⟩) = w i) : e = spanEquivOfInnerEq h

The canonical span isometry is the unique linear isometric equivalence sending the first family to the second.

theorem TauCeti.exists_linearIsometryEquiv_of_inner_eq {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {v w : ι → E} (h : ∀ (i j : ι), inner 𝕜 (v i) (v j) = inner 𝕜 (w i) (w j)) : ∃ (e : E ≃ₗᵢ[𝕜] E), ∀ (i : ι), e (v i) = w i

Equal Gram data for two families in a finite-dimensional space can be realized by an ambient linear isometric equivalence. The indexing type need not be finite.

theorem TauCeti.gram_eq_iff_exists_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {v w : ι → E} : Matrix.gram 𝕜 v = Matrix.gram 𝕜 w ↔ ∃ (e : E ≃ₗᵢ[𝕜] E), ∀ (i : ι), e (v i) = w i

Equal Gram matrices characterize ambient isometric equivalence of families in a finite-dimensional real or complex inner-product space. The index type may be infinite.