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 32966
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 32957 . 2 class _Qp
2 vp . . 3 setvar 𝑝
3 cprime 16013 . . 3 class
4 vr . . . 4 setvar 𝑟
52cv 1537 . . . . 5 class 𝑝
6 cqp 32955 . . . . 5 class Qp
75, 6cfv 6343 . . . 4 class (Qp‘𝑝)
84cv 1537 . . . . 5 class 𝑟
9 vn . . . . . 6 setvar 𝑛
10 cn 11634 . . . . . 6 class
11 vf . . . . . . . . . . 11 setvar 𝑓
1211cv 1537 . . . . . . . . . 10 class 𝑓
13 cdg1 24661 . . . . . . . . . 10 class deg1
148, 12, 13co 7149 . . . . . . . . 9 class (𝑟 deg1 𝑓)
159cv 1537 . . . . . . . . 9 class 𝑛
16 cle 10674 . . . . . . . . 9 class
1714, 15, 16wbr 5052 . . . . . . . 8 wff (𝑟 deg1 𝑓) ≤ 𝑛
18 vd . . . . . . . . . . . . 13 setvar 𝑑
1918cv 1537 . . . . . . . . . . . 12 class 𝑑
2019ccnv 5541 . . . . . . . . . . 11 class 𝑑
21 cz 11978 . . . . . . . . . . . 12 class
22 cc0 10535 . . . . . . . . . . . . 13 class 0
2322csn 4550 . . . . . . . . . . . 12 class {0}
2421, 23cdif 3916 . . . . . . . . . . 11 class (ℤ ∖ {0})
2520, 24cima 5545 . . . . . . . . . 10 class (𝑑 “ (ℤ ∖ {0}))
26 cfz 12894 . . . . . . . . . . 11 class ...
2722, 15, 26co 7149 . . . . . . . . . 10 class (0...𝑛)
2825, 27wss 3919 . . . . . . . . 9 wff (𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛)
29 cco1 20814 . . . . . . . . . . 11 class coe1
3012, 29cfv 6343 . . . . . . . . . 10 class (coe1𝑓)
3130crn 5543 . . . . . . . . 9 class ran (coe1𝑓)
3228, 18, 31wral 3133 . . . . . . . 8 wff 𝑑 ∈ ran (coe1𝑓)(𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛)
3317, 32wa 399 . . . . . . 7 wff ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1𝑓)(𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))
34 cpl1 20813 . . . . . . . 8 class Poly1
358, 34cfv 6343 . . . . . . 7 class (Poly1𝑟)
3633, 11, 35crab 3137 . . . . . 6 class {𝑓 ∈ (Poly1𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1𝑓)(𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}
379, 10, 36cmpt 5132 . . . . 5 class (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1𝑓)(𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})
38 cpsl 32941 . . . . 5 class polySplitLim
398, 37, 38co 7149 . . . 4 class (𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1𝑓)(𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))
404, 7, 39csb 3866 . . 3 class (Qp‘𝑝) / 𝑟(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1𝑓)(𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))
412, 3, 40cmpt 5132 . 2 class (𝑝 ∈ ℙ ↦ (Qp‘𝑝) / 𝑟(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1𝑓)(𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})))
421, 41wceq 1538 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