`extracted`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArithmeticOf on GitHub at line 197.

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

 194    rw [realizationLift_unique_fun R B f, realizationLift_unique_fun R B g]
 195
 196/-- Arithmetic extracted from the realization's own identity-step orbit. -/
 197def extracted (R : LogicRealization) : ArithmeticOf R where
 198  peano := realizationPeano R
 199  initial := realization_initial R
 200
 201/-- Peano surface for the extracted arithmetic of any realization. -/
 202theorem extracted_peanoSurface (R : LogicRealization) :
 203    PeanoSurface (extracted R) where
 204  zero_ne_step := R.orbit_no_confusion
 205  step_injective := R.orbit_step_injective
 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

papers checked against this theorem

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