# Adjoint of operators on Hilbert spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• continuous_linear_map.adjoint : (E βL[π] F) ββα΅’β[π] (F βL[π] E): the adjoint of a continuous linear map, bundled as a conjugate-linear isometric equivalence.
• linear_map.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 adjoint_aux is only an intermediate definition and is not meant to be used outside this file.

## Tags #

noncomputable def continuous_linear_map.adjoint_aux {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F]  :
(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.

Equations
@[simp]
theorem continuous_linear_map.adjoint_aux_apply {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) (x : F) :
theorem continuous_linear_map.adjoint_aux_inner_left {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) (x : E) (y : F) :
= (βA x)
theorem continuous_linear_map.adjoint_aux_inner_right {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) (x : E) (y : F) :
theorem continuous_linear_map.adjoint_aux_adjoint_aux {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) :
@[simp]
theorem continuous_linear_map.adjoint_aux_norm {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) :
noncomputable def continuous_linear_map.adjoint {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F]  :
(E βL[π] F) ββα΅’β[π] F βL[π] E

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

Equations
theorem continuous_linear_map.adjoint_inner_left {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) (x : E) (y : F) :
= (βA x)

The fundamental property of the adjoint.

theorem continuous_linear_map.adjoint_inner_right {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) (x : E) (y : F) :

The fundamental property of the adjoint.

@[simp]
theorem continuous_linear_map.adjoint_adjoint {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) :

@[simp]
theorem continuous_linear_map.adjoint_comp {π : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [is_R_or_C π] [ E] [ F] [ G] (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 continuous_linear_map.apply_norm_sq_eq_inner_adjoint_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (A : E βL[π] E) (x : E) :
theorem continuous_linear_map.apply_norm_eq_sqrt_inner_adjoint_left {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (A : E βL[π] E) (x : E) :
theorem continuous_linear_map.apply_norm_sq_eq_inner_adjoint_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (A : E βL[π] E) (x : E) :
theorem continuous_linear_map.apply_norm_eq_sqrt_inner_adjoint_right {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (A : E βL[π] E) (x : E) :
theorem continuous_linear_map.eq_adjoint_iff {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] (A : E βL[π] F) (B : F βL[π] E) :
β β (x : E) (y : F), has_inner.inner (βA x) y = (β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 continuous_linear_map.adjoint_id {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E]  :
theorem submodule.adjoint_subtypeL {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (U : submodule π E)  :
theorem submodule.adjoint_orthogonal_projection {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (U : submodule π E)  :
@[protected, instance]
noncomputable def continuous_linear_map.has_star {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E]  :
has_star (E βL[π] E)

E βL[π] E is a star algebra with the adjoint as the star operation.

Equations
@[protected, instance]
noncomputable def continuous_linear_map.has_involutive_star {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E]  :
Equations
@[protected, instance]
noncomputable def continuous_linear_map.star_semigroup {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E]  :
Equations
@[protected, instance]
noncomputable def continuous_linear_map.star_ring {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E]  :
star_ring (E βL[π] E)
Equations
@[protected, instance]
def continuous_linear_map.star_module {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E]  :
star_module π (E βL[π] E)
theorem continuous_linear_map.star_eq_adjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (A : E βL[π] E) :
theorem continuous_linear_map.is_self_adjoint_iff' {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {A : E βL[π] E} :

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

@[protected, instance]
def continuous_linear_map.cstar_ring {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E]  :
cstar_ring (E βL[π] E)

theorem is_self_adjoint.adjoint_eq {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {A : E βL[π] E} (hA : is_self_adjoint A) :
theorem is_self_adjoint.is_symmetric {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {A : E βL[π] E} (hA : is_self_adjoint A) :

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

theorem is_self_adjoint.conj_adjoint {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] {T : E βL[π] E} (hT : is_self_adjoint T) (S : E βL[π] F) :

theorem is_self_adjoint.adjoint_conj {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] {T : E βL[π] E} (hT : is_self_adjoint T) (S : F βL[π] E) :

theorem continuous_linear_map.is_self_adjoint_iff_is_symmetric {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {A : E βL[π] E} :
theorem linear_map.is_symmetric.is_self_adjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {A : E βL[π] E} (hA : βA.is_symmetric) :
theorem orthogonal_projection_is_self_adjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] (U : submodule π E)  :

theorem is_self_adjoint.conj_orthogonal_projection {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {T : E βL[π] E} (hT : is_self_adjoint T) (U : submodule π E)  :
def linear_map.is_symmetric.to_self_adjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {T : E ββ[π] E} (hT : T.is_symmetric) :

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

Equations
theorem linear_map.is_symmetric.coe_to_self_adjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {T : E ββ[π] E} (hT : T.is_symmetric) :
theorem linear_map.is_symmetric.to_self_adjoint_apply {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {T : E ββ[π] E} (hT : T.is_symmetric) {x : E} :
noncomputable def linear_map.adjoint {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] :
(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.

Equations
theorem linear_map.adjoint_to_continuous_linear_map {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] (A : E ββ[π] F) :
theorem linear_map.adjoint_eq_to_clm_adjoint {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] (A : E ββ[π] F) :
theorem linear_map.adjoint_inner_left {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] (A : E ββ[π] F) (x : E) (y : F) :
x = (βA x)

The fundamental property of the adjoint.

theorem linear_map.adjoint_inner_right {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] (A : E ββ[π] F) (x : E) (y : F) :

The fundamental property of the adjoint.

@[simp]
theorem linear_map.adjoint_adjoint {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] (A : E ββ[π] F) :

@[simp]
theorem linear_map.adjoint_comp {π : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [is_R_or_C π] [ E] [ F] [ G] [ E] [ F] [ G] (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 linear_map.eq_adjoint_iff {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] (A : E ββ[π] F) (B : F ββ[π] E) :
β β (x : E) (y : F), has_inner.inner (βA x) y = (β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 linear_map.eq_adjoint_iff_basis {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] {ΞΉβ : Type u_4} {ΞΉβ : Type u_5} (bβ : basis ΞΉβ π E) (bβ : basis ΞΉβ π F) (A : E ββ[π] F) (B : F ββ[π] E) :
β β (iβ : ΞΉβ) (iβ : ΞΉβ), has_inner.inner (βA (βbβ iβ)) (βbβ iβ) = has_inner.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 linear_map.eq_adjoint_iff_basis_left {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] {ΞΉ : Type u_4} (b : basis ΞΉ π E) (A : E ββ[π] F) (B : F ββ[π] E) :
β β (i : ΞΉ) (y : F), has_inner.inner (βA (βb i)) y = has_inner.inner (βb i) (βB y)
theorem linear_map.eq_adjoint_iff_basis_right {π : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π] [ E] [ F] [ E] [ F] {ΞΉ : Type u_4} (b : basis ΞΉ π F) (A : E ββ[π] F) (B : F ββ[π] E) :
β β (i : ΞΉ) (x : E), has_inner.inner (βA x) (βb i) = (βB (βb i))
@[protected, instance]
noncomputable def linear_map.has_star {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] :
has_star (E ββ[π] E)

E ββ[π] E is a star algebra with the adjoint as the star operation.

Equations
@[protected, instance]
noncomputable def linear_map.has_involutive_star {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] :
Equations
@[protected, instance]
noncomputable def linear_map.star_semigroup {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] :
Equations
@[protected, instance]
noncomputable def linear_map.star_ring {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] :
Equations
@[protected, instance]
def linear_map.star_module {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] :
star_module π (E ββ[π] E)
theorem linear_map.star_eq_adjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] (A : E ββ[π] E) :
theorem linear_map.is_self_adjoint_iff' {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] {A : E ββ[π] E} :

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

theorem linear_map.is_symmetric_iff_is_self_adjoint {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] (A : E ββ[π] E) :
theorem linear_map.is_adjoint_pair_inner {E' : Type u_5} {F' : Type u_6} (A : E' ββ[β] F') :
theorem linear_map.is_symmetric_adjoint_mul_self {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] (T : E ββ[π] E) :

The Gram operator Tβ T is symmetric.

theorem linear_map.re_inner_adjoint_mul_self_nonneg {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] (T : E ββ[π] E) (x : E) :

The Gram operator Tβ T is a positive operator.

@[simp]
theorem linear_map.im_inner_adjoint_mul_self_eq_zero {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] [ E] (T : E ββ[π] E) (x : E) :
theorem matrix.to_euclidean_lin_conj_transpose_eq_adjoint {π : Type u_1} [is_R_or_C π] {m : Type u_5} {n : Type u_6} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] (A : n π) :

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