Definition df-qpa 33621

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 33612	. 2 class _Qp
2		vp	. . 3 setvar 𝑝
3		cprime 16376	. . 3 class ℙ
4		vr	. . . 4 setvar 𝑟
5	2	cv 1538	. . . . 5 class 𝑝
6		cqp 33610	. . . . 5 class Qp
7	5, 6	cfv 6433	. . . 4 class (Qp‘𝑝)
8	4	cv 1538	. . . . 5 class 𝑟
9		vn	. . . . . 6 setvar 𝑛
10		cn 11973	. . . . . 6 class ℕ
11		vf	. . . . . . . . . . 11 setvar 𝑓
12	11	cv 1538	. . . . . . . . . 10 class 𝑓
13		cdg1 25216	. . . . . . . . . 10 class deg1
14	8, 12, 13	co 7275	. . . . . . . . 9 class (𝑟 deg1 𝑓)
15	9	cv 1538	. . . . . . . . 9 class 𝑛
16		cle 11010	. . . . . . . . 9 class ≤
17	14, 15, 16	wbr 5074	. . . . . . . 8 wff (𝑟 deg1 𝑓) ≤ 𝑛
18		vd	. . . . . . . . . . . . 13 setvar 𝑑
19	18	cv 1538	. . . . . . . . . . . 12 class 𝑑
20	19	ccnv 5588	. . . . . . . . . . 11 class ◡𝑑
21		cz 12319	. . . . . . . . . . . 12 class ℤ
22		cc0 10871	. . . . . . . . . . . . 13 class 0
23	22	csn 4561	. . . . . . . . . . . 12 class {0}
24	21, 23	cdif 3884	. . . . . . . . . . 11 class (ℤ ∖ {0})
25	20, 24	cima 5592	. . . . . . . . . 10 class (◡𝑑 “ (ℤ ∖ {0}))
26		cfz 13239	. . . . . . . . . . 11 class ...
27	22, 15, 26	co 7275	. . . . . . . . . 10 class (0...𝑛)
28	25, 27	wss 3887	. . . . . . . . 9 wff (◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛)
29		cco1 21349	. . . . . . . . . . 11 class coe1
30	12, 29	cfv 6433	. . . . . . . . . 10 class (coe1‘𝑓)
31	30	crn 5590	. . . . . . . . 9 class ran (coe1‘𝑓)
32	28, 18, 31	wral 3064	. . . . . . . 8 wff ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛)
33	17, 32	wa 396	. . . . . . 7 wff ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))
34		cpl1 21348	. . . . . . . 8 class Poly1
35	8, 34	cfv 6433	. . . . . . 7 class (Poly1‘𝑟)
36	33, 11, 35	crab 3068	. . . . . 6 class {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}
37	9, 10, 36	cmpt 5157	. . . . 5 class (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})
38		cpsl 33596	. . . . 5 class polySplitLim
39	8, 37, 38	co 7275	. . . 4 class (𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))
40	4, 7, 39	csb 3832	. . 3 class ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))
41	2, 3, 40	cmpt 5157	. 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)