Normed algebra preserves ultrametricity #
This file contains the proof that a normed division ring over an ultrametric field is ultrametric.
theorem
IsUltrametricDist.of_normedAlgebra'
{K : Type u_1}
(L : Type u_2)
[NormedField K]
[SeminormedRing L]
[NormOneClass L]
[NormedAlgebra K L]
[h : IsUltrametricDist L]
:
The other direction of IsUltrametricDist.of_normedAlgebra.
Let K be a normed field. If a seminormed ring L is a normed K-algebra, and ‖1‖ = 1 in L,
then K is ultrametric (i.e. the norm on L is nonarchimedean) if F is.
This can be further generalized to the case where ‖1‖ ≠ 0 in L.
theorem
IsUltrametricDist.of_normedAlgebra
(K : Type u_1)
{L : Type u_2}
[NormedField K]
[NormedDivisionRing L]
[NormedAlgebra K L]
[h : IsUltrametricDist K]
:
Let K be a normed field. If a normed division ring L is a normed K-algebra,
then L is ultrametric (i.e. the norm on L is nonarchimedean) if K is.
theorem
IsUltrametricDist.normedAlgebra_iff
(K : Type u_1)
(L : Type u_2)
[NormedField K]
[NormedDivisionRing L]
[NormedAlgebra K L]
:
Let K be a normed field. If a normed division ring L is a normed K-algebra,
then L is ultrametric (i.e. the norm on L is nonarchimedean) if and only if K is.