Adjoints of linear maps #

An endomorphism and its adjoint have the same real quadratic form (ContinuousLinearMap.re_inner_star_apply_self). For bounded operators between complete inner product spaces, the adjoint takes values in the orthogonal complement of the kernel (ContinuousLinearMap.adjoint_apply_mem_orthogonal_ker). An operator on a Hilbert space is invertible exactly when its adjoint is (ContinuousLinearMap.isUnit_adjoint_iff), and inversion commutes with the adjoint (ContinuousLinearMap.ringInverse_adjoint). An operator on a Hilbert space that is bounded below by M⁻¹ and has injective adjoint is invertible with ‖T⁻¹‖ ≤ M (ContinuousLinearMap.isUnit_and_norm_ringInverse_le_of_forall_norm_le). If an invertible operator satisfies ‖x‖ ≤ M ‖T x‖, every vector is T† z with ‖z‖ ≤ M ‖y‖ (ContinuousLinearMap.exists_adjoint_apply_eq_and_norm_le). For a continuous linear equivalence between complete inner product spaces, the adjoint is bijective (ContinuousLinearEquiv.adjoint_bijective). Its adjoint gives an equivalence in the reverse direction (ContinuousLinearEquiv.adjointEquiv), with the adjoint of the inverse as inverse. For a finite-dimensional linear isometry, the adjoint returns its image vectors to their preimages (LinearIsometry.adjoint_apply_apply).

An isometric inclusion also identifies the operator algebra of its source isometrically with an orthogonal corner in the target's operator algebra: extend by zero using e T e†. Compression is its inverse on this corner, and extension preserves composition and adjoints.

Main definitions #

ContinuousLinearMap.compression A X: the compression X† A X of A along X.
LinearIsometry.cornerEmbedding: extension by zero T ↦ e T e†, an isometric embedding of operator spaces along an isometric inclusion.
ContinuousLinearEquiv.adjointEquiv: the adjoint as a continuous linear equivalence.
ContinuousLinearMap.adjointRealCLM: the adjoint T ↦ T† of operators between complex Hilbert spaces as a real-linear continuous map.

Further results #

Two families of adjoints of linear maps between finite-dimensional inner product spaces:

the adjoint of an isometric isomorphism e : E ≃ₗᵢ[𝕜] F, viewed as a linear map, is its inverse (LinearIsometryEquiv.adjoint_coe_eq_symm). This is Mathlib's LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, stated for the coercion (e : E →ₗ[𝕜] F) in which compositions with isometric isomorphisms are usually written;
on the L² product WithLp 2 (E × F), the coordinate projections WithLp.fstₗ and WithLp.sndₗ are adjoint to the inclusions x ↦ (x, 0) and y ↦ (0, y) of the two factors.

Finally, a pointwise bound ‖C x‖ ≤ c * ‖x‖ passes to the adjoint (LinearMap.norm_adjoint_apply_le). This is the operator-norm bound ‖C†‖ ≤ ‖C‖ in pointwise form for algebraic linear maps, deduced from Mathlib's isometry ContinuousLinearMap.adjoint. Similarly, if ‖e⁻¹ x‖ ≤ ‖x‖ / √λ, then ‖M‖ ≤ λ⁻¹ ‖e† ∘ M ∘ e‖ (ContinuousLinearEquiv.norm_le_inv_mul_norm_adjoint_comp_comp). If a linear map vanishes on Tᗮ, its adjoint takes values in T (LinearMap.adjoint_apply_mem_of_forall_mem_orthogonal). The determinant of the adjoint of an endomorphism is the conjugate of its determinant (LinearMap.det_adjoint). For a surjective linear map, the orthogonal complement of its kernel has the dimension of the codomain (LinearMap.finrank_orthogonal_ker_of_surjective).

Passing a finite-dimensional operator to continuous linear maps preserves its adjoint (LinearMap.toContinuousLinearMap_star) and its normality (the instance LinearMap.isStarNormal_toContinuousLinearMap).

Adjoints of linear maps #

Main definitions #

Further results #

Operator corners #