Definition df-qpa

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)

	Ref	Expression
Assertion	df-qpa	⊢ _Qp = ( 𝑝 ∈ ℙ ↦ ⦋ ( Qp ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { 𝑓 ∈ ( Poly1 ‘ 𝑟 ) ∣ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqpa	⊢ _Qp
1		vp	⊢ 𝑝
2		cprime	⊢ ℙ
3		cqp	⊢ Qp
4	1	cv	⊢ 𝑝
5	4 3	cfv	⊢ ( Qp ‘ 𝑝 )
6		vr	⊢ 𝑟
7	6	cv	⊢ 𝑟
8		cpsl	⊢ polySplitLim
9		vn	⊢ 𝑛
10		cn	⊢ ℕ
11		vf	⊢ 𝑓
12		cpl1	⊢ Poly1
13	7 12	cfv	⊢ ( Poly1 ‘ 𝑟 )
14		cdg1	⊢ deg1
15	11	cv	⊢ 𝑓
16	7 15 14	co	⊢ ( 𝑟 deg1 𝑓 )
17		cle	⊢ ≤
18	9	cv	⊢ 𝑛
19	16 18 17	wbr	⊢ ( 𝑟 deg1 𝑓 ) ≤ 𝑛
20		vd	⊢ 𝑑
21		cco1	⊢ coe1
22	15 21	cfv	⊢ ( coe1 ‘ 𝑓 )
23	22	crn	⊢ ran ( coe1 ‘ 𝑓 )
24	20	cv	⊢ 𝑑
25	24	ccnv	⊢ ◡ 𝑑
26		cz	⊢ ℤ
27		cc0	⊢ 0
28	27	csn	⊢ { 0 }
29	26 28	cdif	⊢ ( ℤ ∖ { 0 } )
30	25 29	cima	⊢ ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) )
31		cfz	⊢ ...
32	27 18 31	co	⊢ ( 0 ... 𝑛 )
33	30 32	wss	⊢ ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 )
34	33 20 23	wral	⊢ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 )
35	19 34	wa	⊢ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) )
36	35 11 13	crab	⊢ { 𝑓 ∈ ( Poly1 ‘ 𝑟 ) ∣ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) ) }
37	9 10 36	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ { 𝑓 ∈ ( Poly1 ‘ 𝑟 ) ∣ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) ) } )
38	7 37 8	co	⊢ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { 𝑓 ∈ ( Poly1 ‘ 𝑟 ) ∣ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) ) } ) )
39	6 5 38	csb	⊢ ⦋ ( Qp ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { 𝑓 ∈ ( Poly1 ‘ 𝑟 ) ∣ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) ) } ) )
40	1 2 39	cmpt	⊢ ( 𝑝 ∈ ℙ ↦ ⦋ ( Qp ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { 𝑓 ∈ ( Poly1 ‘ 𝑟 ) ∣ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) ) } ) ) )
41	0 40	wceq	⊢ _Qp = ( 𝑝 ∈ ℙ ↦ ⦋ ( Qp ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { 𝑓 ∈ ( Poly1 ‘ 𝑟 ) ∣ ( ( 𝑟 deg1 𝑓 ) ≤ 𝑛 ∧ ∀ 𝑑 ∈ ran ( coe1 ‘ 𝑓 ) ( ◡ 𝑑 “ ( ℤ ∖ { 0 } ) ) ⊆ ( 0 ... 𝑛 ) ) } ) ) )