Physlib

Physlib.Mathematics.InnerProductSpace.Adjoint

Adjoint of a linear map

This module defines the adjoint of a linear map `f : E → F` where `E` and `F` carry the instances of `InnerProductSpace'` over a field `𝕜`.

This is a generalization of the usual adjoint defined on `InnerProductSpace` for continuous linear maps.

18 declarations

definition

Adjoint of a map f:EFf: E \to F

For a map f:EFf : E \to F between two inner product spaces EE and FF over a field k\mathbb{k}, the adjoint f:FEf^\dagger : F \to E is defined as the unique map satisfying the property f(x),y=x,f(y)\langle f(x), y \rangle = \langle x, f^\dagger(y) \rangle for all xEx \in E and yFy \in F. If such a map exists (i.e., if ff has an adjoint), the definition returns that map; otherwise, it returns the zero map.

theorem

x,f(y)=f(x),y\langle x, f'(y) \rangle = \langle f(x), y \rangle for the adjoint ff'

Let EE and FF be generalized inner product spaces over a field k\mathbb{k}. If f:EFf: E \to F is a map and f:FEf': F \to E is its adjoint (meaning they satisfy the `HasAdjoint` property), then for any xEx \in E and yFy \in F, the inner product satisfies x,f(y)=f(x),y\langle x, f'(y) \rangle = \langle f(x), y \rangle.

theorem

Existence of an Adjoint for Continuous Linear Maps between Complete Generalized Inner Product Spaces

Let EE and FF be generalized inner product spaces over a field k\mathbb{k} (where k\mathbb{k} is R\mathbb{R} or C\mathbb{C}). Suppose EE and FF are complete with respect to their respective norms. For any continuous linear map f:EFf : E \to F, there exists an adjoint map f:FEf^\dagger : F \to E such that f(x),y=x,f(y)\langle f(x), y \rangle = \langle x, f^\dagger(y) \rangle for all xEx \in E and yFy \in F. Specifically, this adjoint is given by the composition: f=fromL2(toL2ffromL2)toL2f^\dagger = \text{fromL2} \circ (\text{toL2} \circ f \circ \text{fromL2})^\dagger \circ \text{toL2} where toL2\text{toL2} and fromL2\text{fromL2} are the continuous linear identity maps between the spaces equipped with their original norms and the same spaces equipped with the L2L_2 norm x2=Rex,x\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}, and ()(\cdot)^\dagger denotes the standard Hilbert space adjoint.

theorem

f=fromL2(toL2ffromL2)toL2f^\dagger = \text{fromL2} \circ (\text{toL2} \circ f \circ \text{fromL2})^\dagger \circ \text{toL2}

Let EE and FF be complete generalized inner product spaces over a field k\mathbb{k} (where k\mathbb{k} is R\mathbb{R} or C\mathbb{C}). For any continuous linear map f:EFf : E \to F, the adjoint f:FEf^\dagger : F \to E is equal to the composition of maps: f=fromL2(toL2ffromL2)toL2f^\dagger = \text{fromL2} \circ (\text{toL2} \circ f \circ \text{fromL2})^\dagger \circ \text{toL2} where toL2\text{toL2} and fromL2\text{fromL2} are the continuous linear identity maps between the spaces equipped with their original norms and the same spaces equipped with the L2L_2 norm x2=Rex,x\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}, and the inner ()(\cdot)^\dagger denotes the standard Hilbert space adjoint of the map between these L2L_2 spaces.

theorem

The adjoint map ff' satisfies f(0)=0f'(0) = 0

Let EE and FF be generalized inner product spaces over a field k\mathbb{k}. If f:FEf' : F \to E is an adjoint of a map f:EFf : E \to F (meaning they satisfy the adjoint relation with respect to the inner products on EE and FF), then the image of the zero vector under ff' is zero, i.e., f(0)=0f'(0) = 0.

theorem

If ff' is an adjoint of ff, then f=ff^\dagger = f'

Let EE and FF be generalized inner product spaces over a field k\mathbb{k}. If a map f:EFf: E \to F has an adjoint f:FEf': F \to E (meaning f(x),y=x,f(y)\langle f(x), y \rangle = \langle x, f'(y) \rangle for all xEx \in E and yFy \in F), then the adjoint operator applied to ff, denoted ff^\dagger, is equal to ff'.

theorem

If g=fg' = f' and gg' is an adjoint of ff, then ff' is also an adjoint of ff

Let EE and FF be inner product spaces over a field k\mathbb{k}. Let f:EFf : E \to F be a linear map. If g:FEg' : F \to E is an adjoint of ff and g=fg' = f', then ff' is also an adjoint of ff.

theorem

The identity map is its own adjoint

Let EE be a generalized inner product space over a field k\mathbb{k}. The identity map idE:EE\text{id}_E : E \to E is its own adjoint. That is, the identity function has an adjoint, and that adjoint is also the identity function.

theorem

The adjoint of the zero map is the zero map

Let EE and FF be generalized inner product spaces over a field k\mathbb{k}. The zero map f:EFf : E \to F, defined by f(x)=0f(x) = 0 for all xEx \in E, has an adjoint g:FEg : F \to E which is also the zero map, defined by g(y)=0g(y) = 0 for all yFy \in F.

theorem

The adjoint of fgf \circ g is gfg' \circ f'

Let E,FE, F, and GG be generalized inner product spaces over a field k\mathbb{k}. If a map f:FGf: F \to G has an adjoint f:GFf': G \to F and a map g:EFg: E \to F has an adjoint g:FEg': F \to E, then the composition fgf \circ g has an adjoint given by the composition of the adjoints in reverse order, gfg' \circ f'.

theorem

The adjoint of x(f(x),g(x))x \mapsto (f(x), g(x)) is (y,z)f(y)+g(z)(y, z) \mapsto f'(y) + g'(z)

Let E,FE, F, and GG be generalized inner product spaces over a field k\mathbb{k}. If a map f:EFf: E \to F has an adjoint f:FEf': F \to E and a map g:EGg: E \to G has an adjoint g:GEg': G \to E, then the map EF×GE \to F \times G defined by x(f(x),g(x))x \mapsto (f(x), g(x)) has an adjoint F×GEF \times G \to E defined by (y,z)f(y)+g(z)(y, z) \mapsto f'(y) + g'(z). Here, the product space F×GF \times G is equipped with the standard product inner product (y1,z1),(y2,z2)=y1,y2F+z1,z2G\langle (y_1, z_1), (y_2, z_2) \rangle = \langle y_1, y_2 \rangle_F + \langle z_1, z_2 \rangle_G.

theorem

The adjoint of x(f(x))1x \mapsto (f(x))_1 is yf(y,0)y \mapsto f'(y, 0)

Let E,FE, F, and GG be generalized inner product spaces over a field k\mathbb{k}. If a map f:EF×Gf: E \to F \times G has an adjoint f:F×GEf': F \times G \to E, then the map from EE to FF defined by taking the first component of ff, x(f(x))1x \mapsto (f(x))_1, has an adjoint given by yf(y,0)y \mapsto f'(y, 0).

theorem

The adjoint of x(f(x))2x \mapsto (f(x))_2 is zf(0,z)z \mapsto f'(0, z)

Let E,F,E, F, and GG be generalized inner product spaces over a field k\mathbb{k}. If a map f:EF×Gf: E \to F \times G has an adjoint f:F×GEf': F \times G \to E, then the map x(f(x))2x \mapsto (f(x))_2 (the projection of ff onto the second component) has an adjoint given by zf(0,z)z \mapsto f'(0, z).

theorem

The adjoint of f-f is f-f'

Let EE and FF be generalized inner product spaces over a field k\mathbb{k}. If f:EFf: E \to F is a map that has an adjoint f:FEf': F \to E, then the map defined by xf(x)x \mapsto -f(x) has an adjoint defined by yf(y)y \mapsto -f'(y).

theorem

f+gf + g has adjoint f+gf' + g'

Let EE and FF be generalized inner product spaces over a field k\mathbb{k}. If f,g:EFf, g: E \to F are maps that have adjoints f,g:FEf', g': F \to E respectively, then the map f+gf + g (defined by xf(x)+g(x)x \mapsto f(x) + g(x)) has an adjoint given by f+gf' + g' (defined by yf(y)+g(y)y \mapsto f'(y) + g'(y)).

theorem

Adjoint of fgf - g is fgf' - g'

Let EE and FF be generalized inner product spaces over a field k\mathbb{k}. If the maps f,g:EFf, g: E \to F have adjoints f,g:FEf', g': F \to E respectively, then the map fgf - g (defined by xf(x)g(x)x \mapsto f(x) - g(x)) has an adjoint fgf' - g' (defined by yf(y)g(y)y \mapsto f'(y) - g'(y)).

theorem

The adjoint of cfc \cdot f is cˉf\bar{c} \cdot f'

Let EE and FF be generalized inner product spaces over a field k\mathbb{k} (where k\mathbb{k} is R\mathbb{R} or C\mathbb{C}). If a map f:EFf: E \to F has an adjoint f:FEf': F \to E, then for any scalar ckc \in \mathbb{k}, the map xcf(x)x \mapsto c \cdot f(x) has an adjoint given by ycˉf(y)y \mapsto \bar{c} \cdot f'(y), where cˉ\bar{c} denotes the complex conjugate of cc.

theorem

Adjoint of xf(x)vx \mapsto f(x)v is yf(y,v)y \mapsto f'(\overline{\langle y, v \rangle})

Let EE and FF be generalized inner product spaces over a field k\mathbb{k} (typically R\mathbb{R} or C\mathbb{C}). Let f:Ekf: E \to \mathbb{k} be a linear map and f:kEf': \mathbb{k} \to E be its adjoint, such that f(x),sk=x,f(s)E\langle f(x), s \rangle_{\mathbb{k}} = \langle x, f'(s) \rangle_E for all xEx \in E and sks \in \mathbb{k}. For any vector vFv \in F, the map g:EFg: E \to F defined by g(x)=f(x)vg(x) = f(x)v has an adjoint g:FEg': F \to E given by g(y)=f(y,v)g'(y) = f'(\overline{\langle y, v \rangle}), where y,v\overline{\langle y, v \rangle} denotes the complex conjugate of the inner product in FF.