English
For bases b1 of E and b2 of F, A equals the adjoint of B if and only if ⟪A(b1_i), b2_j⟫ = ⟪b1_i, B(b2_j)⟫ for all indices i, j.
Русский
Для базисов b1 в E и b2 в F, A равно сопряжению B тогда и только тогда, когда ⟪A(b1_i), b2_j⟫ = ⟪b1_i, B(b2_j)⟫ для всех индексов i, j.
LaTeX
$$$$A = B^{*} \iff \forall i,j,\langle A(b_{1,i}), b_{2,j} \rangle = \langle b_{1,i}, B(b_{2,j}) \rangle.$$$$
Lean4
/-- 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`. -/
theorem 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₂)⟫ :=
by
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
refine Basis.ext b₁ fun i₁ => ?_
exact ext_inner_right_basis b₂ fun i₂ => by simp only [adjoint_inner_left, h i₁ i₂]
