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

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArithmeticOf on GitHub at line 209.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.