`CostAlgHomKappa`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 169.

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

 166
 167/-- Morphisms in the full paper-facing `CostAlg` category are power maps
 168    `x ↦ x^α` with `ακ₂ = ±κ₁`. -/
 169structure CostAlgHomKappa (C₁ C₂ : CostAlgObjKappa) where
 170  α : ℝ
 171  α_ne_zero : α ≠ 0
 172  intertwines : α * C₂.κ = C₁.κ ∨ α * C₂.κ = -C₁.κ
 173
 174/-- Extensionality for `CostAlg` morphisms: the exponent `α` determines the
 175    morphism completely. -/
 176@[ext] theorem CostAlgHomKappa.ext
 177    {C₁ C₂ : CostAlgObjKappa} {f g : CostAlgHomKappa C₁ C₂}
 178    (hα : f.α = g.α) : f = g := by
 179  cases f
 180  cases g
 181  cases hα
 182  simp
 183
 184/-- The underlying positive-reals map of a `CostAlg` morphism. -/
 185noncomputable def CostAlgHomKappa.map {C₁ C₂ : CostAlgObjKappa}
 186    (f : CostAlgHomKappa C₁ C₂) (x : ℝ) : ℝ :=
 187  powerMap f.α x
 188
 189/-- A `CostAlg` morphism maps positive reals to positive reals. -/
 190theorem CostAlgHomKappa.map_pos {C₁ C₂ : CostAlgObjKappa}
 191    (f : CostAlgHomKappa C₁ C₂) {x : ℝ} (hx : 0 < x) :
 192    0 < f.map x :=
 193  powerMap_pos f.α hx
 194
 195/-- A `CostAlg` morphism is multiplicative. -/
 196theorem CostAlgHomKappa.map_mul {C₁ C₂ : CostAlgObjKappa}
 197    (f : CostAlgHomKappa C₁ C₂) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 198    f.map (x * y) = f.map x * f.map y :=
 199  powerMap_mul f.α hx hy

papers checked against this theorem

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