norm of units

Stream: Is there code for X?

[Eric Wieser]

Under what assumptions (other than normed_field) is the following true?

example {R} [normed_ring R] (u : Rˣ) : ‖(↑u⁻¹ : R)‖ = ‖(u : R)‖⁻¹ := sorry

I can prove one direction, but get stuck at showing ‖↑u‖ * ‖↑u⁻¹‖ ≤ 1

[Reid Barton]

Usually it won't be true, e.g. in a ring of functions, or just a product of normed fields

[Eric Wieser]

I'll remember to try those examples first next time, thanks! It sounds like I #xy'd this incorrectly and don't need the result anyway.

[Kevin Buzzard]

The way to think about it is geometrically. Imagine that R is the functions on a space, and $||u||$ is the supremum of the sizes of the values that the function $u$ takes. If $u$ takes two values $x$ and $y$ with $|x|<|y|$, then $||u|||\geq |y|$ but $||u^{-1}||\geq |x^{-1}|$ so their product is $\geq |y/x|>1$. Reid's example of a product of (say $d$) normed fields is where the space is finite of size $d$.

Fields are like functions on one point, so the above argument doesn't work for them.