hom_apply_eq_zero_iff
plain-language theorem explainer
An isomorphism of modules sends an element to zero exactly when the element is zero. Homological algebraists cite this when transporting vanishing statements across short-complex isomorphisms. The proof is a two-sided constructor: one direction applies the inverse iso and the left-inverse identity; the other is functoriality of zero.
Claim. Let $e : M \cong N$ be an isomorphism of modules and let $x \in M$. Then $e_{\mathrm{hom}}(x) = 0$ if and only if $x = 0$.
background
The ambient setting is the category of modules (ModuleCat) inside the Foundation arc-complement acyclicity development. Objects $M,N$ carry underlying additive groups; morphisms are module homs, and $e : M \cong N$ is a categorical isomorphism with forward map $e.hom$ and inverse $e.inv$.
The key prior fact is the left-inverse identity: applying $e.inv$ after $e.hom$ recovers the original element ($e.inv(e.hom, x) = x$). Module homs also send zero to zero. Together these make injectivity of isomorphisms an elementary rewrite, which is what the present lemma records in iff form.
The module sits downstream of LinkingVanishingHighDim and prepares the homology vanishing criterion used for arc-complement acyclicity.
proof idea
Tactic proof by constructor on the biconditional.
Forward: from $e.hom, x = 0$, rewrite to $e.inv(e.hom, x) = e.inv, 0$, then apply inv_hom_apply (the left-inverse identity) and map_zero to conclude $x = 0$.
Reverse: from $x = 0$, rewrite by map_zero to get $e.hom, x = 0$.
No further lemmas are needed; the argument is pure iso cancellation.
why it matters
Feeds directly into classOf_eq_zero_iff, the vanishing criterion: the homology class of a cycle is zero iff the cycle is a boundary. That parent lemma instantiates the present fact on the homology-map isomorphism induced by the short-complex iso scIso, so that a homology class vanishes after transport exactly when it was already zero.
In the Recognition Science foundation layer this is bookkeeping for acyclicity of arc complements: once classes can be tested for vanishing through isomorphisms of short complexes, higher linking and dimension-forcing arguments (toward T8 spatial dimension and the eight-tick octave scaffolding) can quote a clean boundary criterion rather than raw chain-level identities.
It is elementary category theory, but it is the precise glue between iso transport and the homology vanishing statements the module is built to deliver.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.