Global levels are cofinal among finite local levels

Let $q$ be a prime, let $\overline{\mathbb{Q}}_q$ denote PadicAlgCl q with its group $\mathrm{Gal}(\overline{\mathbb{Q}}_q/\mathbb{Q}_q)$ of $\mathbb{Q}_q$-algebra automorphisms, and let $P$ be an arbitrary property of subgroups of that group which is inherited by subgroups, i.e. $P(U)$ and $V \le U$ imply $P(V)$. Write $r_q =$ localGaloisToGlobal q for the group homomorphism $\mathrm{Gal}(\overline{\mathbb{Q}}_q/\mathbb{Q}_q) \to \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ obtained by viewing a $\mathbb{Q}_q$-automorphism of $\overline{\mathbb{Q}}_q$ as a $\mathbb{Q}$-automorphism and then restricting it along AlgEquiv.restrictNormalHom to the normal intermediate field AlgebraicClosure ℚ. The assertion is the equivalence of two existence statements: on the one hand, there is an intermediate field $F$ of $\overline{\mathbb{Q}}/\mathbb{Q}$, finite-dimensional over $\mathbb{Q}$, such that $P$ holds of the preimage $r_q^{-1}(\mathrm{Gal}(\overline{\mathbb{Q}}/F))$ of the pointwise fixing subgroup of $F$; on the other hand, there is an intermediate field $K$ of $\overline{\mathbb{Q}}_q/\mathbb{Q}_q$, finite-dimensional over $\mathbb{Q}_q$, such that $P$ holds of the pointwise fixing subgroup $\mathrm{Gal}(\overline{\mathbb{Q}}_q/K)$.

This packages the mutual cofinality of the two natural families of levels in $\mathrm{Gal}(\overline{\mathbb{Q}}_q/\mathbb{Q}_q)$: pull-backs of $\mathrm{Gal}(\overline{\mathbb{Q}}/F)$ for number fields $F$, and the open subgroups $\mathrm{Gal}(\overline{\mathbb{Q}}_q/K)$ for finite extensions $K/\mathbb{Q}_q$. It is used to convert conditions stated at global levels (smoothness of a vector, local constancy of a cochain) into conditions at finite local levels, and conversely.