feat (TopCat.Sphere) : add the open ball, instances

Author: robertmaxton42

Mathlib/Topology/Category/TopCat/Sphere.lean

@@ -5,19 +5,20 @@ Authors: Jiazhen Xia, Elliot Dean Young
 -/
 
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import Mathlib.Topology.Category.TopCat.Basic
+import Mathlib.Topology.Category.TopCat.EpiMono
 
 /-!
 # Euclidean spheres
 
-This files defines the `n`-sphere `𝕊 n`, the `n`-disk `𝔻 n` and its
-boundary `∂𝔻 n` as objects in `TopCat`.
+This files defines the `n`-sphere `𝕊 n`, the `n`-disk `𝔻 n`, its boundary `∂𝔻 n` and its interior
+`𝔹 n` as objects in `TopCat`.
 
 -/
 
 universe u
 
 namespace TopCat
+open CategoryTheory
 
 /-- The `n`-disk is the set of points in ℝⁿ whose norm is at most `1`,
 endowed with the subspace topology. -/
@@ -33,6 +34,11 @@ endowed with the subspace topology. -/
 noncomputable def sphere (n : ℕ) : TopCat.{u} :=
   diskBoundary (n + 1)
 
+/-- The `n`-ball is the set of points in ℝⁿ whose norm is strictly less than `1`,
+endowed with the subspace topology. -/
+noncomputable def ball (n : ℕ) : TopCat.{u} :=
+  TopCat.of <| ULift <| Metric.ball (0 : EuclideanSpace ℝ (Fin n)) 1
+
 /-- `𝔻 n` denotes the `n`-disk. -/
 scoped prefix:arg "𝔻 " => disk
 
@@ -42,6 +48,9 @@ scoped prefix:arg "∂𝔻 " => diskBoundary
 /-- `𝕊 n` denotes the `n`-sphere. -/
 scoped prefix:arg "𝕊 " => sphere
 
+/-- `𝔹 n` denotes the `n`-ball, the interior of the `n`-disk. -/
+scoped prefix:arg "𝔹 " => ball
+
 /-- The inclusion `∂𝔻 n ⟶ 𝔻 n` of the boundary of the `n`-disk. -/
 def diskBoundaryInclusion (n : ℕ) : ∂𝔻 n ⟶ 𝔻 n :=
   ofHom
@@ -50,4 +59,32 @@ def diskBoundaryInclusion (n : ℕ) : ∂𝔻 n ⟶ 𝔻 n :=
         rw [isOpen_induced_iff, ← hst, ← hrs]
         tauto⟩ }
 
+/-- The inclusion `𝔹 n ⟶ 𝔻 n` of the interior of the `n`-disk. -/
+def ballInclusion (n : ℕ) : 𝔹 n ⟶ 𝔻 n :=
+  ofHom
+    { toFun := fun ⟨p, hp⟩ ↦ ⟨p, Metric.ball_subset_closedBall hp⟩
+      continuous_toFun := ⟨fun t ⟨s, ⟨r, hro, hrs⟩, hst⟩ ↦ by
+        rw [isOpen_induced_iff, ← hst, ← hrs]
+        tauto⟩ }
+
+instance {n : ℕ} : Mono (diskBoundaryInclusion n) := mono_iff_injective _ |>.mpr <| by
+  intro ⟨x, hx⟩ ⟨y, hy⟩ h
+  simp [diskBoundaryInclusion, disk] at h
+  cases h; rfl
+
+instance {n : ℕ} : Mono (ballInclusion n) := TopCat.mono_iff_injective _ |>.mpr <| by
+  intro ⟨x, hx⟩ ⟨y, hy⟩ h
+  simp [ballInclusion, disk] at h
+  cases h; rfl
+
+instance compact_disk (n : ℕ) : CompactSpace (𝔻 n) := by
+  convert Homeomorph.compactSpace Homeomorph.ulift.symm
+  rw [← isCompact_iff_compactSpace]
+  fapply ProperSpace.isCompact_closedBall
+
+instance compact_sphere (n : ℕ) : CompactSpace (∂𝔻 n) := by
+  convert Homeomorph.compactSpace Homeomorph.ulift.symm
+  rw [← isCompact_iff_compactSpace]
+  fapply isCompact_sphere
+
 end TopCat