IsInitial
plain-language theorem explainer
A Peano algebra A is initial when a homomorphism from A to any other Peano algebra B exists and any two such homomorphisms agree on their underlying functions. Researchers on categorical logic realizations and universal forcing cite the structure to guarantee uniqueness up to unique isomorphism of the arithmetic object extracted from a logic realization. The declaration is a direct structure definition that packages the lift and uniqueness fields.
Claim. Let $A$ be a Peano algebra. Then $A$ is initial when, for every Peano algebra $B$, there exists a homomorphism $A$ to $B$ and any two such homomorphisms have identical underlying functions on the carriers.
background
A Peano algebra is a carrier type equipped with a distinguished zero element and a successor map. A homomorphism between two Peano algebras is a function that sends zero to zero and commutes with the successor operation. The module ArithmeticOf extracts arithmetic from an abstract Law-of-Logic realization by requiring that the resulting Peano algebra satisfy initiality; the module documentation states that initial objects are unique up to unique isomorphism and that this supplies the mechanism behind Universal Forcing.
proof idea
The declaration is a direct structure definition. It encodes initiality by two fields: a lift supplying a homomorphism to every target algebra, and a uniqueness condition asserting that any two such homomorphisms agree on their carrier functions.
why it matters
The structure supplies the central property used inside the definition of ArithmeticOf, which pairs a Peano algebra with its initiality witness. It is instantiated by logicNat_initial to establish that the logic-derived natural numbers are initial, and by realization_initial to show that the extracted realization orbit is initial. The same notion appears in LawvereNNO and in the isInitial construction for natural-number objects. It therefore supplies the categorical uniqueness mechanism that underpins arithmetic forced from logic realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.