recAlg_comp

formal source

  62  CostMorphism.id C
  63
  64/-- **PROVED: Morphisms compose.** -/
  65def recAlg_comp {C₁ C₂ C₃ : RecAlgObj}
  66    (g : RecAlgHom C₂ C₃) (f : RecAlgHom C₁ C₂) : RecAlgHom C₁ C₃ :=
  67  CostMorphism.comp g f
  68
  69/-- **PROVED: Composition is associative (on underlying maps).** -/
  70theorem recAlg_comp_assoc {C₁ C₂ C₃ C₄ : RecAlgObj}
  71    (h : RecAlgHom C₃ C₄) (g : RecAlgHom C₂ C₃) (f : RecAlgHom C₁ C₂) :
  72    (recAlg_comp h (recAlg_comp g f)).map = (recAlg_comp (recAlg_comp h g) f).map := by
  73  ext x
  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`). -/