Definition df-qpa 35609

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

Step	Hyp	Ref	Expression
1		cqpa 35600	. 2 class _Qp
2		vp	. . 3 setvar 𝑝
3		cprime 16691	. . 3 class ℙ
4		vr	. . . 4 setvar 𝑟
5	2	cv 1538	. . . . 5 class 𝑝
6		cqp 35598	. . . . 5 class Qp
7	5, 6	cfv 6542	. . . 4 class (Qp‘𝑝)
8	4	cv 1538	. . . . 5 class 𝑟
9		vn	. . . . . 6 setvar 𝑛
10		cn 12249	. . . . . 6 class ℕ
11		vf	. . . . . . . . . . 11 setvar 𝑓
12	11	cv 1538	. . . . . . . . . 10 class 𝑓
13		cdg1 26048	. . . . . . . . . 10 class deg1
14	8, 12, 13	co 7414	. . . . . . . . 9 class (𝑟deg1𝑓)
15	9	cv 1538	. . . . . . . . 9 class 𝑛
16		cle 11279	. . . . . . . . 9 class ≤
17	14, 15, 16	wbr 5125	. . . . . . . 8 wff (𝑟deg1𝑓) ≤ 𝑛
18		vd	. . . . . . . . . . . . 13 setvar 𝑑
19	18	cv 1538	. . . . . . . . . . . 12 class 𝑑
20	19	ccnv 5666	. . . . . . . . . . 11 class ◡𝑑
21		cz 12597	. . . . . . . . . . . 12 class ℤ
22		cc0 11138	. . . . . . . . . . . . 13 class 0
23	22	csn 4608	. . . . . . . . . . . 12 class {0}
24	21, 23	cdif 3930	. . . . . . . . . . 11 class (ℤ ∖ {0})
25	20, 24	cima 5670	. . . . . . . . . 10 class (◡𝑑 “ (ℤ ∖ {0}))
26		cfz 13530	. . . . . . . . . . 11 class ...
27	22, 15, 26	co 7414	. . . . . . . . . 10 class (0...𝑛)
28	25, 27	wss 3933	. . . . . . . . 9 wff (◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛)
29		cco1 22146	. . . . . . . . . . 11 class coe1
30	12, 29	cfv 6542	. . . . . . . . . 10 class (coe1‘𝑓)
31	30	crn 5668	. . . . . . . . 9 class ran (coe1‘𝑓)
32	28, 18, 31	wral 3050	. . . . . . . 8 wff ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛)
33	17, 32	wa 395	. . . . . . 7 wff ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))
34		cpl1 22145	. . . . . . . 8 class Poly1
35	8, 34	cfv 6542	. . . . . . 7 class (Poly1‘𝑟)
36	33, 11, 35	crab 3420	. . . . . 6 class {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}
37	9, 10, 36	cmpt 5207	. . . . 5 class (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})
38		cpsl 35579	. . . . 5 class polySplitLim
39	8, 37, 38	co 7414	. . . 4 class (𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))
40	4, 7, 39	csb 3881	. . 3 class ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))
41	2, 3, 40	cmpt 5207	. 2 class (𝑝 ∈ ℙ ↦ ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})))
42	1, 41	wceq 1539	1 wff _Qp = (𝑝 ∈ ℙ ↦ ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})))

This definition is referenced by: (None)