feat(Geometry/Manifold): the interior of a manifold is open

[peabrainiac]

Show that the interior and boundary of manifolds are well-defined in the sense that the definition of interior points does not depend on a choice of chart, and conclude that the interior and boundary of manifolds are open resp. closed.

We only do this for $C^1$ manifolds because while it holds for finite-dimensional topological manifolds too, it is not clear to me whether it holds for infinite-dimensional topological manifolds, so that the finite-dimensional topological case probably needs to be treated separately from this infinite-dimensional $C^1$ case anyway.

---

• depends on: feat(Geometry/Manifold): API for extended coordinate changes #35391

[github-actions]

PR summary 6a39ceeb91

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary	2182	2189	+7 (+0.32%)

Import changes for all files

Files	Import difference
3 files Mathlib.Geometry.Manifold.Riemannian.Basic Mathlib.Geometry.Manifold.Riemannian.PathELength Mathlib.Geometry.Manifold.WhitneyEmbedding	1
3 files Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Topology.Compactification.OnePoint.Sphere	6
4 files Mathlib.Geometry.Manifold.Bordism Mathlib.Geometry.Manifold.Instances.Icc Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary	7

---

Declarations diff

+ _root_.DifferentiableAt.mem_interior_convex_of_surjective_fderiv
+ contDiffOn_extCoordChange
+ contDiffOn_extCoordChange_symm
+ extCoordChange
+ extCoordChange_symm
+ isBoundaryPoint_iff_of_mem_atlas
+ isClosed_boundary
+ isInteriorPoint_iff_of_mem_atlas
+ isInvertible_fderivWithin_extCoordChange
+ isOpen_interior
+ mem_frontier_iff_notMem_interior
+ mem_interior_iff_notMem_frontier
+ uniqueDiffOn_extCoordChange_source
+ uniqueDiffOn_extCoordChange_target

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 scripts/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]

Thanks a lot for your PR! This is a welcome surprise, a bit like an unanticipated Christmas present, received two days early. I took a first look and have mostly minor comments about polish and making the code more maintainable.

[grunweg]

Thanks, I really like where this is going. I have a few more nits. (Otherwise, it's probably good... I just need to find the time to sit down with this PR in a quiet moment. Hopefully, I'll have time at the end of next week.)

[grunweg]

This should be called extendCoordChange.
I also think we should use it in contDiffOn_extend_coord_change (and perhaps rename that one as ContDiffOn.extendCoordChange)... I'm not sure if this will have further fall-out in mathlib; maybe that alone should be a previous PR.

[peabrainiac]

Are you sure it should? It looks like both extend_coord_change and ext_coord_change currently appear in mathlib lemmas, so I imagined either name would be fine - and extCoordChange fits extChartAt, so I somewhat prefer it.

About using the API in existing lemmas like contDiffOn_extend_coord_change, would you be okay with leaving that to a follow-up PR? I think you're right that it would've been nice to do that in an earlier PR already, but seeing as we already have two PRs depending on this one now, it would be nice to get this unblocked instead of opening yet another prerequisite PR.

[grunweg]

I would expect extCoordChange to be about extChartAt, whereas this definition is about extending any chart - so yes, I am sure :-) (Actually checking with the existing names confirms this.)

[grunweg]

My hope is that the other PR can go in quickly, and then won't block this for long. Can we try that, and if it takes longer than a few days, I'll be happy to merge this PR as-is?

[grunweg]

I look forward for orientations to be merged into mathlib, but I'm not sure if this is as critical. From my perspective, other work depending on this PR... well, happens. As long as everything is moving reasonably fast, I have learned to live with it.

[peabrainiac]

I see - I hadn't realised that the difference between ext_coord_change and extend_coord_change lemmas is whether they were are about extChartAt or general extended charts, I thought it was just inconsistent.

I've opened a separate PR for this now.

[grunweg]

Hopefully my last set of comments!

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Geometry/Manifold): API for extended coordinate changes #35391
  By Dependent Issues (🤖). Happy coding!