homeoHom
plain-language theorem explainer
Packages a homeomorphism of topological spaces as a morphism in the category Top of spaces. Anyone pushing chains, cycles, or homology along a homeomorphism of ambient spaces or of open complements will cite it. The body is a one-line wrap of the underlying continuous map via the TopCat-ofHom constructor.
Claim. Given topological spaces $A$ and $B$ and a homeomorphism $e:A\simeq B$, form the corresponding morphism $A\to B$ in the category of topological spaces by taking the continuous underlying map of $e$.
background
The ambient module develops acyclicity of arc complements in low-dimensional homology: one shows that suitable open complements of closed arcs (and of unions of closed halves) have vanishing $H_1$ or $H_2$, via a bisection/Mayer–Vietoris argument on complements.
Lean’s Homeomorph type already carries a continuous map and a continuous inverse. The category TopCat needs morphisms packaged as continuous maps between the objects TopCat.of A and TopCat.of B. This definition is the thin bridge between those two presentations.
Downstream lemmas immediately check that the package respects composition with the inverse homeomorphism, so a homeomorphism becomes an isomorphism in TopCat and can be used to identify chain and homology groups of homeomorphic complements.
proof idea
One-line definitional wrapper. Extract the continuous underlying function of the homeomorphism and pass it to TopCat.ofHom, yielding a morphism TopCat.of A ⟶ TopCat.of B. No further proof obligations: continuity is part of the homeomorphism data.
why it matters
Local plumbing for the arc-complement acyclicity development. It is the morphism used by the two inverse-composition lemmas (composition with the symmetric homeomorphism recovers the identity on each side), which certify that homeomorphisms act as categorical isomorphisms.
Those isomorphisms feed the bisection step bounds_of_halves: a 1-cycle in the complement of a union $KU=KP\cup KM$ that bounds after pushforward into each half-complement already bounds in the full complement, once $H_2$ of the intersection-complement vanishes. Being able to move cycles along homeomorphisms of complements is part of that bookkeeping.
In the broader Recognition foundation this sits under the topological side of the forcing chain (support for dimension and linking/vanishing statements), not under the J-cost or mass-ladder arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.