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	|- _Qp = ( p e. Prime |-> [_ ( Qp ` p ) / r ]_ ( r polySplitLim ( n e. NN |-> { f e. ( Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqpa	|- _Qp
1		vp	|- p
2		cprime	|- Prime
3		cqp	|- Qp
4	1	cv	|- p
5	4 3	cfv	|- ( Qp ` p )
6		vr	|- r
7	6	cv	|- r
8		cpsl	|- polySplitLim
9		vn	|- n
10		cn	|- NN
11		vf	|- f
12		cpl1	|- Poly1
13	7 12	cfv	|- ( Poly1 ` r )
14		cdg1	|- deg1
15	11	cv	|- f
16	7 15 14	co	|- ( r deg1 f )
17		cle	|- <_
18	9	cv	|- n
19	16 18 17	wbr	|- ( r deg1 f ) <_ n
20		vd	|- d
21		cco1	|- coe1
22	15 21	cfv	|- ( coe1 ` f )
23	22	crn	|- ran ( coe1 ` f )
24	20	cv	|- d
25	24	ccnv	|- `' d
26		cz	|- ZZ
27		cc0	|- 0
28	27	csn	|- { 0 }
29	26 28	cdif	|- ( ZZ \ { 0 } )
30	25 29	cima	|- ( `' d " ( ZZ \ { 0 } ) )
31		cfz	|- ...
32	27 18 31	co	|- ( 0 ... n )
33	30 32	wss	|- ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n )
34	33 20 23	wral	|- A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n )
35	19 34	wa	|- ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) )
36	35 11 13	crab	|- { f e. ( Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) }
37	9 10 36	cmpt	|- ( n e. NN |-> { f e. ( Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } )
38	7 37 8	co	|- ( r polySplitLim ( n e. NN |-> { f e. ( Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } ) )
39	6 5 38	csb	|- [_ ( Qp ` p ) / r ]_ ( r polySplitLim ( n e. NN |-> { f e. ( Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } ) )
40	1 2 39	cmpt	|- ( p e. Prime |-> [_ ( Qp ` p ) / r ]_ ( r polySplitLim ( n e. NN |-> { f e. ( Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } ) ) )
41	0 40	wceq	|- _Qp = ( p e. Prime |-> [_ ( Qp ` p ) / r ]_ ( r polySplitLim ( n e. NN |-> { f e. ( Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran ( coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } ) ) )