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