Linearity of a uniform pro-p group (source code)

= Linearity of a uniform pro-p group

Every <uniform pro-p group> embeds continuously in $\operatorname{GL}_n(\mathbb Z_p)$ for some finite $n$. Apply the <Ado theorem> to $\mathbb Q_p\otimes L_G$ and choose a deep power lattice whose representing <matrices> lie in $p\operatorname{End}(\Lambda)$, or $4\operatorname{End}(\Lambda)$ at $p=2$. The <matrix exponential> and <logarithm> give a <faithful representation> of the corresponding open normal power <subgroup>. Induce that representation to the whole <group> using its finitely many <cosets>. An element outside the <open subgroup> permutes the <coset> blocks nontrivially; an element inside it is detected by the original representation. Thus the <induced representation> is faithful. All block <matrices> preserve a finite free $\mathbb Z_p$-module, giving the integral embedding.