Definition df-qpa

Description: Define the completion of the p -adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the n -th set the collection of polynomials with degree less than n and with coefficients < ( p ^ n ) ). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial x ^ ( p ^ n ) - x , which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-qpa	$$⊢\overline{{\mathbb{Q}}_p}=\left(p\in \mathbb{P}⟼⦋{\mathbb{Q}}_p\left(p\right)/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{f\in {\mathrm{Poly}}_1\left(r\right)|\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqpa	$$class\overline{{\mathbb{Q}}_p}$$
1		vp	$$setvarp$$
2		cprime	$$class\mathbb{P}$$
3		cqp	$$class{\mathbb{Q}}_p$$
4	1	cv	$$setvarp$$
5	4 3	cfv	$$class{\mathbb{Q}}_p\left(p\right)$$
6		vr	$$setvarr$$
7	6	cv	$$setvarr$$
8		cpsl	$$class\mathrm{polySplitLim}$$
9		vn	$$setvarn$$
10		cn	$$class\mathbb{N}$$
11		vf	$$setvarf$$
12		cpl1	$$class{\mathrm{Poly}}_1$$
13	7 12	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
14		cdg1	$$class{\mathrm{deg}}_1$$
15	11	cv	$$setvarf$$
16	7 15 14	co	$$class\left(r{\mathrm{deg}}_{1}f\right)$$
17		cle	$$class\le$$
18	9	cv	$$setvarn$$
19	16 18 17	wbr	$$wffr{\mathrm{deg}}_{1}f\le n$$
20		vd	$$setvard$$
21		cco1	$$class{\mathrm{coe}}_1$$
22	15 21	cfv	$$class{\mathrm{coe}}_1\left(f\right)$$
23	22	crn	$$class\mathrm{ran}{\mathrm{coe}}_1\left(f\right)$$
24	20	cv	$$setvard$$
25	24	ccnv	$$class{d}^{-1}$$
26		cz	$$class\mathbb{Z}$$
27		cc0	$$class0$$
28	27	csn	$$class\left\{0\right\}$$
29	26 28	cdif	$$class\left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
30	25 29	cima	$$class{d}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]$$
31		cfz	$$class\dots$$
32	27 18 31	co	$$class\left(0\dots n\right)$$
33	30 32	wss	$$wff{d}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)$$
34	33 20 23	wral	$$wff\forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)$$
35	19 34	wa	$$wff\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)$$
36	35 11 13	crab	$$class\left\{f\in {\mathrm{Poly}}_1\left(r\right)|\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)\right\}$$
37	9 10 36	cmpt	$$class\left(n\in \mathbb{N}⟼\left\{f\in {\mathrm{Poly}}_1\left(r\right)|\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)\right\}\right)$$
38	7 37 8	co	$$class\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{f\in {\mathrm{Poly}}_1\left(r\right)|\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)\right\}\right)\right)$$
39	6 5 38	csb	$$class⦋{\mathbb{Q}}_p\left(p\right)/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{f\in {\mathrm{Poly}}_1\left(r\right)|\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)\right\}\right)\right)$$
40	1 2 39	cmpt	$$class\left(p\in \mathbb{P}⟼⦋{\mathbb{Q}}_p\left(p\right)/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{f\in {\mathrm{Poly}}_1\left(r\right)|\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)\right\}\right)\right)\right)$$
41	0 40	wceq	$$wff\overline{{\mathbb{Q}}_p}=\left(p\in \mathbb{P}⟼⦋{\mathbb{Q}}_p\left(p\right)/r⦌\left(r\mathrm{polySplitLim}\left(n\in \mathbb{N}⟼\left\{f\in {\mathrm{Poly}}_1\left(r\right)|\left(r{\mathrm{deg}}_{1}f\le n\wedge \forall d\in \mathrm{ran}{\mathrm{coe}}_1\left(f\right)d^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq \left(0\dots n\right)\right)\right\}\right)\right)\right)$$