feat(analysis/inner_product_space/dual,adjoint): add some lemmas abou…

…t extensionality with respect to a basis (#11176)

This PR adds some lemmas about extensionality in inner product spaces with respect to a basis.

src/analysis/inner_product_space/adjoint.lean

@@ -246,6 +246,32 @@ begin
   exact ext_inner_right 𝕜 (λ y, by simp only [adjoint_inner_left, h x y])
 end
 
+/-- The adjoint is unique: a map `A` is the adjoint of `B` iff it satisfies `⟪A x, y⟫ = ⟪x, B y⟫`
+for all basis vectors `x` and `y`. -/
+lemma eq_adjoint_iff_basis {ι₁ : Type*} {ι₂ : Type*} (b₁ : basis ι₁ 𝕜 E) (b₂ : basis ι₂ 𝕜 F)
+  (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
+  A = B.adjoint ↔ (∀ (i₁ : ι₁) (i₂ : ι₂), ⟪A (b₁ i₁), b₂ i₂⟫ = ⟪b₁ i₁, B (b₂ i₂)⟫) :=
+begin
+  refine ⟨λ h x y, by rw [h, adjoint_inner_left], λ h, _⟩,
+  refine basis.ext b₁ (λ i₁, _),
+  exact ext_inner_right_basis b₂ (λ i₂, by simp only [adjoint_inner_left, h i₁ i₂]),
+end
+
+lemma eq_adjoint_iff_basis_left {ι : Type*} (b : basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
+  A = B.adjoint ↔ (∀ i y, ⟪A (b i), y⟫ = ⟪b i, B y⟫) :=
+begin
+  refine ⟨λ h x y, by rw [h, adjoint_inner_left], λ h, basis.ext b (λ i, _)⟩,
+  exact ext_inner_right 𝕜 (λ y, by simp only [h i, adjoint_inner_left]),
+end
+
+lemma eq_adjoint_iff_basis_right {ι : Type*} (b : basis ι 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
+  A = B.adjoint ↔ (∀ i x, ⟪A x, b i⟫ = ⟪x, B (b i)⟫) :=
+begin
+  refine ⟨λ h x y, by rw [h, adjoint_inner_left], λ h, _⟩,
+  ext x,
+  refine ext_inner_right_basis b (λ i, by simp only [h i, adjoint_inner_left]),
+end
+
 /-- `E →ₗ[𝕜] E` is a star algebra with the adjoint as the star operation. -/
 instance : has_star (E →ₗ[𝕜] E) := ⟨adjoint⟩
 instance : has_involutive_star (E →ₗ[𝕜] E) := ⟨adjoint_adjoint⟩

src/analysis/inner_product_space/dual.lean

@@ -143,4 +143,25 @@ end
 omit 𝕜
 variable {𝕜}
 
+lemma ext_inner_left_basis {ι : Type*} {x y : E} (b : basis ι 𝕜 E)
+  (h : ∀ i : ι, ⟪b i, x⟫ = ⟪b i, y⟫) : x = y :=
+begin
+  apply (to_dual 𝕜 E).map_eq_iff.mp,
+  refine (function.injective.eq_iff continuous_linear_map.coe_injective).mp (basis.ext b _),
+  intro i,
+  simp only [to_dual_apply, continuous_linear_map.coe_coe],
+  rw [←inner_conj_sym],
+  nth_rewrite_rhs 0 [←inner_conj_sym],
+  exact congr_arg conj (h i)
+end
+
+lemma ext_inner_right_basis {ι : Type*} {x y : E} (b : basis ι 𝕜 E)
+  (h : ∀ i : ι, ⟪x, b i⟫ = ⟪y, b i⟫) : x = y :=
+begin
+  refine ext_inner_left_basis b (λ i, _),
+  rw [←inner_conj_sym],
+  nth_rewrite_rhs 0 [←inner_conj_sym],
+  exact congr_arg conj (h i)
+end
+
 end inner_product_space