Locally flat embeddings are locally bicollared

A locally flat embedding is one that ambient charts flatten onto the standard coordinate slice (TauCeti.IsLocallyFlat). This file extracts from those charts the structure they were isolated to provide: near each point of the domain, an open neighbourhood of the image that is a product, with the image sitting inside it as the zero slice.

In codimension one that structure is a bicollar: an open embedding b : N × ℝ → M with b (x, 0) = f x, so that the image is two-sided inside the open set the collar sweeps out. This is the notion Brown's collaring theorem is about, and the reason local flatness is the hypothesis under which topological manifolds behave: the Alexander horned sphere is an embedded 2-sphere in S³ that is not locally bicollared because it has wild points at which no neighbourhood pair is homeomorphic to the standard coordinate-slice pair.

The file proves both directions of the comparison.

• Local flatness gives local bicollars. The general local-product theorem TauCeti.IsLocallyFlat.exists_isOpenEmbedding_prod from LocallyFlat.Basic, specialised to a one-dimensional complementary model, gives TauCeti.IsLocallyFlat.isLocallyBicollared.
• A bicollar is a local flattening. TauCeti.IsBicollar.isLocallyFlat runs the comparison backwards: a collared map factors through the standard slice N → N × ℝ, which is locally flat once N is charted on F, and local flatness is stable under composing with an open embedding. Needing the domain to be charted on F is where the "an (n-1)-manifold in an n-manifold" of the informal statement enters.

Together they give TauCeti.isLocallyFlat_iff_isEmbedding_and_isLocallyBicollared: over a domain charted on F, a map is locally flat with one-dimensional complementary model exactly when it is an embedding that is locally bicollared. The embedding hypothesis cannot be dropped: a figure-eight immersion of a line into the plane is locally bicollared and is not an embedding, since bicollars only see the domain locally.

This is the codimension-one collaring bullet of layer 2 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md). What remains of that bullet is its global sphere conclusion: a locally flat (n-1)-sphere in Sⁿ is bicollared. That conclusion needs a genuinely global collaring argument and is not proved here. Positive-codimension normal bundles, the companion notion, are flagged by the roadmap as a dependency to be taken from elsewhere rather than built in this layer.

Main definitions

• TauCeti.IsBicollar: an open embedding N × ℝ → M whose zero slice is a given map.
• TauCeti.IsBicollared: admitting a bicollar.
• TauCeti.IsLocallyBicollared: every point of the domain has an open neighbourhood on which the restriction is bicollared.

The last two are defs whose bodies the module system does not expose, so TauCeti.isBicollared_iff and TauCeti.isLocallyBicollared_iff are the only way to introduce or eliminate them downstream.

Main results

• TauCeti.IsLocallyFlat.isLocallyBicollared: a locally flat embedding of codimension one is locally bicollared.
• TauCeti.IsBicollar.isLocallyFlat, TauCeti.IsLocallyBicollared.isLocallyFlat and TauCeti.isLocallyFlat_iff_isEmbedding_and_isLocallyBicollared: the converse, and the resulting characterisation.
• TauCeti.IsBicollar.range_diff_range_eq_union and TauCeti.IsBicollar.disjoint_image_Ioi_Iio: the two sides of a bicollar are disjoint and cover the complement of the image inside the collar.
• TauCeti.IsBicollared.exists_isOpen_sdiff_range_eq_union: a bicollared map with nonempty domain is two-sided.
• TauCeti.IsLocallyBicollared.restrict, TauCeti.IsLocallyBicollared.isOpenEmbedding_comp, and TauCeti.IsLocallyBicollared.comp_homeomorph: the local predicate's basic closure API.

References

• M. Brown, Locally flat imbeddings of topological manifolds, Annals of Mathematics 75 (1962), 331–341, for the global collaring theorem this is the local half of.
• R. Daverman and G. Venema, Embeddings in Manifolds, AMS Graduate Studies in Mathematics 106 (2009), Chapter 2, for bicollars and their role in codimension one.

Bicollars

structure TauCeti.IsBicollar {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (f : N → M) (b : N × ℝ → M) : Prop

A bicollar of a map f : N → M is an open embedding b : N × ℝ → M whose zero slice is f. It exhibits an open neighbourhood of the image of f as a product of N with a line, in which the image is the zero slice; in particular the image is two-sided inside that neighbourhood.

• isOpenEmbedding : Topology.IsOpenEmbedding b

  A bicollar is an open embedding of the product of the domain with a line.

• apply_zero (x : N) : b (x, 0) = f x

  The zero slice of a bicollar is the map it collars.

def TauCeti.IsBicollared {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (f : N → M) : Prop

A map is bicollared if it admits a bicollar.

def TauCeti.IsLocallyBicollared {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (f : N → M) : Prop

A map is locally bicollared if every point of its domain has an open neighbourhood on which the restriction of the map is bicollared. Unlike being bicollared, this says nothing globally: it does not even imply that the map is injective.

theorem TauCeti.isBicollared_iff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} : IsBicollared f ↔ ∃ (b : N × ℝ → M), IsBicollar f b

Being bicollared spelled out: some open embedding of N × ℝ has f as its zero slice. The module system does not expose the body of TauCeti.IsBicollared, so a downstream file cannot unfold it; this lemma is how the definition is introduced and eliminated there.

theorem TauCeti.isLocallyBicollared_iff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} : IsLocallyBicollared f ↔ ∀ (x : N), ∃ (U : Set N), IsOpen U ∧ x ∈ U ∧ IsBicollared (f ∘ Subtype.val)

Being locally bicollared spelled out: every point of the domain has an open neighbourhood on which the restriction of the map is bicollared. The module system does not expose the body of TauCeti.IsLocallyBicollared, so a downstream file cannot unfold it; this lemma is how the definition is introduced and eliminated there.

theorem TauCeti.IsBicollar.isBicollared {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : IsBicollared f

A bicollar witnesses that the map it collars is bicollared.

theorem TauCeti.IsBicollar.isEmbedding {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : Topology.IsEmbedding f

theorem TauCeti.IsBicollar.continuous {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : Continuous f

theorem TauCeti.IsBicollar.injective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : Function.Injective f

theorem TauCeti.IsBicollar.range_subset_range {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : Set.range f ⊆ Set.range b

The image of a collared map lies in the open set its bicollar sweeps out.

theorem TauCeti.IsBicollar.image_prod_singleton_zero {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : b '' Set.univ ×ˢ {0} = Set.range f

Read in a bicollar, the collared image is exactly the zero slice.

@[simp]

theorem TauCeti.IsBicollar.preimage_range {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : b ⁻¹' Set.range f = Set.univ ×ˢ {0}

A bicollar meets the image of the map it collars only along the zero slice.

theorem TauCeti.IsBicollar.range_diff_range_eq_union {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : Set.range b \ Set.range f = b '' Set.univ ×ˢ Set.Ioi 0 ∪ b '' Set.univ ×ˢ Set.Iio 0

Inside a bicollar the complement of the collared image splits into the two sides t > 0 and t < 0 of the collar. This is what makes the collar two-sided, and it is exactly what fails for a wild embedding.

theorem TauCeti.IsBicollar.disjoint_image_Ioi_Iio {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : Disjoint (b '' Set.univ ×ˢ Set.Ioi 0) (b '' Set.univ ×ˢ Set.Iio 0)

The two sides of a bicollar are disjoint.

theorem TauCeti.IsBicollar.apply_mem_closure_image {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) {s : Set ℝ} (hs : 0 ∈ closure s) (x : N) : f x ∈ closure (b '' Set.univ ×ˢ s)

Every point of the image of a bicollared map is a limit of points of the bicollar at depths in s, if 0 is in the closure of s.

theorem TauCeti.IsBicollar.restrict {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) {U : Set N} (hU : IsOpen U) : IsBicollar (f ∘ Subtype.val) (b ∘ Prod.map Subtype.val id)

A bicollar restricts to a bicollar over any open subset of the domain.

theorem TauCeti.IsBicollar.isOpenEmbedding_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] {f : N → M} {b : N × ℝ → M} {g : M → P} (h : IsBicollar f b) (hg : Topology.IsOpenEmbedding g) : IsBicollar (g ∘ f) (g ∘ b)

Bicollars are carried along by open embeddings of the ambient space.

theorem TauCeti.IsBicollar.comp_homeomorph {M : Type u_1} {N : Type u_2} {N' : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) (e : N' ≃ₜ N) : IsBicollar (f ∘ ⇑e) (b ∘ Prod.map (⇑e) id)

Bicollars are carried along by homeomorphisms of the domain.

theorem TauCeti.IsBicollar.comp_prodMap_id_neg {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} {b : N × ℝ → M} (h : IsBicollar f b) : IsBicollar f (b ∘ Prod.map id Neg.neg)

Reversing the depth coordinate of a bicollar gives a bicollar, with its two sides exchanged.

theorem TauCeti.IsBicollar.sigma {M : Type u_1} [TopologicalSpace M] {ι : Type u_7} {N : ι → Type u_8} [(i : ι) → TopologicalSpace (N i)] {f : (i : ι) → N i → M} {b : (i : ι) → N i × ℝ → M} (h : ∀ (i : ι), IsBicollar (f i) (b i)) (hb : Pairwise (Function.onFun Disjoint fun (i : ι) => Set.range (b i))) : IsBicollar (fun (x : (i : ι) × N i) => f x.fst x.snd) fun (p : ((i : ι) × N i) × ℝ) => b p.1.fst (p.1.snd, p.2)

Bicollars with pairwise disjoint images assemble into a bicollar of the map they collar on the disjoint union of their domains.

theorem TauCeti.isBicollar_prodMkLeft {N : Type u_2} [TopologicalSpace N] : IsBicollar (fun (x : N) => (x, 0)) id

The standard local model: the inclusion of N as the zero slice of N × ℝ is bicollared, by the identity.

theorem TauCeti.IsBicollared.isEmbedding {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} (h : IsBicollared f) : Topology.IsEmbedding f

theorem TauCeti.IsBicollared.restrict {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} (h : IsBicollared f) {U : Set N} (hU : IsOpen U) : IsBicollared (f ∘ Subtype.val)

theorem TauCeti.IsBicollared.isOpenEmbedding_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] {f : N → M} {g : M → P} (h : IsBicollared f) (hg : Topology.IsOpenEmbedding g) : IsBicollared (g ∘ f)

theorem TauCeti.IsBicollared.comp_homeomorph {M : Type u_1} {N : Type u_2} {N' : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] {f : N → M} (h : IsBicollared f) (e : N' ≃ₜ N) : IsBicollared (f ∘ ⇑e)

theorem TauCeti.IsBicollared.isLocallyBicollared {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} (h : IsBicollared f) : IsLocallyBicollared f

theorem TauCeti.IsBicollared.exists_isOpen_sdiff_range_eq_union {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} [Nonempty N] (h : IsBicollared f) : ∃ (U : Set M) (V : Set M) (W : Set M), IsOpen U ∧ IsOpen V ∧ IsOpen W ∧ Set.range f ⊆ U ∧ V.Nonempty ∧ W.Nonempty ∧ Disjoint V W ∧ U \ Set.range f = V ∪ W

A bicollared map with nonempty domain is two-sided: its image has an open neighbourhood whose complement in that neighbourhood is the union of two disjoint nonempty open sets, the two sides of a bicollar. Each side is the collar image of the domain times an open half-line.

theorem TauCeti.IsLocallyBicollared.continuous {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} (h : IsLocallyBicollared f) : Continuous f

A locally bicollared map is continuous, being continuous on each open set on which it is bicollared.

theorem TauCeti.IsLocallyBicollared.restrict {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {f : N → M} (h : IsLocallyBicollared f) {U : Set N} (hU : IsOpen U) : IsLocallyBicollared (f ∘ Subtype.val)

Local bicollaring is inherited by the restriction to an open subset of the domain.

theorem TauCeti.IsLocallyBicollared.isOpenEmbedding_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] {f : N → M} {g : M → P} (h : IsLocallyBicollared f) (hg : Topology.IsOpenEmbedding g) : IsLocallyBicollared (g ∘ f)

Local bicollars are carried along by open embeddings of the ambient space.

theorem TauCeti.IsLocallyBicollared.comp_homeomorph {M : Type u_1} {N : Type u_2} {N' : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] {f : N → M} (h : IsLocallyBicollared f) (e : N' ≃ₜ N) : IsLocallyBicollared (f ∘ ⇑e)

Local bicollaring is invariant under homeomorphisms of the domain.

Local flatness and local bicollaring

A locally flat embedding has local product neighbourhoods by the general theorem in LocallyFlat.Basic. In codimension one those neighbourhoods are bicollars, and the construction reverses.

The codimension-one comparison

theorem TauCeti.IsLocallyFlat.isLocallyBicollared {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} (h : IsLocallyFlat F ℝ f) : IsLocallyBicollared f

A locally flat embedding of codimension one is locally bicollared. Each flattening chart, shrunk to a box, is a bicollar of the part of the map it sees.

theorem TauCeti.IsBicollar.isLocallyFlat {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} [ChartedSpace F N] {b : N × ℝ → M} (h : IsBicollar f b) : IsLocallyFlat F ℝ f

A bicollar makes its collared map locally flat, provided the domain is charted on F: the collar is an open embedding of N × ℝ, and the standard slice N → N × ℝ is locally flat there by TauCeti.isLocallyFlat_prodMkLeft.

theorem TauCeti.IsBicollared.isLocallyFlat {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} [ChartedSpace F N] (h : IsBicollared f) : IsLocallyFlat F ℝ f

A bicollared map whose domain is charted on F is locally flat with one-dimensional complementary model.

theorem TauCeti.IsLocallyBicollared.isLocallyFlat {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} [ChartedSpace F N] (h : IsLocallyBicollared f) (hf : Topology.IsEmbedding f) : IsLocallyFlat F ℝ f

A locally bicollared embedding whose domain is charted on F is locally flat with one-dimensional complementary model. Being an embedding is a genuine extra hypothesis, since bicollars are local data on the domain.

theorem TauCeti.isLocallyFlat_iff_isEmbedding_and_isLocallyBicollared {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} [ChartedSpace F N] : IsLocallyFlat F ℝ f ↔ Topology.IsEmbedding f ∧ IsLocallyBicollared f

Local flatness in codimension one is exactly local bicollaring, for an embedding. The embedding hypothesis is not automatic: bicollars are local data, so a non-injective immersion of a line into the plane is locally bicollared without being an embedding.