feat: the disjoint union of smooth manifolds (#20659)

- the disjoint union of smooth manifolds is a smooth manifold
- the interior and boundary are the disjoint union of the interior and boundary; the disjoint union of boundaryless manifolds is boundaryless

A future PR will prove that `Sum.inl` and `Sum.inr` between `C^n` manifolds are C^n.

From my bordism theory branch.

Author: grunweg

Mathlib/Data/Set/Basic.lean

@@ -1353,6 +1353,11 @@ theorem compl_univ_iff {s : Set α} : sᶜ = univ ↔ s = ∅ :=
 theorem compl_ne_univ : sᶜ ≠ univ ↔ s.Nonempty :=
   compl_univ_iff.not.trans nonempty_iff_ne_empty.symm
 
+lemma inl_compl_union_inr_compl {α β : Type*} {s : Set α} {t : Set β} :
+    Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ := by
+  rw [compl_union]
+  aesop
+
 theorem nonempty_compl : sᶜ.Nonempty ↔ s ≠ univ :=
   (ne_univ_iff_exists_not_mem s).symm
 

Mathlib/Data/Sum/Basic.lean

@@ -17,6 +17,8 @@ universe u v w x
 
 variable {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {γ δ : Type*}
 
+lemma not_isLeft_and_isRight {x : α ⊕ β} : ¬(x.isLeft ∧ x.isRight) := by simp
+
 namespace Sum
 
 -- Lean has removed the `@[simp]` attribute on these. For now Mathlib adds it back.

Mathlib/Geometry/Manifold/InteriorBoundary.lean

@@ -28,6 +28,13 @@ of `M` and `N`.
 - `ModelWithCorners.boundary_prod`: the boundary of `M × N` is `∂M × N ∪ (M × ∂N)`.
 - `ModelWithCorners.BoundarylessManifold.prod`: if `M` and `N` are boundaryless, so is `M × N`
 
+- `ModelWithCorners.interior_disjointUnion`: the interior of a disjoint union `M ⊔ M'`
+  is the union of the interior of `M` and `M'`
+- `ModelWithCorners.boundary_disjointUnion`: the boundary of a disjoint union `M ⊔ M'`
+  is the union of the boundaries of `M` and `M'`
+- `ModelWithCorners.boundaryless_disjointUnion`: if `M` and `M'` are boundaryless,
+  so is their disjoint union `M ⊔ M'`
+
 ## Tags
 manifold, interior, boundary
 
@@ -85,7 +92,7 @@ lemma isBoundaryPoint_iff {x : M} : I.IsBoundaryPoint x ↔ extChartAt I x x ∈
 lemma isInteriorPoint_or_isBoundaryPoint (x : M) : I.IsInteriorPoint x ∨ I.IsBoundaryPoint x := by
   rw [IsInteriorPoint, or_iff_not_imp_left, I.isBoundaryPoint_iff, ← closure_diff_interior,
     I.isClosed_range.closure_eq, mem_diff]
-  exact fun h => ⟨mem_range_self _, h⟩
+  exact fun h ↦ ⟨mem_range_self _, h⟩
 
 /-- A manifold decomposes into interior and boundary. -/
 lemma interior_union_boundary_eq_univ : (I.interior M) ∪ (I.boundary M) = (univ : Set M) :=
@@ -97,13 +104,22 @@ lemma disjoint_interior_boundary : Disjoint (I.interior M) (I.boundary M) := by
   -- Choose some x in the intersection of interior and boundary.
   obtain ⟨x, h1, h2⟩ := not_disjoint_iff.mp h
   rw [← mem_empty_iff_false (extChartAt I x x),
-    ← disjoint_iff_inter_eq_empty.mp (disjoint_interior_frontier (s := range I)), mem_inter_iff]
+    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
   exact ⟨h1, h2⟩
 
+lemma isInteriorPoint_iff_not_isBoundaryPoint (x : M) :
+    I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x := by
+  refine ⟨?_,
+    by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)⟩
+  by_contra! h
+  rw [← mem_empty_iff_false (extChartAt I x x),
+    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
+  exact h
+
 /-- 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
-  exact disjoint_iff_inter_eq_empty.mp (I.disjoint_interior_boundary)
+  exact disjoint_iff_inter_eq_empty.mp I.disjoint_interior_boundary
 
 /-- The interior is the complement of the boundary. -/
 lemma compl_boundary : (I.boundary M)ᶜ = I.interior M:= by
@@ -231,4 +247,115 @@ instance BoundarylessManifold.prod [BoundarylessManifold I M] [BoundarylessManif
 
 end prod
 
+section disjointUnion
+
+variable {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] {n : WithTop ℕ∞}
+  [hM : IsManifold I n M] [hM' : IsManifold I n M']
+  [Nonempty M] [Nonempty M'] [Nonempty H]
+  {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
+  {J : Type*} {J : ModelWithCorners 𝕜 E' H'}
+  {N N' : Type*} [TopologicalSpace N] [TopologicalSpace N'] [ChartedSpace H' N] [ChartedSpace H' N']
+  [IsManifold J n N] [IsManifold J n N'] [Nonempty N] [Nonempty N'] [Nonempty H']
+
+open Topology
+
+lemma interiorPoint_inl (x : M) (hx : I.IsInteriorPoint x) :
+    I.IsInteriorPoint (.inl x: M ⊕ M') := by
+  rw [I.isInteriorPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]
+  dsimp only [PartialHomeomorph.extend.eq_1, PartialEquiv.trans_target, toPartialEquiv_coe_symm,
+    PartialHomeomorph.lift_openEmbedding_target, PartialEquiv.coe_trans, toPartialEquiv_coe,
+    PartialHomeomorph.toFun_eq_coe, PartialHomeomorph.lift_openEmbedding_toFun, Function.comp_apply]
+  rw [Sum.inl_injective.extend_apply (chartAt H x)]
+  simpa [I.isInteriorPoint_iff, extChartAt] using hx
+
+lemma boundaryPoint_inl (x : M) (hx : I.IsBoundaryPoint x) :
+    I.IsBoundaryPoint (.inl x: M ⊕ M') := by
+  rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]
+  dsimp
+  rw [Sum.inl_injective.extend_apply (chartAt H x)]
+  simpa [I.isBoundaryPoint_iff, extChartAt] using hx
+
+lemma interiorPoint_inr (x : M') (hx : I.IsInteriorPoint x) :
+    I.IsInteriorPoint (.inr x : M ⊕ M') := by
+  rw [I.isInteriorPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inr]
+  dsimp
+  rw [Sum.inr_injective.extend_apply (chartAt H x)]
+  simpa [I.isInteriorPoint_iff, extChartAt] using hx
+
+lemma boundaryPoint_inr (x : M') (hx : I.IsBoundaryPoint x) :
+    I.IsBoundaryPoint (.inr x : M ⊕ M') := by
+  rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inr]
+  dsimp
+  rw [Sum.inr_injective.extend_apply (chartAt H x)]
+  simpa [I.isBoundaryPoint_iff, extChartAt] using hx
+
+-- Converse to the previous direction: if `x` were not an interior point,
+-- it had to be a boundary point, hence `p` were a boundary point also, contradiction.
+lemma isInteriorPoint_disjointUnion_left {p : M ⊕ M'} (hp : I.IsInteriorPoint p)
+    (hleft : Sum.isLeft p) : I.IsInteriorPoint (Sum.getLeft p hleft) := by
+  by_contra h
+  set x := Sum.getLeft p hleft
+  rw [isInteriorPoint_iff_not_isBoundaryPoint x, not_not] at h
+  rw [isInteriorPoint_iff_not_isBoundaryPoint p] at hp
+  have := boundaryPoint_inl (M' := M') x (by tauto)
+  rw [← Sum.eq_left_getLeft_of_isLeft hleft] at this
+  exact hp this
+
+lemma isInteriorPoint_disjointUnion_right {p : M ⊕ M'} (hp : I.IsInteriorPoint p)
+    (hright : Sum.isRight p) : I.IsInteriorPoint (Sum.getRight p hright) := by
+  by_contra h
+  set x := Sum.getRight p hright
+  rw [← mem_empty_iff_false p, ← (disjoint_interior_boundary (I := I)).inter_eq]
+  constructor
+  · rw [ModelWithCorners.interior, mem_setOf]; exact hp
+  · rw [ModelWithCorners.boundary, mem_setOf, Sum.eq_right_getRight_of_isRight hright]
+    have := isInteriorPoint_or_isBoundaryPoint (I := I) x
+    exact boundaryPoint_inr (M' := M') x (by tauto)
+
+lemma interior_disjointUnion :
+    ModelWithCorners.interior (I := I) (M ⊕ M') =
+      Sum.inl '' (ModelWithCorners.interior (I := I) M)
+      ∪ Sum.inr '' (ModelWithCorners.interior (I := I) M') := by
+  ext p
+  constructor
+  · intro hp
+    by_cases h : Sum.isLeft p
+    · left
+      exact ⟨Sum.getLeft p h, isInteriorPoint_disjointUnion_left hp h, Sum.inl_getLeft p h⟩
+    · replace h := Sum.not_isLeft.mp h
+      right
+      exact ⟨Sum.getRight p h, isInteriorPoint_disjointUnion_right hp h, Sum.inr_getRight p h⟩
+  · intro hp
+    by_cases h : Sum.isLeft p
+    · set x := Sum.getLeft p h with x_eq
+      rw [Sum.eq_left_getLeft_of_isLeft h]
+      apply interiorPoint_inl x
+      have hp : p ∈ Sum.inl '' (ModelWithCorners.interior (I := I) M) := by
+        obtain (good | ⟨y, hy, hxy⟩) := hp
+        exacts [good, (not_isLeft_and_isRight ⟨h, by rw [← hxy]; exact rfl⟩).elim]
+      obtain ⟨x', hx', hx'p⟩ := hp
+      simpa [x_eq, ← hx'p, Sum.getLeft_inl]
+    · set x := Sum.getRight p (Sum.not_isLeft.mp h) with x_eq
+      rw [Sum.eq_right_getRight_of_isRight (Sum.not_isLeft.mp h)]
+      apply interiorPoint_inr x
+      have hp : p ∈ Sum.inr '' (ModelWithCorners.interior (I := I) M') := by
+        obtain (⟨y, hy, hxy⟩ | good) := hp
+        exacts [(not_isLeft_and_isRight ⟨by rw [← hxy]; exact rfl, Sum.not_isLeft.mp h⟩).elim, good]
+      obtain ⟨x', hx', hx'p⟩ := hp
+      simpa [x_eq, ← hx'p, Sum.getRight_inr]
+
+lemma boundary_disjointUnion : ModelWithCorners.boundary (I := I) (M ⊕ M') =
+      Sum.inl '' (ModelWithCorners.boundary (I := I) M)
+      ∪ Sum.inr '' (ModelWithCorners.boundary (I := I) M') := by
+  simp only [← ModelWithCorners.compl_interior, interior_disjointUnion, inl_compl_union_inr_compl]
+
+/-- If `M` and `M'` are boundaryless, so is their disjoint union `M ⊔ M'`. -/
+instance boundaryless_disjointUnion
+    [hM: BoundarylessManifold I M] [hM': BoundarylessManifold I M'] :
+    BoundarylessManifold I (M ⊕ M') := by
+  rw [← Boundaryless.iff_boundary_eq_empty] at hM hM' ⊢
+  simp [boundary_disjointUnion, hM, hM']
+
+end disjointUnion
+
 end ModelWithCorners

Mathlib/Geometry/Manifold/IsManifold.lean

@@ -46,6 +46,11 @@ but add these assumptions later as needed. (Quite a few results still do not req
   we register them as `PartialEquiv`s.
   `extChartAt I x` is the canonical such partial equiv around `x`.
 
+We define a few constructions of smooth manifolds:
+* every empty type is a smooth manifold
+* the product of two smooth manifolds
+* the disjoint union of two manifolds (over the same charted space)
+
 As specific examples of models with corners, we define (in `Geometry.Manifold.Instances.Real`)
 * `modelWithCornersEuclideanHalfSpace n :
   ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)` for the model space used to
@@ -598,6 +603,26 @@ theorem contDiffGroupoid_zero_eq : contDiffGroupoid 0 I = continuousGroupoid H :
   · refine I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)
     exact (mapsTo_preimage _ _).mono_left inter_subset_left
 
+-- FIXME: does this generalise to other groupoids? The argument is not specific
+-- to C^n functions, but uses something about the groupoid's property that is not easy to abstract.
+/-- Any change of coordinates with empty source belongs to `contDiffGroupoid`. -/
+lemma ContDiffGroupoid.mem_of_source_eq_empty (f : PartialHomeomorph H H)
+    (hf : f.source = ∅) : f ∈ contDiffGroupoid n I := by
+  constructor
+  · intro x ⟨hx, _⟩
+    rw [mem_preimage] at hx
+    simp_all only [mem_empty_iff_false]
+  · intro x ⟨hx, _⟩
+    have : f.target = ∅ := by simp [← f.image_source_eq_target, hf]
+    simp_all [hx]
+
+include I in
+/-- Any change of coordinates with empty source belongs to `continuousGroupoid`. -/
+lemma ContinuousGroupoid.mem_of_source_eq_empty (f : PartialHomeomorph H H)
+    (hf : f.source = ∅) : f ∈ continuousGroupoid H := by
+  rw [← contDiffGroupoid_zero_eq (I := I)]
+  exact ContDiffGroupoid.mem_of_source_eq_empty f hf
+
 /-- An identity partial homeomorphism belongs to the `C^n` groupoid. -/
 theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
     PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I := by
@@ -797,6 +822,34 @@ instance prod {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedA
     have h2 := (contDiffGroupoid n I').compatible hf2 hg2
     exact contDiffGroupoid_prod h1 h2
 
+section DisjointUnion
+
+variable {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M']
+  [hM : IsManifold I n M] [hM' : IsManifold I n M']
+
+/-- The disjoint union of two `C^n` manifolds modelled on `(E, H)`
+is a `C^n` manifold modeled on `(E, H)`. -/
+instance disjointUnion [Nonempty M] [Nonempty M'] [Nonempty H] : IsManifold I n (M ⊕ M') where
+  compatible {e} e' he he' := by
+    obtain (⟨f, hf, hef⟩ | ⟨f, hf, hef⟩) := ChartedSpace.mem_atlas_sum he
+    · obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
+      · rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inl]
+        exact hM.compatible hf hf'
+      · rw [hef, he'f']
+        apply ContDiffGroupoid.mem_of_source_eq_empty
+        ext x
+        exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all [hx₂], fun hx ↦ hx.elim⟩
+    · -- Analogous argument to the first case: is there a way to deduplicate?
+      obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
+      · rw [hef, he'f']
+        apply ContDiffGroupoid.mem_of_source_eq_empty
+        ext x
+        exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all [hx₂], fun hx ↦ hx.elim⟩
+      · rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inr]
+        exact hM'.compatible hf hf'
+
+end DisjointUnion
+
 end IsManifold
 
 theorem PartialHomeomorph.isManifold_singleton
@@ -1675,4 +1728,4 @@ instance : PathConnectedSpace (TangentSpace I x) := inferInstanceAs (PathConnect
 
 end Real
 
-set_option linter.style.longFile 1700
+set_option linter.style.longFile 1900

Mathlib/Topology/PartialHomeomorph.lean

@@ -1374,10 +1374,6 @@ lemma lift_openEmbedding_apply (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding
   simp_rw [e.lift_openEmbedding_toFun]
   apply hf.injective.extend_apply
 
-@[simp]
-lemma lift_openEmbedding_symm (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
-    (e.lift_openEmbedding hf).symm = f ∘ e.symm := rfl
-
 @[simp]
 lemma lift_openEmbedding_source (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
     (e.lift_openEmbedding hf).source = f '' e.source := rfl
@@ -1386,4 +1382,34 @@ lemma lift_openEmbedding_source (e : PartialHomeomorph X Z) (hf : IsOpenEmbeddin
 lemma lift_openEmbedding_target (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
     (e.lift_openEmbedding hf).target = e.target := rfl
 
+@[simp]
+lemma lift_openEmbedding_symm (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
+    (e.lift_openEmbedding hf).symm = f ∘ e.symm := rfl
+
+@[simp]
+lemma lift_openEmbedding_symm_source (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
+    (e.lift_openEmbedding hf).symm.source = e.target := rfl
+
+@[simp]
+lemma lift_openEmbedding_symm_target (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
+    (e.lift_openEmbedding hf).symm.target = f '' e.source := by
+  rw [PartialHomeomorph.symm_target, e.lift_openEmbedding_source]
+
+lemma lift_openEmbedding_trans_apply
+    (e e' : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) (z : Z) :
+    (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) z = (e.symm.trans e') z := by
+  simp [hf.injective.extend_apply e']
+
+@[simp]
+lemma lift_openEmbedding_trans (e e' : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
+    (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e' := by
+  ext x
+  · exact e.lift_openEmbedding_trans_apply e' hf x
+  · simp [hf.injective.extend_apply e]
+  · simp_rw [PartialHomeomorph.trans_source, e.lift_openEmbedding_symm_source, e.symm_source,
+      e.lift_openEmbedding_symm, e'.lift_openEmbedding_source]
+    refine ⟨fun ⟨hx, ⟨y, hy, hxy⟩⟩ ↦ ⟨hx, ?_⟩, fun ⟨hx, hx'⟩ ↦ ⟨hx, mem_image_of_mem f hx'⟩⟩
+    rw [mem_preimage]; rw [comp_apply] at hxy
+    exact (hf.injective hxy) ▸ hy
+
 end PartialHomeomorph