Constructing nonarchimedean (ultrametric) normed groups from nonarchimedean normed homs #
This file defines constructions that upgrade Add(Comm)Group to (Semi)NormedAdd(Comm)Group
using an AddGroup(Semi)normClass when the codomain is the reals and the hom is nonarchimedean.
Implementation details #
The lemmas need to assume [Dist α] to be able to be stated, so they take an extra argument
that shows that this distance instance is propositionally equal to the one that comes from the
hom-based AddGroupSeminormClass.toSeminormedAddGroup f construction. To help at use site,
the argument is an autoparam that resolves by definitional equality when using these constructions.
theorem
AddGroupSeminormClass.isUltrametricDist
{F : Type u_1}
{α : Type u_2}
[FunLike F α ℝ]
[AddGroup α]
[AddGroupSeminormClass F α ℝ]
[inst : Dist α]
{f : F}
(hna : IsNonarchimedean ⇑f)
(hd : inst = PseudoMetricSpace.toDist := by rfl)
:
Proves that when a SeminormedAddGroup structure is constructed from an
AddGroupSeminormClass that satifies IsNonarchimedean, the group has an IsUltrametricDist.