`CostAlgHomKappa`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 169.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.