Commit 2026-02-25 03:11 d300915b

View on Github →

refactor: improve API connecting ℝ- and 𝕜-linear functionals (#34543) This PR concerns the extension of ℝ-linear (continuous or not) functionals to 𝕜-linear functionals. This does several things, but I felt it was better to do it all at once, rather than having repeated churn in the same files because the current setup is a mess for numerous reasons. Unfortunately, that means the diff is a bit of a mess; I think the easiest way to review this PR is read the following discussion and then only look at the new code (and check that the deprecations exist). I will begin by highlighting the current problems:

  1. Naming: the primary declarations LinearMap.extendTo𝕜' and ContinuousLinearMap.extendTo𝕜' are in the wrong namespaces (Module.Dual and StrongDual), and contain a variable name 𝕜.
  2. These declarations are primed, and their unprimed counterparts operate directly on RestrictScalars. This is nominally (according to the module documentation) for convenience, but it leads to defeq abuse (see #34530) and so should be avoided anyway. That PR removes the only occurrence of the use of the unprimed declarations in Mathlib.
  3. The declaration ContinuousLinearMap.extendTo𝕜' has type class assumptions (normed ones) that are too strong, thereby making it unusable for non-normed spaces (e.g., when one wants to consider continuous linear functionals on the weak dual of a Banach space).
  4. Point (3) led to the creation of RCLike.extendTo𝕜'ₗ which is just ContinuousLinearMap.extendTo𝕜' except reproven with weaker type class assumptions and bundled into a linear map.
  5. There are missing simp lemmas, namely, ones concerning the imaginary part of the extension applied to a vector.
  6. We're missing appropriately bundled versions, with RCLike.extendTo𝕜'ₗ being the only bundling currently. In this PR: we fix the above by doing the following:
  7. Renaming LinearMap.extendTo𝕜' → Module.Dual.extendRCLike and ContinuousLinearMap.extendTo𝕜' → StrongDual.extendRCLike.
  8. Removing the unprimed counterparts that operate on RestrictScalars
  9. Weakening the type class assumptions on the newly renamed StrongDual.extendRCLike
  10. Move RCLike.extendTo𝕜'ₗ out of its current location (Analysis/LocallyConvex/Separation) and next to StrongDual.extendRCLike; use the newly generalized StrongDual.extendRCLike to define it; rename it to StrongDual.extendRCLikeₗ; upgrade it from a linear map to a linear equivalence.
  11. Add the missing simp lemmas for imaginary parts.
  12. Add other appropriate bundlings, namely Module.Dual.extendRCLikeₗ : Dual E ℝ ≃ₗ[ℝ] Dual E 𝕜, and, in the context of normed spaces StrongDual.extendRCLikeₗᵢ : StrongDual E ℝ ≃ₗᵢ[ℝ] StrongDual E 𝕜.

Estimated changes