pith. machine review for the scientific record. sign in
def definition def or abbrev high

id

show as:
view Lean formalization →

The identity map on a Peano algebra is the homomorphism sending every carrier element to itself. Researchers establishing initiality of arithmetic objects in logic realizations cite it to obtain uniqueness up to unique isomorphism. The definition sets the underlying function to the identity and verifies zero and step preservation by reflexivity.

claimFor any Peano algebra $A$ with carrier, zero element $0_A$ and step map $s_A$, the identity homomorphism $id_A : A → A$ is the map $id_A(x) = x$ that satisfies $id_A(0_A) = 0_A$ and $id_A(s_A(x)) = s_A(id_A(x))$.

background

PeanoObject is a structure consisting of a carrier type, a zero element and a step map. Hom is the structure of maps between two PeanoObjects that send zero to zero and commute with the step operation. The module extracts arithmetic from an abstract Law-of-Logic realization. The key point is initiality: once a realization supplies identity/step data, the forced arithmetic object is the initial Peano algebra generated by that data. Initial objects are unique up to unique isomorphism; this is the mechanism behind Universal Forcing.

proof idea

The definition supplies the identity function as toFun and discharges the map_zero and map_step obligations by reflexivity.

why it matters in Recognition Science

This supplies the identity morphism in the category of Peano algebras, enabling composition and initiality arguments that feed into CostAlgebra results such as comp_id, eq_id_of_map_two_eq_two and eq_id_or_reciprocal. It realizes the identity step required for uniqueness of the arithmetic object extracted from logic realizations, directly supporting the universal forcing mechanism described in the module.

scope and limits

formal statement (Lean)

  42def id (A : PeanoObject) : Hom A A where
  43  toFun := fun x => x

proof body

Definition body.

  44  map_zero := rfl
  45  map_step := fun _ => rfl
  46
  47/-- Composition of homomorphisms. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (13)

Lean names referenced from this declaration's body.