recAlg_id_left

formal source

  74  simp [recAlg_comp, CostMorphism.comp, Function.comp]
  75
  76/-- **PROVED: Identity is left-neutral (on underlying maps).** -/
  77theorem recAlg_id_left {C₁ C₂ : RecAlgObj} (f : RecAlgHom C₁ C₂) :
  78    (recAlg_comp (recAlg_id C₂) f).map = f.map := by
  79  ext x
  80  simp [recAlg_comp, recAlg_id, CostMorphism.comp, CostMorphism.id, Function.comp]
  81
  82/-- **PROVED: Identity is right-neutral (on underlying maps).** -/
  83theorem recAlg_id_right {C₁ C₂ : RecAlgObj} (f : RecAlgHom C₁ C₂) :
  84    (recAlg_comp f (recAlg_id C₁)).map = f.map := by
  85  ext x
  86  simp [recAlg_comp, recAlg_id, CostMorphism.comp, CostMorphism.id, Function.comp]
  87
  88/-! ## §2. The Initial Object -/
  89
  90/-- The **canonical cost algebra** J is the initial object in RecAlg.
  91    For any calibrated cost algebra C, there is a unique morphism J → C. -/
  92noncomputable def initialObject : RecAlgObj := canonicalCostAlgebra
  93
  94/-- From the initial object to any calibrated object,
  95    there exists a morphism (the identity-on-ℝ₊ map, when `C.cost = J`). -/
  96noncomputable def initial_morphism_exists :
  97    ∀ C : RecAlgObj, C.cost = J → RecAlgHom initialObject C := by
  98  intro C hC
  99  exact {
 100    map := fun x => x
 101    pos := fun _ h => h
 102    multiplicative := fun _ _ _ _ => rfl
 103    preserves_cost := fun x hx => by
 104      simpa [initialObject, canonicalCostAlgebra] using congrArg (fun f => f x) hC
 105  }
 106
 107/-! ## §3. The Paper-Facing Category `CostAlg⁺` -/