English
If φ is a star NNReal-algebra homomorphism, then φ.realContinuousMapOfNNReal is continuous whenever φ is continuous.
Русский
Если φ — звёздный гомоморфизм NNReal-сильного типа, то φ.realContinuousMapOfNNReal непрерывно тогда, когда φ непрерывно.
LaTeX
$$Continuous (φ.realContinuousMapOfNNReal) holds if Continuous φ.$$
Lean4
/-- Given a star `ℝ≥0`-algebra homomorphism `φ` from `C(X, ℝ≥0)` into an `ℝ`-algebra `A`, this is
the unique extension of `φ` from `C(X, ℝ)` to `A` as a star `ℝ`-algebra homomorphism. -/
@[simps]
noncomputable def realContinuousMapOfNNReal (φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A) : C(X, ℝ) →⋆ₐ[ℝ] A
where
toFun f := φ f.toNNReal - φ (-f).toNNReal
map_one' := by simp
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 ⊢
convert this using 1
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 ⊢
convert this using 1
abel
commutes'
r := by
obtain (hr | hr) := le_total 0 r
· lift r to ℝ≥0 using hr
simpa only [ContinuousMap.toNNReal_algebraMap, ContinuousMap.toNNReal_neg_algebraMap, map_zero, sub_zero] using
AlgHomClass.commutes φ r
· rw [← neg_neg r, ← map_neg, neg_neg (-r)]
rw [← neg_nonneg] at hr
lift -r to ℝ≥0 using hr with r
simpa only [map_neg, ContinuousMap.toNNReal_neg_algebraMap, map_zero, ContinuousMap.toNNReal_algebraMap, zero_sub,
neg_inj] using AlgHomClass.commutes φ r
map_star' f := by simp only [star_trivial, star_sub, ← map_star]
