PhyslibSearch

Physlib.Mathematics.InnerProductSpace.Adjoint

18 declarations

definition

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

#adjoint

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'

#adjoint_inner_right

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

#hasAdjoint

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}

#adjoint_eq_clm_adjoint

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

#adjoint_apply_zero

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'

#adjoint

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

#congr_adj

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

#hasAdjoint_id

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

#hasAdjoint_zero

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'

#comp

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)

#prodMk

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)

#fst

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)

#snd

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'

#neg

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'

#add

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'

#sub

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'

#smul_left

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})

#smul_right

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.