homeoHom_symm_comp
plain-language theorem explainer
For a homeomorphism e between topological spaces, the Top-category morphism induced by e inverse, composed with the morphism induced by e, is the identity on the codomain. Algebraic topologists working with arc-complement complexes or continuous maps of subtypes would cite it. The proof is pointwise: extensionality plus the homeomorphism inverse law e(e^{-1}x)=x.
Claim. Let $A$ and $B$ be topological spaces and let $e:A\simeq_t B$ be a homeomorphism. Writing $h(e)$ for the morphism $\mathbf{Top}(A)\to\mathbf{Top}(B)$ induced by the continuous map underlying $e$, one has $h(e^{-1})\gg h(e)=\mathrm{id}_{\mathbf{Top}(B)}$.
background
The ambient module develops acyclicity of arc complements in the topological category, importing high-dimensional linking-vanishing infrastructure. Morphisms are taken in TopCat, the category of topological spaces and continuous maps.
The sibling definition homeoHom turns a homeomorphism $e:A\simeq_t B$ into a TopCat arrow $\mathrm{TopCat.of},A\to\mathrm{TopCat.of},B$ by packaging the underlying continuous map. Composition of arrows is written in diagrammatic order (≫), so the statement is the right inverse law for that packaging: first apply the arrow of $e^{-1}$, then the arrow of $e$, and recover the identity on $B$.
Sibling lemmas in the same block record the matching left inverse, the zero-class characterizations, and naturality of chain maps on complement subtypes; the present fact is the pure categorical half of that package.
proof idea
Tactic proof in two steps. First ext x reduces equality of TopCat morphisms to equality of underlying functions at an arbitrary point of $B$. The goal becomes $e(e^{-!1}x)=x$, which is exactly the library fact Homeomorph.apply_symm_apply. No continuity or topology beyond the homeomorphism structure is used.
why it matters
Arc-complement acyclicity arguments need to move simplices and homology classes across homeomorphic presentations of the ambient space and of complement subtypes. Packaging homeomorphisms as TopCat morphisms lets those moves sit inside the categorical chain-map calculus already used for simplex pushing and lifting in this module.
No downstream consumers are recorded yet (used_by is empty), so the lemma is presently local infrastructure rather than a cited step of the forcing chain (T0–T8). It sits beside the imported linking-vanishing material and the simplex-pushing section that immediately follows in the file, and is the categorical counterpart of the pointwise inverse laws hom_inv_apply / inv_hom_apply among the siblings.
It does not itself touch J-cost, the eight-tick octave, or dimension forcing; it only keeps the topological scaffolding coherent for those later geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.