Definition df-qpa 31556

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.)

Assertion

Ref	Expression
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 ) ) } ) ) )

Distinct variable group:   f, d, n, p, r

Detailed syntax breakdown of Definition df-qpa

Step	Hyp	Ref	Expression
1		cqpa 31546	. 2 class _Qp
2		vp	. . 3 setvar p
3		cprime 15385	. . 3 class Prime
4		vr	. . . 4 setvar r
5	2	cv 1482	. . . . 5 class p
6		cqp 31543	. . . . 5 class Qp
7	5, 6	cfv 5888	. . . 4 class (Qp ` p )
8	4	cv 1482	. . . . 5 class r
9		vn	. . . . . 6 setvar n
10		cn 11020	. . . . . 6 class NN
11		vf	. . . . . . . . . . 11 setvar f
12	11	cv 1482	. . . . . . . . . 10 class f
13		cdg1 23814	. . . . . . . . . 10 class deg1
14	8, 12, 13	co 6650	. . . . . . . . 9 class ( r deg1 f )
15	9	cv 1482	. . . . . . . . 9 class n
16		cle 10075	. . . . . . . . 9 class <_
17	14, 15, 16	wbr 4653	. . . . . . . 8 wff ( r deg1 f ) <_ n
18		vd	. . . . . . . . . . . . 13 setvar d
19	18	cv 1482	. . . . . . . . . . . 12 class d
20	19	ccnv 5113	. . . . . . . . . . 11 class `' d
21		cz 11377	. . . . . . . . . . . 12 class ZZ
22		cc0 9936	. . . . . . . . . . . . 13 class 0
23	22	csn 4177	. . . . . . . . . . . 12 class { 0 }
24	21, 23	cdif 3571	. . . . . . . . . . 11 class ( ZZ \ { 0 } )
25	20, 24	cima 5117	. . . . . . . . . 10 class ( `' d " ( ZZ \ { 0 } ) )
26		cfz 12326	. . . . . . . . . . 11 class ...
27	22, 15, 26	co 6650	. . . . . . . . . 10 class ( 0 ... n )
28	25, 27	wss 3574	. . . . . . . . 9 wff ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n )
29		cco1 19548	. . . . . . . . . . 11 class coe1
30	12, 29	cfv 5888	. . . . . . . . . 10 class (coe1 ` f )
31	30	crn 5115	. . . . . . . . 9 class ran (coe1 ` f )
32	28, 18, 31	wral 2912	. . . . . . . 8 wff A. d e. ran (coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n )
33	17, 32	wa 384	. . . . . . 7 wff ( ( r deg1 f ) <_ n /\ A. d e. ran (coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) )
34		cpl1 19547	. . . . . . . 8 class Poly1
35	8, 34	cfv 5888	. . . . . . 7 class (Poly1 ` r )
36	33, 11, 35	crab 2916	. . . . . 6 class { 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 4729	. . . . 5 class ( n e. NN |-> { f e. (Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran (coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } )
38		cpsl 31529	. . . . 5 class polySplitLim
39	8, 37, 38	co 6650	. . . 4 class ( 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	4, 7, 39	csb 3533	. . 3 class [_ (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	2, 3, 40	cmpt 4729	. 2 class ( 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 ) ) } ) ) )
42	1, 41	wceq 1483	1 wff _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 ) ) } ) ) )

This definition is referenced by: (None)