[Merged by Bors] - feat: continuous linear maps with a continuous left/right inverseContinuousinverse by grunweg · Pull Request #34991 · leanprover-community/mathlib4

grunweg · 2026-02-08T18:09:16Z

Define continuous linear maps which admit a continuous left resp. right inverse,
prove their basic properties (closure under products, composition and continuous linear equivalences admitting both inverses) and a sufficient condition in finite dimension.

A future PRs will add an equivalent characterisation of maps with a continuous left inverse,
and use this to prove that the composition of immersions (resp. submersions) is an immersion (resp. submersion).

Part of the path towards immersions, submersions, embedded submanifolds and the regular value theorem.

github-actions · 2026-02-08T18:10:22Z

PR summary 8115783e28

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Normed.Module.ContinuousInverse` (new file)	2119

Declarations diff

+ ContinuousLinearMap.HasLeftInverse
+ ContinuousLinearMap.HasRightInverse
+ _root_.ContinuousLinearEquiv.hasLeftInverse
+ _root_.ContinuousLinearEquiv.hasRightInverse
+ _root_.ContinuousLinearEquiv.leftInverse_hasLeftInverse
+ _root_.ContinuousLinearEquiv.rightInverse_hasRightInverse
+ fst
+ injective
+ inl
+ inr
+ leftInverse
+ leftInverse_leftInverse
+ of_injective_of_finiteDimensional
+ of_surjective_of_finiteDimensional
+ rightInverse
+ rightInverse_rightInverse
+ snd
+ surjective
++ comp
++ comp_continuousLinearEquivalence
++ congr
++ continuousLinearEquivalence_comp
++ of_comp
++ of_isInvertible
++ prodMap

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 script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

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).

Mathlib/Analysis/Normed/Module/ContinuousInverse.lean

Mathlib/Analysis/NormedSpace/ContinuousInverse.lean

grunweg · 2026-02-08T20:43:28Z

Thanks for the review comments; I should have addressed them all.

j-loreaux

Only minor quibbles.

Mathlib/Analysis/Normed/Module/ContinuousInverse.lean

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

grunweg · 2026-02-10T22:52:17Z

Thanks for the useful and careful review comments. I should have addressed them all.
-awaiting-author

j-loreaux

Thanks!

bors d+

Mathlib/Analysis/Normed/Module/ContinuousInverse.lean

mathlib-bors · 2026-02-11T19:34:14Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

grunweg · 2026-02-11T22:37:43Z

Thank you for the quick review! Did I say this is great? It makes a lot of a difference when contribution a stack of PRs (like mine).
bors merge

…inuousinverse (#34991) Define continuous linear maps which admit a continuous left resp. right inverse, prove their basic properties (closure under products, composition and continuous linear equivalences admitting both inverses) and a sufficient condition in finite dimension. A future PRs will add an equivalent characterisation of maps with a continuous left inverse, and use this to prove that the composition of immersions (resp. submersions) is an immersion (resp. submersion). Part of the path towards immersions, submersions, embedded submanifolds and the regular value theorem.

mathlib-bors · 2026-02-11T22:50:53Z

Pull request successfully merged into master.

Build succeeded:

…inuousinverse (leanprover-community#34991) Define continuous linear maps which admit a continuous left resp. right inverse, prove their basic properties (closure under products, composition and continuous linear equivalences admitting both inverses) and a sufficient condition in finite dimension. A future PRs will add an equivalent characterisation of maps with a continuous left inverse, and use this to prove that the composition of immersions (resp. submersions) is an immersion (resp. submersion). Part of the path towards immersions, submersions, embedded submanifolds and the regular value theorem.

grunweg added 6 commits February 8, 2026 18:49

First version

0ac7234

Prove sorries

709e098

Generalise last typeclasses

8c9191c

Final docs fixes

ebd320a

Add material for left inverses

5ba9caa

TODO about relation to a closed complement

37d93e4

grunweg added the t-analysis Analysis (normed *, calculus) label Feb 8, 2026

chrisflav reviewed Feb 8, 2026

View reviewed changes

Mathlib/Analysis/Normed/Module/ContinuousInverse.lean Show resolved Hide resolved

themathqueen reviewed Feb 8, 2026

View reviewed changes

Mathlib/Analysis/NormedSpace/ContinuousInverse.lean Outdated Show resolved Hide resolved

themathqueen reviewed Feb 8, 2026

View reviewed changes

Mathlib/Analysis/NormedSpace/ContinuousInverse.lean Outdated Show resolved Hide resolved

grunweg added 3 commits February 8, 2026 21:35

Rename: HasBounded{Left,Right}Inverse -> Has{Left,Right}Inverse

f2ae09e

Review comments

3d2204a

More review comments; add left results to the module doc-string also

915b791

Move

36442a2

This was referenced Feb 9, 2026

[Merged by Bors] - feat: equivalent characterisation of split continuous linear maps #35057

Closed

feat: analytification of schemes (affine case) #34626

Open

Fixup rename

047aba7

j-loreaux reviewed Feb 10, 2026

View reviewed changes

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

grunweg and others added 2 commits February 10, 2026 23:31

Apply suggestions from code review

328f1ff

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Review comments

6301963

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 10, 2026

grunweg added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 11, 2026

j-loreaux reviewed Feb 11, 2026

View reviewed changes

Mathlib/Analysis/Normed/Module/ContinuousInverse.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 11, 2026

Apply suggestion from @j-loreaux

b3eca25

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

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

mathlib-bors bot changed the title ~~feat: continuous linear maps with a continuous left/right inverseContinuousinverse~~ [Merged by Bors] - feat: continuous linear maps with a continuous left/right inverseContinuousinverse Feb 11, 2026

mathlib-bors bot closed this Feb 11, 2026

grunweg deleted the continuousinverse branch February 11, 2026 23:17

Conversation

grunweg commented Feb 8, 2026

Uh oh!

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

Uh oh!

PR summary 8115783e28

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Feb 8, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Feb 10, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 11, 2026

Uh oh!

grunweg commented Feb 11, 2026

Uh oh!

mathlib-bors bot commented Feb 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Feb 8, 2026 •

edited

Loading