Irreducible manifold predicate

This file packages the tame sphere-bounds-a-ball condition used as the irreducibility hypothesis for Haken 3-manifolds. The disk and its boundary are Mathlib's standard 𝔻 3 and 𝕊 2 objects, so the predicate quantifies over closed locally flat embedded spheres and embedded balls extending them.

Main definitions

• TauCeti.IsSphereBoundsBall: every closed locally flat embedded 2-sphere bounds an embedded 3-ball.

Main results

• TauCeti.isSphereBoundsBall_iff: the defining characterization of IsSphereBoundsBall.

def TauCeti.IsSphereBoundsBall (M : Type u) [TopologicalSpace M] : Prop

A space satisfies the sphere-bounds-a-ball condition when every closed locally flat embedded 2-sphere extends across an embedded 3-ball. The disk and its boundary are Mathlib's standard 𝔻 3 and 𝕊 2 objects, so this is the usual tame condition used in irreducible 3-manifolds.

@[simp]

theorem TauCeti.isSphereBoundsBall_iff (M : Type u) [TopologicalSpace M] : IsSphereBoundsBall M ↔ ∀ (f : C(↑(TopCat.sphere 2), M)), Topology.IsClosedEmbedding ⇑f → IsLocallyFlat (EuclideanSpace ℝ (Fin 2)) ℝ ⇑f → ∃ (g : C(↑(TopCat.disk 3), M)), Topology.IsClosedEmbedding ⇑g ∧ g.comp (TopCat.Hom.hom (TopCat.diskBoundaryInclusion 3)) = f

The sphere-bounds-a-ball condition defining IsSphereBoundsBall.