realizationLift

formal source

 131  fun n => (logicNatLift B).toFun (R.orbitEquivLogicNat n)
 132
 133/-- Homomorphism from the extracted realization orbit into any Peano object. -/
 134def realizationLift (R : LogicRealization) (B : PeanoObject) :
 135    PeanoObject.Hom (realizationPeano R) B where
 136  toFun := realizationFold R B
 137  map_zero := by
 138    unfold realizationFold
 139    change (logicNatLift B).toFun (R.orbitEquivLogicNat R.orbitZero) = B.zero
 140    rw [R.orbitEquiv_zero]
 141    rfl
 142  map_step := by
 143    intro x
 144    unfold realizationFold
 145    change (logicNatLift B).toFun (R.orbitEquivLogicNat (R.orbitStep x)) =
 146      B.step ((logicNatLift B).toFun (R.orbitEquivLogicNat x))
 147    rw [R.orbitEquiv_step]
 148    rfl
 149
 150private theorem realizationLift_unique_fun (R : LogicRealization) (B : PeanoObject)
 151    (f : PeanoObject.Hom (realizationPeano R) B) :
 152    f.toFun = (realizationLift R B).toFun := by
 153  funext n
 154  have hlogic :
 155      (f.toFun ∘ R.orbitEquivLogicNat.symm) =
 156        (logicNatLift B).toFun := by
 157    exact logicNatLift_unique_fun B
 158      { toFun := f.toFun ∘ R.orbitEquivLogicNat.symm
 159        map_zero := by
 160          simp [Function.comp_def]
 161          have hz := f.map_zero
 162          have hsymm0 : R.orbitEquivLogicNat.symm LogicNat.zero = R.orbitZero := by
 163            apply R.orbitEquivLogicNat.injective
 164            simp [R.orbitEquiv_zero]