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

Definition df-psl 23973
Description: Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring  r, a strict order on  r, and a sequence  p : NN --> ( ~P r  i^i  Fin ) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-psl  |- polySplitLim  =  (
r  e.  _V ,  p  e.  ( ( ~P ( Base `  r
)  i^i  Fin )  ^m  NN )  |->  [_ ( 1st  o.  seq  0 ( ( g  e.  _V ,  q  e.  _V  |->  [_ ( 1st `  g
)  /  e ]_ [_ ( 1st `  e
)  /  s ]_ [_ ( s splitFld  ran  (
x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g )  o.  ( 2nd `  f
) ) >. ) ,  ( p  u. 
{ <. 0 ,  <. <.
r ,  (/) >. ,  (  _I  |`  ( Base `  r ) ) >. >. } ) ) )  /  f ]_ (
( 1st  o.  (
f  shift  1 ) ) HomLim 
( 2nd  o.  f
) ) )
Distinct variable group:    e, f, g, p, q, r, s, x

Detailed syntax breakdown of Definition df-psl
StepHypRef Expression
1 cpsl 23965 . 2  class polySplitLim
2 vr . . 3  set  r
3 vp . . 3  set  p
4 cvv 2788 . . 3  class  _V
52cv 1622 . . . . . . 7  class  r
6 cbs 13148 . . . . . . 7  class  Base
75, 6cfv 5255 . . . . . 6  class  ( Base `  r )
87cpw 3625 . . . . 5  class  ~P ( Base `  r )
9 cfn 6863 . . . . 5  class  Fin
108, 9cin 3151 . . . 4  class  ( ~P ( Base `  r
)  i^i  Fin )
11 cn 9746 . . . 4  class  NN
12 cmap 6772 . . . 4  class  ^m
1310, 11, 12co 5858 . . 3  class  ( ( ~P ( Base `  r
)  i^i  Fin )  ^m  NN )
14 vf . . . 4  set  f
15 c1st 6120 . . . . 5  class  1st
16 vg . . . . . . 7  set  g
17 vq . . . . . . 7  set  q
18 ve . . . . . . . 8  set  e
1916cv 1622 . . . . . . . . 9  class  g
2019, 15cfv 5255 . . . . . . . 8  class  ( 1st `  g )
21 vs . . . . . . . . 9  set  s
2218cv 1622 . . . . . . . . . 10  class  e
2322, 15cfv 5255 . . . . . . . . 9  class  ( 1st `  e )
2421cv 1622 . . . . . . . . . . 11  class  s
25 vx . . . . . . . . . . . . 13  set  x
2617cv 1622 . . . . . . . . . . . . 13  class  q
2725cv 1622 . . . . . . . . . . . . . 14  class  x
28 c2nd 6121 . . . . . . . . . . . . . . 15  class  2nd
2919, 28cfv 5255 . . . . . . . . . . . . . 14  class  ( 2nd `  g )
3027, 29ccom 4693 . . . . . . . . . . . . 13  class  ( x  o.  ( 2nd `  g
) )
3125, 26, 30cmpt 4077 . . . . . . . . . . . 12  class  ( x  e.  q  |->  ( x  o.  ( 2nd `  g
) ) )
3231crn 4690 . . . . . . . . . . 11  class  ran  (
x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) )
33 csf 23964 . . . . . . . . . . 11  class splitFld
3424, 32, 33co 5858 . . . . . . . . . 10  class  ( s splitFld  ran  ( x  e.  q 
|->  ( x  o.  ( 2nd `  g ) ) ) )
3514cv 1622 . . . . . . . . . . 11  class  f
3635, 28cfv 5255 . . . . . . . . . . . 12  class  ( 2nd `  f )
3729, 36ccom 4693 . . . . . . . . . . 11  class  ( ( 2nd `  g )  o.  ( 2nd `  f
) )
3835, 37cop 3643 . . . . . . . . . 10  class  <. f ,  ( ( 2nd `  g )  o.  ( 2nd `  f ) )
>.
3914, 34, 38csb 3081 . . . . . . . . 9  class  [_ (
s splitFld  ran  ( x  e.  q  |->  ( x  o.  ( 2nd `  g
) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g )  o.  ( 2nd `  f ) )
>.
4021, 23, 39csb 3081 . . . . . . . 8  class  [_ ( 1st `  e )  / 
s ]_ [_ ( s splitFld  ran  ( x  e.  q 
|->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g
)  o.  ( 2nd `  f ) ) >.
4118, 20, 40csb 3081 . . . . . . 7  class  [_ ( 1st `  g )  / 
e ]_ [_ ( 1st `  e )  /  s ]_ [_ ( s splitFld  ran  ( x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g
)  o.  ( 2nd `  f ) ) >.
4216, 17, 4, 4, 41cmpt2 5860 . . . . . 6  class  ( g  e.  _V ,  q  e.  _V  |->  [_ ( 1st `  g )  / 
e ]_ [_ ( 1st `  e )  /  s ]_ [_ ( s splitFld  ran  ( x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g
)  o.  ( 2nd `  f ) ) >.
)
433cv 1622 . . . . . . 7  class  p
44 cc0 8737 . . . . . . . . 9  class  0
45 c0 3455 . . . . . . . . . . 11  class  (/)
465, 45cop 3643 . . . . . . . . . 10  class  <. r ,  (/) >.
47 cid 4304 . . . . . . . . . . 11  class  _I
4847, 7cres 4691 . . . . . . . . . 10  class  (  _I  |`  ( Base `  r
) )
4946, 48cop 3643 . . . . . . . . 9  class  <. <. r ,  (/) >. ,  (  _I  |`  ( Base `  r
) ) >.
5044, 49cop 3643 . . . . . . . 8  class  <. 0 ,  <. <. r ,  (/) >. ,  (  _I  |`  ( Base `  r ) )
>. >.
5150csn 3640 . . . . . . 7  class  { <. 0 ,  <. <. r ,  (/) >. ,  (  _I  |`  ( Base `  r
) ) >. >. }
5243, 51cun 3150 . . . . . 6  class  ( p  u.  { <. 0 ,  <. <. r ,  (/) >. ,  (  _I  |`  ( Base `  r ) )
>. >. } )
5342, 52, 44cseq 11046 . . . . 5  class  seq  0
( ( g  e. 
_V ,  q  e. 
_V  |->  [_ ( 1st `  g
)  /  e ]_ [_ ( 1st `  e
)  /  s ]_ [_ ( s splitFld  ran  (
x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g )  o.  ( 2nd `  f
) ) >. ) ,  ( p  u. 
{ <. 0 ,  <. <.
r ,  (/) >. ,  (  _I  |`  ( Base `  r ) ) >. >. } ) )
5415, 53ccom 4693 . . . 4  class  ( 1st 
o.  seq  0 ( ( g  e.  _V ,  q  e.  _V  |->  [_ ( 1st `  g
)  /  e ]_ [_ ( 1st `  e
)  /  s ]_ [_ ( s splitFld  ran  (
x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g )  o.  ( 2nd `  f
) ) >. ) ,  ( p  u. 
{ <. 0 ,  <. <.
r ,  (/) >. ,  (  _I  |`  ( Base `  r ) ) >. >. } ) ) )
55 c1 8738 . . . . . . 7  class  1
56 cshi 11561 . . . . . . 7  class  shift
5735, 55, 56co 5858 . . . . . 6  class  ( f 
shift  1 )
5815, 57ccom 4693 . . . . 5  class  ( 1st 
o.  ( f  shift  1 ) )
5928, 35ccom 4693 . . . . 5  class  ( 2nd 
o.  f )
60 chlim 23961 . . . . 5  class HomLim
6158, 59, 60co 5858 . . . 4  class  ( ( 1st  o.  ( f 
shift  1 ) ) HomLim  ( 2nd  o.  f ) )
6214, 54, 61csb 3081 . . 3  class  [_ ( 1st  o.  seq  0 ( ( g  e.  _V ,  q  e.  _V  |->  [_ ( 1st `  g
)  /  e ]_ [_ ( 1st `  e
)  /  s ]_ [_ ( s splitFld  ran  (
x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g )  o.  ( 2nd `  f
) ) >. ) ,  ( p  u. 
{ <. 0 ,  <. <.
r ,  (/) >. ,  (  _I  |`  ( Base `  r ) ) >. >. } ) ) )  /  f ]_ (
( 1st  o.  (
f  shift  1 ) ) HomLim 
( 2nd  o.  f
) )
632, 3, 4, 13, 62cmpt2 5860 . 2  class  ( r  e.  _V ,  p  e.  ( ( ~P ( Base `  r )  i^i 
Fin )  ^m  NN )  |->  [_ ( 1st  o.  seq  0 ( ( g  e.  _V ,  q  e.  _V  |->  [_ ( 1st `  g )  / 
e ]_ [_ ( 1st `  e )  /  s ]_ [_ ( s splitFld  ran  ( x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g
)  o.  ( 2nd `  f ) ) >.
) ,  ( p  u.  { <. 0 ,  <. <. r ,  (/) >. ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) )  /  f ]_ ( ( 1st  o.  ( f  shift  1 ) ) HomLim  ( 2nd  o.  f ) ) )
641, 63wceq 1623 1  wff polySplitLim  =  (
r  e.  _V ,  p  e.  ( ( ~P ( Base `  r
)  i^i  Fin )  ^m  NN )  |->  [_ ( 1st  o.  seq  0 ( ( g  e.  _V ,  q  e.  _V  |->  [_ ( 1st `  g
)  /  e ]_ [_ ( 1st `  e
)  /  s ]_ [_ ( s splitFld  ran  (
x  e.  q  |->  ( x  o.  ( 2nd `  g ) ) ) )  /  f ]_ <. f ,  ( ( 2nd `  g )  o.  ( 2nd `  f
) ) >. ) ,  ( p  u. 
{ <. 0 ,  <. <.
r ,  (/) >. ,  (  _I  |`  ( Base `  r ) ) >. >. } ) ) )  /  f ]_ (
( 1st  o.  (
f  shift  1 ) ) HomLim 
( 2nd  o.  f
) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator