Cyclotomic characters agree under restriction to ℚ̄

Let $p$ be a prime and let $\sigma$ be an automorphism of the field PadicAlgCl p as a $\mathbb{Q}_p$-algebra. Write localGaloisToGlobal p for the monoid homomorphism from $\mathbb{Q}_p$-algebra automorphisms of PadicAlgCl p to $\mathbb{Q}$-algebra automorphisms of AlgebraicClosure ℚ obtained by first restricting scalars from $\mathbb{Q}_p$ to $\mathbb{Q}$ and then applying AlgEquiv.restrictNormalHom, i.e. restricting the resulting $\mathbb{Q}$-algebra automorphism to the normal subextension AlgebraicClosure ℚ of PadicAlgCl p determined by the fixed embedding padicEmbedding p. The assertion is an equality in $\mathbb{Z}_p^{\times}$: the $p$-adic cyclotomic character of AlgebraicClosure ℚ evaluated at the ring isomorphism underlying localGaloisToGlobal p σ equals the $p$-adic cyclotomic character of PadicAlgCl p evaluated at the ring isomorphism underlying $\sigma$. Both characters are Mathlib's cyclotomicCharacter, available because each field contains enough $p^n$-th roots of unity for every $n$.

This is the compatibility of the global and local $p$-adic cyclotomic characters along the chosen embedding $\overline{\mathbb Q}\hookrightarrow\overline{\mathbb Q}_p$, and it allows the two spellings of $\chi_p$ used in the project (on $\overline{\mathbb Q}$ via restriction, and directly on $\overline{\mathbb Q}_p$) to be interchanged. It is used in PadicComplex.eq_zero_of_forall_mem_fixingSubgroup_smul_eq_cyclotomicCharacter_zpow_mul.