feat: manifolds with smooth boundary by grunweg · Pull Request #22059 · leanprover-community/mathlib4

grunweg · 2025-02-18T20:16:03Z

Needs polish, and closing the remaining sorries (or deciding they can be postponed later).

From my bordism theory project.

github-actions · 2025-02-18T20:16:59Z

PR summary a6e6e20ceb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Manifold.HasSmoothBoundary` (new file)	1932

Declarations diff

+ BoundaryManifoldData
+ BoundaryManifoldData.Icc
+ BoundaryManifoldData.euclideanHalfSpace_self
+ BoundaryManifoldData.prod_Icc
+ BoundaryManifoldData.prod_of_boundaryless_right_model
+ BoundaryManifoldData.sum
+ BoundaryManifoldData.{u}
+ HasNiceBoundary
+ Homeomorph.finTwo
+ Homeomorph.foo
+ Homeomorph.sumEquivBoolProd
+ IsEmbedding.sum_elim_of_foo
+ contMDiff_congr
+ instance (bd : BoundaryManifoldData M I) [h : HasNiceBoundary bd] [BoundarylessManifold J N] :
+ instance (bd : BoundaryManifoldData N J) [HasNiceBoundary bd] [BoundarylessManifold I M] :
+ instance (d : BoundaryManifoldData M I k I₀) : ChartedSpace H₀ d.M₀ := d.chartedSpace
+ instance (d : BoundaryManifoldData M I k I₀) : IsManifold I₀ k d.M₀ := d.isManifold
+ instance (d : BoundaryManifoldData M I k I₀) : TopologicalSpace d.M₀ := d.topologicalSpace
+ instance (d : BoundaryManifoldData M I) : ChartedSpace d.H' (I.boundary M) := d.charts
+ instance (d : BoundaryManifoldData M I) : IsManifold d.model ⊤ (I.boundary M)
+ instance (d : BoundaryManifoldData M I) : NormedAddCommGroup d.E' := d.normedAddCommGroup
+ instance (d : BoundaryManifoldData M I) : NormedSpace ℝ d.E' := d.normedSpace
+ instance (d : BoundaryManifoldData M I) : TopologicalSpace d.H' := d.topologicalSpace
+ instance [BoundarylessManifold I M] :
+ manifolds
+ mfderiv_prod_map
+ mfderiv_sumMap_at_inl
+ mfderiv_sumMap_at_inr
+ missing
++ BoundaryManifoldData.of_Euclidean_halfSpace
++ BoundaryManifoldData.of_boundaryless
++ BoundaryManifoldData.prod_of_boundaryless_left
++ BoundaryManifoldData.prod_of_boundaryless_right

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

Not fully there yet, but all the easy tedious pieces are done

The necessary pieces are all in mathlib (for the open and/or the closed case), this is just a matter of putting them together. This comes up when constructing the smooth boundary of a disjoint union. Extracted from #22059; from my bordism theory project.

Extracted from #22059; from my bordism theory project. Co-authored-by: grunweg <[email protected]>

and move the empty charted space and the space over itself there. Also add a section around ModelProd and ModelPi.

…eton Step 3 of #5462, except that we need to prescribe non-emptiness, right?

We need to either require H to be Unique instead, or M to be empty iff H is.

This reverts commit f8f2c5d.

will replace this with a proof from a dependent PR

leanprover-community-bot-assistant · 2025-04-11T14:37:51Z

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

Part of my bordism theory project: these will be needed for #22059. Updated version of #22642.

mathlib4-dependent-issues-bot · 2025-10-29T01:14:04Z

This PR/issue depends on:

grunweg · 2025-11-07T09:20:23Z

This PR has been migrated to a fork: #31351

Part of my bordism theory project: these will be needed for leanprover-community#22059. Updated version of leanprover-community#22642.

grunweg added 7 commits February 18, 2025 19:33

Snapshot

28505b6

Compiles/sorried all broken proofs

4edf6ca

Revamp definition

e74615e

Progress

18b1ab9

Another definition compiles; make everything universe-polymorphic

f3d3dee

Fixing further; trying to complete one proof

1caa9fe

Down to one topology sorry

11c3dc8

grunweg added WIP Work in progress t-differential-geometry Manifolds etc labels Feb 18, 2025

grunweg mentioned this pull request Feb 18, 2025

[Merged by Bors] - feat: define singular manifolds #15906

Closed

grunweg added 6 commits February 18, 2025 21:49

Topology lemma

9365594

Progress in making things compile

26c10d6

A few more small sorries: code is revamped now

d429d2a

WIP: state the disjoint union of boundary data

96f235f

Not fully there yet, but all the easy tedious pieces are done

chore: move helper results to topology files

dcd8632

Missing docs; rename one field

60df139

grunweg mentioned this pull request Feb 19, 2025

[Merged by Bors] - feat: add Is{Open,Closed}Embedding.sum_elim #22070

Closed

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 Feb 19, 2025

grunweg added 3 commits February 19, 2025 15:41

Fix; re-use existing lemmas

4244b76

feat: isClosedMap_prod_mk_{left,right}

8e344b2

chore: fixup for the move

54f02fb

grunweg mentioned this pull request Feb 19, 2025

[Merged by Bors] - feat: isClosedMap_prodMk_{left,right} #22082

Closed

mathlib-bors bot pushed a commit that referenced this pull request Feb 19, 2025

feat: isClosedMap_prodMk_{left,right} (#22082)

5716f46

Extracted from #22059; from my bordism theory project. Co-authored-by: grunweg <[email protected]>

grunweg added 5 commits February 19, 2025 22:13

chore: create section Constructions

704aaf9

and move the empty charted space and the space over itself there. Also add a section around ModelProd and ModelPi.

feat: basic API for PartialHomeomorph.const

85af918

feat: a discrete space is a charted space over any non-empty subsingl…

ac12764

…eton Step 3 of #5462, except that we need to prescribe non-emptiness, right?

XXX: can we drop the non-emptiness hypothesis? No, we can't.

f8f2c5d

We need to either require H to be Unique instead, or M to be empty iff H is.

Revert "XXX: can we drop the non-emptiness hypothesis? No, we can't."

cf1e0a2

This reverts commit f8f2c5d.

Merge branch 'master' into MR-hassmoothboundary

4643294

github-actions 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 Feb 20, 2025

Fix merge

35bc0b9

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 24, 2025

grunweg added 7 commits February 26, 2025 18:30

Rename file

2e88257

Remove two TODOs

83de96c

Comment unused lemmas

c759c42

Fix foundational sorries in BoundaryManifoldData.sum: last sorry is easy

ec8d946

Remove partial progress towards IsEmbedding.sum_elim_of_sth:

1bdd1ff

will replace this with a proof from a dependent PR

Simplify, inconsequential

d6d2927

Merge branch 'master' into MR-hassmoothboundary

a6e6e20

github-actions 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 Feb 26, 2025

grunweg mentioned this pull request Mar 6, 2025

WIP: add mfderiv_prod and mfderiv_prodMap #22642

Closed

grunweg mentioned this pull request Mar 20, 2025

feat: (unoriented) bordism groups #23138

Closed

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 11, 2025

grunweg mentioned this pull request Sep 12, 2025

[Merged by Bors] - feat: add mfderiv_prod and mfderiv_prodMap #29589

Closed

1 task

mathlib-bors bot pushed a commit that referenced this pull request Oct 28, 2025

feat: add mfderiv_prod and mfderiv_prodMap (#29589)

50e084d

Part of my bordism theory project: these will be needed for #22059. Updated version of #22642.

mathlib-bors bot pushed a commit that referenced this pull request Oct 28, 2025

feat: add mfderiv_prod and mfderiv_prodMap (#29589)

c21bdba

Part of my bordism theory project: these will be needed for #22059. Updated version of #22642.

mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025

feat: add mfderiv_prod and mfderiv_prodMap (#29589)

2fe1cd3

Part of my bordism theory project: these will be needed for #22059. Updated version of #22642.

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 Oct 29, 2025

grunweg mentioned this pull request Nov 5, 2025

[Merged by Bors] - feat: mfderiv of Sum.inl and Sum.inr #31200

Closed

1 task

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 Nov 5, 2025

This was referenced Nov 7, 2025

feat: (unoriented) bordism groups #31350

Open

feat: manifolds with smooth boundary #31351

Open

grunweg closed this Nov 8, 2025

grunweg deleted the MR-hassmoothboundary branch November 8, 2025 09:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: manifolds with smooth boundary#22059

feat: manifolds with smooth boundary#22059
grunweg wants to merge 54 commits intomasterfrom
MR-hassmoothboundary

grunweg commented Feb 18, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Feb 18, 2025 •

edited

Loading

Declarations diff

Uh oh!

leanprover-community-bot-assistant commented Apr 11, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Oct 29, 2025 •

edited

Loading

Uh oh!

grunweg commented Nov 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

grunweg commented Feb 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary a6e6e20ceb

Import changes for modified files

Declarations diff

Uh oh!

leanprover-community-bot-assistant commented Apr 11, 2025

Uh oh!

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

Uh oh!

Uh oh!

grunweg commented Nov 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

grunweg commented Feb 18, 2025 •

edited

Loading

github-actions bot commented Feb 18, 2025 •

edited

Loading

mathlib4-dependent-issues-bot commented Oct 29, 2025 •

edited

Loading