inv_hom_apply
plain-language theorem explainer
For any isomorphism of modules in ModuleCat, the inverse map undoes the forward map on every element. Homological algebraists cite it when transporting cycles and homology classes along short-complex isomorphisms. The proof is a one-line rewrite through composition, the iso unit law, and identity application.
Claim. Let $e : M \cong N$ be an isomorphism of modules (in $\mathbf{ModuleCat}$). Then for every $x \in M$, $e^{-1}(e(x)) = x$.
background
The ambient module is Foundation.ArcComplementAcyclic, which builds chain-level tools for showing that arc-complement complexes are acyclic and that homology classes are represented by genuine cycles. Objects $M,N$ are modules in Mathlib's ModuleCat; an isomorphism $e : M \cong N$ supplies mutually inverse morphisms hom and inv with the usual unit/counit identities.
The forgetful coercion $\uparrow M$ extracts the underlying carrier, so the statement is the pointwise left-inverse law for $e$. Downstream lemmas use this to move vanishing and representability statements across short-complex isomorphisms (scIso) that identify a complex with its homology data.
proof idea
One-line wrapper. Rewrite the composite application via ModuleCat.comp_apply (so $e.\mathrm{inv}\circ e.\mathrm{hom}$ appears), replace that composite by the identity using the isomorphism law e.hom_inv_id, then apply ModuleCat.id_apply to conclude the identity acts as $x$.
why it matters
Local plumbing for the arc-complement acyclicity development. It is the left half of the iso cancellation pair used by hom_apply_eq_zero_iff, which states $e.\mathrm{hom},x=0\Leftrightarrow x=0$; that injectivity is how vanishing of homology is transferred along scIso. The same identity appears inside exists_classOf ("every homology element is the class of a cycle"), where homology isos are applied and inverted on representatives.
In the broader Recognition foundation stack this supports the chain-level bookkeeping behind high-dimensional linking/vanishing arguments imported from LinkingVanishingHighDim, rather than a numbered forcing step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.