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 = (toSeminormedAddGroup f).toDist := by rfl) :
Proves that when a SeminormedAddGroup structure is constructed from an
AddGroupSeminormClass that satisfies IsNonarchimedean, the group has an IsUltrametricDist.