pith. machine review for the scientific record. sign in
def

equivOfInitial

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.ArithmeticOf
domain
Foundation
line
209 · 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 209.

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

Derivations using this theorem

depends on

used by

formal source

 206  induction := R.orbit_induction
 207
 208/-- The natural equivalence between two initial Peano objects. -/
 209noncomputable def equivOfInitial {R S : LogicRealization}
 210    (A : ArithmeticOf R) (B : ArithmeticOf S) : A.peano.carrier ≃ B.peano.carrier where
 211  toFun := (A.initial.lift B.peano).toFun
 212  invFun := (B.initial.lift A.peano).toFun
 213  left_inv := by
 214    intro x
 215    have hcomp :
 216        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano)).toFun =
 217          (PeanoObject.Hom.id A.peano).toFun :=
 218      A.initial.uniq A.peano
 219        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano))
 220        (PeanoObject.Hom.id A.peano)
 221    exact congrFun hcomp x
 222  right_inv := by
 223    intro y
 224    have hcomp :
 225        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano)).toFun =
 226          (PeanoObject.Hom.id B.peano).toFun :=
 227      B.initial.uniq B.peano
 228        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano))
 229        (PeanoObject.Hom.id B.peano)
 230    exact congrFun hcomp y
 231
 232/-- Canonical arithmetic object for any realization: the initial Peano object.
 233
 234This definition is intentionally realization-independent at this stage. The
 235realization supplies the interpretation; initiality supplies the invariant
 236arithmetic content. -/
 237def canonical (R : LogicRealization) : ArithmeticOf R where
 238  peano := logicNatPeano
 239  initial := logicNat_initial

papers checked against this theorem

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