toHom
plain-language theorem explainer
Extracts the underlying Peano-algebra homomorphism from a structure-preserving Peano isomorphism: same carrier map, with zero and successor preserved. Downstream uniqueness and fold-compatibility arguments cite it to feed initiality. The body is a field-by-field record construction from the bundled equivalence.
Claim. Given Peano algebras $A$ and $B$ and a structure-preserving isomorphism $e$ (a carrier equivalence that sends zero to zero and commutes with successor), there is an induced Peano homomorphism $A \to B$ whose underlying function is the forward map of $e$.
background
A Peano algebra is a carrier type with a distinguished zero and a step (successor) map. Homomorphisms are functions that send zero to zero and commute with step. The module works in the arithmetic-extraction layer of Universal Forcing: bare carrier bijections between forced arithmetics of Law-of-Logic realizations are upgraded to structure-preserving maps.
PeanoEquiv bundles an equivalence of carriers together with the two preservation identities (zero and step). That is strictly stronger than a bare set bijection: it is an isomorphism of Peano algebras. The ambient ArithmeticOf package supplies the forced Peano object of a realization and the initiality data used later for uniqueness.
This definition is the forgetful bridge from the iso bundle to the plain Hom type that initiality quantifies over.
proof idea
Record construction, not a proof. The Hom fields are filled directly from the PeanoEquiv fields: toFun is the forward map of toEquiv, while map_zero and map_step are copied verbatim from the iso's preservation proofs. No lemmas are applied.
why it matters
Needed so uniqueness and composition arguments can treat a Peano iso as a Hom and invoke initiality. peanoEquiv_unique compares two isos by applying initiality to their induced Homs, concluding they share the same underlying function (the Universal Forcing iso is therefore the unique structure-preserving one). fold_iso_compat composes the induced Hom with a fold Hom and again uses initiality to get fold compatibility with LogicNat.
In the module's own terms, this sits inside the upgrade from bare carrier equivalence to unique Peano-algebra isomorphism (Part II of Universal Forcing). Ring and order structure are explicitly out of scope here: PeanoObject carries only zero and step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.