Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sfl1 Unicode version

Definition df-sfl1 23971
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.)

Assertion
Ref Expression
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 ) ) ) ) ) )
Distinct variable group:    f, b, g, h, j, m, p, r, s, t

Detailed syntax breakdown of Definition df-sfl1
StepHypRef Expression
1 csf1 23963 . 2  class splitFld1
2 vr . . 3  set  r
3 vj . . 3  set  j
4 cvv 2788 . . 3  class  _V
5 vp . . . 4  set  p
62cv 1622 . . . . 5  class  r
7 cpl1 16252 . . . . 5  class Poly1
86, 7cfv 5255 . . . 4  class  (Poly1 `  r
)
9 c1 8738 . . . . . . 7  class  1
105cv 1622 . . . . . . . 8  class  p
11 cdg1 19440 . . . . . . . 8  class deg1
126, 10, 11co 5858 . . . . . . 7  class  ( r deg1  p )
13 cfz 10782 . . . . . . 7  class  ...
149, 12, 13co 5858 . . . . . 6  class  ( 1 ... ( r deg1  p ) )
15 ccrd 7568 . . . . . 6  class  card
1614, 15cfv 5255 . . . . 5  class  ( card `  ( 1 ... (
r deg1  p ) ) )
17 vs . . . . . . 7  set  s
18 vf . . . . . . 7  set  f
19 vm . . . . . . . 8  set  m
2017cv 1622 . . . . . . . . 9  class  s
21 cmpl 16089 . . . . . . . . 9  class mPoly
2220, 21cfv 5255 . . . . . . . 8  class  ( mPoly  `  s
)
23 vb . . . . . . . . 9  set  b
24 vg . . . . . . . . . . . . 13  set  g
2524cv 1622 . . . . . . . . . . . 12  class  g
2618cv 1622 . . . . . . . . . . . . 13  class  f
2710, 26ccom 4693 . . . . . . . . . . . 12  class  ( p  o.  f )
2819cv 1622 . . . . . . . . . . . . 13  class  m
29 cdsr 15420 . . . . . . . . . . . . 13  class  ||r
3028, 29cfv 5255 . . . . . . . . . . . 12  class  ( ||r `  m
)
3125, 27, 30wbr 4023 . . . . . . . . . . 11  wff  g (
||r `  m ) ( p  o.  f )
3220, 25, 11co 5858 . . . . . . . . . . . 12  class  ( s deg1  g )
33 clt 8867 . . . . . . . . . . . 12  class  <
349, 32, 33wbr 4023 . . . . . . . . . . 11  wff  1  <  ( s deg1  g )
3531, 34wa 358 . . . . . . . . . 10  wff  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) )
36 cmn1 19511 . . . . . . . . . . . 12  class Monic1p
3720, 36cfv 5255 . . . . . . . . . . 11  class  (Monic1p `  s
)
38 cir 15422 . . . . . . . . . . . 12  class Irred
3928, 38cfv 5255 . . . . . . . . . . 11  class  (Irred `  m )
4037, 39cin 3151 . . . . . . . . . 10  class  ( (Monic1p `  s )  i^i  (Irred `  m ) )
4135, 24, 40crab 2547 . . . . . . . . 9  class  { g  e.  ( (Monic1p `  s
)  i^i  (Irred `  m
) )  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }
42 c0g 13400 . . . . . . . . . . . . 13  class  0g
4328, 42cfv 5255 . . . . . . . . . . . 12  class  ( 0g
`  m )
4427, 43wceq 1623 . . . . . . . . . . 11  wff  ( p  o.  f )  =  ( 0g `  m
)
4523cv 1622 . . . . . . . . . . . 12  class  b
46 c0 3455 . . . . . . . . . . . 12  class  (/)
4745, 46wceq 1623 . . . . . . . . . . 11  wff  b  =  (/)
4844, 47wo 357 . . . . . . . . . 10  wff  ( ( p  o.  f )  =  ( 0g `  m )  \/  b  =  (/) )
4920, 26cop 3643 . . . . . . . . . 10  class  <. s ,  f >.
50 vh . . . . . . . . . . 11  set  h
51 cglb 14077 . . . . . . . . . . . 12  class  glb
5245, 51cfv 5255 . . . . . . . . . . 11  class  ( glb `  b )
53 vt . . . . . . . . . . . 12  set  t
5450cv 1622 . . . . . . . . . . . . 13  class  h
55 cpfl 23962 . . . . . . . . . . . . 13  class polyFld
5620, 54, 55co 5858 . . . . . . . . . . . 12  class  ( s polyFld  h )
5753cv 1622 . . . . . . . . . . . . . 14  class  t
58 c1st 6120 . . . . . . . . . . . . . 14  class  1st
5957, 58cfv 5255 . . . . . . . . . . . . 13  class  ( 1st `  t )
60 c2nd 6121 . . . . . . . . . . . . . . 15  class  2nd
6157, 60cfv 5255 . . . . . . . . . . . . . 14  class  ( 2nd `  t )
6226, 61ccom 4693 . . . . . . . . . . . . 13  class  ( f  o.  ( 2nd `  t
) )
6359, 62cop 3643 . . . . . . . . . . . 12  class  <. ( 1st `  t ) ,  ( f  o.  ( 2nd `  t ) )
>.
6453, 56, 63csb 3081 . . . . . . . . . . 11  class  [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >.
6550, 52, 64csb 3081 . . . . . . . . . 10  class  [_ ( glb `  b )  /  h ]_ [_ ( s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >.
6648, 49, 65cif 3565 . . . . . . . . 9  class  if ( ( ( p  o.  f )  =  ( 0g `  m )  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ ( s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
6723, 41, 66csb 3081 . . . . . . . 8  class  [_ {
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
) ) >. )
6819, 22, 67csb 3081 . . . . . . 7  class  [_ ( 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
) ) >. )
6917, 18, 4, 4, 68cmpt2 5860 . . . . . 6  class  ( 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
) ) >. )
)
703cv 1622 . . . . . 6  class  j
7169, 70crdg 6422 . . . . 5  class  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 )
7216, 71cfv 5255 . . . 4  class  ( 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 ) ) ) )
735, 8, 72cmpt 4077 . . 3  class  ( 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 ) ) ) ) )
742, 3, 4, 4, 73cmpt2 5860 . 2  class  ( 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 ) ) ) ) ) )
751, 74wceq 1623 1  wff 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 ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator