From f745a1dd06254ccd9fd023364fb3ec7495f492f6 Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Mon, 22 Dec 2025 06:42:34 +0100 Subject: [PATCH 01/11] main lemma --- .../Manifold/IsManifold/InteriorBoundary.lean | 147 ++++++++++++++++++ 1 file changed, 147 insertions(+) diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index e0d66b171e1930..b78f6f13699ffb 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -5,6 +5,8 @@ Authors: Michael Rothgang -/ module +public import Mathlib.Analysis.Calculus.LocalExtr.Basic +public import Mathlib.Analysis.LocallyConvex.Separation public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt /-! @@ -197,6 +199,151 @@ lemma Boundaryless.of_boundary_eq_empty (h : I.boundary M = ∅) : BoundarylessM end BoundarylessManifold +section ChartIndependence + +lemma mem_interior_iff_notMem_frontier {X : Type*} [TopologicalSpace X] {s : Set X} {x : X} + (hx : x ∈ s) : x ∈ interior s ↔ x ∉ frontier s := by + simp [← self_diff_frontier, hx] + +lemma mem_frontier_iff_notMem_interior {X : Type*} [TopologicalSpace X] {s : Set X} {x : X} + (hx : x ∈ s) : x ∈ frontier s ↔ x ∉ interior s := by + simp [← self_diff_frontier, hx] + +/-- The change of charts from `e` to `e'` in the model vector space `E`. -/ +@[simps!] +def extCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E := + (e.extend I).symm.trans (e'.extend I) + +omit [ChartedSpace H M] in +lemma extCoordChange_symm {e e' : OpenPartialHomeomorph M H} : + (I.extCoordChange e e').symm = I.extCoordChange e' e := by + rfl + +lemma contDiffOn_extCoordChange {n : WithTop ℕ∞} {e e' : OpenPartialHomeomorph M H} + (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) : + ContDiffOn 𝕜 n (I.extCoordChange e e') (I.extCoordChange e e').source := + e'.contDiffOn_extend_coord_change he' he + +lemma contDiffOn_extCoordChange_symm {n : WithTop ℕ∞} {e e' : OpenPartialHomeomorph M H} + (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) : + ContDiffOn 𝕜 n (I.extCoordChange e e').symm (I.extCoordChange e e').target := + e.contDiffOn_extend_coord_change he he' + +omit [ChartedSpace H M] in +lemma uniqueDiffOn_extCoordChange_source {e e' : OpenPartialHomeomorph M H} : + UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by + rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter] + exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source + +omit [ChartedSpace H M] in +lemma uniqueDiffOn_extCoordChange_target {e e' : OpenPartialHomeomorph M H} : + UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by + rw [← extCoordChange_symm, PartialEquiv.symm_target] + exact uniqueDiffOn_extCoordChange_source + +lemma isInvertible_fderivWithin_extCoordChange {n : WithTop ℕ∞} + (hn : 1 ≤ n) {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) + (he' : e' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ (I.extCoordChange e e').source) : + (fderivWithin 𝕜 (I.extCoordChange e e') (I.extCoordChange e e').source x).IsInvertible := by + set φ := I.extCoordChange e e' + have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extCoordChange he he' + have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extCoordChange_symm he he' + refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_ + · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp _ + (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):) + ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) φ.symm_mapsTo + (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)), + fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx)] + exact fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)) + · rw [← fderivWithin_comp _ ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) + ((hφ _ hx).differentiableWithinAt hn) φ.mapsTo (I.uniqueDiffOn_extCoordChange_source _ hx), + fderivWithin_congr' φ.leftInvOn.eqOn hx, + fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ hx)] + +/-- A point `x` in a manifold that is at least C¹ is an interior point iff it gets mapped to the +interior of the model space by any given chart - i.e., the notion of interior points does not depend +on any choice of charts, so that talking about `ModelWithCorners.interior` actually makes sense. + +Note that in general, this is actually quite nontrivial; that is why are focusing only on C¹ +manifolds here. For merely topological finite-dimensional manifolds the proof involves singular +homology, and for infinite-dimensional topological manifolds I don't even know if this lemma holds. +-/ +lemma isInteriorPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] (hn : 1 ≤ n) + {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) : + I.IsInteriorPoint x ↔ e.extend I x ∈ interior (e.extend I).target := by + -- it suffices to show that if `x` is interior in one chart `e` it also is in any other chart `e'` + revert e + suffices h : ∀ e ∈ atlas H M, x ∈ e.source → ∀ e' ∈ atlas H M, x ∈ e'.source → + e.extend I x ∈ interior (e.extend I).target → e'.extend I x ∈ interior (e'.extend I).target by + rw [isInteriorPoint_iff] + exact fun e he hx ↦ ⟨h _ (chart_mem_atlas H x) (mem_chart_source H x) _ he hx, + h _ he hx _ (chart_mem_atlas H x) (mem_chart_source H x)⟩ + intro e he hex e' he' hex' hx + /- Since transition maps are diffeomorphisms, it suffices to show that if `e'` were to send `x` + to the boundary of `range I`, the differential of the transition map `φ` from `e` to `e'` at `x` + could not be surjective. -/ + let φ := (e.extend I).symm.trans (e'.extend I) + have hφ : ContDiffOn 𝕜 n φ φ.source := e'.contDiffOn_extend_coord_change + (IsManifold.subset_maximalAtlas he') (IsManifold.subset_maximalAtlas he) + have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := e.contDiffOn_extend_coord_change + (IsManifold.subset_maximalAtlas he) (IsManifold.subset_maximalAtlas he') + suffices h : e'.extend I x ∉ interior (range I) → + ¬Function.Surjective (fderivWithin 𝕜 φ φ.source (e.extend I x)) by + rw [not_imp_not] at h + refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_ + refine ContinuousLinearMap.IsInvertible.surjective ?_ + exact isInvertible_fderivWithin_extCoordChange hn (IsManifold.subset_maximalAtlas he) + (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex'] + intro hx' + /- Reduce the situation to the real case, then apply Hahn-Banach to `x` and `interior (range I)` + to get a functional `F` that is greater on `e'.extend I x` than on all of `interior (range I)`. -/ + wlog _ : IsRCLikeNormedField 𝕜 + · simp [I.range_eq_univ_of_not_isRCLikeNormedField ‹_›] at hx' + let _ := IsRCLikeNormedField.rclike 𝕜 + let _ := Module.compHom E (algebraMap ℝ 𝕜) + have : IsScalarTower ℝ 𝕜 E := ⟨by intros; rw [Algebra.smul_def, mul_smul]; rfl⟩ + let _ : NormedSpace ℝ E := { + norm_smul_le r x := (norm_smul_le (r : 𝕜) x).trans <| by simp } + have hφx : e.extend I x ∈ interior φ.source := by + simp_rw [φ, PartialEquiv.trans_source, PartialEquiv.symm_source, interior_inter, mem_inter_iff, + hx, true_and, e'.extend_source, mem_interior_iff_mem_nhds] + exact e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex' + rw [← ContinuousLinearMap.coe_restrictScalars' (R := ℝ), + (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ) + (uniqueDiffWithinAt_of_mem_nhds <| mem_interior_iff_mem_nhds.1 hφx), + fderivWithin_of_mem_nhds <| mem_interior_iff_mem_nhds.1 hφx] + have ⟨F, hF⟩ := geometric_hahn_banach_open_point I.convex_range.interior isOpen_interior hx' + -- It suffices to show that `fderiv ℝ φ (e.extend I x) y` sends everything to the kernel of `F`. + suffices h : ∀ y, F (fderiv ℝ φ (e.extend I x) y) = 0 by + have ⟨y, hy⟩ := I.nonempty_interior + unfold Function.Surjective; push_neg + refine ⟨e'.extend I x - y, fun z ↦ ne_of_apply_ne F ?_⟩ + rw [h z, F.map_sub] + exact (sub_pos.2 <| hF _ hy).ne + -- This follows from `F ∘ φ` taking on a local maximum at `e.extend I x`. + have hF' : ∀ y ∈ range I, F y ≤ F (e'.extend I x) := by + change MapsTo F _ (Iic _) + rw [← I.isClosed_range.closure_eq, ← closure_Iio, + ← I.convex_range.closure_interior_eq_closure_of_nonempty_interior I.nonempty_interior] + exact MapsTo.closure hF F.continuous + have hFφ : IsLocalMax (F ∘ φ) (e.extend I x) := + Filter.eventually_of_mem (mem_interior_iff_mem_nhds.1 hφx) fun y hy ↦ + (hF' (φ y) ((show φ.target ⊆ range I by simp [φ, inter_assoc]) (φ.mapsTo hy))).trans_eq <| + congr_arg F <| by simp [φ, hex] + have h := hFφ.fderiv_eq_zero + rw [fderiv_comp _ (by fun_prop) (((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt <| + mem_interior_iff_mem_nhds.1 hφx), ContinuousLinearMap.fderiv] at h + exact DFunLike.congr_fun h + +lemma isOpen_interior {n : ℕ} [IsManifold I n M] (hn : 1 ≤ n) : IsOpen (I.interior M) := by + sorry + +lemma isClosed_boundary {n : ℕ} [IsManifold I n M] (hn : 1 ≤ n) : IsClosed (I.boundary M) := by + rw [← I.compl_interior, isClosed_compl_iff] + exact I.isOpen_interior hn + +end ChartIndependence + /-! Interior and boundary of open subsets of a manifold. -/ section opens From 597e517c725913b45f09757bf203718b68c1085a Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Mon, 22 Dec 2025 07:43:34 +0100 Subject: [PATCH 02/11] more lemmas and docstrings --- .../Manifold/IsManifold/InteriorBoundary.lean | 48 ++++++++++++++----- 1 file changed, 37 insertions(+), 11 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index b78f6f13699ffb..c6f039b8730800 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2023 Michael Rothgang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Michael Rothgang +Authors: Michael Rothgang, Ben Eltschig -/ module @@ -27,6 +27,9 @@ Define the interior and boundary of a manifold. - `ModelWithCorners.Boundaryless.boundary_eq_empty` and `of_boundary_eq_empty`: `M` is boundaryless if and only if its boundary is empty +- `ModelWithCorners.isOpen_interior`, `ModelWithCorners.isClosed_boundary`: the interior is open and + and the boundary is closed. This is currently only proven for C¹ manifolds. + - `ModelWithCorners.interior_open`: the interior of `u : Opens M` is the preimage of the interior of `M` under the inclusion - `ModelWithCorners.boundary_open`: the boundary of `u : Opens M` is the preimage of the boundary @@ -49,15 +52,14 @@ of `M` and `N`. manifold, interior, boundary ## TODO -- `x` is an interior point iff *any* chart around `x` maps it to `interior (range I)`; -similarly for the boundary. -- the interior of `M` is open, hence the boundary is closed (and nowhere dense) - In finite dimensions, this requires e.g. the homology of spheres. -- the interior of `M` is a manifold without boundary +- the interior of `M` is dense, the boundary nowhere dense +- the interior of `M` is a boundaryless manifold - `boundary M` is a submanifold (possibly with boundary and corners): -follows from the corresponding statement for the model with corners `I`; -this requires a definition of submanifolds + follows from the corresponding statement for the model with corners `I`; + this requires a definition of submanifolds - if `M` is finite-dimensional, its boundary has measure zero +- generalise lemmas about C¹ manifolds with boundary to also hold for finite-dimensional topological + manifolds; this will require e.g. the homology of spheres. -/ @@ -335,10 +337,34 @@ lemma isInteriorPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] ( mem_interior_iff_mem_nhds.1 hφx), ContinuousLinearMap.fderiv] at h exact DFunLike.congr_fun h -lemma isOpen_interior {n : ℕ} [IsManifold I n M] (hn : 1 ≤ n) : IsOpen (I.interior M) := by - sorry +/-- A point `x` in a manifold that is at least C¹ is a boundary point iff it gets mapped to the +boundary of the model space by any given chart - i.e., the notion of boundary points does not depend +on any choice of charts, so that talking about `ModelWithCorners.boundary` actually makes sense. -lemma isClosed_boundary {n : ℕ} [IsManifold I n M] (hn : 1 ≤ n) : IsClosed (I.boundary M) := by +Also see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ +lemma isBoundaryPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] (hn : 1 ≤ n) + {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) : + I.IsBoundaryPoint x ↔ e.extend I x ∈ frontier (e.extend I).target := by + rw [← not_iff_not, ← I.isInteriorPoint_iff_not_isBoundaryPoint, + I.isInteriorPoint_iff_of_mem_atlas hn he hx, mem_interior_iff_notMem_frontier] + exact (e.extend I).mapsTo <| e.extend_source (I := I) ▸ hx + +/-- The interior of any C¹ manifold is open. + +This is currently only proven for C¹ manifolds, but should hold at least for finite-dimensional +topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ +protected lemma isOpen_interior {n : WithTop ℕ∞} [IsManifold I n M] (hn : 1 ≤ n) : + IsOpen (I.interior M) := by + refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨_, ?_, isOpen_extChartAt_preimage (I := I) x + isOpen_interior, mem_chart_source H x, isInteriorPoint_iff.1 hx⟩ + exact fun y hy ↦ (I.isInteriorPoint_iff_of_mem_atlas hn (chart_mem_atlas H x) hy.1).2 hy.2 + +/-- The boundary of any C¹ manifold is closed. + +This is currently only proven for C¹ manifolds, but should hold at least for finite-dimensional +topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ +protected lemma isClosed_boundary {n : WithTop ℕ∞} [IsManifold I n M] (hn : 1 ≤ n) : + IsClosed (I.boundary M) := by rw [← I.compl_interior, isClosed_compl_iff] exact I.isOpen_interior hn From 8b3a10f5ae3e8a169ac8b76e57e49b2184d76816 Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Mon, 22 Dec 2025 08:04:12 +0100 Subject: [PATCH 03/11] move lemmas, make imports private --- .../Manifold/IsManifold/ExtChartAt.lean | 54 ++++++++++++++++ .../Manifold/IsManifold/InteriorBoundary.lean | 64 +------------------ Mathlib/Topology/Closure.lean | 8 +++ 3 files changed, 65 insertions(+), 61 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index 81af9a4661c729..3add884ce870cb 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -377,6 +377,60 @@ theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ max end OpenPartialHomeomorph +namespace ModelWithCorners + +/-- The change of charts from `e` to `e'` in the model vector space `E`. -/ +@[simps!] +def extCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E := + (e.extend I).symm.trans (e'.extend I) + +lemma extCoordChange_symm {e e' : OpenPartialHomeomorph M H} : + (I.extCoordChange e e').symm = I.extCoordChange e' e := by + rfl + +lemma contDiffOn_extCoordChange [ChartedSpace H M] {n : WithTop ℕ∞} + {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) + (he' : e' ∈ IsManifold.maximalAtlas I n M) : + ContDiffOn 𝕜 n (I.extCoordChange e e') (I.extCoordChange e e').source := + e'.contDiffOn_extend_coord_change he' he + +lemma contDiffOn_extCoordChange_symm [ChartedSpace H M] {n : WithTop ℕ∞} + {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) + (he' : e' ∈ IsManifold.maximalAtlas I n M) : + ContDiffOn 𝕜 n (I.extCoordChange e e').symm (I.extCoordChange e e').target := + e.contDiffOn_extend_coord_change he he' + +lemma uniqueDiffOn_extCoordChange_source {e e' : OpenPartialHomeomorph M H} : + UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by + rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter] + exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source + +lemma uniqueDiffOn_extCoordChange_target {e e' : OpenPartialHomeomorph M H} : + UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by + rw [← extCoordChange_symm, PartialEquiv.symm_target] + exact uniqueDiffOn_extCoordChange_source + +lemma isInvertible_fderivWithin_extCoordChange [ChartedSpace H M] {n : WithTop ℕ∞} + (hn : 1 ≤ n) {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) + (he' : e' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ (I.extCoordChange e e').source) : + (fderivWithin 𝕜 (I.extCoordChange e e') (I.extCoordChange e e').source x).IsInvertible := by + set φ := I.extCoordChange e e' + have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extCoordChange he he' + have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extCoordChange_symm he he' + refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_ + · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp _ + (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):) + ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) φ.symm_mapsTo + (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)), + fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx)] + exact fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)) + · rw [← fderivWithin_comp _ ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) + ((hφ _ hx).differentiableWithinAt hn) φ.mapsTo (I.uniqueDiffOn_extCoordChange_source _ hx), + fderivWithin_congr' φ.leftInvOn.eqOn hx, + fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ hx)] + +end ModelWithCorners + open OpenPartialHomeomorph variable [ChartedSpace H M] [ChartedSpace H' M'] diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index c6f039b8730800..d057ec7973509d 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -5,10 +5,11 @@ Authors: Michael Rothgang, Ben Eltschig -/ module -public import Mathlib.Analysis.Calculus.LocalExtr.Basic -public import Mathlib.Analysis.LocallyConvex.Separation public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt +import Mathlib.Analysis.Calculus.LocalExtr.Basic +import Mathlib.Analysis.LocallyConvex.Separation + /-! # Interior and boundary of a manifold Define the interior and boundary of a manifold. @@ -203,65 +204,6 @@ end BoundarylessManifold section ChartIndependence -lemma mem_interior_iff_notMem_frontier {X : Type*} [TopologicalSpace X] {s : Set X} {x : X} - (hx : x ∈ s) : x ∈ interior s ↔ x ∉ frontier s := by - simp [← self_diff_frontier, hx] - -lemma mem_frontier_iff_notMem_interior {X : Type*} [TopologicalSpace X] {s : Set X} {x : X} - (hx : x ∈ s) : x ∈ frontier s ↔ x ∉ interior s := by - simp [← self_diff_frontier, hx] - -/-- The change of charts from `e` to `e'` in the model vector space `E`. -/ -@[simps!] -def extCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E := - (e.extend I).symm.trans (e'.extend I) - -omit [ChartedSpace H M] in -lemma extCoordChange_symm {e e' : OpenPartialHomeomorph M H} : - (I.extCoordChange e e').symm = I.extCoordChange e' e := by - rfl - -lemma contDiffOn_extCoordChange {n : WithTop ℕ∞} {e e' : OpenPartialHomeomorph M H} - (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) : - ContDiffOn 𝕜 n (I.extCoordChange e e') (I.extCoordChange e e').source := - e'.contDiffOn_extend_coord_change he' he - -lemma contDiffOn_extCoordChange_symm {n : WithTop ℕ∞} {e e' : OpenPartialHomeomorph M H} - (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) : - ContDiffOn 𝕜 n (I.extCoordChange e e').symm (I.extCoordChange e e').target := - e.contDiffOn_extend_coord_change he he' - -omit [ChartedSpace H M] in -lemma uniqueDiffOn_extCoordChange_source {e e' : OpenPartialHomeomorph M H} : - UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by - rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter] - exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source - -omit [ChartedSpace H M] in -lemma uniqueDiffOn_extCoordChange_target {e e' : OpenPartialHomeomorph M H} : - UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by - rw [← extCoordChange_symm, PartialEquiv.symm_target] - exact uniqueDiffOn_extCoordChange_source - -lemma isInvertible_fderivWithin_extCoordChange {n : WithTop ℕ∞} - (hn : 1 ≤ n) {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) - (he' : e' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ (I.extCoordChange e e').source) : - (fderivWithin 𝕜 (I.extCoordChange e e') (I.extCoordChange e e').source x).IsInvertible := by - set φ := I.extCoordChange e e' - have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extCoordChange he he' - have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extCoordChange_symm he he' - refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_ - · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp _ - (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):) - ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) φ.symm_mapsTo - (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)), - fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx)] - exact fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)) - · rw [← fderivWithin_comp _ ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) - ((hφ _ hx).differentiableWithinAt hn) φ.mapsTo (I.uniqueDiffOn_extCoordChange_source _ hx), - fderivWithin_congr' φ.leftInvOn.eqOn hx, - fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ hx)] - /-- A point `x` in a manifold that is at least C¹ is an interior point iff it gets mapped to the interior of the model space by any given chart - i.e., the notion of interior points does not depend on any choice of charts, so that talking about `ModelWithCorners.interior` actually makes sense. diff --git a/Mathlib/Topology/Closure.lean b/Mathlib/Topology/Closure.lean index 446d979e67fac9..baae5e05c455db 100644 --- a/Mathlib/Topology/Closure.lean +++ b/Mathlib/Topology/Closure.lean @@ -475,6 +475,14 @@ theorem self_diff_frontier (s : Set X) : s \ frontier s = interior s := by rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure, inter_eq_self_of_subset_right interior_subset, empty_union] +lemma mem_interior_iff_notMem_frontier {s : Set X} {x : X} (hx : x ∈ s) : + x ∈ interior s ↔ x ∉ frontier s := by + simp [← self_diff_frontier, hx] + +lemma mem_frontier_iff_notMem_interior {s : Set X} {x : X} (hx : x ∈ s) : + x ∈ frontier s ↔ x ∉ interior s := by + simp [← self_diff_frontier, hx] + theorem frontier_eq_closure_inter_closure : frontier s = closure s ∩ closure sᶜ := by rw [closure_compl, frontier, diff_eq] From f627987e7660974feafe26bb548e0107b587fbe4 Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sat, 31 Jan 2026 22:07:59 +0100 Subject: [PATCH 04/11] apply some smaller suggestions --- .../Geometry/Manifold/IsManifold/InteriorBoundary.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index eb858a9d0f04e7..b8996a260337b2 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -279,8 +279,8 @@ lemma isInteriorPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] ( mem_interior_iff_mem_nhds.1 hφx), ContinuousLinearMap.fderiv] at h exact DFunLike.congr_fun h -/-- A point `x` in a manifold that is at least C¹ is a boundary point iff it gets mapped to the -boundary of the model space by any given chart - i.e., the notion of boundary points does not depend +/-- A point `x` in a C¹ manifold is a boundary point iff it gets mapped to the boundary of the +model space by any given chart - i.e., the notion of boundary points does not depend on any choice of charts, so that talking about `ModelWithCorners.boundary` actually makes sense. Also see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ @@ -293,7 +293,7 @@ lemma isBoundaryPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] ( /-- The interior of any C¹ manifold is open. -This is currently only proven for C¹ manifolds, but should hold at least for finite-dimensional +This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ protected lemma isOpen_interior {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) : IsOpen (I.interior M) := by @@ -303,7 +303,7 @@ protected lemma isOpen_interior {n : WithTop ℕ∞} [IsManifold I n M] (hn : n /-- The boundary of any C¹ manifold is closed. -This is currently only proven for C¹ manifolds, but should hold at least for finite-dimensional +This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ protected lemma isClosed_boundary {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) : IsClosed (I.boundary M) := by From b2d5c9c6d7ed600f29b509de4ef717f9ae7a7b41 Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sat, 31 Jan 2026 23:55:57 +0100 Subject: [PATCH 05/11] factor out lemma --- .../Manifold/IsManifold/InteriorBoundary.lean | 56 +++++++++++-------- 1 file changed, 34 insertions(+), 22 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index b8996a260337b2..2ec40efab94cce 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -204,6 +204,33 @@ end BoundarylessManifold section ChartIndependence +/-- If a function `f : E → H` is differentiable at `x`, sends a neighbourhood `u` of `x` to a +closed convex set `s` with nonempty interior and has surjective differential at `x`, it must send +`x` to the interior of `s`. +TODO: find home (`#find_home` says this file) -/ +lemma _root_.DifferentiableAt.mem_interior_convex_of_surjective_fderiv {E H : Type*} + [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [NormedSpace ℝ H] {f : E → H} + {x : E} (hf : DifferentiableAt ℝ f x) {u : Set E} (hu : u ∈ 𝓝 x) {s : Set H} (hs : Convex ℝ s) + (hs' : IsClosed s) (hs'' : (interior s).Nonempty) (hfus : Set.MapsTo f u s) + (hfx : Function.Surjective (fderiv ℝ f x)) : f x ∈ interior s := by + contrapose hfx + have ⟨F, hF⟩ := geometric_hahn_banach_open_point hs.interior isOpen_interior hfx + -- It suffices to show that `fderiv ℝ f x` sends everything to the kernel of `F`. + suffices h : ∀ y, F (fderiv ℝ f x y) = 0 by + have ⟨y, hy⟩ := hs'' + unfold Function.Surjective; push_neg + refine ⟨f x - y, fun z ↦ ne_of_apply_ne F ?_⟩ + rw [h z, F.map_sub] + exact (sub_pos.2 <| hF _ hy).ne + -- This follows from `F ∘ f` taking on a local maximum at `e.extend I x`. + have hF' : MapsTo F s (Iic (F (f x))) := by + rw [← hs'.closure_eq, ← closure_Iio, ← hs.closure_interior_eq_closure_of_nonempty_interior hs''] + exact MapsTo.closure hF F.continuous + have hFφ : IsLocalMax (F ∘ f) x := Filter.eventually_of_mem hu fun y hy ↦ hF' <| hfus hy + have h := hFφ.fderiv_eq_zero + rw [fderiv_comp _ (by fun_prop) hf, ContinuousLinearMap.fderiv] at h + exact DFunLike.congr_fun h + /-- A point `x` in a manifold that is at least C¹ is an interior point iff it gets mapped to the interior of the model space by any given chart - i.e., the notion of interior points does not depend on any choice of charts, so that talking about `ModelWithCorners.interior` actually makes sense. @@ -256,28 +283,13 @@ lemma isInteriorPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] ( (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ) (uniqueDiffWithinAt_of_mem_nhds <| mem_interior_iff_mem_nhds.1 hφx), fderivWithin_of_mem_nhds <| mem_interior_iff_mem_nhds.1 hφx] - have ⟨F, hF⟩ := geometric_hahn_banach_open_point I.convex_range.interior isOpen_interior hx' - -- It suffices to show that `fderiv ℝ φ (e.extend I x) y` sends everything to the kernel of `F`. - suffices h : ∀ y, F (fderiv ℝ φ (e.extend I x) y) = 0 by - have ⟨y, hy⟩ := I.nonempty_interior - unfold Function.Surjective; push_neg - refine ⟨e'.extend I x - y, fun z ↦ ne_of_apply_ne F ?_⟩ - rw [h z, F.map_sub] - exact (sub_pos.2 <| hF _ hy).ne - -- This follows from `F ∘ φ` taking on a local maximum at `e.extend I x`. - have hF' : ∀ y ∈ range I, F y ≤ F (e'.extend I x) := by - change MapsTo F _ (Iic _) - rw [← I.isClosed_range.closure_eq, ← closure_Iio, - ← I.convex_range.closure_interior_eq_closure_of_nonempty_interior I.nonempty_interior] - exact MapsTo.closure hF F.continuous - have hFφ : IsLocalMax (F ∘ φ) (e.extend I x) := - Filter.eventually_of_mem (mem_interior_iff_mem_nhds.1 hφx) fun y hy ↦ - (hF' (φ y) ((show φ.target ⊆ range I by simp [φ, inter_assoc]) (φ.mapsTo hy))).trans_eq <| - congr_arg F <| by simp [φ, hex] - have h := hFφ.fderiv_eq_zero - rw [fderiv_comp _ (by fun_prop) (((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt <| - mem_interior_iff_mem_nhds.1 hφx), ContinuousLinearMap.fderiv] at h - exact DFunLike.congr_fun h + contrapose hx' + rw [show e'.extend I x = φ (e.extend I x) by simp [φ, hex]] + replace hφ := (((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt <| + mem_interior_iff_mem_nhds.1 hφx) + exact hφ.mem_interior_convex_of_surjective_fderiv (mem_interior_iff_mem_nhds.1 hφx) + I.convex_range I.isClosed_range I.nonempty_interior + (φ.mapsTo.mono_right <| by simp [φ, inter_assoc]) hx' /-- A point `x` in a C¹ manifold is a boundary point iff it gets mapped to the boundary of the model space by any given chart - i.e., the notion of boundary points does not depend From d4cd19b9423b40c445b918bcdbd2811cebc2354c Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sun, 1 Feb 2026 00:27:58 +0100 Subject: [PATCH 06/11] golf and simplify proof some more --- .../Manifold/IsManifold/InteriorBoundary.lean | 45 +++++++------------ 1 file changed, 17 insertions(+), 28 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index 2ec40efab94cce..002cfa9a9f605b 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -225,7 +225,7 @@ lemma _root_.DifferentiableAt.mem_interior_convex_of_surjective_fderiv {E H : Ty -- This follows from `F ∘ f` taking on a local maximum at `e.extend I x`. have hF' : MapsTo F s (Iic (F (f x))) := by rw [← hs'.closure_eq, ← closure_Iio, ← hs.closure_interior_eq_closure_of_nonempty_interior hs''] - exact MapsTo.closure hF F.continuous + exact .closure hF F.continuous have hFφ : IsLocalMax (F ∘ f) x := Filter.eventually_of_mem hu fun y hy ↦ hF' <| hfus hy have h := hFφ.fderiv_eq_zero rw [fderiv_comp _ (by fun_prop) hf, ContinuousLinearMap.fderiv] at h @@ -256,40 +256,29 @@ lemma isInteriorPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] ( let φ := (e.extend I).symm.trans (e'.extend I) have hφ : ContDiffOn 𝕜 n φ φ.source := e'.contDiffOn_extend_coord_change (IsManifold.subset_maximalAtlas he') (IsManifold.subset_maximalAtlas he) - have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := e.contDiffOn_extend_coord_change - (IsManifold.subset_maximalAtlas he) (IsManifold.subset_maximalAtlas he') - suffices h : e'.extend I x ∉ interior (range I) → - ¬Function.Surjective (fderivWithin 𝕜 φ φ.source (e.extend I x)) by - rw [not_imp_not] at h + suffices h : Function.Surjective (fderivWithin 𝕜 φ φ.source (e.extend I x)) → + e'.extend I x ∈ interior (range I) by refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_ - refine ContinuousLinearMap.IsInvertible.surjective ?_ - exact isInvertible_fderivWithin_extCoordChange hn (IsManifold.subset_maximalAtlas he) - (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex'] - intro hx' - /- Reduce the situation to the real case, then apply Hahn-Banach to `x` and `interior (range I)` - to get a functional `F` that is greater on `e'.extend I x` than on all of `interior (range I)`. -/ + exact (isInvertible_fderivWithin_extCoordChange hn (IsManifold.subset_maximalAtlas he) + (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex']).surjective + intro hφx' + /- Reduce the situation to the real case, then apply + `DifferentiableAt.mem_interior_convex_of_surjective_fderiv`. -/ wlog _ : IsRCLikeNormedField 𝕜 - · simp [I.range_eq_univ_of_not_isRCLikeNormedField ‹_›] at hx' + · simp [I.range_eq_univ_of_not_isRCLikeNormedField ‹_›] let _ := IsRCLikeNormedField.rclike 𝕜 - let _ := Module.compHom E (algebraMap ℝ 𝕜) - have : IsScalarTower ℝ 𝕜 E := ⟨by intros; rw [Algebra.smul_def, mul_smul]; rfl⟩ - let _ : NormedSpace ℝ E := { - norm_smul_le r x := (norm_smul_le (r : 𝕜) x).trans <| by simp } - have hφx : e.extend I x ∈ interior φ.source := by - simp_rw [φ, PartialEquiv.trans_source, PartialEquiv.symm_source, interior_inter, mem_inter_iff, - hx, true_and, e'.extend_source, mem_interior_iff_mem_nhds] + let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E + have hφx : φ.source ∈ 𝓝 (e.extend I x) := by + simp_rw [φ, PartialEquiv.trans_source, PartialEquiv.symm_source, Filter.inter_mem_iff, + mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source] exact e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex' rw [← ContinuousLinearMap.coe_restrictScalars' (R := ℝ), (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ) - (uniqueDiffWithinAt_of_mem_nhds <| mem_interior_iff_mem_nhds.1 hφx), - fderivWithin_of_mem_nhds <| mem_interior_iff_mem_nhds.1 hφx] - contrapose hx' + (uniqueDiffWithinAt_of_mem_nhds hφx), fderivWithin_of_mem_nhds <| hφx] at hφx' rw [show e'.extend I x = φ (e.extend I x) by simp [φ, hex]] - replace hφ := (((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt <| - mem_interior_iff_mem_nhds.1 hφx) - exact hφ.mem_interior_convex_of_surjective_fderiv (mem_interior_iff_mem_nhds.1 hφx) - I.convex_range I.isClosed_range I.nonempty_interior - (φ.mapsTo.mono_right <| by simp [φ, inter_assoc]) hx' + replace hφ := ((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt hφx + exact hφ.mem_interior_convex_of_surjective_fderiv hφx I.convex_range I.isClosed_range + I.nonempty_interior (φ.mapsTo.mono_right <| by simp [φ, inter_assoc]) hφx' /-- A point `x` in a C¹ manifold is a boundary point iff it gets mapped to the boundary of the model space by any given chart - i.e., the notion of boundary points does not depend From 04f19a89365ab00e58d93466cf62563052e816af Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sun, 1 Feb 2026 00:53:36 +0100 Subject: [PATCH 07/11] apply some more suggestions --- .../Geometry/Manifold/IsManifold/ExtChartAt.lean | 13 +++++++------ .../Manifold/IsManifold/InteriorBoundary.lean | 6 +++--- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index ffa61c244cfa87..a8b855677419be 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -411,12 +411,13 @@ lemma isInvertible_fderivWithin_extCoordChange [ChartedSpace H M] {n : WithTop have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extCoordChange he he' have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extCoordChange_symm he he' refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_ - · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp _ - (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):) - ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) φ.symm_mapsTo - (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)), - fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx)] - exact fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)) + · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp, + fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id] + · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx) + · exact (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):) + · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn + · exact φ.symm_mapsTo + · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx) · rw [← fderivWithin_comp _ ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) ((hφ _ hx).differentiableWithinAt hn) φ.mapsTo (I.uniqueDiffOn_extCoordChange_source _ hx), fderivWithin_congr' φ.leftInvOn.eqOn hx, diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index 002cfa9a9f605b..4dd1981ae753ec 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -231,9 +231,9 @@ lemma _root_.DifferentiableAt.mem_interior_convex_of_surjective_fderiv {E H : Ty rw [fderiv_comp _ (by fun_prop) hf, ContinuousLinearMap.fderiv] at h exact DFunLike.congr_fun h -/-- A point `x` in a manifold that is at least C¹ is an interior point iff it gets mapped to the -interior of the model space by any given chart - i.e., the notion of interior points does not depend -on any choice of charts, so that talking about `ModelWithCorners.interior` actually makes sense. +/-- A point `x` in a C¹ manifold is an interior point iff it gets mapped to the interior of +the model space by any given chart - in other words, the notion of interior points does not depend +on any choice of charts. Note that in general, this is actually quite nontrivial; that is why are focusing only on C¹ manifolds here. For merely topological finite-dimensional manifolds the proof involves singular From e600bf17fd84cce6c680989099300d14f944c871 Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sun, 1 Feb 2026 01:13:36 +0100 Subject: [PATCH 08/11] clean up second long rewrite too --- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index a8b855677419be..d8327f9f771a12 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -418,10 +418,12 @@ lemma isInvertible_fderivWithin_extCoordChange [ChartedSpace H M] {n : WithTop · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn · exact φ.symm_mapsTo · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx) - · rw [← fderivWithin_comp _ ((hφ' _ (φ.map_source hx)).differentiableWithinAt hn) - ((hφ _ hx).differentiableWithinAt hn) φ.mapsTo (I.uniqueDiffOn_extCoordChange_source _ hx), - fderivWithin_congr' φ.leftInvOn.eqOn hx, - fderivWithin_id (I.uniqueDiffOn_extCoordChange_source _ hx)] + · rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id] + · exact I.uniqueDiffOn_extCoordChange_source _ hx + · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn + · exact (hφ _ hx).differentiableWithinAt hn + · exact φ.mapsTo + · exact I.uniqueDiffOn_extCoordChange_source _ hx end ModelWithCorners From b8c62e5c4f81d64060192890a4adaedfde4b24b3 Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sun, 1 Feb 2026 20:39:52 +0100 Subject: [PATCH 09/11] extract a few things as variables --- .../Manifold/IsManifold/ExtChartAt.lean | 34 +++++++++---------- 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index d8327f9f771a12..39075d78ecd526 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -377,34 +377,32 @@ namespace ModelWithCorners def extCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E := (e.extend I).symm.trans (e'.extend I) -lemma extCoordChange_symm {e e' : OpenPartialHomeomorph M H} : - (I.extCoordChange e e').symm = I.extCoordChange e' e := by +variable {e e' : OpenPartialHomeomorph M H} + +lemma extCoordChange_symm : (I.extCoordChange e e').symm = I.extCoordChange e' e := by rfl -lemma contDiffOn_extCoordChange [ChartedSpace H M] {n : WithTop ℕ∞} - {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) +lemma uniqueDiffOn_extCoordChange_source : UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by + rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter] + exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source + +lemma uniqueDiffOn_extCoordChange_target : UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by + rw [← extCoordChange_symm, PartialEquiv.symm_target] + exact uniqueDiffOn_extCoordChange_source + +variable [ChartedSpace H M] {n : WithTop ℕ∞} + +lemma contDiffOn_extCoordChange (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) : ContDiffOn 𝕜 n (I.extCoordChange e e') (I.extCoordChange e e').source := e'.contDiffOn_extend_coord_change he' he -lemma contDiffOn_extCoordChange_symm [ChartedSpace H M] {n : WithTop ℕ∞} - {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) +lemma contDiffOn_extCoordChange_symm (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) : ContDiffOn 𝕜 n (I.extCoordChange e e').symm (I.extCoordChange e e').target := e.contDiffOn_extend_coord_change he he' -lemma uniqueDiffOn_extCoordChange_source {e e' : OpenPartialHomeomorph M H} : - UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by - rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter] - exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source - -lemma uniqueDiffOn_extCoordChange_target {e e' : OpenPartialHomeomorph M H} : - UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by - rw [← extCoordChange_symm, PartialEquiv.symm_target] - exact uniqueDiffOn_extCoordChange_source - -lemma isInvertible_fderivWithin_extCoordChange [ChartedSpace H M] {n : WithTop ℕ∞} - (hn : n ≠ 0) {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) +lemma isInvertible_fderivWithin_extCoordChange (hn : n ≠ 0) (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ (I.extCoordChange e e').source) : (fderivWithin 𝕜 (I.extCoordChange e e') (I.extCoordChange e e').source x).IsInvertible := by set φ := I.extCoordChange e e' From e8fe461eaaaceba258576c484c7c30d9b24c159d Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sun, 1 Feb 2026 20:44:46 +0100 Subject: [PATCH 10/11] improve docstrings --- .../Manifold/IsManifold/InteriorBoundary.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index 4dd1981ae753ec..2d26ddda2a7ab3 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -78,12 +78,12 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] namespace ModelWithCorners variable (I) in -/-- `p ∈ M` is an interior point of a manifold `M` iff its image in the extended chart +/-- `p ∈ M` is an interior point of a manifold `M` if and only if its image in the extended chart lies in the interior of the model space. -/ def IsInteriorPoint (x : M) := extChartAt I x x ∈ interior (range I) variable (I) in -/-- `p ∈ M` is a boundary point of a manifold `M` iff its image in the extended chart +/-- `p ∈ M` is a boundary point of a manifold `M` if and only if its image in the extended chart lies on the boundary of the model space. -/ def IsBoundaryPoint (x : M) := extChartAt I x x ∈ frontier (range I) @@ -187,7 +187,7 @@ lemma Boundaryless.boundary_eq_empty [BoundarylessManifold I M] : I.boundary M = instance [BoundarylessManifold I M] : IsEmpty (I.boundary M) := isEmpty_coe_sort.mpr Boundaryless.boundary_eq_empty -/-- `M` is boundaryless iff its boundary is empty. -/ +/-- `M` is boundaryless if and only if its boundary is empty. -/ lemma Boundaryless.iff_boundary_eq_empty : I.boundary M = ∅ ↔ BoundarylessManifold I M := by refine ⟨fun h ↦ { isInteriorPoint' := ?_ }, fun a ↦ boundary_eq_empty⟩ intro x @@ -231,9 +231,9 @@ lemma _root_.DifferentiableAt.mem_interior_convex_of_surjective_fderiv {E H : Ty rw [fderiv_comp _ (by fun_prop) hf, ContinuousLinearMap.fderiv] at h exact DFunLike.congr_fun h -/-- A point `x` in a C¹ manifold is an interior point iff it gets mapped to the interior of -the model space by any given chart - in other words, the notion of interior points does not depend -on any choice of charts. +/-- A point `x` in a C¹ manifold is an interior point if and only if it gets mapped to the interior +of the model space by any given chart - in other words, the notion of interior points does not +depend on any choice of charts. Note that in general, this is actually quite nontrivial; that is why are focusing only on C¹ manifolds here. For merely topological finite-dimensional manifolds the proof involves singular @@ -280,9 +280,9 @@ lemma isInteriorPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] ( exact hφ.mem_interior_convex_of_surjective_fderiv hφx I.convex_range I.isClosed_range I.nonempty_interior (φ.mapsTo.mono_right <| by simp [φ, inter_assoc]) hφx' -/-- A point `x` in a C¹ manifold is a boundary point iff it gets mapped to the boundary of the -model space by any given chart - i.e., the notion of boundary points does not depend -on any choice of charts, so that talking about `ModelWithCorners.boundary` actually makes sense. +/-- A point `x` in a C¹ manifold is a boundary point if and only if it gets mapped to the boundary +of the model space by any given chart - in other words, the notion of boundary points does not +depend on any choice of charts. Also see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`. -/ lemma isBoundaryPoint_iff_of_mem_atlas {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) From d431d6b983c1dd4c6d354bfc97e4d900606f80ef Mon Sep 17 00:00:00 2001 From: Ben Eltschig Date: Sat, 7 Feb 2026 05:40:13 +0100 Subject: [PATCH 11/11] local diffeomorphisms preserve interior and boundary --- .../Manifold/IsManifold/ExtChartAt.lean | 7 ++ .../Manifold/IsManifold/InteriorBoundary.lean | 112 +++++++++++++++++- 2 files changed, 114 insertions(+), 5 deletions(-) diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index 39075d78ecd526..ebb77cc902a307 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -798,6 +798,13 @@ theorem writtenInExtChartAt_extChartAt_symm {x : M} {y : E} (h : y ∈ (extChart writtenInExtChartAt 𝓘(𝕜, E) I (extChartAt I x x) (extChartAt I x).symm y = y := by simp_all only [mfld_simps] +theorem writtenInExtChartAt_mapsTo {x : M} {f : M → M'} : + MapsTo (writtenInExtChartAt I I' x f) + ((extChartAt I x).target ∩ f ∘ (extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) + (extChartAt I' (f x)).target := by + intro x' hx' + simpa using (chartAt H' (f x)).mapsTo (by simpa using hx'.2) + section variable {G G' F F' N N' : Type*} diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index 2d26ddda2a7ab3..08b17d10a5dd0f 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -5,7 +5,7 @@ Authors: Michael Rothgang, Ben Eltschig -/ module -public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt +public import Mathlib.Geometry.Manifold.LocalDiffeomorph import Mathlib.Analysis.Calculus.LocalExtr.Basic import Mathlib.Analysis.LocallyConvex.Separation @@ -61,13 +61,15 @@ manifold, interior, boundary - if `M` is finite-dimensional, its boundary has measure zero - generalise lemmas about C¹ manifolds with boundary to also hold for finite-dimensional topological manifolds; this will require e.g. the homology of spheres. +- submersions send interior points to interior points. This should be an easy consequence of + `MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv` once submersions are defined. -/ @[expose] public section -open Set -open scoped Topology +open Set Function +open scoped Topology Manifold -- Let `M` be a manifold with corners over the pair `(E, H)`. variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] @@ -131,6 +133,10 @@ lemma isInteriorPoint_iff_not_isBoundaryPoint (x : M) : ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff] exact h +lemma isBoundaryPoint_iff_not_isInteriorPoint (x : M) : + I.IsBoundaryPoint x ↔ ¬I.IsInteriorPoint x := by + simp [isInteriorPoint_iff_not_isBoundaryPoint] + /-- The boundary is the complement of the interior. -/ lemma compl_interior : (I.interior M)ᶜ = I.boundary M := by apply compl_unique ?_ I.interior_union_boundary_eq_univ @@ -313,6 +319,104 @@ protected lemma isClosed_boundary {n : WithTop ℕ∞} [IsManifold I n M] (hn : end ChartIndependence +/-! Interior and boundary are preserved under (local) diffeomorphisms. -/ +section Diffeomorph + +variable + {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] + {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} + {N : Type*} [TopologicalSpace N] [ChartedSpace H' N] + {n : WithTop ℕ∞} + +/-- If a function `f` is differentiable at `x` with surjective `mfderiv I I' f x` and `x` is an +interior point with respect to `I`, `f x` must be an interior point with respect to `I'`. -/ +lemma _root_.MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv {f : M → N} {x : M} + (hf : MDifferentiableAt I I' f x) (hf' : Surjective (mfderiv I I' f x)) + (hx : I.IsInteriorPoint x) : I'.IsInteriorPoint (f x) := by + wlog _ : IsRCLikeNormedField 𝕜 + · simp [IsInteriorPoint, I'.range_eq_univ_of_not_isRCLikeNormedField ‹_›] + let _ := IsRCLikeNormedField.rclike 𝕜 + let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E + let _ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E' + simp only [mfderiv, hf, ite_true] at hf' + have hf'' := hf.differentiableWithinAt_writtenInExtChartAt.differentiableAt <| by + simpa [← mem_interior_iff_mem_nhds] using hx + rw [fderivWithin_eq_fderiv (I.uniqueDiffOn _ <| by simp) hf''] at hf' + replace hf' : Surjective (fderiv ℝ (writtenInExtChartAt I I' x f) (extChartAt I x x)) := by + rwa [hf''.fderiv_restrictScalars (𝕜 := ℝ), ContinuousLinearMap.coe_restrictScalars'] + replace hf'' := hf''.restrictScalars ℝ + have := hf''.mem_interior_convex_of_surjective_fderiv (Filter.inter_mem ?_ ?_) I'.convex_range + I'.isClosed_range I'.nonempty_interior (writtenInExtChartAt_mapsTo.mono_right ?_) hf' + · simpa using this + · rw [← nhdsWithin_eq_nhds.2 (mem_interior_iff_mem_nhds.1 hx)] + exact extChartAt_target_mem_nhdsWithin x + · exact extChartAt_preimage_mem_nhds <| hf.continuousAt.preimage_mem_nhds <| + extChartAt_source_mem_nhds _ + · exact extChartAt_target_subset_range _ + +lemma _root_.IsLocalDiffeomorphAt.isInteriorPoint_iff (hn : n ≠ 0) {f : M → N} {x : M} + (hf : IsLocalDiffeomorphAt I I' n f x) : I.IsInteriorPoint x ↔ I'.IsInteriorPoint (f x) := by + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · refine (hf.mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h + exact (hf.mfderivToContinuousLinearEquiv hn).surjective + · rw [← hf.localInverse_left_inv hf.localInverse_mem_target] + refine (hf.localInverse_mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h + exact (hf.mfderivToContinuousLinearEquiv hn).symm.surjective + +lemma _root_.IsLocalDiffeomorphAt.isBoundaryPoint_iff (hn : n ≠ 0) {f : M → N} {x : M} + (hf : IsLocalDiffeomorphAt I I' n f x) : I.IsBoundaryPoint x ↔ I'.IsBoundaryPoint (f x) := by + simp [isBoundaryPoint_iff_not_isInteriorPoint, hf.isInteriorPoint_iff hn] + + +lemma _root_.IsLocalDiffeomorphOn.preimage_interior_inter (hn : n ≠ 0) {f : M → N} {s : Set M} + (hf : IsLocalDiffeomorphOn I I' n f s) : f ⁻¹' I'.interior N ∩ s = I.interior M ∩ s := by + ext x + simpa using fun hx ↦ ((hf ⟨x, hx⟩).isInteriorPoint_iff hn).symm + +lemma _root_.IsLocalDiffeomorphOn.preimage_boundary_inter (hn : n ≠ 0) {f : M → N} {s : Set M} + (hf : IsLocalDiffeomorphOn I I' n f s) : f ⁻¹' I'.boundary N ∩ s = I.boundary M ∩ s := by + ext x + simpa using fun hx ↦ ((hf ⟨x, hx⟩).isBoundaryPoint_iff hn).symm + +lemma _root_.IsLocalDiffeomorph.preimage_interior (hn : n ≠ 0) {f : M → N} + (hf : IsLocalDiffeomorph I I' n f) : f ⁻¹' I'.interior N = I.interior M := by + simpa using (hf.isLocalDiffeomorphOn univ).preimage_interior_inter hn + +lemma _root_.IsLocalDiffeomorph.preimage_boundary (hn : n ≠ 0) {f : M → N} + (hf : IsLocalDiffeomorph I I' n f) : f ⁻¹' I'.boundary N = I.boundary M := by + simpa using (hf.isLocalDiffeomorphOn univ).preimage_boundary_inter hn + +lemma _root_.IsLocalDiffeomorph.boundarylessManifold (hn : n ≠ 0) {f : M → N} + (hf : IsLocalDiffeomorph I I' n f) [BoundarylessManifold I' N] : BoundarylessManifold I M := by + simp [← Boundaryless.iff_boundary_eq_empty, ← hf.preimage_boundary hn, + Boundaryless.boundary_eq_empty] + +lemma _root_.Diffeomorph.preimage_interior (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ ⁻¹' I'.interior N = I.interior M := + Φ.isLocalDiffeomorph.preimage_interior hn + +lemma _root_.Diffeomorph.preimage_boundary (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ ⁻¹' I'.boundary N = I.boundary M := + Φ.isLocalDiffeomorph.preimage_boundary hn + +lemma _root_.Diffeomorph.image_interior (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ '' I.interior M = I'.interior N := + (Φ.eq_preimage_iff_image_eq _ _).1 (Φ.preimage_interior hn).symm + +lemma _root_.Diffeomorph.image_boundary (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + Φ '' I.boundary M = I'.boundary N := + (Φ.eq_preimage_iff_image_eq _ _).1 (Φ.preimage_boundary hn).symm + +lemma _root_.Diffeomorph.boundarylessManifold (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) + [BoundarylessManifold I M] : BoundarylessManifold I' N := + Φ.symm.isLocalDiffeomorph.boundarylessManifold hn + +lemma _root_.Diffeomorph.boundarylessManifold_iff (hn : n ≠ 0) (Φ : M ≃ₘ^n⟮I, I'⟯ N) : + BoundarylessManifold I M ↔ BoundarylessManifold I' N := + ⟨fun _ ↦ Φ.boundarylessManifold hn, fun _ ↦ Φ.symm.boundarylessManifold hn⟩ + +end Diffeomorph + /-! Interior and boundary of open subsets of a manifold. -/ section opens @@ -410,8 +514,6 @@ end prod section disjointUnion variable {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞} - {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] - {N N' : Type*} [TopologicalSpace N] [TopologicalSpace N'] [ChartedSpace H' N] [ChartedSpace H' N'] open Topology