`id`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticOf
domain: Foundation
line: 42 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArithmeticOf on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  62end PeanoObject
  63
  64/-- The arithmetic object forced by a Law-of-Logic realization. -/
  65structure ArithmeticOf (R : LogicRealization) where
  66  peano : PeanoObject
  67  initial : PeanoObject.IsInitial peano
  68
  69namespace ArithmeticOf
  70
  71/-- Peano surface of a forced arithmetic object. -/
  72structure PeanoSurface {R : LogicRealization} (A : ArithmeticOf R) : Prop where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.