Locally flat embeddings

Topological manifolds admit embeddings that no smooth embedding can imitate: the Alexander horned sphere is a topologically embedded 2-sphere in S³ bounding a non-simply-connected region, and a wild arc in ℝ³ is knotted although its domain is an interval. Theorems about topological manifolds therefore quantify over locally flat embeddings, those that in suitable ambient charts look like the standard coordinate slice.

This file introduces that notion and the structural API it is used through. The definition is built in three layers.

• TauCeti.IsSliceChart φ S A says that a single chart φ of the ambient space flattens the set A onto the model slice S, in the sense that φ '' (φ.source ∩ A) = φ.target ∩ S.
• TauCeti.IsSliceEmbedding S f says that f is a topological embedding admitting a slice chart for Set.range f around every point of its image. Here S is an arbitrary subset of an arbitrary model space, so this is not local flatness; it is the transport layer on which the closure properties are proved, and it is stated relatively so that they can be.
• TauCeti.IsLocallyFlat F F' f is local flatness proper: it is IsSliceEmbedding for the standard coordinate slice F × {0} of the model space F × F', so ambient charts take values in F × F' and carry the image of f exactly onto the vanishing locus of the last F' coordinates. With F = ℝⁿ and F' = ℝᵏ this is the textbook ℝⁿ × {0} ⊆ ℝⁿ⁺ᵏ.

Codimension is not baked in: it is the choice of the complementary model F', so codimension 0 (F' a subsingleton, where local flatness is openness of the embedding), codimension 1 (where collaring lives) and codimension 2 (where knotting lives) are all instances of the one predicate, which is the point.

Local flatness is a local condition, so the load-bearing content is not the definition but its closure properties: restriction to an open subset of the domain, locality, invariance under homeomorphisms and open embeddings on either side, invariance under a change of model space, and products. Those are proved here, together with two results that pin the notion down: in codimension zero local flatness is exactly openness of the embedding, and a locally flat embedding has locally closed image as soon as the origin of the complementary model is closed (on the relative layer, as soon as the model slice is locally closed).

This is layer 2 of the geometric-topology roadmap, the substrate for topologically locally flat discs (topological sliceness) and for stating the annulus conjecture.

Main definitions

• TauCeti.IsSliceChart: an ambient chart flattening a set onto a model slice.
• TauCeti.IsSliceChart.subtypeChart: the chart on a flattened set induced by a zero-slice chart, with values in the tangential model.
• TauCeti.IsSliceEmbedding: an embedding flattened onto a given model slice by ambient charts.
• TauCeti.IsLocallyFlat: a locally flat embedding, the case of the standard coordinate slice.

Main results

• TauCeti.isSliceChart_iff: a chart is a slice chart iff, on its source, membership in the set is read off as membership of the coordinates in the slice.
• TauCeti.IsSliceChart.exists_target_eq: a slice chart can be shrunk to have any prescribed open subset of its target as its target.
• TauCeti.isLocallyFlat_iff_isSliceEmbedding, TauCeti.isLocallyFlat_iff and TauCeti.IsLocallyFlat.exists_isSliceChart: the defining flattening charts, as the slice embedding for the standard slice, in pointwise form, and as an eliminator.
• TauCeti.IsLocallyFlat.restrict and TauCeti.IsLocallyFlat.of_forall_exists_isOpen: local flatness is a local property of the domain.
• TauCeti.IsLocallyFlat.isOpenEmbedding_comp, TauCeti.IsLocallyFlat.of_isOpenEmbedding_comp, TauCeti.IsLocallyFlat.codRestrict, TauCeti.IsLocallyFlat.homeomorph_comp, TauCeti.IsLocallyFlat.comp_isOpenEmbedding, TauCeti.IsLocallyFlat.comp_homeomorph: invariance under open embeddings and homeomorphisms of the ambient space and of the domain.
• TauCeti.IsSliceEmbedding.transHomeomorph: invariance under a homeomorphic change of model space, and TauCeti.IsLocallyFlat.transHomeomorph, its form for the complementary model of a locally flat embedding.
• TauCeti.IsLocallyFlat.comp: a composite of locally flat embeddings is locally flat, under an explicit hypothesis that their flattening charts can be chosen compatibly, and TauCeti.IsLocallyFlat.of_compatible_isSliceChart, the form of it that assumes only the compatible pair of charts.
• TauCeti.IsLocallyFlat.prodMap: a product of locally flat embeddings is locally flat.
• TauCeti.IsLocallyFlat.prodMap_of_isOpenEmbedding: the product of a locally flat embedding with an open embedding is locally flat, with the same complementary model.
• TauCeti.isLocallyFlat_iff_isOpenEmbedding: in codimension zero, locally flat means open.
• TauCeti.IsLocallyFlat.isLocallyClosed_range: a locally flat image is locally closed, as soon as the origin of the complementary model is closed.
• TauCeti.isLocallyFlat_prodMkLeft: over a domain charted on F, the standard model x ↦ (x, 0) is locally flat.
• TauCeti.isLocallyFlat_graph: the graph of a continuous map is locally flat.
• TauCeti.exists_isSliceChart_of_inter_eq_inter_range: a set which, near a point, is the graph of a continuous map over the first coordinate of a homeomorphism M ≃ₜ F × F' is flattened by a chart around that point.
• TauCeti.IsLocallyFlat.exists_isOpenEmbedding_prod: a locally flat embedding with seminormed complementary model has local product neighbourhoods.

Implementation notes

The relative predicate IsSliceEmbedding is deliberately not the definition of local flatness, and is not a substitute for it: its slice is an arbitrary subset of an arbitrary space, so taking the model space to be M itself, the slice to be Set.range f and the chart to be OpenPartialHomeomorph.refl M makes every embedding, wild ones included, a slice embedding. It is the layer on which transport is proved, because the closure properties genuinely need a slice that varies (a product of standard slices is a standard slice only after a permutation of coordinates, which is where IsSliceEmbedding.transHomeomorph is used). Local flatness is IsLocallyFlat F F' f, which fixes the slice to be the standard one, and that predicate does have teeth: TauCeti.isLocallyFlat_iff_isOpenEmbedding shows that in codimension zero it is equivalent to openness of the embedding, and TauCeti.IsLocallyFlat.isLocallyClosed_range rules out an image that is not locally closed, which the horned sphere's complement-side wildness aside is already enough to exclude embeddings no chart can flatten.

No membership in a prescribed atlas is required of the flattening chart: an OpenPartialHomeomorph M (F × F') is automatically a chart of the maximal topological atlas of a topological manifold M modelled on F × F', so demanding atlas membership would be redundant there and would needlessly restrict the definition on ambient spaces that are not manifolds. The model-space data enters exactly as it does for ChartedSpace, through the codomain of the charts.

A slice chart is only asked to flatten the set relative to its own target, that is φ '' (φ.source ∩ A) = φ.target ∩ S rather than φ.target = F together with φ '' (φ.source ∩ A) = S. The relative form is the one that is genuinely local, hence the one closed under restriction; the textbook form is not, since shrinking the source shrinks the target. For the standard model, a chart in the relative sense can be shrunk to a ball around the point and rescaled onto (ℝᵐ, ℝⁿ), recovering the textbook form, but that comparison needs the linear structure and is not formalised here.

Composing two locally flat embeddings N ↪ M ↪ P is not a formal consequence of the definition: the chart of M flattening the inner embedding and the chart of P flattening the outer one are chosen independently, and nothing makes them agree. TauCeti.IsLocallyFlat.comp therefore carries that agreement as an explicit hypothesis on charts witnessing the local flatness of the two factors — the outer chart reads the intermediate coordinates off the inner one along g — rather than assuming the conclusion; the outer chart then flattens the composite, and the complementary models multiply. Composition comes in two levels, because a witnessing chart can only be referred to by exhibiting it, so the compatibility hypothesis necessarily re-exhibits the two charts and thereby already carries the flattening content of the two factors. TauCeti.IsLocallyFlat.comp is the statement in the shape it is used and read, with both factors locally flat; TauCeti.IsLocallyFlat.of_compatible_isSliceChart is what its proof actually consumes, a compatible pair of charts around each point together with the embedding content of the conclusion itself, and comp is a two-line consequence of it. There the compatibility hypothesis is kept down to the part not already implied by the rest of it: the outer chart is only asked to detect range g in one direction, the other direction and the fact that the inner chart is a chart around f x both following from the agreement of the two charts together with injectivity of the outer map. Both are stated only for the standard slice, since the compatibility condition refers to the splitting F × F' of the intermediate model, which the relative layer does not have. The ambient codimension-zero case needs no such hypothesis and is kept separate, as TauCeti.IsLocallyFlat.isOpenEmbedding_comp and its converse.

References

• R. Daverman and G. Venema, Embeddings in Manifolds, AMS Graduate Studies in Mathematics 106 (2009), Chapter 1, for local flatness and wild embeddings.
• M. Brown, Locally flat imbeddings of topological manifolds, Annals of Mathematics 75 (1962), 331–341, for the collaring theorem that local flatness was isolated to prove.

def TauCeti.IsSliceChart {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] (φ : OpenPartialHomeomorph M F) (S : Set F) (A : Set M) : Prop

IsSliceChart φ S A says that the ambient chart φ flattens the set A onto the model slice S: the chart carries the part of A it sees exactly onto the part of S in its target.

Equations

• TauCeti.IsSliceChart φ S A = (↑φ '' (φ.source ∩ A) = φ.target ∩ S)

theorem TauCeti.isSliceChart_iff {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} : IsSliceChart φ S A ↔ ∀ y ∈ φ.source, y ∈ A ↔ ↑φ y ∈ S

A chart is a slice chart for A exactly when, on its source, membership in A can be read off as membership of the coordinates in the slice. This pointwise form is how the predicate is used.

theorem TauCeti.IsSliceChart.mem_iff {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} (h : IsSliceChart φ S A) {y : M} (hy : y ∈ φ.source) : y ∈ A ↔ ↑φ y ∈ S

On the source of a slice chart, membership in the flattened set is membership of the coordinates in the model slice. This is the pointwise form of TauCeti.isSliceChart_iff in the shape proofs use it, as an elimination rule at a single point.

theorem TauCeti.IsSliceChart.symm_mk_zero_mem {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) {y : Y} (hy : (y, 0) ∈ e.target) : ↑e.symm (y, 0) ∈ s

The ambient inverse of a point on the zero slice belongs to the set flattened by a zero-slice chart.

theorem TauCeti.IsSliceChart.mk_fst_zero_eq {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) {x : X} (hx : x ∈ e.source) (hxs : x ∈ s) : ((↑e x).1, 0) = ↑e x

On the flattened set, a zero-slice chart is recovered by reinserting the zero transverse coordinate after taking the first projection.

noncomputable def TauCeti.IsSliceChart.subtypeChart {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) [Nonempty ↑s] : OpenPartialHomeomorph (↑s) Y

Restrict an ambient zero-slice chart to the flattened set and retain its tangential coordinate.

Equations

• h.subtypeChart = e.subtypeCoord s ⋯ (fun (y : Y) => (y, 0)) Prod.fst ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.IsSliceChart.subtypeChart_source {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) [Nonempty ↑s] : h.subtypeChart.source = Subtype.val ⁻¹' e.source

The source of a zero-slice subtype chart is the part of the subtype in the ambient source.

@[simp]

theorem TauCeti.IsSliceChart.subtypeChart_target {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) [Nonempty ↑s] : h.subtypeChart.target = (fun (y : Y) => (y, 0)) ⁻¹' e.target

The target of a zero-slice subtype chart consists of the tangential coordinates whose zero-slice points lie in the ambient target.

@[simp]

theorem TauCeti.IsSliceChart.subtypeChart_apply {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) [Nonempty ↑s] (x : ↑s) : ↑h.subtypeChart x = (↑e ↑x).1

A zero-slice subtype chart reads the first coordinate of the ambient chart.

theorem TauCeti.IsSliceChart.subtypeChart_mk_zero_eq {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) [Nonempty ↑s] {x : ↑s} (hx : x ∈ h.subtypeChart.source) : (↑h.subtypeChart x, 0) = ↑e ↑x

On its source, a subtype chart recovers the ambient coordinates by reinserting the zero transverse coordinate.

@[simp]

theorem TauCeti.IsSliceChart.coe_subtypeChart_symm_apply {X : Type u_7} {Y : Type u_8} {Y' : Type u_9} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [Zero Y'] {e : OpenPartialHomeomorph X (Y × Y')} {s : Set X} (h : IsSliceChart e (Set.univ ×ˢ {0}) s) [Nonempty ↑s] {y : Y} (hy : (y, 0) ∈ e.target) : ↑(↑h.subtypeChart.symm y) = ↑e.symm (y, 0)

On its target, the inverse of a zero-slice subtype chart is the ambient inverse evaluated on the zero slice.

theorem TauCeti.IsSliceChart.source_inter_eq {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} (h : IsSliceChart φ S A) : φ.source ∩ A = φ.source ∩ ↑φ ⁻¹' S

On the source of a slice chart, the flattened set is cut out by the slice.

theorem TauCeti.IsSliceChart.exists_target_eq {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} (h : IsSliceChart φ S A) {T : Set F} (hT : IsOpen T) (hTφ : T ⊆ φ.target) : ∃ (ψ : OpenPartialHomeomorph M F), ↑ψ = ↑φ ∧ ψ.source = φ.source ∩ ↑φ ⁻¹' T ∧ ψ.target = T ∧ IsSliceChart ψ S A

A slice chart can be shrunk so that its target becomes a prescribed open subset of the old target, without changing the map.

theorem TauCeti.IsSliceChart.restrOpen {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} (h : IsSliceChart φ S A) {V : Set M} (hV : IsOpen V) : IsSliceChart (φ.restrOpen V hV) S (A ∩ V)

Restricting a slice chart to an open set restricts the flattened set to the same open set.

theorem TauCeti.IsSliceChart.of_inter {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {S : Set F} {A V : Set M} (h : IsSliceChart φ S (A ∩ V)) (hV : IsOpen V) : IsSliceChart (φ.restrOpen V hV) S A

Conversely, a chart flattening A ∩ V for an open V restricts to a chart flattening A.

theorem TauCeti.IsSliceChart.comp {M : Type u_1} {P : Type u_4} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace P] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} (h : IsSliceChart φ S A) (e : OpenPartialHomeomorph P M) : IsSliceChart (e.trans φ) S (e.source ∩ ↑e ⁻¹' A)

Slice charts pull back along any chart of a second ambient space. This is the single transport lemma behind invariance under open embeddings and homeomorphisms.

theorem TauCeti.IsSliceChart.transHomeomorph {M : Type u_1} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace F] [TopologicalSpace F'] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} (h : IsSliceChart φ S A) (e : F ≃ₜ F') : IsSliceChart (φ.trans e.toOpenPartialHomeomorph) (⇑e '' S) A

Composing a slice chart with a homeomorphism of the model space transports the slice.

theorem TauCeti.IsSliceChart.prod {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {φ : OpenPartialHomeomorph M F} {S : Set F} {A : Set M} {ψ : OpenPartialHomeomorph N F'} {S' : Set F'} {B : Set N} (h : IsSliceChart φ S A) (h' : IsSliceChart ψ S' B) : IsSliceChart (φ.prod ψ) (S ×ˢ S') (A ×ˢ B)

The product of two slice charts is a slice chart for the product slice.

@[simp]

theorem TauCeti.isSliceChart_univ_iff {M : Type u_1} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace F] {φ : OpenPartialHomeomorph M F} {A : Set M} : IsSliceChart φ Set.univ A ↔ φ.source ⊆ A

A chart is a slice chart for the full model space exactly when everything it sees lies in the set: this is the codimension-zero case.

structure TauCeti.IsSliceEmbedding {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] (S : Set F) (f : N → M) : Prop

A topological embedding f : N → M is a slice embedding for the model slice S ⊆ F if around every point of its image there is a chart of M with values in the model space F carrying the image of f onto S.

This is a relative notion: S is arbitrary, so it is not local flatness, which is the case of the standard slice, TauCeti.IsLocallyFlat. It is the layer the transport lemmas are proved on, since they move the slice around.

• isEmbedding : Topology.IsEmbedding f

  A slice embedding is in particular a topological embedding.

• exists_isSliceChart (x : N) : ∃ (φ : OpenPartialHomeomorph M F), f x ∈ φ.source ∧ IsSliceChart φ S (Set.range f)

  Around every point of the image there is a chart flattening the image onto the slice.

def TauCeti.IsLocallyFlat {M : Type u_1} {N : Type u_2} (F : Type u_5) (F' : Type u_6) [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] [Zero F'] (f : N → M) : Prop

A topological embedding f : N → M is locally flat with model F × F' if around every point of its image there is a chart of M with values in F × F' carrying the image of f onto the standard coordinate slice F × {0}.

For M a topological manifold modelled on F × F' and N one modelled on F this is the usual condition that f looks like ℝⁿ × {0} ⊆ ℝⁿ⁺ᵏ in ambient charts; the codimension is the choice of the complementary model F', and is not otherwise constrained.

Equations

• TauCeti.IsLocallyFlat F F' f = TauCeti.IsSliceEmbedding (Set.univ ×ˢ {0}) f

theorem TauCeti.IsSliceEmbedding.continuous {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {S : Set F} {f : N → M} (h : IsSliceEmbedding S f) : Continuous f

theorem TauCeti.IsSliceEmbedding.injective {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {S : Set F} {f : N → M} (h : IsSliceEmbedding S f) : Function.Injective f

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

Being a slice embedding is inherited by the restriction to an open subset of the domain.

theorem TauCeti.IsSliceEmbedding.of_forall_exists_isOpen {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {S : Set F} {f : N → M} (hf : Topology.IsEmbedding f) (h : ∀ (x : N), ∃ (U : Set N), IsOpen U ∧ x ∈ U ∧ IsSliceEmbedding S (f ∘ Subtype.val)) : IsSliceEmbedding S f

Being a slice embedding is a local property of the domain: if every point of N has an open neighbourhood on which the restriction of f is a slice embedding, then f is one.

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

Being a slice embedding is invariant under precomposition with a homeomorphism of the domain.

theorem TauCeti.IsSliceEmbedding.comp_isOpenEmbedding {M : Type u_1} {N : Type u_2} {N' : Type u_3} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] [TopologicalSpace F] {S : Set F} {f : N → M} {e : N' → N} (h : IsSliceEmbedding S f) (he : Topology.IsOpenEmbedding e) : IsSliceEmbedding S (f ∘ e)

Being a slice embedding is invariant under precomposition with an open embedding of the domain: such a precomposition is a restriction to an open subset, read through the homeomorphism onto its range.

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

Pushing a slice embedding forward along an open embedding of the ambient space keeps it a slice embedding. Taking g the inclusion of an open subset, this is the statement that a slice embedding into an open subset is one into the whole space.

theorem TauCeti.IsSliceEmbedding.of_isOpenEmbedding_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [TopologicalSpace F] {S : Set F} {f : N → M} {g : M → P} (hg : Topology.IsOpenEmbedding g) (h : IsSliceEmbedding S (g ∘ f)) : IsSliceEmbedding S f

Conversely, an embedding that becomes a slice embedding after an open embedding of the ambient space was already one. Taking g the inclusion of an open subset, this corestricts a slice embedding to an open neighbourhood of its image.

theorem TauCeti.IsSliceEmbedding.codRestrict {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {S : Set F} {f : N → M} (h : IsSliceEmbedding S f) {V : Set M} (hV : IsOpen V) (hf : ∀ (x : N), f x ∈ V) : IsSliceEmbedding S fun (x : N) => ⟨f x, ⋯⟩

Corestriction: a slice embedding whose image lies in an open subset V of the ambient space is a slice embedding as a map into V.

theorem TauCeti.IsSliceEmbedding.homeomorph_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [TopologicalSpace F] {S : Set F} {f : N → M} (h : IsSliceEmbedding S f) (e : M ≃ₜ P) : IsSliceEmbedding S (⇑e ∘ f)

Being a slice embedding is invariant under a homeomorphism of the ambient space.

theorem TauCeti.IsSliceEmbedding.transHomeomorph {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {S : Set F} {f : N → M} (h : IsSliceEmbedding S f) (e : F ≃ₜ F') : IsSliceEmbedding (⇑e '' S) f

Being a slice embedding only depends on the model space up to homeomorphism, the slice being transported along.

theorem TauCeti.IsSliceEmbedding.prodMap {M : Type u_1} {N : Type u_2} {N' : Type u_3} {P : Type u_4} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] [TopologicalSpace P] [TopologicalSpace F] [TopologicalSpace F'] {S : Set F} {f : N → M} {S' : Set F'} {g : N' → P} (h : IsSliceEmbedding S f) (h' : IsSliceEmbedding S' g) : IsSliceEmbedding (S ×ˢ S') (Prod.map f g)

A product of slice embeddings is a slice embedding for the product slice: a product of slice charts is a slice chart.

theorem TauCeti.IsSliceEmbedding.isOpenEmbedding {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} (h : IsSliceEmbedding Set.univ f) : Topology.IsOpenEmbedding f

A slice embedding for the full model space is an open embedding.

theorem TauCeti.IsSliceEmbedding.isLocallyClosed_range {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {S : Set F} {f : N → M} (h : IsSliceEmbedding S f) (hS : IsLocallyClosed S) : IsLocallyClosed (Set.range f)

The image of a slice embedding is locally closed as soon as the model slice is. This is where the definition has teeth: the image of a wild embedding need not be locally closed in any chart in this way.

theorem TauCeti.isSliceEmbedding_univ_of_isOpenEmbedding {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} [ChartedSpace F M] (h : Topology.IsOpenEmbedding f) : IsSliceEmbedding Set.univ f

An open embedding into a space charted on F is a slice embedding for the full model space.

theorem TauCeti.isSliceEmbedding_univ_iff {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} [ChartedSpace F M] : IsSliceEmbedding Set.univ f ↔ Topology.IsOpenEmbedding f

Codimension zero: a map into a space charted on F is a slice embedding for the whole model space exactly when it is an open embedding.

theorem TauCeti.IsLocallyFlat.isEmbedding {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) : Topology.IsEmbedding f

theorem TauCeti.IsLocallyFlat.exists_isSliceChart {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) (x : N) : ∃ (φ : OpenPartialHomeomorph M (F × F')), f x ∈ φ.source ∧ IsSliceChart φ (Set.univ ×ˢ {0}) (Set.range f)

The defining charts of a locally flat embedding: around every point of the image there is a chart of the ambient space, with values in F × F', carrying the image onto the standard coordinate slice. This is the eliminator consumers use to get hold of a flattening chart.

theorem TauCeti.IsLocallyFlat.continuous {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) : Continuous f

theorem TauCeti.IsLocallyFlat.injective {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) : Function.Injective f

theorem TauCeti.IsLocallyFlat.restrict {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) {U : Set N} (hU : IsOpen U) : IsLocallyFlat F F' (f ∘ Subtype.val)

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

theorem TauCeti.IsLocallyFlat.of_forall_exists_isOpen {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (hf : Topology.IsEmbedding f) (h : ∀ (x : N), ∃ (U : Set N), IsOpen U ∧ x ∈ U ∧ IsLocallyFlat F F' (f ∘ Subtype.val)) : IsLocallyFlat F F' f

Local flatness is a local property of the domain: if every point of N has an open neighbourhood on which the restriction of f is locally flat, then f is locally flat.

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

Local flatness is invariant under precomposition with a homeomorphism of the domain.

theorem TauCeti.IsLocallyFlat.comp_isOpenEmbedding {M : Type u_1} {N : Type u_2} {N' : Type u_3} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {e : N' → N} (h : IsLocallyFlat F F' f) (he : Topology.IsOpenEmbedding e) : IsLocallyFlat F F' (f ∘ e)

Local flatness is invariant under precomposition with an open embedding of the domain.

theorem TauCeti.IsLocallyFlat.isOpenEmbedding_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {g : M → P} (h : IsLocallyFlat F F' f) (hg : Topology.IsOpenEmbedding g) : IsLocallyFlat F F' (g ∘ f)

Pushing a locally flat embedding forward along an open embedding of the ambient space keeps it locally flat. Taking g the inclusion of an open subset, this is the statement that a locally flat embedding into an open subset is locally flat into the whole space.

theorem TauCeti.IsLocallyFlat.of_isOpenEmbedding_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {g : M → P} (hg : Topology.IsOpenEmbedding g) (h : IsLocallyFlat F F' (g ∘ f)) : IsLocallyFlat F F' f

Conversely, an embedding that becomes locally flat after an open embedding of the ambient space was already locally flat.

theorem TauCeti.IsLocallyFlat.codRestrict {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) {V : Set M} (hV : IsOpen V) (hf : ∀ (x : N), f x ∈ V) : IsLocallyFlat F F' fun (x : N) => ⟨f x, ⋯⟩

Corestriction: a locally flat embedding whose image lies in an open subset V of the ambient space is locally flat as a map into V.

theorem TauCeti.IsLocallyFlat.homeomorph_comp {M : Type u_1} {N : Type u_2} {P : Type u_4} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) (e : M ≃ₜ P) : IsLocallyFlat F F' (⇑e ∘ f)

Local flatness is invariant under a homeomorphism of the ambient space.

theorem TauCeti.IsLocallyFlat.transHomeomorph {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {F'' : Type u_7} [TopologicalSpace F''] [Zero F''] (h : IsLocallyFlat F F' f) (e : F' ≃ₜ F'') (he : e 0 = 0) : IsLocallyFlat F F'' f

Local flatness only depends on the complementary model up to a homeomorphism fixing the origin.

theorem TauCeti.IsLocallyFlat.of_compatible_isSliceChart {M : Type u_1} {N : Type u_2} {P : Type u_4} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {G' : Type u_7} [TopologicalSpace G'] [Zero G'] {g : M → P} (hgf : Topology.IsEmbedding (g ∘ f)) (hg : Function.Injective g) (hcompat : ∀ (x : N), ∃ (ψ : OpenPartialHomeomorph P ((F × F') × G')) (φ : OpenPartialHomeomorph M (F × F')), g (f x) ∈ ψ.source ∧ (∀ p ∈ ψ.source, (↑ψ p).2 = 0 → p ∈ Set.range g) ∧ IsSliceChart φ (Set.univ ×ˢ {0}) (Set.range f) ∧ ψ.source ∩ Set.range g ⊆ g '' φ.source ∧ ∀ y ∈ φ.source, ↑ψ (g y) = (↑φ y, 0)) : IsLocallyFlat F (F' × G') (g ∘ f)

The general form of TauCeti.IsLocallyFlat.comp: what makes a composite locally flat is a compatible pair of charts around each point of the domain, and nothing else. It asks for a chart ψ of P at g (f x) and a flattening chart φ of M for f such that ψ reads the intermediate coordinates off φ along g, in the sense ψ (g y) = (φ y, 0) on the source of φ, such that ψ sees no more of range g than φ charts, and such that on its source ψ detects range g from the vanishing of the outer coordinate. That same ψ then flattens g ∘ f, whose complementary model is the product of the two complementary models. Since hcompat already supplies every flattening chart the conclusion needs, the only embedding content assumed is what the conclusion itself carries, that g ∘ f is an embedding, together with injectivity of g. Only the stated half of the flattening of range g by ψ is assumed, the other half being forced by hagree and hsub; likewise f x ∈ φ.source is not assumed, since hsub and injectivity of g already give it.

theorem TauCeti.IsLocallyFlat.comp {M : Type u_1} {N : Type u_2} {P : Type u_4} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {G' : Type u_7} [TopologicalSpace G'] [Zero G'] {g : M → P} (hg : IsLocallyFlat (F × F') G' g) (hf : IsLocallyFlat F F' f) (hcompat : ∀ (x : N), ∃ (ψ : OpenPartialHomeomorph P ((F × F') × G')) (φ : OpenPartialHomeomorph M (F × F')), g (f x) ∈ ψ.source ∧ f x ∈ φ.source ∧ IsSliceChart ψ (Set.univ ×ˢ {0}) (Set.range g) ∧ IsSliceChart φ (Set.univ ×ˢ {0}) (Set.range f) ∧ ψ.source ∩ Set.range g ⊆ g '' φ.source ∧ ∀ y ∈ φ.source, ↑ψ (g y) = (↑φ y, 0)) : IsLocallyFlat F (F' × G') (g ∘ f)

Composition of locally flat embeddings, under an explicit compatibility hypothesis on their flattening charts. Local flatness of f : N → M and of g : M → P does not by itself make g ∘ f locally flat, because the chart of M flattening f and the chart of P flattening g are chosen independently and nothing makes them agree; hcompat is the hypothesis that charts witnessing hf and hg can be chosen coherently around each point of the domain, namely so that the outer chart reads the intermediate coordinates off the inner one along g, in the sense ψ (g y) = (φ y, 0) on the source of φ, and sees no more of range g than the inner one charts. The outer chart then flattens the composite, whose complementary model is the product of the two complementary models.

Only the compatible pair of charts is used, not the two local flatness hypotheses in full; that sharper form is TauCeti.IsLocallyFlat.of_compatible_isSliceChart, from which this is derived.

theorem TauCeti.IsLocallyFlat.prodMap {M : Type u_1} {N : Type u_2} {N' : Type u_3} {P : Type u_4} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] [TopologicalSpace P] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {G : Type u_7} {G' : Type u_8} [TopologicalSpace G] [TopologicalSpace G'] [Zero G'] {g : N' → P} (h : IsLocallyFlat F F' f) (h' : IsLocallyFlat G G' g) : IsLocallyFlat (F × G) (F' × G') (Prod.map f g)

A product of locally flat embeddings is locally flat, the models multiplying: the product of two standard slices is the standard slice of the product, after the permutation of coordinates exchanging the two middle factors.

theorem TauCeti.IsLocallyFlat.prodMap_of_isOpenEmbedding {M : Type u_1} {N : Type u_2} {N' : Type u_3} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace N'] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] {G : Type u_7} {P : Type u_8} [TopologicalSpace G] [TopologicalSpace P] [ChartedSpace G P] {g : N' → P} (h : IsLocallyFlat F F' f) (hg : Topology.IsOpenEmbedding g) : IsLocallyFlat (F × G) F' (Prod.map f g)

The product of a locally flat embedding with an open embedding into a space charted on G is locally flat, with the same complementary model: the product of a flattening chart with a chart of the open image is a flattening chart, once the new factor is moved into the tangential model.

theorem TauCeti.IsLocallyFlat.isLocallyClosed_range {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] (h : IsLocallyFlat F F' f) (h0 : IsClosed {0}) : IsLocallyClosed (Set.range f)

The image of a locally flat embedding is locally closed as soon as the origin of the complementary model is closed, the standard slice then being closed. This is where the definition has teeth: the image of a wild embedding need not be locally closed.

theorem TauCeti.isLocallyFlat_iff_isSliceEmbedding {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] : IsLocallyFlat F F' f ↔ IsSliceEmbedding (Set.univ ×ˢ {0}) f

Local flatness is exactly being a slice embedding for the standard coordinate slice F × {0} of F × F'. This is the characterisation to use downstream, where the definition of TauCeti.IsLocallyFlat is not unfolded.

theorem TauCeti.isLocallyFlat_iff {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] : IsLocallyFlat F F' f ↔ Topology.IsEmbedding f ∧ ∀ (x : N), ∃ (φ : OpenPartialHomeomorph M (F × F')), f x ∈ φ.source ∧ ∀ y ∈ φ.source, y ∈ Set.range f ↔ (↑φ y).2 = 0

Local flatness spelled out pointwise: f is a topological embedding, and around every point of its image there is an ambient chart in which the image is exactly the vanishing locus of the complementary coordinates.

theorem TauCeti.isLocallyFlat_iff_isOpenEmbedding {M : Type u_1} {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] {f : N → M} [Zero F'] [Subsingleton F'] [ChartedSpace (F × F') M] : IsLocallyFlat F F' f ↔ Topology.IsOpenEmbedding f

Codimension zero: with a trivial complementary model, over a space charted on F × F', locally flat is exactly open embedding. In particular local flatness is strictly stronger than embedding: not every embedding is locally flat.

theorem TauCeti.isLocallyFlat_prodMkLeft {N : Type u_2} {F : Type u_5} {F' : Type u_6} [TopologicalSpace N] [TopologicalSpace F] [TopologicalSpace F'] [Zero F'] [ChartedSpace F N] : IsLocallyFlat F F' fun (x : N) => (x, 0)

The standard local model: over a space N charted on F, the inclusion of N as the slice N × {0} of N × F' is locally flat, its flattening charts being the charts of N times the identity. With N = F = ℝⁿ and F' = ℝᵏ this is the coordinate slice ℝⁿ × {0} ⊆ ℝⁿ⁺ᵏ that local flatness is modelled on.

Graphs

theorem TauCeti.isLocallyFlat_graph {E : Type u_7} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] (f : E → F) (hf : Continuous f) : IsLocallyFlat E F fun (x : E) => (x, f x)

The graph of a continuous map is locally flat, with complementary model F.

theorem TauCeti.exists_isSliceChart_of_inter_eq_inter_range {M : Type u_1} {F : Type u_5} {F' : Type u_6} [TopologicalSpace M] [TopologicalSpace F] [TopologicalSpace F'] [AddGroup F'] [IsTopologicalAddGroup F'] (Φ : M ≃ₜ F × F') {g : F → M} (hg : Continuous g) (hΦg : ∀ (s : F), (Φ (g s)).1 = s) {U A : Set M} (hU : IsOpen U) (hA : U ∩ A = U ∩ Set.range g) : ∃ (φ : OpenPartialHomeomorph M (F × F')), φ.source = U ∧ IsSliceChart φ (Set.univ ×ˢ {0}) A

A graph is flat. Let Φ identify M with F × F', and let g : F → M be a continuous section of the first coordinate of Φ, so that Φ ∘ g is the graph of the continuous map s ↦ (Φ (g s)).2. If on an open set U the set A agrees with the range of g, then shearing Φ by that map, and restricting to U, gives a chart with source U flattening A onto the standard slice F × {0}.

Local product neighbourhoods

A flattening chart is already a local trivialisation once its target has been shrunk to a box, so a locally flat embedding has local product neighbourhoods in any codimension.

theorem TauCeti.IsLocallyFlat.exists_isOpenEmbedding_prod {M : Type u_1} {N : Type u_2} {F : Type u_5} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace F] {f : N → M} {G : Type u_7} [SeminormedAddCommGroup G] [NormedSpace ℝ G] (h : IsLocallyFlat F G f) (x : N) : ∃ (U : Set N), IsOpen U ∧ x ∈ U ∧ ∃ (b : ↑U × G → M), Topology.IsOpenEmbedding b ∧ ∀ (y : ↑U), b (y, 0) = f ↑y

A locally flat embedding has local product neighbourhoods: every point of the domain has an open neighbourhood U such that an open subset of the ambient space is a product U × G, in which the map is the zero slice.

The complementary model is only asked to be a real seminormed space, so this covers every codimension. What is codimension-sensitive is patching these local products into a global one, which is not proved here.