hom_inv_apply
plain-language theorem explainer
For any module isomorphism e : M ≅ N, the composite of the inverse map followed by the forward map is the identity on N. Homological algebraists cite this when chasing elements through short complexes and homology maps. The proof is a one-line rewrite via composition evaluation, the inverse-hom identity, and the identity map.
Claim. Let $e : M \cong N$ be an isomorphism of modules (in $\mathbf{Mod}$). Then for every $x \in N$, $e_{\mathrm{hom}}(e_{\mathrm{inv}}(x)) = x$.
background
The ambient category is modules over $\mathbb{Z}$ (Mathlib's ModuleCat), with morphisms evaluated pointwise on underlying carriers. An isomorphism $e : M \cong N$ supplies a forward map $e_{\mathrm{hom}} : M \to N$ and an inverse $e_{\mathrm{inv}} : N \to M$ satisfying the usual triangle identities $e_{\mathrm{hom}} \circ e_{\mathrm{inv}} = \mathrm{id}N$ and $e{\mathrm{inv}} \circ e_{\mathrm{hom}} = \mathrm{id}_M$.
This file develops arc-complement acyclicity for chain complexes of modules: homology classes of cycles, the zero class criterion, and naturality of class formation along chain maps. The present lemma is the elementwise form of one triangle identity, needed whenever an iso is applied to a concrete cycle representative.
Sibling material includes the opposite composite identity and the characterization of the zero class; downstream naturality of homology classes uses both.
proof idea
One-line wrapper by rewrite. First replace the pointwise application $e_{\mathrm{hom}}(e_{\mathrm{inv}}, x)$ by the composite morphism applied to $x$ (composition evaluation). Then rewrite the composite via the isomorphism law $e_{\mathrm{inv}} \circ e_{\mathrm{hom}} = \mathrm{id}$ oriented as $e_{\mathrm{hom}} \circ e_{\mathrm{inv}} = \mathrm{id}_N$. Finally reduce the identity morphism on $x$ to $x$ itself.
why it matters
Feeds classOf_natural in the same module: naturality of homology classes under chain maps, which states that classes push forward along chain maps. Elementwise recovery of representatives after transporting by an iso is the bookkeeping step that lets short-complex functors and homology maps commute with class formation.
In the Recognition foundation layer this sits under arc-complement acyclicity: showing certain complements of arcs in the chain complex are acyclic, so homology concentrates where the forcing chain expects it. It is pure categorical plumbing rather than a T0–T8 forcing step, but without it the naturality diagram for class-of-cycle cannot close in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.