# Adjoint of operators on Hilbert spaces #

Given an operator A : E →L[𝕜] F, where E and F are Hilbert spaces, its adjoint adjoint A : F →L[𝕜] E is the unique operator such that ⟪x, A y⟫ = ⟪adjoint A x, y⟫ for all x and y.

We then use this to put a C⋆-algebra structure on E →L[𝕜] E with the adjoint as the star operation.

This construction is used to define an adjoint for linear maps (i.e. not continuous) between finite dimensional spaces.

## Main definitions #

• ContinuousLinearMap.adjoint : (E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] (F →L[𝕜] E): the adjoint of a continuous linear map, bundled as a conjugate-linear isometric equivalence.
• LinearMap.adjoint : (E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] (F →ₗ[𝕜] E): the adjoint of a linear map between finite-dimensional spaces, this time only as a conjugate-linear equivalence, since there is no norm defined on these maps.

## Implementation notes #

• The continuous conjugate-linear version adjointAux is only an intermediate definition and is not meant to be used outside this file.

## Tags #

noncomputable def ContinuousLinearMap.adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] :
(E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E

The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary definition for the main definition adjoint, where this is bundled as a conjugate-linear isometric equivalence.

Instances For
@[simp]
theorem ContinuousLinearMap.adjointAux_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] (A : E →L[𝕜] F) (x : F) :
↑(ContinuousLinearMap.adjointAux A) x = ↑() (↑(ContinuousLinearMap.toSesqForm A) x)
theorem ContinuousLinearMap.adjointAux_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
inner (↑(ContinuousLinearMap.adjointAux A) y) x = inner y (A x)
theorem ContinuousLinearMap.adjointAux_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
inner x (↑(ContinuousLinearMap.adjointAux A) y) = inner (A x) y
theorem ContinuousLinearMap.adjointAux_adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :
@[simp]
theorem ContinuousLinearMap.adjointAux_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :
def ContinuousLinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] :
(E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] F →L[𝕜] E

The adjoint of a bounded operator from Hilbert space E to Hilbert space F.

Instances For
Instances For
theorem ContinuousLinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
inner (↑(ContinuousLinearMap.adjoint A) y) x = inner y (A x)

The fundamental property of the adjoint.

theorem ContinuousLinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
inner x (↑(ContinuousLinearMap.adjoint A) y) = inner (A x) y

The fundamental property of the adjoint.

@[simp]
theorem ContinuousLinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :

@[simp]
theorem ContinuousLinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] [] [] [] (A : F →L[𝕜] G) (B : E →L[𝕜] F) :

The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →L[𝕜] E) (x : E) :
A x ^ 2 = IsROrC.re (inner (↑(ContinuousLinearMap.adjoint A * A) x) x)
theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →L[𝕜] E) (x : E) :
A x = Real.sqrt (IsROrC.re (inner (↑(ContinuousLinearMap.adjoint A * A) x) x))
theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →L[𝕜] E) (x : E) :
A x ^ 2 = IsROrC.re (inner x (↑(ContinuousLinearMap.adjoint A * A) x))
theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →L[𝕜] E) (x : E) :
A x = Real.sqrt (IsROrC.re (inner x (↑(ContinuousLinearMap.adjoint A * A) x)))
theorem ContinuousLinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (B : F →L[𝕜] E) :
A = ContinuousLinearMap.adjoint B ∀ (x : E) (y : (fun x => F) x), inner (A x) y = inner x (B y)

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

@[simp]
theorem ContinuousLinearMap.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
theorem Submodule.adjoint_subtypeL {𝕜 : Type u_1} {E : Type u_2} [] [] [] (U : ) [CompleteSpace { x // x U }] :
theorem Submodule.adjoint_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [] [] [] (U : ) [CompleteSpace { x // x U }] :

E →L[𝕜] E is a star algebra with the adjoint as the star operation.

theorem ContinuousLinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →L[𝕜] E) :
theorem ContinuousLinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} :

A continuous linear operator is self-adjoint iff it is equal to its adjoint.

theorem ContinuousLinearMap.isAdjointPair_inner {E' : Type u_5} {F' : Type u_6} [] [] [] [] [] [] (A : E' →L[] F') :

theorem IsSelfAdjoint.adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} (hA : ) :
theorem IsSelfAdjoint.isSymmetric {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} (hA : ) :

Every self-adjoint operator on an inner product space is symmetric.

theorem IsSelfAdjoint.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {T : E →L[𝕜] E} (hT : ) (S : E →L[𝕜] F) :

theorem IsSelfAdjoint.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {T : E →L[𝕜] E} (hT : ) (S : F →L[𝕜] E) :

theorem ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} :
theorem LinearMap.IsSymmetric.isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} (hA : ) :
theorem orthogonalProjection_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (U : ) [CompleteSpace { x // x U }] :

theorem IsSelfAdjoint.conj_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →L[𝕜] E} (hT : ) (U : ) [CompleteSpace { x // x U }] :
def LinearMap.IsSymmetric.toSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →ₗ[𝕜] E} (hT : ) :
{ x // x selfAdjoint (E →L[𝕜] E) }

The Hellinger--Toeplitz theorem: Construct a self-adjoint operator from an everywhere defined symmetric operator.

Instances For
theorem LinearMap.IsSymmetric.coe_toSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →ₗ[𝕜] E} (hT : ) :
theorem LinearMap.IsSymmetric.toSelfAdjoint_apply {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →ₗ[𝕜] E} (hT : ) {x : E} :
= T x
def LinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] :
(E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] F →ₗ[𝕜] E

The adjoint of an operator from the finite-dimensional inner product space E to the finite-dimensional inner product space F.

Instances For
theorem LinearMap.adjoint_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) :
theorem LinearMap.adjoint_eq_toClm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) :
theorem LinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) (x : E) (y : F) :
inner (↑(LinearMap.adjoint A) y) x = inner y (A x)

The fundamental property of the adjoint.

theorem LinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) (x : E) (y : F) :
inner x (↑(LinearMap.adjoint A) y) = inner (A x) y

The fundamental property of the adjoint.

@[simp]
theorem LinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) :

@[simp]
theorem LinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] [] [] [] (A : F →ₗ[𝕜] G) (B : E →ₗ[𝕜] F) :

The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

theorem LinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (x : E) (y : (fun x => F) x), inner (A x) y = inner x (B y)

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

theorem LinearMap.eq_adjoint_iff_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {ι₁ : Type u_5} {ι₂ : Type u_6} (b₁ : Basis ι₁ 𝕜 E) (b₂ : Basis ι₂ 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (i₁ : ι₁) (i₂ : ι₂), inner (A (b₁ i₁)) (b₂ i₂) = inner (b₁ i₁) (B (b₂ i₂))

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 LinearMap.eq_adjoint_iff_basis_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {ι : Type u_5} (b : Basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (i : ι) (y : (fun x => F) (b i)), inner (A (b i)) y = inner (b i) (B y)
theorem LinearMap.eq_adjoint_iff_basis_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {ι : Type u_5} (b : Basis ι 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (i : ι) (x : E), inner (A x) (b i) = inner x (B (b i))

E →ₗ[𝕜] E is a star algebra with the adjoint as the star operation.

theorem LinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →ₗ[𝕜] E) :
theorem LinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →ₗ[𝕜] E} :

A continuous linear operator is self-adjoint iff it is equal to its adjoint.

theorem LinearMap.isSymmetric_iff_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →ₗ[𝕜] E) :
theorem LinearMap.isAdjointPair_inner {E' : Type u_5} {F' : Type u_6} [] [] [] [] [] [] (A : E' →ₗ[] F') :
theorem LinearMap.isSymmetric_adjoint_mul_self {𝕜 : Type u_1} {E : Type u_2} [] [] [] (T : E →ₗ[𝕜] E) :

The Gram operator T†T is symmetric.

theorem LinearMap.re_inner_adjoint_mul_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [] [] [] (T : E →ₗ[𝕜] E) (x : E) :
0 IsROrC.re (inner x (↑(LinearMap.adjoint T * T) x))

The Gram operator T†T is a positive operator.

@[simp]
theorem LinearMap.im_inner_adjoint_mul_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [] [] [] (T : E →ₗ[𝕜] E) (x : E) :
IsROrC.im (inner x (↑(LinearMap.adjoint T) (T x))) = 0
theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint {𝕜 : Type u_1} [] {m : Type u_5} {n : Type u_6} [] [] [] [] (A : Matrix m n 𝕜) :
Matrix.toEuclideanLin () = LinearMap.adjoint (Matrix.toEuclideanLin A)

The adjoint of the linear map associated to a matrix is the linear map associated to the conjugate transpose of that matrix.