feat: a `SliceModel` typeclass for models with corners for embedded submanifolds by grunweg · Pull Request #25505 · leanprover-community/mathlib4

grunweg · 2025-06-05T23:37:29Z

TODO: write a proper PR description (once things settle down a bit, and the dependent PRs have landed)
Then ask e.g. Sebastien for review.

One sorry left, about embeddings between subtypes.

Rebased and extended version of #24550:

on the current master branch
does not import the definition of smooth immersions/embeddings: this only defines slice models (no more)

depends on: feat: ContinuousLinearEquiv.{prodUnique,uniqueProd} #23971
depends on: chore: add ContinuousLinearEquiv.prodAssoc #25522
depends on: feat: EuclideanSpace.finAddEquivProd #25524
depends on: [Merged by Bors] - feat: is{Inducing,Embedding}_prodMkLeft #25705

github-actions · 2025-06-05T23:38:41Z

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

mathlib4-dependent-issues-bot · 2025-06-06T03:35:09Z

This PR/issue depends on:

grunweg · 2025-06-18T13:00:41Z

This PR has been migrated to a fork-based workflow: #26087

@peabrainiac

I need this for #25505 (to show that R^n is a submanifold of R^m for n \leq m) and for my bordism theory branch. Previous zulip discussions: - [#Is there code for X? > Product of Euclidean spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Product.20of.20Euclidean.20spaces/near/500124944) - [#mathlib4 > Create `LinearIsometryEquiv` with `WithLp 2 (α × β)` and.. @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Create.20.60LinearIsometryEquiv.60.20with.20.60WithLp.202.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.20and.2E.2E/near/505938119) - [#mathlib4 > Manifold structure on Moebius strip @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Manifold.20structure.20on.20Moebius.20strip/near/522156122) Co-authored-by: @peabrainiac

@peabrainiac

I need this for leanprover-community#25505 (to show that R^n is a submanifold of R^m for n \leq m) and for my bordism theory branch. Previous zulip discussions: - [#Is there code for X? > Product of Euclidean spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Product.20of.20Euclidean.20spaces/near/500124944) - [#mathlib4 > Create &leanprover-community#96;LinearIsometryEquiv&leanprover-community#96; with &leanprover-community#96;WithLp 2 (α × β)&leanprover-community#96; and.. @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Create.20.60LinearIsometryEquiv.60.20with.20.60WithLp.202.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.20and.2E.2E/near/505938119) - [#mathlib4 > Manifold structure on Moebius strip @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Manifold.20structure.20on.20Moebius.20strip/near/522156122) Co-authored-by: @peabrainiac

@peabrainiac

I need this for leanprover-community#25505 (to show that R^n is a submanifold of R^m for n \leq m) and for my bordism theory branch. Previous zulip discussions: - [#Is there code for X? > Product of Euclidean spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Product.20of.20Euclidean.20spaces/near/500124944) - [#mathlib4 > Create &leanprover-community#96;LinearIsometryEquiv&leanprover-community#96; with &leanprover-community#96;WithLp 2 (α × β)&leanprover-community#96; and.. @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Create.20.60LinearIsometryEquiv.60.20with.20.60WithLp.202.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.20and.2E.2E/near/505938119) - [#mathlib4 > Manifold structure on Moebius strip @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Manifold.20structure.20on.20Moebius.20strip/near/522156122) Co-authored-by: @peabrainiac

@peabrainiac

I need this for leanprover-community#25505 (to show that R^n is a submanifold of R^m for n \leq m) and for my bordism theory branch. Previous zulip discussions: - [#Is there code for X? > Product of Euclidean spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Product.20of.20Euclidean.20spaces/near/500124944) - [#mathlib4 > Create &leanprover-community#96;LinearIsometryEquiv&leanprover-community#96; with &leanprover-community#96;WithLp 2 (α × β)&leanprover-community#96; and.. @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Create.20.60LinearIsometryEquiv.60.20with.20.60WithLp.202.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.20and.2E.2E/near/505938119) - [#mathlib4 > Manifold structure on Moebius strip @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Manifold.20structure.20on.20Moebius.20strip/near/522156122) Co-authored-by: @peabrainiac

grunweg added 5 commits June 6, 2025 00:35

wip: add slicemodel file from the current branch

a651e26

chore: copy over product of Euclidean spaces

f52f8e0

feat: add ContinuousLinearEquiv.prodCongr

2be8036

Prove some sorries

f7c7ea9

Application for the product of Euclidean spaces

58b8e86

grunweg added WIP Work in progress t-differential-geometry Manifolds etc labels Jun 5, 2025

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 6, 2025

grunweg mentioned this pull request Jun 6, 2025

chore: add ContinuousLinearEquiv.prodAssoc #25522

Closed

grunweg added 5 commits June 6, 2025 08:56

Note two more upstream PRs

7c20b57

One more missing map

dba21e0

One API lemma, progress

f4e2c46

Further

4f9a5e0

Enough for now

28f339e

grunweg mentioned this pull request Jun 6, 2025

feat: EuclideanSpace.finAddEquivProd #25524

Closed

grunweg changed the title ~~Mr slicemodels2~~ feat: a SliceModel typeclass for models with corners for embedded submanifolds Jun 6, 2025

grunweg added 5 commits June 11, 2025 16:58

Fix one sorry

edf5065

wip

61da0c8

Merge branch 'master' into MR-slicemodels2

81a671c

Update for merged master

983dea2

Clean up and fix sorry: just one left

569835b

grunweg mentioned this pull request Jun 18, 2025

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

Open

4 tasks

grunweg added the migrated-to-fork label Jun 18, 2025

grunweg closed this Jun 18, 2025

grunweg mentioned this pull request Jun 18, 2025

[Merged by Bors] - feat: EuclideanSpace.finAddEquivProd #26086

Closed

grunweg deleted the MR-slicemodels2 branch June 18, 2025 17:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

feat: a `SliceModel` typeclass for models with corners for embedded submanifolds#25505
grunweg wants to merge 15 commits intomasterfrom
MR-slicemodels2

grunweg commented Jun 5, 2025 •

edited by github-actions bot

Loading

Uh oh!

github-actions bot commented Jun 5, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jun 6, 2025 •

edited

Loading

Uh oh!

grunweg commented Jun 18, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

grunweg commented Jun 5, 2025 • edited by github-actions bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8b2141b23d

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jun 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg commented Jun 18, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

grunweg commented Jun 5, 2025 •

edited by github-actions bot

Loading

github-actions bot commented Jun 5, 2025 •

edited

Loading

mathlib4-dependent-issues-bot commented Jun 6, 2025 •

edited

Loading