The Thom isomorphism for a normal bundle

Stream: Is there code for X?

[Jeremy Ravenel]

A while ago some asked about the Chern classes. Right now it seems like there are many lemmas about manifolds with boundary that might best be understood as falling under the theory of Thom spaces.

One of those sources is the thread about model spaces, in which a key lemma concerns invariance of domain. Invariance of domain follows from Spanier-Whitehead duality concerning the Thom space of a stable normal bundle of a manifold.

In the case of a sphere immersed in a sphere this subsumes invariance of domain implying that ℝⁿ and ℝᵐ are not homeomorphic for n and m distinct.

A complete point of view for that theory seems just as important as the eventual completion of the thread concerning Chern classes, while giving organizing principles for the boundaries of smooth manifolds.

I thought it could be a good idea to discuss that in a theead of its own. Maybe we can collect progress here- even though it is far off, even the basic result of the inverse function theorem requires invariance of domain in the proof of openness. This result has its natural place in Alexander and Spanier-Whitehead duality, in which complements of submanifolds are related to the Thom space of a normal bundle.

[Michael Rothgang]

Let me keep it short: I think Thom spaces would be great to have eventually --- but adding these to mathlib feels like a longer-term project. (For instance, mathlib doesn't have smooth submanifolds yet; I'm working on these. Then you want to define sub-bundles in general, and the normal bundle in particular. Then you begin to talk about the stable normal bundle of a manifold, etc.)

[Michael Rothgang]

Two days ago, @Floris van Doorn mentioned that you could presumably also define singular homology via Eilenberg-MacLane spaces (in a manner similar to homotopy type theory): while EM spaces are certainly nice to have, I don't think they provide a short-term faster route to invariance of domain.

[Jeremy Ravenel]

Thanks for helping me with what's current. I think I'm not ready to prove the axioms yet- maybe in several months.

Just now I found the slides at your website and I'm reading through them.

[Jeremy Ravenel]

On the other hand I think that the homotopy equivalence between S⁰ and Sⁿ⁺¹ minus the C¹-submanifold of Sⁿ (however immersed) is more useful than meets the eye: both invariance of domain for C¹-functions and the inverse function theorem use
it. (edit: or probably better to say, they follow from it, since the existence of a tubular neighborhood is demonstrated using the inverse function theorem and not the other way around).

[Michael Rothgang]

I'm sure that homotopy equivalence can be used somewhere.
I'm not sure this would be used in mathlib to prove these results, though: I'd rather have invariance of domain for C⁰ functions (using homology of spheres, which follows from the homology axioms) and prove the inverse function theorem on manifolds by reduction to the normed space case.

[Michael Rothgang]

In fact, I have "most" of the second point on an old branch --- which needs some dusting off, polishing and completing it. (Help with that could be welcome.)

[Michael Rothgang]

Jeremy Ravenel said:

Thanks for helping me with what's current. I think I'm not ready to prove the axioms yet- maybe in several months.

Just now I found the slides at your website and I'm reading through them.

Sure, no worries. If you feel like trying a project, feel free to DM me and we can think about a suitable one.

[Michael Rothgang]

(There are certainly lots of other things, with a lower barrier to entry, that would be useful to have.)

[Jeremy Ravenel]

4.4 here is pretty close to the axioms.

Maybe like uou suggested in the spirit of Mathlib to finish the openness part of the inverse function theorem by assuming invariance of domain because of how the homology axioms and Mayer-Vietoris axiom are not done yet and because it is stronger than necessary.

[Jeremy Ravenel]

However I can't follow why the homology of a limit works in that case, and the proof of theorem 9.24 in Rudin's Principles of Mathematical Analysis is also very interesting:

image.jpeg

[Jeremy Ravenel]

After some thought I realized it is just that π₀ is left adjoint that one needs for the connected components, along with the MV-sequence in 4.3 at the link. I think that is enough for invariance of domain.

[Jeremy Ravenel]

Evidently this also works for π𛲔 of filtered colimits.

[Jeremy Ravenel]

Thanks for your help with this problem @Michael Rothgang . Could you direct me to the progress you've made?

[Jeremy Ravenel]

If a topological space P is a disjoint union of subspaces X and Y as a set, and X with the subspace topology is homeomorphic to a space with a single connected component, and Y with the subspace topology is homeomorphic to a space with a single connected component, and P has two connected components, then both X and Y must be both closed and open in P.

[Michael Rothgang]

Jeremy Ravenel said:

Thanks for your help with this problem Michael Rothgang . Could you direct me to the progress you've made?

Do you mean for the inverse function theorem? (I didn't work on Mayer-Vietoris.)

[Jeremy Ravenel]

@Michael Rothgang Yes that- this week I have time to study it and maybe I can make some progress.

(The Mayer-Vietoris sequence follows from the ES-axioms)

[Michael Rothgang]

Sure! I just dug up my old branch and adapted it to current master. I'll push it soon. (edit: #26115)

[Michael Rothgang]

Be warned, though: the proofs are in an intermediate state of "being broken" --- just looking at them may not be the clearest. (Feel free to ask me, though --- and perhaps I can take some time tomorrow to polish this slightly).

[Joël Riou]

Jeremy Ravenel said:

Evidently this also works for π𛲔 of filtered colimits.

This reference seems to be quite wrong. If "Space" means "simplicial set", then it is ok. If "Space" means "topological space", it might be wrong. In the category of topological spaces, if T is compact, it is unclear to me that Hom(T, -) commutes with filtered colimits. What I know is that if X ⟶ Y is a transfinite composition of closed $T_1$ inclusions, then Hom(T, Y) identifies to a suitable colimit of Hom types (I have formalized this at https://github.com/joelriou/topcat-model-category/blob/e5705bfcc6944a0f8119f7b1cf717b686f39fbfd/TopCatModelCategory/TopCat/T1Inclusion.lean#L310 ; @Reid Barton also did; more details in the book by Hovey, Model categories, paragraph 2.4). For a general direct system of topological spaces, I would not claim it is true. (The technical details about such issues are omitted in many references.)

[pro-Lie stabilizer]

thanks for the correction, I agree. However in our case these are inclusions of open subobjects and so this should in fact follow from compactness of spheres and discs. I found a reference of Proposition 2B.1. in Hatcher for that. (sorry, I've realized I just responded from a friend's account - Jeremy)

[Robin Carlier]

@Joël Riou, the reference given is fully in infinity-category land and so "Space" means "the quasicagegory of Kan complexes".

It's still a bit early for using infinity-categorical references for formalisation in mathlib, though

[Joël Riou]

I am not saying Lurie is wrong, but that he is misquoted!

[Robin Carlier]

I was more saying that since the author is writing $\mathcal{S}_*$ for pointed spaces, an answer in Lurie-only framework disregarding the other uses of word "Space" was to be expected.
I guess this is why some people started using the word "anima" for Kan complexes/Spaces/Infinity-groupoids...

[Robin Carlier]

Oh, but you were referring to using this particular link in the situation of this thread, apologies for the confusion...

[Jeremy Ravenel]

Sorry for not being more careful.

[Jeremy Ravenel]

@Michael Rothgang thanks very much for sharing this. I'm going to learn some of it this week.

[pro-Lie stabilizer]

Most parts of this theory are clearly far off, but the mention of the Thom isomorphism is pretty key I think because of how the "real orientation" function from Immersion(Sⁿ × 𝔻¹, Sⁿ × 𝔻¹) to S⁰ can be used to show invariance of domain.

[pro-Lie stabilizer]

The above was a bit of a mistake.

Let $f : S^{n-1} × [0,1] → S^{n-1} × [0,\infty)$ be an injection sending $(z,0)$ to $(z,0)$ for each $z$ in $S^{n-1}$. The orientation function $\text{orientation} : S^{n-1} \times [0,\infty) - Im(f \circ \iota) \rightarrow S^0$, where $\iota : S^{n-1} \rightarrow S^{n-1} \times [0,1]$ sends $z$ to $(z,1)$ sends $\text{im}(\iota)$ to $-1$, and for each $z \in S^{n-1}$, there is $r \in [0,\infty)$ such that for $x \geq r$, $(z,x)$ is sent to $1$.

[pro-Lie stabilizer]

That orientation is a morphism of $\text{real topological manifolds}$ implies that $\text{orientation}^{-1}(\{-1\})$ is open (and yet the construction is not changed, only interpreted in terms of real orientation).

[pro-Lie stabilizer]

Screenshot 2025-07-03 at 3.42.05 AM.png

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

@Transitive discrete group action with pro-Lie stabilizer @Jeremy Ravenel it looks like you meant $S^{n-1} \times \{ 0 \}$ and not $im(\iota)$, no?

And so the openness in invariance of domain is interpreted as the continuity of a function defined on the complement of the image of a sphere, but this doesn't prove the fact about filtered colimits of open subobjects.

I don't fully understand whether we can avoid use of the Mayer-Vietoris sequence + a mesh on the cube + filtered colimits of open subsets, so I appreciate the page from the book since the appearance of λ = ||A⁻¹||/2 appears related to tubular neighborhoods as well.

[Xinyi Zhang]

Joël Riou said:

Jeremy Ravenel said:

Evidently this also works for π𛲔 of filtered colimits.

This reference seems to be quite wrong. If "Space" means "simplicial set", then it is ok. If "Space" means "topological space", it might be wrong. In the category of topological spaces, if T is compact, it is unclear to me that Hom(T, -) commutes with filtered colimits. What I know is that if X ⟶ Y is a transfinite composition of closed $T_1$ inclusions, then Hom(T, Y) identifies to a suitable colimit of Hom types (I have formalized this at https://github.com/joelriou/topcat-model-category/blob/e5705bfcc6944a0f8119f7b1cf717b686f39fbfd/TopCatModelCategory/TopCat/T1Inclusion.lean#L310 ; Reid Barton also did; more details in the book by Hovey, Model categories, paragraph 2.4). For a general direct system of topological spaces, I would not claim it is true. (The technical details about such issues are omitted in many references.)

I don't think enough was specified to say what was supposed to work in both situations. It's definitely not a quote.

[Xinyi Zhang]

@Jeremy Ravenel what is supposed to work for π𛲔 of filtered colimits, and is it a problem in this situation if it only holds for homotopy colimits of filtered diagrams?

[Joël Riou]

Xinyi Zhang said:

I don't think enough was specified to say what was supposed to work in both situations. It's definitely not a quote.

I was basically just saying that one has to be careful about the category where the colimits are computed. The nth homotopy group functor of (pointed) simplicial sets commutes with filtered colimits (I have formalised this for Kan complexes, and with some more work, it will also hold for arbitrary simplicial sets), but it is unclear it works for arbitrary filtered colimits of topological spaces. Currently, we are not even remotely able to formalize homotopy colimits, but it is true that the homotopy groups of a filtered hocolim identify to the colimit of the homotopy groups (because it shall be true in the category of simplicial sets, and then also in a Quillen-equivalent category...). In any case, results about homotopy colimits seem to be quite irrelevant to the topic of this thread.