Subdivison Lemma/ Lemma of Small Simplices/ Excision Theorem

Stream: new members

[Ajay Kumar Nair]

Hi Everyone!

I am Ajay, currently a PostDoc at Indian Institute of Science Bangalore.

I am looking for some formalisation projects in Topology. I came to know that Excision theorem has not yet been formalised, so I thought I would try my hand at it. I believe I have a decent theoretical understanding of the proof of Excision theorem. I am currently going through the Mathlib.AlgebraicTopology.SingularHomology.Basic file from Mathlib.

I would like to know: what is a good action plan to approach this? Where is a good place to start? Also, is anyone already working on this?

[Joël Riou]

I have formalized the subdivision functor on simplicial sets and obtained some version of a lemma about the diameter of the subdivision https://github.com/joelriou/topcat-model-category/blob/202ea039d99ada0d4bc1d8223d2bf4f51d8208f5/TopCatModelCategory/SSet/Mesh.lean#L208 but otherwise I am not aware of ongoing related work (apart from the formalization https://github.com/Shamrock-Frost/BrouwerFixedPoint by @Brendan Seamas Murphy in Lean 3).
The definition of singular homology in mathlib allows a very general coefficient category C. In order to formalize certain results, it may be convenient to construct certain chain homotopy equivalences starting with the particular case C := ModuleCat R with R a ring, and later deduce more general results using the universal role of ℤ.

[Joël Riou]

As @Yury G. Kudryashov was asking, here are some additional details about how we could formalize excision. Let X be a topological space, let U be a family of subsets of X such that the interiors of the subsets in U cover X (e.g. U is an open covering), then there is a subcomplex $C(U)$ of the singular complex $C(X)$ of X whose chains correspond to linear combination of simplices (continuous maps from a topological simplex to X) that are contained in one of the subsets in U (there is a easy way to generalize what I am saying here to the slightly more abstract definitions in mathlib with a general coefficient category), and the result is that the inclusion of $C(U)$ in $C(X)$ is a homotopy equivalence (depending on the strategy of proof, it may be slightly easier to show that it is a quasi-isomorphism, but here it does not make a real difference).
One of the key ingredients of the proof of excision does not depend on the covering U, but only on X: there is a natural endomorphism of the chain complex $C(X)$, the subdivision, and it is homotopic to the identity. Because of the expected naturality, if we look at the subdivision endomorphism and the homotopy in a fixed degree n, it is completely determined by its action on the "universal" simplex given by the identity of the standard topological n-simplex.
Then, the right approach is probably to consider the R-linearization (e.g. R := ℤ) of the category of topological spaces, which would allow to consider formal R-linear combination of continuous maps between topological simplices. In each degree, the data of the subdivision endomorphism and the homotopy towards the identity are given by elements in such groups: the core of the argument (a construction by induction on the degree) should involve definitions and computations in such groups. At some point, I made #30933 as I thought it could help doing this, but @Kim Morrison rightfully pointed out it was already in mathlib, even though there may be some range for improvements.
The other main ingredient is that if we have a singular chain of X, we can find an homotopic chain in $C(U)$ by applying sufficiently many times the subdivision operator. This is related to the lemma I have formalized above, but it is not completely clear how to make the connection...

[Yury G. Kudryashov]

My main issue with the current formalization is that it uses a lot of category theory bundling without giving a reference (e.g., in the docstring) for people like me who only dealt with homologies with coefficients in an abelian group.

[Yury G. Kudryashov]

E.g., if I want to formalize something, what book/paper/... should I read to get the generality right?

[Joël Riou]

As I have said above, the core of the argument involves usual chains with integer coefficients. For the definition, the only difference is that in mathlib, the free module on a type S (of continuous maps from the topological n-simplex to a topological space X) is replaced by a coproduct of copies of an arbitrary object indexed by the type S.
Any book like Spanier or Hatcher should be fine.

[Andrew Yang]

I might start thinking about this in my spare time if no-one else is working on it.

[Ajay Kumar Nair]

@Divakaran Divakaran and I are planning to get started on this. We might need some guidance during the project, though.

[Sébastien Gouëzel]

There is already ongoing work, see #homology > Homotopy invariance of singular homology @ 💬 . Better synchronize!

[Andrew Yang]

If there are already people working on it then I'll leave it to them. I'll probably still formalize something to learn the material but it'll just be shelved somewhere in my laptop.

I do have a question on the approach though:
I don't think one needs to consider formal linear combinations of maps. One only needs linear combinations of actual continuous maps $\Delta^n \to \Delta^m$ which should work just fine?

But what's the best strategy to show that it is homologous to the identity? The usual proof seems to be "By universality one only needs to check on $C(\Delta_n)$, which is a projective resolution, so any two endomorphisms with equal 0-th degree map are homologous." but obviously this only works if the coefficient (the S you are taking coproducts of) is projective. One can probably prove it for projectives and then (assuming the existence of a projective generator?) extend to all coefficients but is there a better way?

[Joël Riou]

Andrew Yang said:

I don't think one needs to consider formal linear combinations of maps. One only needs linear combinations of actual continuous maps $\Delta^n \to \Delta^m$ which should work just fine?

I do not see the nuance here.

But what's the best strategy to show that it is homologous to the identity?

I am suggesting using the "universal role" of the integers. Both the subdivision (as a chain map) and the homotopy to the identity are given in each degree by linear combinations with integer coefficients, these "act" on the singular chains of any topological space with arbitrary coefficients.

[Andrew Yang]

Oh I was stuck when I don't have a suitable analog of the integers in my category, but you are saying that they could "act" even across categories so I only need to prove it for $\mathbb{Z}$ in $\mathbf{Ab}$ and then everything else follows?

[Joël Riou]

Yes, we just use the canonical map from $\mathbb{Z}$ to the ring of endomorphisms of S.

[Andrew Yang]

I think I now have a fairly good idea about how this would work in lean. @Ajay Kumar Nair I'd love to help to get this into mathlib sooner. I could write a quick sketch in lean (i.e. files with data filled in but with a bunch of sorried proofs) if that would be useful to you. It would be especially useful if you have less experience because definitions are notoriously difficult to get right. But if you already have some plans then you could probably learn more by doing it from scratch.

[Ajay Kumar Nair]

That would be really helpful. Thank you very much.
My experience in writing proofs in Lean is minimal.

[Ajay Kumar Nair]

Hi @Andrew Yang , just checking in on this. I realize you're likely busy, so I wanted to ask if you might still have time to work on the sketch you mentioned?

If you're too swamped right now, @Divakaran Divakaran and I are happy to try writing the definitions ourselves and reach out if we hit any roadblocks. In that case, even just a brief initial idea of which definitions you had in mind would be really helpful to get us started.