feat: define C^n submersions by Marygold-Dusk · Pull Request #35122 · leanprover-community/mathlib4

Marygold-Dusk · 2026-02-11T10:14:00Z

This PR defines submersions between C^n manifolds. In the infinite-dimensional setting, submersions are defined via local normal forms rather than surjectivity of the mfderiv. A map f is a submersion at x if, in suitable charts around x and f x, it has the form (u, v) ↦ u after identifying the model space with a product.

We prove a few basic properties:

being a submersion is a local property,
products of submersions are submersions,
the set of submersed points is open

Future PRs will prove that submersions are C^n and deduce equivalence with the standard definition in finite dimensions. From the path towards the regular value theorem.

This file was developed under the supervision of Michael Rothgang.

Co-authored-by: Michael Rothgang rothgang@math.uni-bonn.de

Most of the design is analogues to immersions.

github-actions · 2026-02-11T10:15:13Z

PR summary 3138261609

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Manifold.Submersion` (new file)	2152

Declarations diff

+ IsSubmersion
+ IsSubmersionAt
+ IsSubmersionAtOfComplement
+ IsSubmersionOfComplement
+ SubmersionAtProp
+ _root_.isOpen_isSubmersionAt
+ _root_.isOpen_isSubmersionAt'
+ congr_iff
+ congr_iff_of_eventuallyEq
+ instance (h : IsSubmersion I J n f) : NormedAddCommGroup h.complement
+ instance (h : IsSubmersion I J n f) : NormedSpace 𝕜 h.complement
+ instance (h : IsSubmersionAt I J n f x) : NormedAddCommGroup h.complement := by
+ instance (h : IsSubmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
+ instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement
+ instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement
+ isLocalSourceTargetProperty_submmersionAtProp
+ isSubmersion
+ isSubmersionAtOfComplement_complement
+ isSubmersionOfComplement_complement
+ small
+ smallComplement
+ smallEquiv
++ codChart
++ codChart_mem_maximalAtlas
++ complement
++ congr
++ congr_F
++ congr_of_eventuallyEq
++ domChart
++ domChart_mem_maximalAtlas
++ equiv
++ id
++ map_target_subset_target
++ mem_codChart_source
++ mem_domChart_source
++ mk_of_charts
++ mk_of_continuousAt
++ property
++ source_subset_preimage_source
++ target_subset_preimage_target
++ trans_F
++ writtenInCharts
+++ isSubmersionAt
++++ prodMap

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

github-actions · 2026-02-11T10:15:16Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

…athlib4 into submersion_basic

grunweg

Two small comments I noticed already.

…athlib4 into submersion_basic

grunweg

I just tweaked the module doc-string, by comparing it closely with the immersions one. Some phrasings of yours I preferred (and copied to the immersions doc-string); some I disagree with stylistically. A few were slightly wrong, so I changed these also.

grunweg

Thanks for the PR! I looked at the code in detail, also comparing it to the Immersions file to make sure there are no unnecessary differences. I have a number of comments, but most of them are very minor.

grunweg · 2026-04-17T14:19:27Z

I pushed a fix for one of the backward options --- I'll be happy to walk you through it in person.

- remove superfluous noncomputable - golf one proof very slightly - a few wording improvements to the module doc-string (content-neutral) Noticed while reviewing #35122.

…y#38162) - remove superfluous noncomputable - golf one proof very slightly - a few wording improvements to the module doc-string (content-neutral) Noticed while reviewing leanprover-community#35122.

…athlib4 into submersion_basic

…y#38162) - remove superfluous noncomputable - golf one proof very slightly - a few wording improvements to the module doc-string (content-neutral) Noticed while reviewing leanprover-community#35122.

chrisflav

Thanks! Everything looks quite clean and as far as I can see, faithfully mirrors the Immersion file. I have left some comments below, feel free to ping me again when this is ready for review again.

chrisflav · 2026-05-06T12:19:08Z

+## Implementation notes
+
+* In most applications, there is no need to control the choice of complement in the definition of a
+  submersion, so `IsSubmersion(At)` is perfectly adequate. Nevertheless, explicit control over


I think we can safely refer to the (almost identical) implementation notes in the Immersion file here instead of repeating them.

chrisflav · 2026-05-06T12:49:04Z

+immersion or a submersion.
+Unless you have a particular reason, prefer to use `IsSubmersionAt` instead.
+-/
+irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=


Can we use @[no_expose] here instead of irreducible_def? With this the slightly unfortunate rw in a definition in domChart below would no longer be needed (you will also have to add a @[no_expose] there or just drop the @[expose] from the public section above).

I am aware that this is deviating from the Immersion implementation, but immersions might have landed before the module system switch.

irreducible_def works also without the module system; this was important for IsImmersion.prod at some point...

Making lots of things no_expose is nice, though. Hm...

I don't understand the statement about IsImmersion.prod. What do you mean by "this was important"? We won't remove the module system anytime soon.

This is how the analogous change for immersions would look: #39002
If not for the module system questions, I'd take it immediately.

After some thought, I think this PR should make the changes analogous to #39002.
@Marygold-Dusk I'll be happy to walk to through that PR tomorrow.

chrisflav · 2026-05-06T12:54:43Z

+/-- If `f = g` and `f` is a submersion, so is `g`. -/
+theorem congr (h : IsSubmersionOfComplement F I J n f) (heq : f = g) :


I don't think this lemma is necessary (I think I made the same remark for Immersions back then). What was the reason why it was still added?

I believe it was "you didn't care strongly about having it and I didn't care strongly about changing the PR". I'm happy to drop it (also from immersions) if you prefer.

Now you should have some more practical experience with this definition: Did you ever use this lemma?

Instead of using an `irreducible_def`, make it an unexposed definition. This has the same effect in other modules, but leads to much shorter code as we can remove all `rw [foo_def]` for the immersion definitions. It also allows removing the `@[expose]` section from the file (which is nice). There is a small downside: in downstream projects not using the module system, the definition of immersions will be unfolded now. At this point, this is a mostly hypothetical risk (and weighs lower than the real benefits of this change). The [discussion](#28793 (comment)) leading to this change did not have substantial evidence either. Inspired by the discussion in #35122.

Submersions

c93d43b

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 11, 2026

github-actions Bot added the t-differential-geometry Manifolds etc label Feb 11, 2026

Marygold-Dusk changed the title ~~submersions between manifolds~~ feat(geometry/manifold): define C^n submersions Feb 11, 2026

grunweg added 3 commits February 11, 2026 12:03

Fix CI

5a3f3e5

Extend documentation

5b29a7d

Golf a proof

143933d

grunweg self-assigned this Feb 11, 2026

grunweg changed the title ~~feat(geometry/manifold): define C^n submersions~~ feat: define C^n submersions Feb 11, 2026

Marygold-Dusk added 4 commits February 11, 2026 13:42

add docstrings to submersion definitions

19aabd5

Merge branch 'submersion_basic' of https://github.com/Marygold-Dusk/m…

dd4d176

…athlib4 into submersion_basic

remove #check

529465e

Merge branch 'master' into submersion_basic

0349e85

mathlib-triage Bot assigned PatrickMassot Mar 17, 2026

grunweg reviewed Mar 20, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Manifold/Submersion.lean Outdated

Comment thread Mathlib/Geometry/Manifold/Submersion.lean Outdated

mathlib-triage Bot unassigned grunweg Mar 22, 2026

Marygold-Dusk and others added 7 commits March 26, 2026 09:45

Remove immersions

750c454

Merge branch 'submersion_basic' of https://github.com/Marygold-Dusk/m…

68f76fe

…athlib4 into submersion_basic

Merge branch 'master' into submersion_basic

a3357ea

Merge branch 'master' into submersion_basic

fc4747d

tranparency

798e0cb

chore: wording tweaks for immersion module doc-string

db60057

chore: tweak module doc-string

84f810d

grunweg reviewed Apr 17, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Manifold/Submersion.lean

Comment thread Mathlib/Geometry/Manifold/Submersion.lean

grunweg reviewed Apr 17, 2026

View reviewed changes

grunweg mentioned this pull request Apr 17, 2026

[Merged by Bors] - chore(Geometry/Manifold/Immersion): minor tweaks #38162

Closed

chore: fix one use of backward.isDefEq.respectTransparency option

0be990f

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 17, 2026

grunweg self-assigned this Apr 17, 2026

some corrections

9f85b77

Marygold-Dusk added 4 commits May 4, 2026 14:34

doc-strings and other minor tweaks

84c649f

Merge branch 'master' into submersion_basic

8050623

comment

50d9d45

Merge branch 'submersion_basic' of https://github.com/Marygold-Dusk/m…

2675e8f

…athlib4 into submersion_basic

Merge branch 'master' into submersion_basic

2a3d1c1

grunweg reviewed May 6, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Manifold/Submersion.lean Outdated

Superfluous newline

62bc8fc

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 6, 2026

chrisflav self-requested a review May 6, 2026 08:48

chrisflav reviewed May 6, 2026

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label May 6, 2026

grunweg added 2 commits May 6, 2026 15:20

chore: use no_expose instead

6cb5820

wip: no_expose'ing IsSubmersion creates issues with the instance below

f7ce3f1

grunweg mentioned this pull request May 6, 2026

[Merged by Bors] - refactor: don't expose definitions of immersions #39002

Closed

chore: add schmeding reference

5417e2d

		/-- If `f = g` and `f` is a submersion, so is `g`. -/
		theorem congr (h : IsSubmersionOfComplement F I J n f) (heq : f = g) :

Conversation

Marygold-Dusk commented Feb 11, 2026 • edited by chrisflav Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 3138261609

Import changes for modified files

Declarations diff

Uh oh!

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

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg 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!

Uh oh!

Uh oh!

grunweg commented Apr 17, 2026

Uh oh!

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

chrisflav May 6, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

chrisflav May 6, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg May 6, 2026

Choose a reason for hiding this comment

Uh oh!

chrisflav May 6, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg May 6, 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!

grunweg May 7, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

chrisflav May 6, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg May 6, 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!

chrisflav May 6, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Marygold-Dusk commented Feb 11, 2026 •

edited by chrisflav

Loading

github-actions Bot commented Feb 11, 2026 •

edited

Loading

github-actions Bot commented Feb 11, 2026 •

edited

Loading

grunweg May 6, 2026 •

edited

Loading

grunweg May 6, 2026 •

edited

Loading