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 #
adjoint
Adjoint operator #
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
- One or more equations did not get rendered due to their size.
Instances For
The adjoint of a bounded operator from Hilbert space E
to Hilbert space F
.
Equations
- ContinuousLinearMap.adjoint = LinearIsometryEquiv.ofSurjective (let __src := ContinuousLinearMap.adjointAux; { toLinearMap := ↑__src, norm_map' := ⋯ }) ⋯
Instances For
Equations
- InnerProduct.«term_†» = Lean.ParserDescr.trailingNode `InnerProduct.term_† 1000 1000 (Lean.ParserDescr.symbol "†")
Instances For
The fundamental property of the adjoint.
The fundamental property of the adjoint.
The adjoint is involutive.
The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.
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
.
E →L[𝕜] E
is a star algebra with the adjoint as the star operation.
Equations
- ContinuousLinearMap.instStarId = { star := ⇑ContinuousLinearMap.adjoint }
Equations
- ContinuousLinearMap.instInvolutiveStarId = InvolutiveStar.mk ⋯
Equations
- ContinuousLinearMap.instStarMulId = StarMul.mk ⋯
Equations
- ContinuousLinearMap.instStarRingId = StarRing.mk ⋯
Equations
- ⋯ = ⋯
A continuous linear operator is self-adjoint iff it is equal to its adjoint.
Equations
- ⋯ = ⋯
Self-adjoint operators #
Every self-adjoint operator on an inner product space is symmetric.
Conjugating preserves self-adjointness.
Conjugating preserves self-adjointness.
The orthogonal projection is self-adjoint.
The Hellinger--Toeplitz theorem: Construct a self-adjoint operator from an everywhere defined symmetric operator.
Equations
- hT.toSelfAdjoint = ⟨{ toLinearMap := T, cont := ⋯ }, ⋯⟩
Instances For
The adjoint of an operator from the finite-dimensional inner product space E
to the
finite-dimensional inner product space F
.
Equations
- LinearMap.adjoint = (LinearMap.toContinuousLinearMap.trans ContinuousLinearMap.adjoint.toLinearEquiv).trans LinearMap.toContinuousLinearMap.symm
Instances For
The fundamental property of the adjoint.
The fundamental property of the adjoint.
The adjoint is involutive.
The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.
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
.
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
.
E →ₗ[𝕜] E
is a star algebra with the adjoint as the star operation.
Equations
- LinearMap.instStarId = { star := ⇑LinearMap.adjoint }
Equations
- LinearMap.instInvolutiveStarId = InvolutiveStar.mk ⋯
Equations
- LinearMap.instStarMulId = StarMul.mk ⋯
Equations
- LinearMap.instStarRingId = StarRing.mk ⋯
Equations
- ⋯ = ⋯
A continuous linear operator is self-adjoint iff it is equal to its adjoint.
The Gram operator T†T is symmetric.
The Gram operator T†T is a positive operator.
The unitary elements of continuous linear maps on a Hilbert space coincide with the linear isometric equivalences on that Hilbert space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The linear map associated to the conjugate transpose of a matrix corresponding to two orthonormal bases is the adjoint of the linear map associated to the matrix.
The matrix associated to the adjoint of a linear map corresponding to two orthonormal bases is the conjugate transpose of the matrix associated to the linear map.
The star algebra equivalence between the linear endomorphisms of finite-dimensional inner product space and square matrices induced by the choice of an orthonormal basis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The adjoint of the linear map associated to a matrix is the linear map associated to the conjugate transpose of that matrix.