Skip to content

feat: a SliceModel typeclass for models with corners for embedded submanifolds#26087

Open
grunweg wants to merge 27 commits intoleanprover-community:masterfrom
grunweg:MR-slicemodels2
Open

feat: a SliceModel typeclass for models with corners for embedded submanifolds#26087
grunweg wants to merge 27 commits intoleanprover-community:masterfrom
grunweg:MR-slicemodels2

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jun 18, 2025 •
edited
Loading

We define a new typeclass to denote a model with corners which "embeds" into another one:
there are an embedding of the underlying topological spaces and a continuous linear inclusion between the normed spaces,
which are compatible with the maps given by the models with corners.

This condition is used for defining smooth (immersed and embedded) submanifolds: for M to be a submanifold of N,
to boot their models with corners should be slice models. This will be defined in a future PR.

To prove this definition is workable, we construct many basic instances of slice models

  • each model with corners is one over itself
  • slice models are transitive
  • each model with corners I embeds into two products I.prod J and J.prod I
  • Euclidean n-half-space embeds into Euclidean n-space
  • a Euclidean n-quadrant embeds into Euclidean half-space (hence into Euclidean n-space)
  • if n\leq m, Euclidean n-space embeds into Euclidean m-space

zulip discussion

This PR continues the work from #25505.

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jun 18, 2025

Comments from Original PR #25505

This section contains 1 comment(s) from the original PR, excluding bot comments.

@github-actions (2025-06-05 23:38 UTC):

PR summary 8b2141b23d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Manifold.SliceModel (new file) 1

Declarations diff

+ EuclideanSpace.finAddEquivProd
+ EuclideanSpace.sumEquivProd
+ SliceModel
+ SliceModel.ofEmbedding
+ instTrans
+ instance (h : (E × F) ≃L[𝕜] E') : SliceModel F (𝓘(𝕜, E)) (𝓘(𝕜, E'))
+ 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 : ℕ} [NeZero n] :
+ inverse
+ inverse_left_inv
+ inverse_right_inv
+ prodAssoc
+ prodAssoc_apply
+ prodAssoc_symm_apply
+ prodAssoc_toEquiv
+ prodAssoc_toLinearEquiv
+ prodUnique
+ prodUnique_apply
+ prodUnique_symm_apply
+ prodUnique_toEquiv
++ instance {n : ℕ} [NeZero n] :

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

@grunweg grunweg mentioned this pull request Jun 18, 2025
Closed
4 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 18, 2025 •
edited
Loading

PR summary 24d904ee7b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Manifold.SliceModel (new file) 2254

Declarations diff

+ SliceModel
+ SliceModel.modelWithCornersSelf
+ SliceModel.ofEmbedding
+ 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
++ instance {n : ℕ} [NeZero n] :

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

@github-actions github-actions bot added the t-differential-geometry Manifolds etc label Jun 18, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 18, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 24, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

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

This PR/issue depends on:

@grunweg grunweg mentioned this pull request Jun 25, 2025
Draft
2 tasks
@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 17, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

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

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

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Jan 30, 2026
grunweg added a commit to grunweg/mathlib4 that referenced this pull request Jan 30, 2026
@grunweg
Cherry-pick leanprover-community#26087. A SliceModel typeclass, for m…
0cfd3ee 
…odels with corners in embedded submanifolds
@grunweg grunweg mentioned this pull request Jan 30, 2026
Open
4 tasks
@grunweg grunweg mentioned this pull request Feb 15, 2026
Closed
1 task
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

t-differential-geometry Manifolds etc

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