Incompressible embeddings

An embedding of a surface in a 3-manifold is incompressible when it is injective on the fundamental group. This file records the dimension-independent topological core of that condition. The embedding and π₁-injectivity conditions are stated independently of surface and manifold hypotheses so that this API can be reused in their presence.

The main predicate IsIncompressible combines a topological embedding with injectivity of the fundamental-group map at every basepoint. A continuous retraction supplies both properties, and the product inclusion x ↦ (x, y₀) is the basic example.

The definition follows the standard usage in 3-manifold topology; see A. Hatcher, Algebraic Topology, §1.2, and W. Jaco, Lectures on Three-Manifold Topology, Chapter II.

def TauCeti.IsIncompressible {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] (f : C(S, M)) : Prop

A continuous map is incompressible when it is a topological embedding and induces an injective map on fundamental groups at every basepoint. The separate embedding conjunct is intentional: π₁-injectivity alone does not prevent a map from identifying points.

Equations

• TauCeti.IsIncompressible f = (Topology.IsEmbedding ⇑f ∧ ∀ (s : S), Function.Injective ⇑(FundamentalGroup.map f s))

theorem TauCeti.isIncompressible_iff {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] {f : C(S, M)} : IsIncompressible f ↔ Topology.IsEmbedding ⇑f ∧ ∀ (s : S), Function.Injective ⇑(FundamentalGroup.map f s)

The defining embedding and fundamental-group injectivity conditions for an incompressible map.

theorem TauCeti.IsIncompressible.isEmbedding {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] {f : C(S, M)} (h : IsIncompressible f) : Topology.IsEmbedding ⇑f

The embedding part of an incompressible map.

theorem TauCeti.IsIncompressible.fundamentalGroup_injective {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] {f : C(S, M)} (h : IsIncompressible f) (s : S) : Function.Injective ⇑(FundamentalGroup.map f s)

The induced map on π₁ is injective at every basepoint.

theorem TauCeti.IsIncompressible.comp {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] {f : C(S, M)} {T : Type u_3} [TopologicalSpace T] {g : C(M, T)} (hg : IsIncompressible g) (hf : IsIncompressible f) : IsIncompressible (g.comp f)

The composition of incompressible maps is incompressible.

theorem TauCeti.isIncompressible_of_leftInverse {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] {f : C(S, M)} {r : C(M, S)} (h : r.comp f = ContinuousMap.id S) : IsIncompressible f

A continuous left inverse makes an embedding incompressible.

theorem TauCeti.isIncompressible_prodMk {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] (y₀ : M) : IsIncompressible ((ContinuousMap.id S).prodMk (ContinuousMap.const S y₀))

The product inclusion into a slice is incompressible.

theorem TauCeti.not_isIncompressible_of_simplyConnectedSpace {S : Type u_1} {M : Type u_2} [TopologicalSpace S] [TopologicalSpace M] [SimplyConnectedSpace M] (f : C(S, M)) (s : S) [Nontrivial (FundamentalGroup S s)] : ¬IsIncompressible f

A map from a space with a nontrivial fundamental group into a simply connected space is not incompressible.