pith. machine review for the scientific record. sign in
structure definition def or abbrev

CostAlgHomKappa

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Definition body.

 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
 200
 201/-- A full `CostAlg` morphism preserves the explicit cost family. -/
 202theorem CostAlgHomKappa.preserves_cost {C₁ C₂ : CostAlgObjKappa}
 203    (f : CostAlgHomKappa C₁ C₂) {x : ℝ} (hx : 0 < x) :
 204    C₂.cost (f.map x) = C₁.cost x := by
 205  rcases f.intertwines with h | h
 206  · simpa [CostAlgObjKappa.cost, h] using
 207      (costFamily_comp_powerMap C₂.κ f.α hx)
 208  · calc
 209      C₂.cost (f.map x) = costFamily (f.α * C₂.κ) x := by
 210        simpa [CostAlgObjKappa.cost] using
 211          (costFamily_comp_powerMap C₂.κ f.α hx)
 212      _ = costFamily (-C₁.κ) x := by rw [h]
 213      _ = costFamily C₁.κ x := costFamily_neg_param C₁.κ x
 214      _ = C₁.cost x := rfl
 215
 216/-- Identity morphism in the full paper-facing `CostAlg` category. -/
 217def CostAlgHomKappa.id (C : CostAlgObjKappa) : CostAlgHomKappa C C where
 218  α := 1
 219  α_ne_zero := one_ne_zero
 220  intertwines := Or.inl (by ring)
 221
 222/-- Composition of full `CostAlg` morphisms. -/
 223def CostAlgHomKappa.comp {C₁ C₂ C₃ : CostAlgObjKappa}
 224    (g : CostAlgHomKappa C₂ C₃) (f : CostAlgHomKappa C₁ C₂) :
 225    CostAlgHomKappa C₁ C₃ where
 226  α := f.α * g.α
 227  α_ne_zero := mul_ne_zero f.α_ne_zero g.α_ne_zero
 228  intertwines := by
 229    rcases f.intertwines with hf | hf <;> rcases g.intertwines with hg | hg
 230    · left
 231      calc
 232        (f.α * g.α) * C₃.κ = f.α * (g.α * C₃.κ) := by ring
 233        _ = f.α * C₂.κ := by rw [hg]
 234        _ = C₁.κ := by rw [hf]
 235    · right
 236      calc
 237        (f.α * g.α) * C₃.κ = f.α * (g.α * C₃.κ) := by ring
 238        _ = f.α * (-C₂.κ) := by rw [hg]
 239        _ = -(f.α * C₂.κ) := by ring
 240        _ = -C₁.κ := by rw [hf]
 241    · right
 242      calc
 243        (f.α * g.α) * C₃.κ = f.α * (g.α * C₃.κ) := by ring
 244        _ = f.α * C₂.κ := by rw [hg]
 245        _ = -C₁.κ := by rw [hf]
 246    · left
 247      calc
 248        (f.α * g.α) * C₃.κ = f.α * (g.α * C₃.κ) := by ring
 249        _ = f.α * (-C₂.κ) := by rw [hg]
 250        _ = -(f.α * C₂.κ) := by ring
 251        _ = C₁.κ := by rw [hf]; ring
 252
 253/-- The canonical object of the full paper-facing `CostAlg` category is the
 254    calibrated `κ = 1` family. -/

depends on (40)

Lean names referenced from this declaration's body.

… and 10 more