Skip to content

feat: immersed submanifolds - #26391

Draft
grunweg wants to merge 88 commits into
leanprover-community:masterfrom
grunweg:MR-embedded-submanifolds-v3
Draft

feat: immersed submanifolds#26391
grunweg wants to merge 88 commits into
leanprover-community:masterfrom
grunweg:MR-embedded-submanifolds-v3

Conversation

@grunweg

@grunweg grunweg commented Jun 25, 2025 •
edited
Loading

Copy link
Copy Markdown
Contributor

grunweg added 30 commits March 17, 2025 22:41
@grunweg
feat: define immersions and smooth embeddings in infinite dimensions
4e1014d 
Sadly, we cannot prove most nice things about them yet, as we don't have
the inverse function theorem yet.
@grunweg
Tinygolf
8384948
@grunweg
Update Mathlib.lean; rename data fields
797ea58
@grunweg
WIP: refactor definition of IsImmersionAt, to be a Prop instead
6018681
@grunweg
fix: my definition of IsImmersionAt was too strong;
81fee7c 
I'd merely like to ask for equality on the source of the inverse extChart
@grunweg
Refactor definitions to be a Prop, state differentiability.
7ca8a5d
@grunweg
Prove/sketch congruence lemmas
aafff52
@grunweg
Re-order theorems, add missing assumption and re-use variables
bbe5603
@grunweg
XXX: is the composition of immersions an immersion?
f7ccb36 
In finite dimensions, that certainly holds; need to think about inf-dim
@grunweg
It seems the composition of immersions need not be an immersion.
fca6394 
The naive proof certainly fails (we get a coordinate change between the
two charts in the middle, which can be anything, and need not be linear at
all). Can we always "modify" a slice chart to match a modification downstairs?
I presume no, but would need to think...
@grunweg
Progress, enough for today
bf688fd
@grunweg
First version
2cc7999
@grunweg
A few basic lemmas
1e7b20f
@grunweg
Most basic API for ContinuousLinearMap.splits done: missing a proof o…
2572faa 
…f composition (coming next, after lunch)
@grunweg
Sketch some outline of Splits.comp
878b0b2
@grunweg
Enough for today: most of the API for 'splits on normed spaces' done
a9584ab
@grunweg
Move diffeomorphism results to MSplits(At); prove iff version of comp…
16b7fcc 
…osition lemmas with diffeos.
@grunweg
Last commits for today.
79b99eb
@grunweg
Delete bare Splits definition; just the manifold one suffices
671a26b
@grunweg
Progress towards 'composition of split map splits'. One direction of …
110d1e9 
…what I need is mostly in mathlib.
@grunweg
wip: set-up done
1782abf
@grunweg
WIP: missing helper lemma ContinuousLinearMap.equivRange_symm_apply
01a86c2
@grunweg
Almost done with the antilipschitz lemma
c9a2606
@grunweg
Just one sorry remaining, then my helper is done
074678c
@grunweg
Generalise and move up
2a5c2bf
@grunweg
Change
6e29970
@grunweg
Fix, courtesy of Ruben Van de Velde
0f8ec3c
@grunweg
Merge branch 'MR-cle-closedrange' into MR-define-immersions
75d44f5
@grunweg
Checkpoint
368ffaf
@grunweg
Note trouble with the .comp lemma
8f4ebd9
grunweg added 18 commits April 10, 2025 19:41
@grunweg
One local diffeomorphism sorry
335765e
@grunweg
Two missing API lemmas, and fix hypotheses order for dot notation.
c4cc682
@grunweg
fixup restore some proofs: comp order now matches remaining library
ed66124
@grunweg
Two easy sorries
6e80e2c
@grunweg
One more local diffeomorphism application is more tricky than I thought.
24f3584
@grunweg
chore: state ClosedCompleted.prod, which we want
5133404
@grunweg
Two more easy sorries
7a80e03
@grunweg
Add MSplits(At).prodMap, hint at proof for immersions
93f7c1d
@grunweg
Merge branch 'master' into MR-define-immersions
eaefc2a
@grunweg
chore: fix statements a bit
c500387 
Need to assume interior points for some of the statements,
and also n being at least 1. (If a map is not differential, its mfderiv certainly doesn't split.)
@grunweg
fix: add missing condition to the definition of immersions
1ae63e7 
Otherwise, proving continuity of immersions at boundary points runs into an
issue. This matches the definition in Roig-Domingues (and Lang seems to glance
over that issue/doesn't consider manifolds with boundary anyway), so should
be fine.
@grunweg
Small fixes and documentation tweaks.
8a0fe2d
@grunweg
Add SliceModel file; merge branch 'master' into MR-embedded-submanifo…
c253858 
…lds-v3
@grunweg
wip: towards a candidate definition of immersed submanifolds
152c1b7
@grunweg
checkpoint
7b090f2
@grunweg
Correct definition of the local inverse
1d9435f
@grunweg
Outline sorries for left and right inverse
3f476fb
@grunweg
One half of continuity proven; good enough
dd82c00
@grunweg grunweg added WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-differential-geometry Manifolds etc labels Jun 25, 2025
@github-actions

github-actions Bot commented Jun 25, 2025 •
edited
Loading

Copy link
Copy Markdown

PR summary f2e9b91e31

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.NormedSpace.HahnBanach.Splits (new file) 1882
Mathlib.Geometry.Manifold.MSplits (new file) 1982
Mathlib.Geometry.Manifold.IsImmersionEmbedding (new file) 1984
Mathlib.Geometry.Manifold.EmbeddedSubmanifold (new file) 2039

Declarations diff

+ ContinuousLinearMap.Splits
+ IsImmersedSubmanifold
+ IsImmersion
+ IsImmersionAt
+ IsSmoothEmbedding
+ MSplits
+ MSplitsAt
+ SliceModel
+ SliceModel.modelWithCornersSelf
+ SliceModel.ofEmbedding
+ Submodule.ClosedComplemented.prod
+ Submodule.sum_assoc
+ _root_.ContinuousLinearEquiv.splits
+ _root_.Diffeomorph.splits
+ _root_.Function.localInverseOn
+ _root_.Function.localInverseOn_invOn_of_injOn
+ _root_.IsLocalDiffeomorph.splits
+ _root_.IsLocalDiffeomorphAt.msplitsAt
+ _root_.PartialEquiv.pullback_sliceModel
+ _root_.Submodule.map_add
+ _root_.isImmersionAt_iff_msplitsAt
+ antilipschitzConstant
+ antilipschitzWith
+ antilipschitz_aux
+ chartedSpace
+ chartedSpace_of_nonempty
+ closedComplemented
+ codChart
+ codChart_mem_maximalAtlas
+ compCLE_left
+ compCLE_right
+ comp_diffeomorph_left_iff
+ comp_diffeomorph_right_iff
+ comp_isLocalDiffeomorphAt_left
+ comp_isLocalDiffeomorphAt_left_iff
+ comp_isLocalDiffeomorphAt_right
+ comp_isLocalDiffeomorphAt_right_iff
+ comp_isLocalDiffeomorph_left
+ comp_isLocalDiffeomorph_right
+ complement
+ complement_isClosed
+ complement_isCompl
+ congr_of_eventuallyEq
+ contMDiffAt
+ continuousOn_inverse_range
+ continuousWithinAt
+ disjoint_aux
+ domChart
+ domChart_mem_maximalAtlas
+ equiv
+ extend
+ extend_mfderiv_toContinousLinearEquiv
+ extend_mfderiv_toContinousLinearEquiv_coe
+ extend_symm
+ extend_symm_mfderiv_toContinousLinearEquiv
+ extend_symm_mfderiv_toContinousLinearEquiv_coe
+ injective
+ instTrans
+ instance : SliceModel (⊥ : Subspace 𝕜 E) I I
+ instance [h : SliceModel F I I'] : SliceModel F (I.prod J) (I'.prod J)
+ instance [h : SliceModel F I I'] : SliceModel F (J.prod I) (J.prod I')
+ instance {n m : ℕ} :
+ inverse
+ inverse_left_inv
+ inverse_right_inv
+ isClosedMap
+ isClosed_range
+ isEmbedding
+ isImmersion
+ isImmersionAt
+ map_target_subset_target
+ mdifferentiableAt
+ mdifferentiableAt_of_mfderiv_injective
+ mem_codChart_source
+ mem_domChart_source
+ mk_of_injective
+ msplitsAt
+ of_finiteDimensional_of_mfderiv_injective
+ of_injective_of_finiteDimensional'
+ of_injective_of_finiteDimensional_of_completeSpace
+ of_mfderiv_injective
+ of_mfderiv_injective_of_compactSpace_of_T2Space
+ prodAssoc
+ prodAssoc_apply
+ prodAssoc_symm_apply
+ prodAssoc_toEquiv
+ prodAssoc_toLinearEquiv
+ pull_sliceModel_source
+ pull_sliceModel_target
+ pullback_sliceModel
+ range_prodMap
+ writtenInCharts
++ contMDiff
++ continuousAt
++ instance {n : ℕ} [NeZero n] :
++ of_injective_of_finiteDimensional
+++ foo
+++ mfderiv_injective
++++ congr
+++++ prodMap
++++++ comp

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.

Increase in tech debt: (relative, absolute) = (2.00, 0.00)
Current number Change Type
840 2 erw

Current commit cf367500fe
Reference commit f2e9b91e31

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

mathlib4-dependent-issues-bot commented Jun 25, 2025

Copy link
Copy Markdown
Collaborator

This PR/issue depends on:

grunweg added 3 commits June 25, 2025 06:42
@grunweg
Progress: get a charted space
85cbed3
@grunweg
WIP: try removing non-emptiness hypotheses... harder than I thought
3ceab66 
- my construction only makes sense if H and M are both non-empty
- if both are empty, there is another construction
- *if* we knew M has a charted space, we'd deduce that non-emptiness of M
  implies that of M. but we do not know yet... need to think!
@grunweg
Revert "WIP: try removing non-emptiness hypotheses... harder than I t…
696ac29 
…hought"

This reverts commit 3ceab66.
@grunweg
grunweg force-pushed the MR-embedded-submanifolds-v3 branch from 8b8a4b4 to 696ac29 Compare June 25, 2025 13:37
@mathlib4-merge-conflict-bot 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 Nov 6, 2025
@mathlib4-merge-conflict-bot

mathlib4-merge-conflict-bot commented Nov 6, 2025

Copy link
Copy Markdown
Collaborator

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-differential-geometry Manifolds etc WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@grunweg @mathlib4-dependent-issues-bot @mathlib4-merge-conflict-bot