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

Definition df-qpa 34643
Description: Define the completion of the š‘-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the š‘›-th set the collection of polynomials with degree less than š‘› and with coefficients < (š‘ā†‘š‘›)). 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 š‘„ā†‘(š‘ā†‘š‘›) āˆ’ š‘„, 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 = (š‘ āˆˆ ā„™ ā†¦ ā¦‹(Qpā€˜š‘) / š‘Ÿā¦Œ(š‘Ÿ polySplitLim (š‘› āˆˆ ā„• ā†¦ {š‘“ āˆˆ (Poly1ā€˜š‘Ÿ) āˆ£ ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))})))
Distinct variable group:   š‘“,š‘‘,š‘›,š‘,š‘Ÿ

Detailed syntax breakdown of Definition df-qpa
StepHypRef Expression
1 cqpa 34634 . 2 class _Qp
2 vp . . 3 setvar š‘
3 cprime 16607 . . 3 class ā„™
4 vr . . . 4 setvar š‘Ÿ
52cv 1540 . . . . 5 class š‘
6 cqp 34632 . . . . 5 class Qp
75, 6cfv 6543 . . . 4 class (Qpā€˜š‘)
84cv 1540 . . . . 5 class š‘Ÿ
9 vn . . . . . 6 setvar š‘›
10 cn 12211 . . . . . 6 class ā„•
11 vf . . . . . . . . . . 11 setvar š‘“
1211cv 1540 . . . . . . . . . 10 class š‘“
13 cdg1 25568 . . . . . . . . . 10 class deg1
148, 12, 13co 7408 . . . . . . . . 9 class (š‘Ÿ deg1 š‘“)
159cv 1540 . . . . . . . . 9 class š‘›
16 cle 11248 . . . . . . . . 9 class ā‰¤
1714, 15, 16wbr 5148 . . . . . . . 8 wff (š‘Ÿ deg1 š‘“) ā‰¤ š‘›
18 vd . . . . . . . . . . . . 13 setvar š‘‘
1918cv 1540 . . . . . . . . . . . 12 class š‘‘
2019ccnv 5675 . . . . . . . . . . 11 class ā—”š‘‘
21 cz 12557 . . . . . . . . . . . 12 class ā„¤
22 cc0 11109 . . . . . . . . . . . . 13 class 0
2322csn 4628 . . . . . . . . . . . 12 class {0}
2421, 23cdif 3945 . . . . . . . . . . 11 class (ā„¤ āˆ– {0})
2520, 24cima 5679 . . . . . . . . . 10 class (ā—”š‘‘ ā€œ (ā„¤ āˆ– {0}))
26 cfz 13483 . . . . . . . . . . 11 class ...
2722, 15, 26co 7408 . . . . . . . . . 10 class (0...š‘›)
2825, 27wss 3948 . . . . . . . . 9 wff (ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›)
29 cco1 21701 . . . . . . . . . . 11 class coe1
3012, 29cfv 6543 . . . . . . . . . 10 class (coe1ā€˜š‘“)
3130crn 5677 . . . . . . . . 9 class ran (coe1ā€˜š‘“)
3228, 18, 31wral 3061 . . . . . . . 8 wff āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›)
3317, 32wa 396 . . . . . . 7 wff ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))
34 cpl1 21700 . . . . . . . 8 class Poly1
358, 34cfv 6543 . . . . . . 7 class (Poly1ā€˜š‘Ÿ)
3633, 11, 35crab 3432 . . . . . 6 class {š‘“ āˆˆ (Poly1ā€˜š‘Ÿ) āˆ£ ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))}
379, 10, 36cmpt 5231 . . . . 5 class (š‘› āˆˆ ā„• ā†¦ {š‘“ āˆˆ (Poly1ā€˜š‘Ÿ) āˆ£ ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))})
38 cpsl 34619 . . . . 5 class polySplitLim
398, 37, 38co 7408 . . . 4 class (š‘Ÿ polySplitLim (š‘› āˆˆ ā„• ā†¦ {š‘“ āˆˆ (Poly1ā€˜š‘Ÿ) āˆ£ ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))}))
404, 7, 39csb 3893 . . 3 class ā¦‹(Qpā€˜š‘) / š‘Ÿā¦Œ(š‘Ÿ polySplitLim (š‘› āˆˆ ā„• ā†¦ {š‘“ āˆˆ (Poly1ā€˜š‘Ÿ) āˆ£ ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))}))
412, 3, 40cmpt 5231 . 2 class (š‘ āˆˆ ā„™ ā†¦ ā¦‹(Qpā€˜š‘) / š‘Ÿā¦Œ(š‘Ÿ polySplitLim (š‘› āˆˆ ā„• ā†¦ {š‘“ āˆˆ (Poly1ā€˜š‘Ÿ) āˆ£ ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))})))
421, 41wceq 1541 1 wff _Qp = (š‘ āˆˆ ā„™ ā†¦ ā¦‹(Qpā€˜š‘) / š‘Ÿā¦Œ(š‘Ÿ polySplitLim (š‘› āˆˆ ā„• ā†¦ {š‘“ āˆˆ (Poly1ā€˜š‘Ÿ) āˆ£ ((š‘Ÿ deg1 š‘“) ā‰¤ š‘› āˆ§ āˆ€š‘‘ āˆˆ ran (coe1ā€˜š‘“)(ā—”š‘‘ ā€œ (ā„¤ āˆ– {0})) āŠ† (0...š‘›))})))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator