PeanoObject

formal source

  20universe u
  21
  22/-- A Peano algebra: a type with a zero element and a step map. -/
  23structure PeanoObject where
  24  carrier : Type u
  25  zero : carrier
  26  step : carrier → carrier
  27
  28namespace PeanoObject
  29
  30/-- Homomorphisms of Peano algebras. -/
  31structure Hom (A B : PeanoObject) where
  32  toFun : A.carrier → B.carrier
  33  map_zero : toFun A.zero = B.zero
  34  map_step : ∀ x : A.carrier, toFun (A.step x) = B.step (toFun x)
  35
  36namespace Hom
  37
  38instance (A B : PeanoObject) : CoeFun (Hom A B) (fun _ => A.carrier → B.carrier) where
  39  coe f := f.toFun
  40
  41/-- Identity homomorphism. -/
  42def id (A : PeanoObject) : Hom A A where
  43  toFun := fun x => x
  44  map_zero := rfl
  45  map_step := fun _ => rfl
  46
  47/-- Composition of homomorphisms. -/
  48def comp {A B C : PeanoObject} (g : Hom B C) (f : Hom A B) : Hom A C where
  49  toFun := g.toFun ∘ f.toFun
  50  map_zero := by rw [Function.comp_apply, f.map_zero, g.map_zero]
  51  map_step := by
  52    intro x
  53    rw [Function.comp_apply, f.map_step, g.map_step, Function.comp_apply]