[Merged by Bors] - refactor: improve API connecting `ℝ`- and `𝕜`-linear functionals by j-loreaux · Pull Request #34543 · leanprover-community/mathlib4

j-loreaux · 2026-01-28T18:28:10Z

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:

Naming: the primary declarations LinearMap.extendTo𝕜' and ContinuousLinearMap.extendTo𝕜' are in the wrong namespaces (Module.Dual and StrongDual), and contain a variable name 𝕜.
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 [Merged by Bors] - fix: remove defeq abuse in the Hahn-Banach theorem #34530) and so should be avoided anyway. That PR removes the only occurrence of the use of the unprimed declarations in Mathlib.
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).
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.
There are missing simp lemmas, namely, ones concerning the imaginary part of the extension applied to a vector.
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:

Renaming LinearMap.extendTo𝕜' → Module.Dual.extendRCLike and ContinuousLinearMap.extendTo𝕜' → StrongDual.extendRCLike.
Removing the unprimed counterparts that operate on RestrictScalars
Weakening the type class assumptions on the newly renamed StrongDual.extendRCLike
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.
Add the missing simp lemmas for imaginary parts.
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 𝕜.

In a follow-up PR, I will add the bundling:

WeakDual.extendRCLikeL : WeakDual E ℝ ≃L[ℝ] WeakDual E 𝕜.

depends on: [Merged by Bors] - fix: remove defeq abuse in the Hahn-Banach theorem #34530

github-actions · 2026-01-28T18:29:21Z

PR summary 08657ed7f8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ extendRCLikeₗᵢ
+ norm_extendRCLike
+ norm_extendRCLike_apply_sq
+ norm_extendRCLike_bound
++ extendRCLike
++ extendRCLike_apply
++ extendRCLikeₗ
++ im_extendRCLike_apply
++ re_extendRCLike_apply
++-- extendTo𝕜
++-- extendTo𝕜'
++-- extendTo𝕜'_apply
++-- extendTo𝕜_apply
- extendTo𝕜'ₗ
- instance : NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F)
- re_extendTo𝕜'ₗ

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
13072	-1	backward.isDefEq

Current commit a2e2012816
Reference commit 08657ed7f8

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib4-dependent-issues-bot · 2026-01-29T08:44:34Z

This PR/issue depends on:

~~[Merged by Bors] - fix: remove defeq abuse in the Hahn-Banach theorem #34530~~
By Dependent Issues (🤖). Happy coding!

mathlib4-merge-conflict-bot · 2026-01-29T21:47:41Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-02-18T06:12:54Z

This pull request has conflicts, please merge master and resolve them.

urkud · 2026-02-23T20:03:57Z

 @[simp]
-theorem extendTo𝕜'_apply_re (fr : Dual ℝ F) (x : F) : re (fr.extendTo𝕜' x : 𝕜) = fr x := by
-  simp only [extendTo𝕜'_apply, map_sub, zero_mul, mul_zero, sub_zero, rclike_simps]
+theorem re_extendRCLike_apply (fr : Dual ℝ F) (x : F) : re (fr.extendRCLike x : 𝕜) = fr x := by


Should we add confluence lemmas for Complex.re and Complex.im? Also, should we add a lemma saying that extending from Real to Real gives fr?

I don't love adding those confluence lemmas, because it just means that we have to duplicate everything whenever RCLike.re appears anywhere in a statement. In fact, I would prefer that the transition RCLike.re → Complex.re were not marked @[simp] for this reason. It would be okay if it were in some sort of simp set.

We could have the real version, but I suspect it's probably not necessary. If you're working over ℝ, you probably have no reason to do this extension anyway.

I know I'm late to the game, but can @j-loreaux explain more about the " ...it just means that we have to duplicate everything whenever RCLike.re ..."? I can't really see why we're happy with re_extendRCLike_apply being simp (which I am) and we wouldn't be with RCLike.re -> Complex.re.

urkud · 2026-02-24T03:39:49Z


-end ScalarTower
+/-- `StrongDual.extendRCLike` bundled into a linear isometry equivalence. -/
+noncomputable def extendRCLikeₗᵢ : StrongDual ℝ F ≃ₗᵢ[ℝ] StrongDual 𝕜 F where


This one should come with @[simp] lemmas, probably generated by @[simps]. Same for other bundled versions, if there are missing @[simps]. BTW, should we have a ContinuousLinearEquiv version for topological vector spaces? This may be out of scope for this PR.

As with the other bundled versions, I have just added @[simps! -isSimp apply symm_apply]. We don't want these to be actual simp lemmas, because we don't want to lose whichever bundling of extendRCLike we are currently using just because we applied it to some vector. So you have to ask to delete the bundling explicitly by doing simp [extendRCLikeₗᵢ_apply] or whatever.

Let me know if you disagree with this.

Yes, we should add the bundling for TVS, but I'll do it in another PR.

Just for sanity: here you mean TVS as opposed to normed F (which is the current assumption)?

urkud · 2026-02-24T03:40:50Z

@j-loreaux Once you address the comments, please DM me on Zulip, and I'll try to quickly merge it (I'm not delegating, because I want to read answers to my questions before merging).

urkud · 2026-02-25T03:11:07Z

bors merge

) 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: 1. Renaming `LinearMap.extendTo𝕜'` → `Module.Dual.extendRCLike` and `ContinuousLinearMap.extendTo𝕜'` → `StrongDual.extendRCLike`. 2. Removing the unprimed counterparts that operate on `RestrictScalars` 3. Weakening the type class assumptions on the newly renamed `StrongDual.extendRCLike` 4. 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. 5. Add the missing simp lemmas for imaginary parts. 6. 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 𝕜`.

mathlib-bors · 2026-02-25T03:27:53Z

Pull request successfully merged into master.

Build succeeded:

…nprover-community#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 leanprover-community#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: 1. Renaming `LinearMap.extendTo𝕜'` → `Module.Dual.extendRCLike` and `ContinuousLinearMap.extendTo𝕜'` → `StrongDual.extendRCLike`. 2. Removing the unprimed counterparts that operate on `RestrictScalars` 3. Weakening the type class assumptions on the newly renamed `StrongDual.extendRCLike` 4. 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. 5. Add the missing simp lemmas for imaginary parts. 6. 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 𝕜`.

j-loreaux added 3 commits January 28, 2026 09:45

fix: remove defeq abuse in the Hahn-Banach theorem

1796b8f

refactor: ContinuousLinearMap.extendTo𝕜' → StrongDual.extendRCLike

5a80916

improvements

a7f509e

github-actions bot added the t-analysis Analysis (normed *, calculus) label Jan 28, 2026

fix

2240395

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jan 28, 2026

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 29, 2026

j-loreaux added 2 commits February 1, 2026 08:05

Merge branch 'master' into dual-extend

dd10f96

correct statement

0d5ea1f

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 1, 2026

j-loreaux mentioned this pull request Feb 2, 2026

feat: continuous linear equivalence between continuous ℝ- and 𝕜-linear functionals (in either the strong or weak-⋆ topologies) #34728

Open

1 task

j-loreaux requested a review from faenuccio February 12, 2026 21:08

mathlib-triage bot assigned urkud Feb 17, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2026

Merge branch 'master' into dual-extend

2dec4c3

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2026

urkud reviewed Feb 23, 2026

View reviewed changes

urkud reviewed Feb 24, 2026

View reviewed changes

Comment thread Mathlib/Analysis/Normed/Module/RCLike/Extend.lean Outdated

urkud reviewed Feb 24, 2026

View reviewed changes

urkud added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 24, 2026

code review

a2e2012

j-loreaux removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 24, 2026

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 25, 2026

mathlib-bors bot changed the title ~~refactor: improve API connecting ℝ- and 𝕜-linear functionals~~ [Merged by Bors] - refactor: improve API connecting ℝ- and 𝕜-linear functionals Feb 25, 2026

mathlib-bors bot closed this Feb 25, 2026

Conversation

j-loreaux commented Jan 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 08657ed7f8

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jan 29, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Jan 29, 2026

Uh oh!

mathlib-merge-conflicts bot commented Feb 18, 2026

Uh oh!

urkud Feb 23, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Feb 24, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Feb 24, 2026

Choose a reason for hiding this comment

Uh oh!

faenuccio Feb 25, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

urkud Feb 24, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

faenuccio Feb 25, 2026

Choose a reason for hiding this comment

Uh oh!

urkud commented Feb 24, 2026

Uh oh!

urkud commented Feb 25, 2026

Uh oh!

mathlib-bors bot commented Feb 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

j-loreaux commented Jan 28, 2026 •

edited

Loading

github-actions bot commented Jan 28, 2026 •

edited

Loading

j-loreaux Feb 24, 2026 •

edited

Loading