Splitting Topology/Homeomorph

Stream: mathlib4

[Michael Rothgang]

In #22137, I would like to use IsInducing (Sum.swap X Y) inside Topology/Constructions.lean, to deduplicate a proof.
However, the easiest way to prove this statement is to use Homeomorph.sumComm, which is defined further downstream in Homeomorph.lean.
Hence, from this PR's point of view, it would be nice to split Homeomorph.lean, for instance

• splitting out a file just for the basic definitions (which should have less imports than Topology/Constructions.lean, hence can be imported there)
• defining the homeomorphisms between various constructions in that file, including mine

I know @Yaël Dillies has been unhappy about Homeomorph.lean for a long time. Does that seem like a useful step?

To be clear: in my PR, the duplication is perhaps 5 lines (so not worth boiling the ocean for) --- on the other hand, the argument I was going at seems like a fairly natural one, so I wouldn't be surprised if others would try the same.

[Yaël Dillies]

Yes, that's exactly what I would like to see happen :smile:

[Michael Rothgang]

#22681 is the first step of this (and should be ready for review - perhaps one or two fixes will be needed, but nothing essential).

[Michael Rothgang]

#22682 builds on this, and collects all material about sum, products and their distributivity in one file. That one still needs a bit of clean-up of the module doc-strings.

[Anne Baanen]

(I recall a previous discussion on this topic having some pushback against splitting Homeomorph.lean since it was convenient to have all the properties preserved by homeomorphisms available without thinking about imports. But I can't find evidence of that discussion. In any case from my outsider perspective I would be glad to see this knot in our import tangle worked out.)

[Michael Rothgang]

Sure, that is a point I can understand. I'm not sure if this is currently followed, though: does that file really contain all properties preserved homeomorphisms?

[Michael Rothgang]

In any case, this does not speak against #22681: importing Homeomorph.Lemmas after that PR still gets you everything you had before (so no real harm done), but downstream files have a choice now (a win in my book).

[Kim Morrison]

@Michael Rothgang, there's a merge conflict on #22681 at present.

[Aaron Liu]

fixed it

[Michael Rothgang]

The next PR in that sequence is #22827 (CI is still running, but will hopefully pass now)