English
There is a canonical way to extend NNReal-valued continuous maps to Real-valued continuous maps via a suitable extension process; the construction commutes with the embedding of NNReal into Real.
Русский
Существует стандартное расширение NNReal-значимых непрерывных отображений до Real-значимых непрерывных отображений; вложение NNReal в Real сохраняется в процессе расширения.
LaTeX
$$extension_commutes := (Real).toNNReal ∘ f = φ f \\\\ (where φ is the extended homomorphism)$$
Lean4
/-- Given a non-unital star `ℝ≥0`-algebra homomorphism `φ` from `C(X, ℝ≥0)₀` into a non-unital
`ℝ`-algebra `A`, this is the unique extension of `φ` from `C(X, ℝ)₀` to `A` as a non-unital
star `ℝ`-algebra homomorphism. -/
@[simps]
noncomputable def realContinuousMapZeroOfNNReal (φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) : C(X, ℝ)₀ →⋆ₙₐ[ℝ] A
where
toFun f := φ f.toNNReal - φ (-f).toNNReal
map_zero' := by simp
map_mul' f
g := by
have := congr(φ $(f.toNNReal_mul_add_neg_mul_add_mul_neg_eq g))
simp only [map_add, map_mul, sub_mul, mul_sub] at this ⊢
rw [← sub_eq_zero] at this ⊢
rw [← this]
abel
map_add' f
g := by
have := congr(φ $(f.toNNReal_add_add_neg_add_neg_eq g))
simp only [map_add] at this ⊢
rw [← sub_eq_zero] at this ⊢
rw [← this]
abel
map_smul' r
f := by
simp only [MonoidHom.id_apply]
by_cases hr : 0 ≤ r
· lift r to ℝ≥0 using hr
simp only [← smul_def, toNNReal_smul, map_smul, toNNReal_neg_smul, smul_sub]
· rw [not_le, ← neg_pos] at hr
rw [← neg_smul]
nth_rw 1 [← neg_neg r]
nth_rw 3 [← neg_neg r]
lift -r to ℝ≥0 using hr.le with r
simp only [neg_smul, ← smul_def, toNNReal_neg_smul, map_smul, toNNReal_smul, smul_sub, sub_neg_eq_add]
rw [sub_eq_add_neg, add_comm]
map_star' f := by simp only [star_trivial, star_sub, ← map_star]
