A continuous injection $\mathbb{Z}_p^{\,n} \hookrightarrow U_p(\mathbb{F})$ with principal-unit values is $\mathbb{Z}_p$-linear, so $n \le \operatorname{rank}_{\mathbb{Z}_p} U_1$

Let $p$ be a prime and $\mathbb{F}$ a number field, with semilocal units $U_p(\mathbb{F}) = \prod_{\wp \mid p} \mathcal{O}_\wp^\times$ (Section 1.1 of the source). Write

for the product of the principal units of the completions at the primes above $p$. Each factor is a pro-$p$ group and hence a topological $\mathbb{Z}_p$-module, with $u^a = \lim_n u^{a_n}$ for integers $a_n \to a$ (Definitions.Def_OneUnits, switched on at the primes above $p$ by Definitions.Def_PrimesOverNorm).

Suppose $f : \mathbb{Z}_p^{\,n} \to U_p(\mathbb{F})$ is a continuous injective group homomorphism all of whose values are principal units, that is, $\|f(x)_\wp - 1\| < 1$ for every $x$ and every $\wp \mid p$. Then

The reason is that such an $f$ is automatically $\mathbb{Z}_p$-linear: for $a \in \mathbb{Z}_p$ and integers $a_n \to a$, continuity gives $f(a x) = \lim f(a_n x) = \lim f(x)^{a_n} = f(x)^{a}$. So $f$ is an injective $\mathbb{Z}_p$-linear map from the free module $\mathbb{Z}_p^{\,n}$ into $U_1(\mathbb{F})$, and the rank of the source is at most the rank of the target.

This is the bridge between the two ways of measuring $\mathbb{Z}_p$-ranks in this mission: the definition file measures the rank of the $p$-adic closure $\bar{E}$ from below by continuous injections of $\mathbb{Z}_p^{\,n}$ (zpRankBelow), while the structure theory of local units is naturally expressed through Module.rank ℤ_[p]. It reduces the open lemma Leopoldt.le_finrank_of_continuous_injective_semilocalUnits, once the values are moved into the principal units by a finite power, to the statement $\operatorname{rank}_{\mathbb{Z}_p} U_1(\mathbb{F}) \le [\mathbb{F} : \mathbb{Q}]$.

Formalization Note $\mathbb{Z}_p^{\,n}$ is Multiplicative (Fin n → ℤ_[p]) with the product topology, and the target module is ∀ v : PrimesOver p F, Additive (oneUnits (v.1.adicCompletion F)), whose ℤ_[p]-module structure is OneUnits.instModule from the definition files. The principal-unit hypothesis is stated on the coordinates of $f(x)$ viewed in the completion $\mathbb{F}_\wp$. The conclusion is an inequality of cardinals, since Module.rank is a cardinal; $U_1(\mathbb{F})$ is in fact finitely generated, but that is not assumed here.