`CostAlgPlusHom`

definition

show as: view math explainer →

module: IndisputableMonolith.Algebra.RecognitionCategory
domain: Algebra
line: 332 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 332.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 329/-- Morphisms in `CostAlg⁺` are the positive exponents `α > 0` satisfying
 330    the parameter relation `α κ₂ = κ₁`. This is the paper's
 331    order-preserving morphism classification. -/
 332structure CostAlgPlusHom (C₁ C₂ : CostAlgPlusObj) where
 333  α : ℝ
 334  α_pos : 0 < α
 335  intertwines : α * C₂.κ = C₁.κ
 336
 337/-- Extensionality for `CostAlg⁺` morphisms: the exponent `α` determines the
 338    morphism completely. -/
 339@[ext] theorem CostAlgPlusHom.ext
 340    {C₁ C₂ : CostAlgPlusObj} {f g : CostAlgPlusHom C₁ C₂}
 341    (hα : f.α = g.α) : f = g := by
 342  cases f
 343  cases g
 344  cases hα
 345  simp
 346
 347/-- The underlying positive-reals map of a `CostAlg⁺` morphism. -/
 348noncomputable def CostAlgPlusHom.map {C₁ C₂ : CostAlgPlusObj}
 349    (f : CostAlgPlusHom C₁ C₂) (x : ℝ) : ℝ :=
 350  powerMap f.α x
 351
 352/-- A `CostAlg⁺` morphism maps positive reals to positive reals. -/
 353theorem CostAlgPlusHom.map_pos {C₁ C₂ : CostAlgPlusObj}
 354    (f : CostAlgPlusHom C₁ C₂) {x : ℝ} (hx : 0 < x) :
 355    0 < f.map x :=
 356  powerMap_pos f.α hx
 357
 358/-- A `CostAlg⁺` morphism is multiplicative. -/
 359theorem CostAlgPlusHom.map_mul {C₁ C₂ : CostAlgPlusObj}
 360    (f : CostAlgPlusHom C₁ C₂) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 361    f.map (x * y) = f.map x * f.map y :=
 362  powerMap_mul f.α hx hy

papers checked against this theorem

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