Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-qpa Unicode version

Definition df-qpa 24005
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
StepHypRef Expression
1 cqpa 23996 . 2  class _Qp
2 vp . . 3  set  p
3 cprime 12774 . . 3  class  Prime
4 vr . . . 4  set  r
52cv 1631 . . . . 5  class  p
6 cqp 23994 . . . . 5  class Qp
75, 6cfv 5271 . . . 4  class  (Qp `  p )
84cv 1631 . . . . 5  class  r
9 vn . . . . . 6  set  n
10 cn 9762 . . . . . 6  class  NN
11 vf . . . . . . . . . . 11  set  f
1211cv 1631 . . . . . . . . . 10  class  f
13 cdg1 19456 . . . . . . . . . 10  class deg1
148, 12, 13co 5874 . . . . . . . . 9  class  ( r deg1  f )
159cv 1631 . . . . . . . . 9  class  n
16 cle 8884 . . . . . . . . 9  class  <_
1714, 15, 16wbr 4039 . . . . . . . 8  wff  ( r deg1  f )  <_  n
18 vd . . . . . . . . . . . . 13  set  d
1918cv 1631 . . . . . . . . . . . 12  class  d
2019ccnv 4704 . . . . . . . . . . 11  class  `' d
21 cz 10040 . . . . . . . . . . . 12  class  ZZ
22 cc0 8753 . . . . . . . . . . . . 13  class  0
2322csn 3653 . . . . . . . . . . . 12  class  { 0 }
2421, 23cdif 3162 . . . . . . . . . . 11  class  ( ZZ 
\  { 0 } )
2520, 24cima 4708 . . . . . . . . . 10  class  ( `' d " ( ZZ 
\  { 0 } ) )
26 cfz 10798 . . . . . . . . . . 11  class  ...
2722, 15, 26co 5874 . . . . . . . . . 10  class  ( 0 ... n )
2825, 27wss 3165 . . . . . . . . 9  wff  ( `' d " ( ZZ 
\  { 0 } ) )  C_  (
0 ... n )
29 cco1 16271 . . . . . . . . . . 11  class coe1
3012, 29cfv 5271 . . . . . . . . . 10  class  (coe1 `  f
)
3130crn 4706 . . . . . . . . 9  class  ran  (coe1 `  f )
3228, 18, 31wral 2556 . . . . . . . 8  wff  A. d  e.  ran  (coe1 `  f ) ( `' d " ( ZZ  \  { 0 } ) )  C_  (
0 ... n )
3317, 32wa 358 . . . . . . 7  wff  ( ( r deg1  f )  <_  n  /\  A. d  e.  ran  (coe1 `  f ) ( `' d " ( ZZ 
\  { 0 } ) )  C_  (
0 ... n ) )
34 cpl1 16268 . . . . . . . 8  class Poly1
358, 34cfv 5271 . . . . . . 7  class  (Poly1 `  r
)
3633, 11, 35crab 2560 . . . . . 6  class  { f  e.  (Poly1 `  r )  |  ( ( r deg1  f )  <_  n  /\  A. d  e.  ran  (coe1 `  f
) ( `' d
" ( ZZ  \  { 0 } ) )  C_  ( 0 ... n ) ) }
379, 10, 36cmpt 4093 . . . . 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 23980 . . . . 5  class polySplitLim
398, 37, 38co 5874 . . . 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 ) ) } ) )
404, 7, 39csb 3094 . . 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 ) ) } ) )
412, 3, 40cmpt 4093 . 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 ) ) } ) ) )
421, 41wceq 1632 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 ) ) } ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator