Hom

formal source

  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]
  54
  55end Hom
  56
  57/-- Initiality of a Peano algebra. This is data, so it lives in `Type`. -/
  58structure IsInitial (A : PeanoObject) where
  59  lift : ∀ B : PeanoObject, Hom A B
  60  uniq : ∀ (B : PeanoObject) (f g : Hom A B), f.toFun = g.toFun
  61