[Merged by Bors] - 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 bb7d1ba4d9

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

Declarations diff (regex)

+ IsSubmersion
+ IsSubmersionAt
+ IsSubmersionAtOfComplement
+ IsSubmersionOfComplement
+ SubmersionAtProp
+ _root_.isOpen_isSubmersionAt
+ _root_.isOpen_isSubmersionAtOfComplement
+ 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
+ instance (h : IsSubmersionAt I J n f x) : NormedSpace 𝕜 h.complement
+ 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_F
++ congr_of_eventuallyEq
++ domChart
++ domChart_mem_maximalAtlas
++ equiv
++ id
++ image_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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit bb7d1ba).

+70 new declarations
−0 removed declarations

+Manifold.IsSubmersion
+Manifold.IsSubmersion.complement
+Manifold.IsSubmersion.id
+Manifold.IsSubmersion.instNormedAddCommGroupComplement
+Manifold.IsSubmersion.instNormedSpaceComplement
+Manifold.IsSubmersion.isSubmersionAt
+Manifold.IsSubmersion.isSubmersionOfComplement_complement
+Manifold.IsSubmersion.prodMap
+Manifold.IsSubmersionAt
+Manifold.IsSubmersionAt.codChart
+Manifold.IsSubmersionAt.codChart_mem_maximalAtlas
+Manifold.IsSubmersionAt.complement
+Manifold.IsSubmersionAt.congr_iff
+Manifold.IsSubmersionAt.congr_of_eventuallyEq
+Manifold.IsSubmersionAt.domChart
+Manifold.IsSubmersionAt.domChart_mem_maximalAtlas
+Manifold.IsSubmersionAt.equiv
+Manifold.IsSubmersionAt.image_target_subset_target
+Manifold.IsSubmersionAt.instNormedAddCommGroupComplement
+Manifold.IsSubmersionAt.instNormedSpaceComplement
+Manifold.IsSubmersionAt.isSubmersionAtOfComplement_complement
+Manifold.IsSubmersionAt.mem_codChart_source
+Manifold.IsSubmersionAt.mem_domChart_source
+Manifold.IsSubmersionAt.mk_of_charts
+Manifold.IsSubmersionAt.mk_of_continuousAt
+Manifold.IsSubmersionAt.prodMap
+Manifold.IsSubmersionAt.property
+Manifold.IsSubmersionAt.source_subset_preimage_source
+Manifold.IsSubmersionAt.target_subset_preimage_target
+Manifold.IsSubmersionAt.writtenInCharts
+Manifold.IsSubmersionAtOfComplement
+Manifold.IsSubmersionAtOfComplement.codChart
+Manifold.IsSubmersionAtOfComplement.codChart.congr_simp
+Manifold.IsSubmersionAtOfComplement.codChart_mem_maximalAtlas
+Manifold.IsSubmersionAtOfComplement.congr_F
+Manifold.IsSubmersionAtOfComplement.congr_iff_of_eventuallyEq
+Manifold.IsSubmersionAtOfComplement.congr_of_eventuallyEq
+Manifold.IsSubmersionAtOfComplement.domChart
+Manifold.IsSubmersionAtOfComplement.domChart.congr_simp
+Manifold.IsSubmersionAtOfComplement.domChart_mem_maximalAtlas
+Manifold.IsSubmersionAtOfComplement.equiv
+Manifold.IsSubmersionAtOfComplement.equiv.congr_simp
+Manifold.IsSubmersionAtOfComplement.image_target_subset_target
+Manifold.IsSubmersionAtOfComplement.instNormedAddCommGroupSmallComplement
+Manifold.IsSubmersionAtOfComplement.instNormedSpaceSmallComplement
+Manifold.IsSubmersionAtOfComplement.isSubmersionAt
+Manifold.IsSubmersionAtOfComplement.mem_codChart_source
+Manifold.IsSubmersionAtOfComplement.mem_domChart_source
+Manifold.IsSubmersionAtOfComplement.mk_of_charts
+Manifold.IsSubmersionAtOfComplement.mk_of_continuousAt
+Manifold.IsSubmersionAtOfComplement.prodMap
+Manifold.IsSubmersionAtOfComplement.property
+Manifold.IsSubmersionAtOfComplement.small
+Manifold.IsSubmersionAtOfComplement.smallComplement
+Manifold.IsSubmersionAtOfComplement.smallEquiv
+Manifold.IsSubmersionAtOfComplement.source_subset_preimage_source
+Manifold.IsSubmersionAtOfComplement.target_subset_preimage_target
+Manifold.IsSubmersionAtOfComplement.trans_F
+Manifold.IsSubmersionAtOfComplement.writtenInCharts
+Manifold.IsSubmersionOfComplement
+Manifold.IsSubmersionOfComplement.congr_F
+Manifold.IsSubmersionOfComplement.id
+Manifold.IsSubmersionOfComplement.isSubmersion
+Manifold.IsSubmersionOfComplement.isSubmersionAt
+Manifold.IsSubmersionOfComplement.prodMap
+Manifold.IsSubmersionOfComplement.trans_F
+Manifold.SubmersionAtProp
+Manifold.isLocalSourceTargetProperty_submmersionAtProp
+isOpen_isSubmersionAt
+isOpen_isSubmersionAtOfComplement

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

Current number	Change	Type (strong)
5676	1	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit bb7d1ba4d9
Reference commit d925b897b5

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

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.

grunweg · 2026-05-18T08:06:43Z

It seems this Pr is ready for review again. @chrisflav

chrisflav

Modulo one comment, LGTM!

chrisflav · 2026-06-10T18:00:29Z

Great, thanks!

maintainer merge

github-actions · 2026-06-10T18:00:56Z

🚀 Pull request has been placed on the maintainer queue by chrisflav.

sgouezel

bors d+
Thanks!

mathlib-bors · 2026-06-10T19:27:24Z

✌️ Marygold-Dusk can now approve this pull request until 2026-06-24 19:27 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

Marygold-Dusk · 2026-06-11T08:46:14Z

bors r+

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> Co-authored-by: Samantha M. Naranjo <naranjosamantha1j@gmail.com> Co-authored-by: Samantha Naranjo <naranjosamantha1j@gmail.com>

mathlib-bors · 2026-06-11T09:04:36Z

Pull request successfully merged into master.

Build succeeded:

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> Co-authored-by: Samantha M. Naranjo <naranjosamantha1j@gmail.com> Co-authored-by: Samantha Naranjo <naranjosamantha1j@gmail.com>

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 Outdated

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

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 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 18, 2026

mathlib-triage Bot unassigned grunweg and PatrickMassot Jun 9, 2026

grunweg reviewed Jun 10, 2026

View reviewed changes

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

chrisflav approved these changes Jun 10, 2026

View reviewed changes

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

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

Marygold-Dusk added 2 commits June 10, 2026 14:12

congr

0da5f13

Merge branch 'master' into submersion_basic

f07a5b4

Marygold-Dusk requested a review from chrisflav June 10, 2026 12:32

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 10, 2026

sgouezel reviewed Jun 10, 2026

View reviewed changes

Marygold-Dusk added 2 commits June 11, 2026 10:13

a few comments

81879df

Merge branch 'master' into submersion_basic

bb7d1ba

mathlib-bors Bot changed the title ~~feat: define C^n submersions~~ [Merged by Bors] - feat: define C^n submersions Jun 11, 2026

mathlib-bors Bot closed this Jun 11, 2026

Marygold-Dusk mentioned this pull request Jun 12, 2026

[Merged by Bors] - feat: submersions are C^n #40547

Closed

Uh oh!

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 bb7d1ba4d9

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

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!

grunweg commented May 18, 2026

Uh oh!

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

chrisflav commented Jun 10, 2026

Uh oh!

github-actions Bot commented Jun 10, 2026

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors Bot commented Jun 10, 2026

Uh oh!

Marygold-Dusk commented Jun 11, 2026

Uh oh!

mathlib-bors Bot commented Jun 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

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