Resolvents and restriction of scalars

An unbounded operator A : X →ₗ.[𝕜'] X over a normed field extension 𝕜' can also be read over a smaller field 𝕜, as A.restrictScalars 𝕜. This file shows that the two resolvent notions agree at the points of 𝕜: for mu : 𝕜,

mu ∈ resolventSet (A.restrictScalars 𝕜) ↔ algebraMap 𝕜 𝕜' mu ∈ resolventSet A,

and the resolvents themselves correspond under ContinuousLinearMap.restrictScalars. The actions on X form a scalar tower; no norm compatibility between the two fields is required.

Only the forward direction has content. A bounded 𝕜-linear inverse R of mu • I - A is automatically 𝕜'-homogeneous: z • R y and R (z • y) have the same image under mu • I - A, because A is 𝕜'-linear, so they agree. This homogeneity statement also works over an arbitrary ring algebra, without a norm or topology on the larger algebra.

This is what lets a real-variable theorem about an operator on a complex Banach space — such as the Laplace-transform resolvent of a C₀-semigroup, which is built over ℝ — be read as a statement about the genuinely complex resolvent set.

Main results

• LinearPMap.IsResolventAt.restrictScalars: restricting scalars in an inverse of lambda • I - A.
• TauCeti.LinearPMap.map_smul_of_isResolventAt_restrictScalars: a bounded inverse over 𝕜 is 𝕜'-homogeneous.
• TauCeti.LinearPMap.exists_isResolventAt_of_isResolventAt_restrictScalars: it therefore comes from an inverse over 𝕜'.
• TauCeti.LinearPMap.mem_resolventSet_restrictScalars_iff: the resolvent sets agree at the points of 𝕜.
• TauCeti.LinearPMap.restrictScalars_resolvent: the resolvents agree there.

theorem TauCeti.LinearPMap.map_smul_of_isResolventAt_restrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [Ring 𝕜'] [Algebra 𝕜 𝕜'] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [Module 𝕜' X] [IsScalarTower 𝕜 𝕜' X] {A : X →ₗ.[𝕜'] X} {mu : 𝕜} {R₀ : X →L[𝕜] X} (h : (LinearPMap.restrictScalars 𝕜 A).IsResolventAt mu R₀) (z : 𝕜') (y : X) : R₀ (z • y) = z • R₀ y

A bounded 𝕜-linear inverse of mu • I - A respects the action of the larger algebra 𝕜'. No norm or topology on 𝕜' is needed.

theorem LinearPMap.IsResolventAt.restrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [Algebra 𝕜 𝕜'] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedSpace 𝕜' X] [IsScalarTower 𝕜 𝕜' X] {A : X →ₗ.[𝕜'] X} {mu : 𝕜} {R : X →L[𝕜'] X} (h : A.IsResolventAt ((algebraMap 𝕜 𝕜') mu) R) : (LinearPMap.restrictScalars 𝕜 A).IsResolventAt mu (ContinuousLinearMap.restrictScalars 𝕜 R)

An inverse of algebraMap 𝕜 𝕜' mu • I - A restricts to an inverse of mu • I - A for the restriction of scalars.

theorem TauCeti.LinearPMap.exists_isResolventAt_of_isResolventAt_restrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [Algebra 𝕜 𝕜'] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedSpace 𝕜' X] [IsScalarTower 𝕜 𝕜' X] {A : X →ₗ.[𝕜'] X} {mu : 𝕜} {R₀ : X →L[𝕜] X} (h : (LinearPMap.restrictScalars 𝕜 A).IsResolventAt mu R₀) : ∃ (R : X →L[𝕜'] X), ContinuousLinearMap.restrictScalars 𝕜 R = R₀ ∧ A.IsResolventAt ((algebraMap 𝕜 𝕜') mu) R

A bounded inverse of mu • I - A over the smaller field is the restriction of scalars of a bounded inverse over the larger one.

@[simp]

theorem TauCeti.LinearPMap.mem_resolventSet_restrictScalars_iff {𝕜 : Type u_1} {𝕜' : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [Algebra 𝕜 𝕜'] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedSpace 𝕜' X] [IsScalarTower 𝕜 𝕜' X] {A : X →ₗ.[𝕜'] X} {mu : 𝕜} : mu ∈ (LinearPMap.restrictScalars 𝕜 A).resolventSet ↔ (algebraMap 𝕜 𝕜') mu ∈ A.resolventSet

The resolvent sets of an operator and of its restriction of scalars agree at the points of the smaller field.

@[simp]

theorem TauCeti.LinearPMap.restrictScalars_resolvent {𝕜 : Type u_1} {𝕜' : Type u_2} {X : Type u_3} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [Algebra 𝕜 𝕜'] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedSpace 𝕜' X] [IsScalarTower 𝕜 𝕜' X] {A : X →ₗ.[𝕜'] X} {mu : 𝕜} (h : mu ∈ (LinearPMap.restrictScalars 𝕜 A).resolventSet) : ContinuousLinearMap.restrictScalars 𝕜 (A.resolvent ((algebraMap 𝕜 𝕜') mu)) = (LinearPMap.restrictScalars 𝕜 A).resolvent mu

The resolvent of the restriction of scalars is the restriction of scalars of the resolvent.