`extracted`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticOf
domain: Foundation
line: 197 · 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 197.

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

 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.