Physlib

Physlib.Mathematics.Calculus.AdjFDeriv

Adjoint Fréchet derivative

`adjFDeriv 𝕜 f x = (fderiv 𝕜 f x).adjoint`

The main purpose of defining `adjFDeriv` is to compute `gradient f x = adjFDeriv 𝕜 f x 1`. The advantage of working with `adjFDeriv` is that we can formulate composition theorem.

The reason why we do not want to compute `fderiv` and then `adjoint` is that to compute `fderiv 𝕜 f` or `adjoint f` we decompose `f = f₁ ∘ ... ∘ fₙ` and then apply composition theorem. The problem is that this decomposition has to be done differently for `fderiv` and `adjoint`. The problem is that when working with `fderiv` the natural product type is `X × Y` but when working with `adjoint` the natural product is `WithLp 2 (X × Y)`. For example:

32 declarations

definition

Adjoint Fréchet derivative (Df(x))∗(dy)(Df(x))^*(dy)

Given a function f:E→Ff: E \to F between two inner product spaces EE and FF over a field k\mathbb{k}, let Df(x):E→FDf(x): E \to F denote the Fréchet derivative of ff at the point x∈Ex \in E. The adjoint Fréchet derivative at xx is the adjoint of this linear map, denoted (Df(x))∗:F→E(Df(x))^*: F \to E. For a vector dy∈Fdy \in F, the function returns the value (Df(x))∗(dy)∈E(Df(x))^*(dy) \in E, which is the unique vector satisfying ⟨Df(x)⋅v,dy⟩F=⟨v,(Df(x))∗⋅dy⟩E\langle Df(x) \cdot v, dy \rangle_F = \langle v, (Df(x))^* \cdot dy \rangle_E for all v∈Ev \in E.

theorem

adjFDeriv f x=f′\text{adjFDeriv } f \ x = f' if ff has an adjoint Fréchet derivative f′f' at xx

Let EE and FF be inner product spaces over a field k\mathbb{k}. For a function f:E→Ff: E \to F and a point x∈Ex \in E, if ff has an adjoint Fréchet derivative f′f' at xx (expressed by the proposition `HasAdjFDerivAt 𝕜 f f' x`), then the defined adjoint Fréchet derivative adjFDeriv k f x\text{adjFDeriv } \mathbb{k} \ f \ x is equal to f′f'.

theorem

Differentiability at xx implies existence of adjoint Fréchet derivative (Df(x))∗(Df(x))^*

Let EE and FF be complete generalized inner product spaces over a field k\mathbb{k}. If a function f:E→Ff: E \to F is Fréchet differentiable at a point x∈Ex \in E, then ff possesses an adjoint Fréchet derivative at xx, which is given by the adjoint of its Fréchet derivative, denoted as adjFDeriv k f x=(Df(x))∗\text{adjFDeriv } \mathbb{k} \ f \ x = (Df(x))^*.

theorem

The mapping (L,y)↦L∗y(L, y) \mapsto L^* y is a bounded bilinear map over R\mathbb{R}

Let XX and YY be real inner product spaces. The map that sends a pair (L,y)∈L(X,Y)×Y(L, y) \in \mathcal{L}(X, Y) \times Y to L∗yL^* y, where L∗:Y→XL^*: Y \to X is the adjoint of the continuous linear map LL, is a bounded bilinear map over R\mathbb{R}.

theorem

f∈Cn+1  ⟹  ((x,y,dz)↦(Dyf(x,y))∗dz)∈Cnf \in C^{n+1} \implies ((x, y, dz) \mapsto (D_y f(x, y))^* dz) \in C^n

Let EE be a real normed space, and let FF and GG be complete real generalized inner product spaces. Suppose f:E×F→Gf: E \times F \to G is a function such that for every x∈Ex \in E and y∈Fy \in F, the partial map fx:y↦f(x,y)f_x: y \mapsto f(x, y) has an adjoint Fréchet derivative f′(x,y):G→Ff'(x, y): G \to F at yy. If ff is Cn+1C^{n+1} as a function of (x,y)(x, y), then the map (x,y,dz)↦f′(x,y)⋅dz(x, y, dz) \mapsto f'(x, y) \cdot dz from E×F×GE \times F \times G to FF is CnC^n. Here, the adjoint Fréchet derivative f′(x,y)f'(x, y) is the adjoint of the linear map Dyf(x,y):F→GD_y f(x, y): F \to G, satisfying ⟨Dyf(x,y)⋅v,dz⟩G=⟨v,f′(x,y)⋅dz⟩F\langle D_y f(x, y) \cdot v, dz \rangle_G = \langle v, f'(x, y) \cdot dz \rangle_F for all v∈Fv \in F and dz∈Gdz \in G.

theorem

∇f(x)=(Df(x))∗(1)\nabla f(x) = (Df(x))^*(1)

Let UU be an inner product space over a field k\mathbb{k} (where k\mathbb{k} is typically R\mathbb{R} or C\mathbb{C}). For any function f:U→kf: U \to \mathbb{k} that is Fréchet differentiable at a point x∈Ux \in U, the gradient ∇f(x)\nabla f(x) is equal to the adjoint Fréchet derivative of ff at xx applied to the unit 1∈k1 \in \mathbb{k}. That is, ∇f(x)=(Df(x))∗(1)\nabla f(x) = (Df(x))^*(1), where (Df(x))∗(Df(x))^* denotes the adjoint of the Fréchet derivative Df(x):U→kDf(x): U \to \mathbb{k}.

theorem

The identity map has the identity as its adjoint Fréchet derivative at any point xx

Let EE be an inner product space over a field k\mathbb{k}. For any x∈Ex \in E, the identity function f:E→Ef : E \to E defined by f(x)=xf(x) = x has an adjoint Fréchet derivative at xx which is the identity function f′(dx)=dxf'(dx) = dx.

theorem

The Adjoint Fréchet Derivative of the Identity Function is the Identity Map

Let EE be an inner product space over a field k\mathbb{k}. The adjoint Fréchet derivative of the identity function f:E→Ef: E \to E, defined by f(x)=xf(x) = x, is the identity map at every point. Specifically, for any point x∈Ex \in E and any vector dx∈Edx \in E, the adjoint Fréchet derivative satisfies (adjFDeriv k f x) dx=dx(\text{adjFDeriv } \mathbb{k} \ f \ x) \ dx = dx.

theorem

The Adjoint Fréchet Derivative of the Identity Map is the Identity Map

Let EE be an inner product space over a field k\mathbb{k}. The adjoint Fréchet derivative of the identity function id:E→E\text{id} : E \to E is the identity map at every point. Specifically, for any point x∈Ex \in E and any vector dx∈Edx \in E, the adjoint Fréchet derivative satisfies (adjFDeriv k id x) dx=dx(\text{adjFDeriv } \mathbb{k} \ \text{id} \ x) \ dx = dx.

theorem

The adjoint Fréchet derivative of a constant function is zero

Let EE and FF be inner product spaces over a field k\mathbb{k}. For any point x∈Ex \in E and any value y∈Fy \in F, the constant function f:E→Ff: E \to F defined by f(z)=yf(z) = y has an adjoint Fréchet derivative at xx given by the zero linear map dz↦0dz \mapsto 0.

theorem

The adjoint Fréchet derivative of a constant function is zero

Let EE and FF be inner product spaces over a field k\mathbb{k}. For any constant y∈Fy \in F, let f:E→Ff: E \to F be the constant function f(x)=yf(x) = y. The adjoint Fréchet derivative of ff is zero at every point x∈Ex \in E, meaning that for all x∈Ex \in E and all vectors dy∈Fdy \in F, (adjFDeriv k f x)(dy)=0(\text{adjFDeriv } \mathbb{k} \ f \ x)(dy) = 0.

theorem

Chain Rule for Adjoint Fréchet Derivatives

Let E,FE, F, and GG be inner product spaces over a field k\mathbb{k}. Let g:E→Fg: E \to F and f:F→Gf: F \to G be functions. Suppose gg has an adjoint Fréchet derivative g′g' at a point x∈Ex \in E, and ff has an adjoint Fréchet derivative f′f' at the point g(x)g(x). Then the composition f∘gf \circ g has an adjoint Fréchet derivative at xx given by the composition of the adjoint derivatives g′∘f′g' \circ f'.

theorem

Chain Rule for Adjoint Fréchet Derivatives: (D(f∘g)(x))∗=(Dg(x))∗∘(Df(g(x)))∗(D(f \circ g)(x))^* = (Dg(x))^* \circ (Df(g(x)))^*

Let E,FE, F, and GG be complete inner product spaces over a field k\mathbb{k}. Suppose g:E→Fg: E \to F is a function differentiable at a point x∈Ex \in E and f:F→Gf: F \to G is a function differentiable at g(x)g(x). The adjoint Fréchet derivative of the composition f∘gf \circ g at xx is the composition of the adjoint Fréchet derivatives of gg at xx and ff at g(x)g(x). That is, for any dy∈Gdy \in G: (adjFDeriv k (f∘g) x)(dy)=(adjFDeriv k g x)((adjFDeriv k f (g(x)))(dy)) (\text{adjFDeriv } \mathbb{k} \ (f \circ g) \ x)(dy) = (\text{adjFDeriv } \mathbb{k} \ g \ x)((\text{adjFDeriv } \mathbb{k} \ f \ (g(x)))(dy)) In terms of the adjoint of the Fréchet derivative operator DD, this is expressed as: (D(f∘g)(x))∗=(Dg(x))∗∘(Df(g(x)))∗ (D(f \circ g)(x))^* = (Dg(x))^* \circ (Df(g(x)))^*

theorem

The adjoint Fréchet derivative of x↦(f(x),g(x))x \mapsto (f(x), g(x)) is (dy,dz)↦f′(dy)+g′(dz)(dy, dz) \mapsto f'(dy) + g'(dz)

Let E,FE, F, and GG be inner product spaces over a field k\mathbb{k}. Suppose f:E→Ff: E \to F and g:E→Gg: E \to G are functions such that at a point x∈Ex \in E, ff has an adjoint Fréchet derivative f′:F→Ef': F \to E and gg has an adjoint Fréchet derivative g′:G→Eg': G \to E. Then the map h:E→F×Gh: E \to F \times G defined by h(x)=(f(x),g(x))h(x) = (f(x), g(x)) has an adjoint Fréchet derivative at xx given by the map (dy,dz)↦f′(dy)+g′(dz)(dy, dz) \mapsto f'(dy) + g'(dz). Here, the product space F×GF \times G is equipped with the standard product inner product ⟨(y1,z1),(y2,z2)⟩=⟨y1,y2⟩F+⟨z1,z2⟩G\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 Fréchet derivative of x↦(f(x))1x \mapsto (f(x))_1 is dy↦f′(dy,0)dy \mapsto f'(dy, 0)

Let E,FE, F, and GG be generalized inner product spaces over a field k\mathbb{k}. If a function f:E→F×Gf: E \to F \times G has an adjoint Fréchet derivative f′:F×G→Ef' : F \times G \to E at a point x∈Ex \in E, then the map x↦(f(x))1x \mapsto (f(x))_1 (the projection onto the first component) has an adjoint Fréchet derivative at xx given by the function dy↦f′(dy,0)dy \mapsto f'(dy, 0).

theorem

The adjoint Fréchet derivative of x↦(f(x))1x \mapsto (f(x))_1 is dy↦(Df(x))∗(dy,0)dy \mapsto (Df(x))^*(dy, 0)

Let E,FE, F, and GG be complete generalized inner product spaces over a field k\mathbb{k}. For a function f:E→F×Gf: E \to F \times G that is Fréchet differentiable at a point x∈Ex \in E, the adjoint Fréchet derivative of its first component f1:E→Ff_1: E \to F (where f1(x)=(f(x))1f_1(x) = (f(x))_1) at xx is given by the linear map dy↦(Df(x))∗(dy,0)dy \mapsto (Df(x))^*(dy, 0). Here, (Df(x))∗:F×G→E(Df(x))^*: F \times G \to E denotes the adjoint Fréchet derivative of ff at xx. The product space F×GF \times G is equipped with the standard product inner product ⟨(y1,z1),(y2,z2)⟩=⟨y1,y2⟩F+⟨z1,z2⟩G\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 Fréchet derivative of the first projection is a↦(a,0)a \mapsto (a, 0)

Let EE and FF be complete generalized inner product spaces over a field k\mathbb{k}. For the projection map π1:F×E→F\pi_1: F \times E \to F defined by π1(y,z)=y\pi_1(y, z) = y, its adjoint Fréchet derivative at any point x∈F×Ex \in F \times E is the linear map that sends a∈Fa \in F to the pair (a,0)∈F×E(a, 0) \in F \times E.

theorem

The adjoint Fréchet derivative of x↦(f(x))2x \mapsto (f(x))_2 is dz↦f′(0,dz)dz \mapsto f'(0, dz)

Let E,FE, F, and GG be inner product spaces over a field k\mathbb{k}. Let f:E→F×Gf: E \to F \times G be a function and x∈Ex \in E. If ff has an adjoint Fréchet derivative f′:F×G→Ef': F \times G \to E at xx, then the map x↦π2(f(x))x \mapsto \pi_2(f(x)) (the projection onto the second component) also has an adjoint Fréchet derivative at xx, which is given by the linear map dz↦f′(0,dz)dz \mapsto f'(0, dz).

theorem

Adjoint Fréchet derivative of x↦(f(x))2x \mapsto (f(x))_2 is dy↦(Df(x))∗(0,dy)dy \mapsto (Df(x))^*(0, dy)

Let E,FE, F, and GG be complete generalized inner product spaces over a field k\mathbb{k}. Let f:E→F×Gf: E \to F \times G be a function that is differentiable at a point x∈Ex \in E. Then the adjoint Fréchet derivative of the map x↦(f(x))2x \mapsto (f(x))_2 (the projection of ff onto its second component) at xx is given by the linear map that sends dy∈Gdy \in G to (Df(x))∗(0,dy)(Df(x))^*(0, dy), where (Df(x))∗:F×G→E(Df(x))^*: F \times G \to E denotes the adjoint Fréchet derivative of ff at xx.

theorem

The adjoint Fréchet derivative of proj2\text{proj}_2 is a↦(0,a)a \mapsto (0, a)

Let EE and FF be complete inner product spaces over a field k\mathbb{k}. The adjoint Fréchet derivative of the second projection map proj2:F×E→E\text{proj}_2 : F \times E \to E, defined by proj2(y,z)=z\text{proj}_2(y, z) = z, at any point x∈F×Ex \in F \times E is the linear map from EE to F×EF \times E that sends a∈Ea \in E to (0,a)(0, a).

theorem

The adjoint Fréchet derivative of f(x,y)f(x, y) is (fx′,fy′)(fx', fy')

Let E,FE, F, and GG be inner product spaces over a field k\mathbb{k}. Let f:E→F→Gf: E \to F \to G be a function, and let (x,y)∈E×F(x, y) \in E \times F. Suppose that: 1. The uncurried function (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is differentiable at (x,y)(x, y). 2. The partial map x′↦f(x′,y)x' \mapsto f(x', y) has an adjoint Fréchet derivative fx′:G→Efx': G \to E at xx. 3. The partial map y′↦f(x,y′)y' \mapsto f(x, y') has an adjoint Fréchet derivative fy′:G→Ffy': G \to F at yy. Then the uncurried function (x,y)↦f(x,y)(x, y) \mapsto f(x, y) has an adjoint Fréchet derivative at (x,y)(x, y) given by the map dz↦(fx′(dz),fy′(dz))dz \mapsto (fx'(dz), fy'(dz)) from GG into E×FE \times F.

theorem

The adjoint Fréchet derivative of f(x,y)f(x, y) is the pair of partial adjoint derivatives ((D1f)∗,(D2f)∗)((D_1f)^*, (D_2f)^*)

Let E,FE, F, and GG be complete inner product spaces over a field k\mathbb{k}. Let f:E→F→Gf: E \to F \to G be a function such that the uncurried function f^(x,y)=f(x,y)\hat{f}(x, y) = f(x, y) is differentiable at a point (x,y)∈E×F(x, y) \in E \times F. The adjoint Fréchet derivative of f^\hat{f} at (x,y)(x, y), denoted (Df^(x,y))∗:G→E×F(D\hat{f}(x, y))^*: G \to E \times F, is given by: (Df^(x,y))∗(dz)=((D1f(x,y))∗(dz),(D2f(x,y))∗(dz))(D\hat{f}(x, y))^*(dz) = \left( (D_1 f(x, y))^*(dz), (D_2 f(x, y))^*(dz) \right) for all dz∈Gdz \in G, where (D1f(x,y))∗:G→E(D_1 f(x, y))^*: G \to E is the adjoint Fréchet derivative of the partial map x′↦f(x′,y)x' \mapsto f(x', y) at xx, and (D2f(x,y))∗:G→F(D_2 f(x, y))^*: G \to F is the adjoint Fréchet derivative of the partial map y′↦f(x,y′)y' \mapsto f(x, y') at yy.

theorem

The adjoint Fréchet derivative of −f-f is −f′-f'

Let EE and FF be inner product spaces over a field k\mathbb{k}. If a function f:E→Ff: E \to F has an adjoint Fréchet derivative f′f' at a point x∈Ex \in E, then the function x↦−f(x)x \mapsto -f(x) also has an adjoint Fréchet derivative at xx, given by the map dy↦−f′(dy)dy \mapsto -f'(dy).

theorem

(D(−f)(x))∗=−(Df(x))∗(D(-f)(x))^* = -(Df(x))^*

Let EE and FF be complete inner product spaces over a field k\mathbb{k}. If a function f:E→Ff: E \to F is Fréchet differentiable at a point x∈Ex \in E, then the adjoint Fréchet derivative of the negated function x↦−f(x)x \mapsto -f(x) at xx is equal to the negation of the adjoint Fréchet derivative of ff at xx. In terms of the adjoint operator (Df(x))∗(Df(x))^*, this is expressed as: (D(−f)(x))∗=−(Df(x))∗ (D(-f)(x))^* = -(Df(x))^* Specifically, for any vector dy∈Fdy \in F, the value is −(Df(x))∗(dy)-(Df(x))^*(dy).

theorem

f+gf + g has adjoint Fréchet derivative f′+g′f' + g'

Let EE and FF be inner product spaces over a field k\mathbb{k}. If f,g:E→Ff, g: E \to F are functions such that ff has an adjoint Fréchet derivative f′f' at x∈Ex \in E and gg has an adjoint Fréchet derivative g′g' at xx, then the sum function f+gf + g (defined by x↦f(x)+g(x)x \mapsto f(x) + g(x)) has an adjoint Fréchet derivative at xx given by f′+g′f' + g' (defined by dy↦f′(dy)+g′(dy)dy \mapsto f'(dy) + g'(dy)).

theorem

(D(f+g)(x))∗=(Df(x))∗+(Dg(x))∗(D(f+g)(x))^* = (Df(x))^* + (Dg(x))^*

Let EE and FF be complete inner product spaces over a field k\mathbb{k}. If f,g:E→Ff, g: E \to F are functions differentiable at x∈Ex \in E, then the adjoint Fréchet derivative of their sum f+gf + g at xx is the sum of their individual adjoint Fréchet derivatives at xx. That is, (D(f+g)(x))∗=(Df(x))∗+(Dg(x))∗, (D(f+g)(x))^* = (Df(x))^* + (Dg(x))^*, where (Df(x))∗(Df(x))^* denotes the adjoint of the Fréchet derivative of ff at xx.

theorem

The adjoint Fréchet derivative of f−gf - g is f′−g′f' - g'

Let EE and FF be inner product spaces over a field k\mathbb{k}. Suppose f,g:E→Ff, g: E \to F are functions that have adjoint Fréchet derivatives f′,g′:F→Ef', g': F \to E at a point x∈Ex \in E, respectively. Then the function f−gf - g (defined by x↦f(x)−g(x)x \mapsto f(x) - g(x)) has an adjoint Fréchet derivative at xx given by f′−g′f' - g' (defined by dy↦f′(dy)−g′(dy)dy \mapsto f'(dy) - g'(dy)).

theorem

Adjoint Fréchet Derivative of f−gf - g is (Df(x))∗−(Dg(x))∗(Df(x))^* - (Dg(x))^*

Let EE and FF be complete inner product spaces over a field k\mathbb{k}. Suppose f,g:E→Ff, g: E \to F are functions that are Fréchet differentiable at a point x∈Ex \in E. Then the adjoint Fréchet derivative of the difference f−gf - g at xx is equal to the difference of the adjoint Fréchet derivatives of ff and gg at xx. That is, for any vector dy∈Fdy \in F: adjFDeriv k (f−g) x (dy)=adjFDeriv k f x (dy)−adjFDeriv k g x (dy) \text{adjFDeriv } \mathbb{k} \ (f - g) \ x \ (dy) = \text{adjFDeriv } \mathbb{k} \ f \ x \ (dy) - \text{adjFDeriv } \mathbb{k} \ g \ x \ (dy) Using the notation (Df(x))∗(Df(x))^* for the adjoint of the Fréchet derivative, this can be written as: (D(f−g)(x))∗=(Df(x))∗−(Dg(x))∗ (D(f - g)(x))^* = (Df(x))^* - (Dg(x))^*

theorem

Adjoint Fréchet Derivative of the Product g(x)f(x)g(x)f(x)

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 f:E→Ff: E \to F is a map with an adjoint Fréchet derivative f′f' at x∈Ex \in E, and g:E→kg: E \to \mathbb{k} is a map with an adjoint Fréchet derivative g′g' at xx. Then the adjoint Fréchet derivative of the scalar-vector product x↦g(x)f(x)x \mapsto g(x)f(x) at the point xx is the linear map F→EF \to E given by: dy↦g(x)‾f′(dy)+g′(⟨dy,f(x)⟩‾) dy \mapsto \overline{g(x)} f'(dy) + g'(\overline{\langle dy, f(x) \rangle}) where z‾\overline{z} denotes the conjugate of z∈kz \in \mathbb{k} and ⟨⋅,⋅⟩\langle \cdot, \cdot \rangle denotes the inner product on FF.

theorem

Adjoint Fréchet Derivative of the Product g(x)f(x)g(x)f(x)

Let EE and FF be complete inner product spaces over a field k\mathbb{k} (where k\mathbb{k} is R\mathbb{R} or C\mathbb{C}). If f:E→Ff: E \to F and g:E→kg: E \to \mathbb{k} are differentiable at a point x∈Ex \in E, then the adjoint Fréchet derivative of the scalar-vector product x↦g(x)f(x)x \mapsto g(x)f(x) at xx is the linear map F→EF \to E given by: dy↦g(x)‾(Df(x))∗(dy)+(Dg(x))∗(⟨dy,f(x)⟩‾) dy \mapsto \overline{g(x)} (Df(x))^*(dy) + (Dg(x))^*(\overline{\langle dy, f(x) \rangle}) where (Df(x))∗(Df(x))^* and (Dg(x))∗(Dg(x))^* denote the adjoint Fréchet derivatives of ff and gg at xx respectively, and ⟨⋅,⋅⟩\langle \cdot, \cdot \rangle denotes the inner product on FF.

theorem

Adjoint Fréchet Derivative of the Inner Product (x1,x2)↦⟨x1,x2⟩(x_1, x_2) \mapsto \langle x_1, x_2 \rangle

Let EE be a real generalized inner product space. For the inner product function f:E×E→Rf: E \times E \to \mathbb{R} defined by f(x1,x2)=⟨x1,x2⟩f(x_1, x_2) = \langle x_1, x_2 \rangle, the adjoint Fréchet derivative at any point x=(x1,x2)∈E×Ex = (x_1, x_2) \in E \times E is the linear map from R\mathbb{R} to E×EE \times E defined by: y↦y⋅(x2,x1) y \mapsto y \cdot (x_2, x_1) for any y∈Ry \in \mathbb{R}.

theorem

Adjoint Fréchet Derivative of Inner Product (x1,x2)↦⟨x1,x2⟩(x_1, x_2) \mapsto \langle x_1, x_2 \rangle is y↦y(x2,x1)y \mapsto y(x_2, x_1)

Let EE be a real generalized inner product space. For the inner product function f:E×E→Rf: E \times E \to \mathbb{R} defined by f(x1,x2)=⟨x1,x2⟩f(x_1, x_2) = \langle x_1, x_2 \rangle, the adjoint Fréchet derivative at any point x=(x1,x2)∈E×Ex = (x_1, x_2) \in E \times E is the linear map from R\mathbb{R} to E×EE \times E defined by: y↦y⋅(x2,x1) y \mapsto y \cdot (x_2, x_1) for any y∈Ry \in \mathbb{R}.