Documentation

TauCeti.Analysis.Normed.Module.Dual.Functoriality

Functoriality of the continuous dual #

Precomposition by a continuous linear map acts contravariantly on continuous duals. This file records the identity and composition laws for modules with arbitrary topologies. For normed spaces, it proves that taking the adjoint preserves the operator norm over ℝ or ℂ, packages this operation as a linear isometry between operator spaces, and proves the naturality of the canonical map into the bidual.

For normed spaces over ℝ or ℂ, the adjoint of T : E →L[𝕜] F, with its arguments exchanged, is the composition of T with Mathlib's canonical bidual isometry NormedSpace.inclusionInDoubleDualLi.

These are the standard functorial properties of the continuous dual; see Rudin, Functional Analysis, Chapter 4.

source
@[simp]
theorem ContinuousLinearMap.precomp_id {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] :
precomp 𝕜 (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 (StrongDual 𝕜 E)

The adjoint of the identity map is the identity map on the continuous dual.

source
@[simp]
theorem ContinuousLinearMap.precomp_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] (T : E →L[𝕜] F) (S : F →L[𝕜] G) :
precomp 𝕜 (S ∘SL T) = precomp 𝕜 T ∘SL precomp 𝕜 S

Taking adjoints reverses composition.

source
theorem ContinuousLinearMap.norm_precomp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) :
‖precomp 𝕜 T‖ ≤ ‖T‖

The operator norm of the adjoint is at most the operator norm of the original map.

source
@[simp]
theorem ContinuousLinearMap.norm_precomp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) :
‖precomp 𝕜 T‖ = ‖T‖

Taking the adjoint preserves the operator norm.

source
@[simp]
theorem ContinuousLinearMap.nnnorm_precomp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) :
‖precomp 𝕜 T‖₊ = ‖T‖₊

Taking the adjoint preserves the nonnegative operator norm.

source
def ContinuousLinearMap.precompLinearIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :
(E →L[𝕜] F) →ₗᵢ[𝕜] StrongDual 𝕜 F →L[𝕜] StrongDual 𝕜 E

Taking adjoints, bundled as a linear isometry between spaces of bounded operators.

Instances For
    source
    @[simp]
    theorem ContinuousLinearMap.precompLinearIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) :
    precompLinearIsometry T = precomp 𝕜 T

    The operator-space isometry for adjoints evaluates to precomposition.

    source
    @[simp]
    theorem ContinuousLinearMap.precomp_precomp_inclusionInDoubleDual {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (x : E) :
    (NormedSpace.inclusionInDoubleDual 𝕜 E) x ∘SL precomp 𝕜 T = (NormedSpace.inclusionInDoubleDual 𝕜 F) (T x)

    Pointwise naturality of the canonical map into the bidual.

    source
    theorem ContinuousLinearMap.precomp_precomp_comp_inclusionInDoubleDual {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) :
    precomp 𝕜 (precomp 𝕜 T) ∘SL NormedSpace.inclusionInDoubleDual 𝕜 E = NormedSpace.inclusionInDoubleDual 𝕜 F ∘SL T

    The canonical map into the bidual is natural under bounded linear maps.

    source
    theorem ContinuousLinearMap.continuous_toWeakDual_precomp_precomp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) :
    Continuous fun (Φ : WeakDual 𝕜 (StrongDual 𝕜 E)) => StrongDual.toWeakDual ((precomp 𝕜 (precomp 𝕜 T)) (WeakDual.toStrongDual Φ))

    The bidual adjoint T** is continuous between the weak-star topologies of the biduals.

    source
    theorem ContinuousLinearMap.toWeakDual_precomp_precomp_inclusionInDoubleDualWeak {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (x : E) :
    StrongDual.toWeakDual ((precomp 𝕜 (precomp 𝕜 T)) (WeakDual.toStrongDual ((NormedSpace.inclusionInDoubleDualWeak 𝕜 E) ((toWeakSpace 𝕜 E) x)))) = (NormedSpace.inclusionInDoubleDualWeak 𝕜 F) ((toWeakSpace 𝕜 F) (T x))

    On the canonical image of E in the weak-star bidual, the bidual adjoint T** acts as T.