`comp`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticOf on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  73  zero_ne_step : ∀ x : A.peano.carrier, A.peano.zero ≠ A.peano.step x
  74  step_injective : Function.Injective A.peano.step
  75  induction :
  76    ∀ P : A.peano.carrier → Prop,
  77      P A.peano.zero →
  78      (∀ n, P n → P (A.peano.step n)) →

papers checked against this theorem

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