Definition df-sfl1

Description: Temporary construction for the splitting field of a polynomial. The inputs are a field r and a polynomial p that we want to split, along with a tuple j in the same format as the output. The output is a tuple <. S , F >. where S is the splitting field and F is an injective homomorphism from the original field r .

The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-sfl1	|- splitFld1 = ( r e. _V , j e. _V |-> ( p e. ( Poly1 ` r ) |-> ( rec ( ( s e. _V , f e. _V |-> [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j ) ` ( card ` ( 1 ... ( r deg1 p ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csf1	|- splitFld1
1		vr	|- r
2		cvv	|- _V
3		vj	|- j
4		vp	|- p
5		cpl1	|- Poly1
6	1	cv	|- r
7	6 5	cfv	|- ( Poly1 ` r )
8		vs	|- s
9		vf	|- f
10	8	cv	|- s
11	10 5	cfv	|- ( Poly1 ` s )
12		vm	|- m
13		vg	|- g
14		cmn1	|- Monic1p
15	10 14	cfv	|- ( Monic1p ` s )
16		cir	|- Irred
17	12	cv	|- m
18	17 16	cfv	|- ( Irred ` m )
19	15 18	cin	|- ( ( Monic1p ` s ) i^i ( Irred ` m ) )
20	13	cv	|- g
21		cdsr	|- ||r
22	17 21	cfv	|- ( ||r ` m )
23	4	cv	|- p
24	9	cv	|- f
25	23 24	ccom	|- ( p o. f )
26	20 25 22	wbr	|- g ( ||r ` m ) ( p o. f )
27		c1	|- 1
28		clt	|- <
29		cdg1	|- deg1
30	10 20 29	co	|- ( s deg1 g )
31	27 30 28	wbr	|- 1 < ( s deg1 g )
32	26 31	wa	|- ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) )
33	32 13 19	crab	|- { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) }
34		vb	|- b
35		c0g	|- 0g
36	17 35	cfv	|- ( 0g ` m )
37	25 36	wceq	|- ( p o. f ) = ( 0g ` m )
38	34	cv	|- b
39		c0	|- (/)
40	38 39	wceq	|- b = (/)
41	37 40	wo	|- ( ( p o. f ) = ( 0g ` m ) \/ b = (/) )
42	10 24	cop	|- <. s , f >.
43		cglb	|- glb
44	38 43	cfv	|- ( glb ` b )
45		vh	|- h
46		cpfl	|- polyFld
47	45	cv	|- h
48	10 47 46	co	|- ( s polyFld h )
49		vt	|- t
50		c1st	|- 1st
51	49	cv	|- t
52	51 50	cfv	|- ( 1st ` t )
53		c2nd	|- 2nd
54	51 53	cfv	|- ( 2nd ` t )
55	24 54	ccom	|- ( f o. ( 2nd ` t ) )
56	52 55	cop	|- <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >.
57	49 48 56	csb	|- [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >.
58	45 44 57	csb	|- [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >.
59	41 42 58	cif	|- if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. )
60	34 33 59	csb	|- [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. )
61	12 11 60	csb	|- [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. )
62	8 9 2 2 61	cmpo	|- ( s e. _V , f e. _V |-> [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) )
63	3	cv	|- j
64	62 63	crdg	|- rec ( ( s e. _V , f e. _V |-> [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j )
65		ccrd	|- card
66		cfz	|- ...
67	6 23 29	co	|- ( r deg1 p )
68	27 67 66	co	|- ( 1 ... ( r deg1 p ) )
69	68 65	cfv	|- ( card ` ( 1 ... ( r deg1 p ) ) )
70	69 64	cfv	|- ( rec ( ( s e. _V , f e. _V |-> [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j ) ` ( card ` ( 1 ... ( r deg1 p ) ) ) )
71	4 7 70	cmpt	|- ( p e. ( Poly1 ` r ) |-> ( rec ( ( s e. _V , f e. _V |-> [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j ) ` ( card ` ( 1 ... ( r deg1 p ) ) ) ) )
72	1 3 2 2 71	cmpo	|- ( r e. _V , j e. _V |-> ( p e. ( Poly1 ` r ) |-> ( rec ( ( s e. _V , f e. _V |-> [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j ) ` ( card ` ( 1 ... ( r deg1 p ) ) ) ) ) )
73	0 72	wceq	|- splitFld1 = ( r e. _V , j e. _V |-> ( p e. ( Poly1 ` r ) |-> ( rec ( ( s e. _V , f e. _V |-> [_ ( Poly1 ` s ) / m ]_ [_ { g e. ( ( Monic1p ` s ) i^i ( Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j ) ` ( card ` ( 1 ... ( r deg1 p ) ) ) ) ) )