English
For any nonzero e ∈ ℝ≥0, there is a MonoidWithZeroHom from the WithZero (Multiplicative Int) to ℝ≥0 sending 0 ↦ 0 and nonzero x to e^(unzero x).toAdd, i.e., a size-weighting homomorphism that respects multiplication and sends 0 to 0.
Русский
Для любого не нуля e ∈ ℝ≥0 существует гомоморфизм монойд с нулём from WithZero (Multiplicative Int) в ℝ≥0, который отправляет 0 в 0, а не нулевой элемент x в e^{ (unzero x).toAdd }, т.е. непрерывный по умножению размерный гомоморфизм.
LaTeX
$$$\exists (φ : WithZero (Multiplicative \mathbb{Z}) \to₀ ℝ_{≥0}), φ(0) = 0 \\land \forall x \,(x \ne 0) \Rightarrow φ(x) = e^{(WithZero.unzero x).toAdd}$$$
Lean4
/-- Given a nonzero `e : ℝ≥0`, this is the map `ℤᵐ⁰ → ℝ≥0` sending `0 ↦ 0` and
`x ↦ e^(WithZero.unzero hx).toAdd` when `x ≠ 0` as a `MonoidWithZeroHom`. -/
def toNNReal {e : ℝ≥0} (he : e ≠ 0) : ℤᵐ⁰ →*₀ ℝ≥0
where
toFun := fun x ↦ if hx : x = 0 then 0 else e ^ (WithZero.unzero hx).toAdd
map_zero' := rfl
map_one' := by
simp only [dif_neg one_ne_zero]
erw [toAdd_one, zpow_zero]
map_mul' x
y := by
by_cases hxy : x * y = 0
· rcases mul_eq_zero.mp hxy with hx | hy
· rw [dif_pos hxy, dif_pos hx, zero_mul]
· rw [dif_pos hxy, dif_pos hy, mul_zero]
· obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy
rw [dif_neg hxy, dif_neg hx, dif_neg hy, ← zpow_add' (Or.inl he), ← toAdd_mul]
congr
rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]
