:: Algebraic Extensions
:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller
::
:: Received March 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

definition

let L1, L2 be doubleLoopStr ;

pred L1 == L2 means :: FIELD_7:def 1
doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #);

reflexivity
for L1 being doubleLoopStr holds doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) ;
symmetry
for L1, L2 being doubleLoopStr st doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #) holds
doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #) = doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) ;

end;

:: deftheorem defines == FIELD_7:def 1 :
for L1, L2 being doubleLoopStr holds
( L1 == L2 iff doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #) );

theorem :: FIELD_7:1

for R, S being Ring holds
( R == S iff ex f being Function of R,S st
( f = id R & f is isomorphism ) )

proof end;

theorem :: FIELD_7:2

for R, S being strict Ring holds
( R == S iff R = S ) ;

Th0: for F1, F2 being Field st F1 is Subfield of F2 & F2 is Subfield of F1 holds
F1 == F2

proof end;

definition

let F1, F2 be Field;

redefine pred F1 == F2 means :: FIELD_7:def 2
( F1 is Subfield of F2 & F2 is Subfield of F1 );

correctness
compatibility
( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) );

proof end;

end;

:: deftheorem defines == FIELD_7:def 2 :
for F1, F2 being Field holds
( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) );

theorem Th1: :: FIELD_7:3

for F being Field
for E being FieldExtension of F
for T being Subset of E holds
( FAdj (F,T) == F iff T is Subset of F )

proof end;

theorem str12: :: FIELD_7:4

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
VecSp (E1,F) = VecSp (E2,F)

proof end;

theorem str11: :: FIELD_7:5

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
deg (E1,F) = deg (E2,F)

proof end;

registration

let F be Field;
let E be FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() E -homomorphic Polynom-Ring F -homomorphic factorial F -extending for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ is E -homomorphic

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring F -homomorphic factorial F -extending E -monomorphic for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ is E -monomorphic

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring F -homomorphic factorial F -extending E -isomorphic for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ is E -isomorphic

proof end;

end;

definition

let R be Ring;
let a, b be Element of R;
:: original: {
redefine func {a,b} -> Subset of R;
coherence
{a,b} is Subset of R

proof end;

end;

definition

let F be Field;
let V be VectSp of F;
let a be Element of V;
:: original: {
redefine func {a} -> Subset of V;
coherence
{a} is Subset of V

proof end;

end;

definition

let F be Field;
let V be VectSp of F;
let a, b be Element of V;
:: original: {
redefine func {a,b} -> Subset of V;
coherence
{a,b} is Subset of V

proof end;

end;

registration

let F be Field;
let V be VectSp of F;

cluster V263(F,V) -> linearly-independent for Element of bool the carrier of V;

coherence
for b₁ being Basis of V holds b₁ is linearly-independent by VECTSP_7:def 3;

end;

theorem ZMODUL033: :: FIELD_7:6

for F being Field
for V being VectSp of F
for X being Subset of V holds
( X is linearly-independent iff for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 )

proof end;

registration

let F be Field;
let E be FieldExtension of F;

cluster V263(F, VecSp (E,F)) -> non empty for Element of bool the carrier of (VecSp (E,F));

coherence
for b₁ being Basis of (VecSp (E,F)) holds not b₁ is empty

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;

cluster deg (E,F) -> non zero ;

coherence
not deg (E,F) is zero

proof end;

end;

registration

let F be Field;
let E be F -finite FieldExtension of F;

cluster V263(F, VecSp (E,F)) -> finite for Element of bool the carrier of (VecSp (E,F));

coherence
for b₁ being Basis of (VecSp (E,F)) holds b₁ is finite

proof end;

end;

theorem quah1: :: FIELD_7:7

for F being Field
for E being FieldExtension of F holds
( deg (E,F) = 1 iff the carrier of E = the carrier of F )

proof end;

theorem str1a: :: FIELD_7:8

for F being Field
for E being FieldExtension of F holds
( deg (E,F) = 1 iff E == F )

proof end;

theorem quah2: :: FIELD_7:9

for F being Field
for E being FieldExtension of F holds
( deg (E,F) = 1 iff {(1. E)} is Basis of (VecSp (E,F)) )

proof end;

registration

let F be Field;
let E be FieldExtension of F;

cluster non empty finite linearly-independent for Element of bool the carrier of (VecSp (E,F));

existence
ex b₁ being Subset of (VecSp (E,F)) st
( not b₁ is empty & b₁ is finite & b₁ is linearly-independent )

proof end;

end;

theorem ext0: :: FIELD_7:10

for F being Field
for E being FieldExtension of F
for T1, T2 being Subset of E st T1 c= T2 holds
FAdj (F,T1) is Subfield of FAdj (F,T2)

proof end;

definition

let F be Field;
let p be Polynomial of F;

func Coeff p -> Subset of F equals :: FIELD_7:def 3
{ (p . i) where i is Element of NAT : p . i <> 0. F } ;

coherence
{ (p . i) where i is Element of NAT : p . i <> 0. F } is Subset of F

proof end;

end;

:: deftheorem defines Coeff FIELD_7:def 3 :
for F being Field
for p being Polynomial of F holds Coeff p = { (p . i) where i is Element of NAT : p . i <> 0. F } ;

registration

let F be Field;
let p be Polynomial of F;

cluster Coeff p -> finite ;

coherence
Coeff p is finite

proof end;

end;

theorem cof1: :: FIELD_7:11

for F being Field
for E being FieldExtension of F
for p being Polynomial of E st Coeff p c= the carrier of F holds
p is Polynomial of F

proof end;

theorem cof2: :: FIELD_7:12

for F being Field
for E being FieldExtension of F
for p being non zero Polynomial of E st Coeff p c= the carrier of F holds
p is non zero Polynomial of F

proof end;

theorem m4: :: FIELD_7:13

for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
Roots (S,p) = Roots q

proof end;

registration

let R be domRing;
let p be non zero Element of the carrier of (Polynom-Ring R);

cluster Roots p -> finite ;

coherence
Roots p is finite ;

end;

registration

let R be domRing;
let S be domRingExtension of R;
let p be non zero Element of the carrier of (Polynom-Ring R);

cluster Roots (S,p) -> finite ;

coherence
Roots (S,p) is finite

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring E -homomorphic factorial F -extending E -extending for doubleLoopStr ;

existence
ex b₁ being FieldExtension of E st b₁ is F -extending

proof end;

end;

registration

let F be Field;
let E be F -finite FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring E -homomorphic factorial F -extending E -extending F -finite for doubleLoopStr ;

existence
ex b₁ being F -extending FieldExtension of F st b₁ is F -finite

proof end;

end;

registration

let F be Field;
let E be F -finite FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring E -homomorphic factorial F -extending E -extending E -finite for doubleLoopStr ;

existence
ex b₁ being F -extending FieldExtension of F st b₁ is E -finite

proof end;

end;

theorem lemma7a: :: FIELD_7:14

for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for U being b₃ -extending FieldExtension of F
for a being Element of E
for b being Element of U st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)

proof end;

theorem lemma7b: :: FIELD_7:15

for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
for U being b₃ -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)

proof end;

definition

let R be Ring;
let S be RingExtension of R;
let a be Element of R;

func @ (a,S) -> Element of S equals :: FIELD_7:def 4
a;

coherence
a is Element of S

proof end;

end;

:: deftheorem defines @ FIELD_7:def 4 :
for R being Ring
for S being RingExtension of R
for a being Element of R holds @ (a,S) = a;

definition

let R be Ring;
let S be RingExtension of R;
let a be Element of S;

attr a is R -membered means :defmem: :: FIELD_7:def 5
a in the carrier of R;

end;

:: deftheorem defmem defines -membered FIELD_7:def 5 :
for R being Ring
for S being RingExtension of R
for a being Element of S holds
( a is R -membered iff a in the carrier of R );

registration

let R be Ring;
let S be RingExtension of R;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable R -membered for Element of the carrier of S;

existence
ex b₁ being Element of S st b₁ is R -membered

proof end;

end;

definition

let R be Ring;
let S be RingExtension of R;
let a be Element of S;
assume AS: a is R -membered ;

func @ (R,a) -> Element of R equals :defred: :: FIELD_7:def 6
a;

coherence
a is Element of R by AS;

end;

:: deftheorem defred defines @ FIELD_7:def 6 :
for R being Ring
for S being RingExtension of R
for a being Element of S st a is R -membered holds
@ (R,a) = a;

registration

let R be Ring;
let S be RingExtension of R;
let a be R -membered Element of S;

reduce @ (R,a) to a;

reducibility
@ (R,a) = a by defred;

end;

registration

let F be Field;
let E be FieldExtension of F;

cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable V278(E) F -algebraic for Element of the carrier of E;

existence
ex b₁ being Element of E st
( not b₁ is zero & b₁ is F -algebraic )

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let a be Element of F;

cluster @ (a,E) -> F -algebraic ;

coherence
@ (a,E) is F -algebraic

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let K be E -extending FieldExtension of F;
let a be F -algebraic Element of E;

cluster @ (a,K) -> F -algebraic ;

coherence
@ (a,K) is F -algebraic

proof end;

end;

help1: for R being domRing
for n being Element of NAT holds (<%(0. R),(1. R)%> `^ n) . n = 1. R

proof end;

help2: for R being domRing
for n, i being Element of NAT st i <> n holds
(<%(0. R),(1. R)%> `^ n) . i = 0. R

proof end;

theorem sp0: :: FIELD_7:16

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for l being Linear_Combination of VecSp (K,F) holds l is Linear_Combination of VecSp (K,E)

proof end;

theorem sp1: :: FIELD_7:17

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for BE being Subset of (VecSp (K,E))
for BF being Subset of (VecSp (K,F)) st BF c= BE holds
for l being Linear_Combination of BF holds l is Linear_Combination of BE

proof end;

theorem sp2: :: FIELD_7:18

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for BE being finite Subset of (VecSp (K,E))
for BF being finite Subset of (VecSp (K,F))
for l1 being Linear_Combination of BF
for l2 being Linear_Combination of BE st l1 = l2 & BF c= BE holds
Sum l1 = Sum l2

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be Subset of (VecSp (E,F));
let BK be Subset of (VecSp (K,E));

func Base (BE,BK) -> Subset of (VecSp (K,F)) equals :: FIELD_7:def 7
{ (a * b) where a, b is Element of K : ( a in BE & b in BK ) } ;

coherence
{ (a * b) where a, b is Element of K : ( a in BE & b in BK ) } is Subset of (VecSp (K,F))

proof end;

end;

:: deftheorem defines Base FIELD_7:def 7 :
for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being Subset of (VecSp (E,F))
for BK being Subset of (VecSp (K,E)) holds Base (BE,BK) = { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } ;

registration

let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty Subset of (VecSp (E,F));
let BK be non empty Subset of (VecSp (K,E));

cluster Base (BE,BK) -> non empty ;

coherence
not Base (BE,BK) is empty

proof end;

end;

BE0: for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being linearly-independent Subset of (VecSp (E,F))
for BK being linearly-independent Subset of (VecSp (K,E))
for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 holds
a1 * b1 <> a2 * b2

proof end;

theorem :: FIELD_7:19

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being linearly-independent Subset of (VecSp (E,F))
for BK being linearly-independent Subset of (VecSp (K,E))
for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = b2 )

proof end;

theorem BE1: :: FIELD_7:20

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty linearly-independent Subset of (VecSp (E,F))
for BK being non empty linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = card [:BE,BK:]

proof end;

theorem BE2: :: FIELD_7:21

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = (card BE) * (card BK)

proof end;

registration

let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty finite linearly-independent Subset of (VecSp (E,F));
let BK be non empty finite linearly-independent Subset of (VecSp (K,E));

cluster Base (BE,BK) -> finite ;

coherence
Base (BE,BK) is finite

proof end;

end;

definition

let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty finite linearly-independent Subset of (VecSp (E,F));
let BK be non empty linearly-independent Subset of (VecSp (K,E));
let l be Linear_Combination of Base (BE,BK);
let b be Element of K;

func down (l,b) -> Linear_Combination of BE means :down1: :: FIELD_7:def 8
( ( for a being Element of K st a in BE & b in BK holds
it . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
it . a = 0. F ) );

existence
ex b₁ being Linear_Combination of BE st
( ( for a being Element of K st a in BE & b in BK holds
b₁ . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b₁ . a = 0. F ) )

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of BE st ( for a being Element of K st a in BE & b in BK holds
b₁ . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b₁ . a = 0. F ) & ( for a being Element of K st a in BE & b in BK holds
b₂ . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b₂ . a = 0. F ) holds
b₁ = b₂

proof end;

end;

:: deftheorem down1 defines down FIELD_7:def 8 :
for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK)
for b being Element of K
for b₈ being Linear_Combination of BE holds
( b₈ = down (l,b) iff ( ( for a being Element of K st a in BE & b in BK holds
b₈ . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b₈ . a = 0. F ) ) );

definition

let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty finite linearly-independent Subset of (VecSp (E,F));
let BK be non empty finite linearly-independent Subset of (VecSp (K,E));
let l be Linear_Combination of Base (BE,BK);

func down l -> Linear_Combination of BK means :down2: :: FIELD_7:def 9
for b being Element of K st b in BK holds
it . b = Sum (down (l,b));

existence
ex b₁ being Linear_Combination of BK st
for b being Element of K st b in BK holds
b₁ . b = Sum (down (l,b))

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of BK st ( for b being Element of K st b in BK holds
b₁ . b = Sum (down (l,b)) ) & ( for b being Element of K st b in BK holds
b₂ . b = Sum (down (l,b)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem down2 defines down FIELD_7:def 9 :
for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK)
for b₇ being Linear_Combination of BK holds
( b₇ = down l iff for b being Element of K st b in BK holds
b₇ . b = Sum (down (l,b)) );

T0: for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being Basis of (VecSp (E,F))
for l1 being Linear_Combination of VecSp (K,E)
for b being Element of K ex l2 being Linear_Combination of BE st l1 . b = Sum l2

proof end;

definition

let F be Field;
let E be F -finite FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be Basis of (VecSp (E,F));
let BK be non empty finite linearly-independent Subset of (VecSp (K,E));
let l1 be Linear_Combination of BK;

func lift (l1,BE) -> Linear_Combination of Base (BE,BK) means :lif: :: FIELD_7:def 10
for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
it . (a * b) = l2 . a ) );

existence
ex b₁ being Linear_Combination of Base (BE,BK) st
for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
b₁ . (a * b) = l2 . a ) )

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of Base (BE,BK) st ( for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
b₁ . (a * b) = l2 . a ) ) ) & ( for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
b₂ . (a * b) = l2 . a ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem lif defines lift FIELD_7:def 10 :
for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l1 being Linear_Combination of BK
for b₇ being Linear_Combination of Base (BE,BK) holds
( b₇ = lift (l1,BE) iff for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
b₇ . (a * b) = l2 . a ) ) );

theorem :: FIELD_7:22

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds lift ((down l),BE) = l

proof end;

theorem Tlift2: :: FIELD_7:23

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of BK holds down (lift (l,BE)) = l

proof end;

theorem LSum1a: :: FIELD_7:24

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l, l1, l2 being Linear_Combination of Base (BE,BK) st l = l1 + l2 holds
for b being Element of K holds down (l,b) = (down (l1,b)) + (down (l2,b))

proof end;

theorem LSum1: :: FIELD_7:25

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l, l1, l2 being Linear_Combination of Base (BE,BK) st l = l1 + l2 holds
down l = (down l1) + (down l2)

proof end;

LSum2: for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st card (Carrier l) = 1 holds
Sum l = Sum (down l)

proof end;

theorem TSum: :: FIELD_7:26

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds Sum l = Sum (down l)

proof end;

theorem T1: :: FIELD_7:27

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {}

proof end;

theorem T2: :: FIELD_7:28

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E)) holds Lin (Base (BE,BK)) = ModuleStr(# the carrier of (VecSp (K,F)), the addF of (VecSp (K,F)), the ZeroF of (VecSp (K,F)), the lmult of (VecSp (K,F)) #)

proof end;

theorem BasKEF: :: FIELD_7:29

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E)) holds Base (BE,BK) is Basis of (VecSp (K,F))

proof end;

theorem degmult: :: FIELD_7:30

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F holds deg (K,F) = (deg (K,E)) * (deg (E,F))

proof end;

theorem alg0: :: FIELD_7:31

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F st K is F -finite holds
( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) )

proof end;

registration

let F be Field;
let E be F -finite FieldExtension of F;

cluster non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative F -extending E -extending E -finite -> F -extending F -finite E -finite for doubleLoopStr ;

coherence
for b₁ being F -extending E -finite FieldExtension of F holds b₁ is F -finite

proof end;

end;

lintrans: for F being Field
for E1 being FieldExtension of F
for E2 being b₂ -homomorphic FieldExtension of F
for h being Homomorphism of E1,E2 st ( for a being Element of E1 st a in F holds
h . a = a ) holds
h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F))

proof end;

definition

let F be Field;
let E be FieldExtension of F;

attr E is F -algebraic means :defa: :: FIELD_7:def 11
for a being Element of E holds a is F -algebraic ;

end;

:: deftheorem defa defines -algebraic FIELD_7:def 11 :
for F being Field
for E being FieldExtension of F holds
( E is F -algebraic iff for a being Element of E holds a is F -algebraic );

lemlin: for F being Field
for E being b₁ -finite FieldExtension of F
for A being finite Subset of (VecSp (E,F)) st card A > dim (VecSp (E,F)) holds
A is linearly-dependent

proof end;

registration

let F be Field;

cluster non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative F -extending F -finite -> F -algebraic for doubleLoopStr ;

coherence
for b₁ being FieldExtension of F st b₁ is F -finite holds
b₁ is F -algebraic

proof end;

end;

registration

let F be Field;
let E be F -algebraic FieldExtension of F;

cluster -> F -algebraic for Element of the carrier of E;

coherence
for b₁ being Element of E holds b₁ is F -algebraic by defa;

end;

theorem :: FIELD_7:32

for F being Field
for E being FieldExtension of F holds
( E is F -algebraic iff for a being Element of E holds FAdj (F,{a}) is F -finite )

proof end;

theorem alg1: :: FIELD_7:33

for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ex B being b₁ -finite FieldExtension of F st
( E is B -extending & a in B ) )

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let T be Subset of E;

attr T is F -algebraic means :defTalg: :: FIELD_7:def 12
for a being Element of E st a in T holds
a is F -algebraic ;

end;

:: deftheorem defTalg defines -algebraic FIELD_7:def 12 :
for F being Field
for E being FieldExtension of F
for T being Subset of E holds
( T is F -algebraic iff for a being Element of E st a in T holds
a is F -algebraic );

registration

let F be Field;
let E be FieldExtension of F;

cluster finite F -algebraic for Element of bool the carrier of E;

existence
ex b₁ being Subset of E st
( b₁ is finite & b₁ is F -algebraic )

proof end;

end;

theorem ug: :: FIELD_7:34

for F being Field
for E being FieldExtension of F
for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})

proof end;

theorem ug1: :: FIELD_7:35

for F being Field
for E being FieldExtension of F
for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,{b})
for T1 being Subset of E1 st E1 = E & T1 = T holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,{b})),T1)

proof end;

registration

let F be Field;
let E be FieldExtension of F;
let T be finite F -algebraic Subset of E;

cluster FieldAdjunction (F,T) -> F -finite ;

coherence
FAdj (F,T) is F -finite

proof end;

end;

theorem ft1: :: FIELD_7:36

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds
( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) )

proof end;

theorem :: FIELD_7:37

for F being Field
for E being FieldExtension of F holds
( E is F -finite iff ex T being finite b₁ -algebraic Subset of E st E == FAdj (F,T) )

proof end;

registration

let F be Field;
let E be FieldExtension of F;
let p be non zero Element of the carrier of (Polynom-Ring F);

cluster Roots (E,p) -> F -algebraic ;

coherence
Roots (E,p) is F -algebraic

proof end;

end;

theorem :: FIELD_7:38

for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of (Polynom-Ring F) holds FAdj (F,(Roots (E,p))) is F -algebraic ;

theorem :: FIELD_7:39

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F st K is E -algebraic & E is F -algebraic holds
K is F -algebraic

proof end;

theorem :: FIELD_7:40

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F st K is F -algebraic holds
( K is E -algebraic & E is F -algebraic )

proof end;

registration

let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;

cluster FieldAdjunction (F,{a,b}) -> F -finite ;

coherence
FAdj (F,{a,b}) is F -finite

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;

cluster 0. E -> F -algebraic ;

coherence
0. E is F -algebraic

proof end;

cluster 1. E -> F -algebraic ;

coherence
1. E is F -algebraic

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;

cluster a + b -> F -algebraic ;

coherence
a + b is F -algebraic

proof end;

cluster a - b -> F -algebraic ;

coherence
a - b is F -algebraic

proof end;

cluster a * b -> F -algebraic ;

coherence
a * b is F -algebraic

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let a be F -algebraic Element of E;

cluster - a -> F -algebraic ;

coherence
- a is F -algebraic

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let a be non zero F -algebraic Element of E;

cluster / a -> F -algebraic ;

coherence
a " is F -algebraic

proof end;

end;

definition

let F be Field;
let E be FieldExtension of F;

func Alg_El E -> Subset of E equals :: FIELD_7:def 13
{ a where a is F -algebraic Element of E : verum } ;

coherence
{ a where a is F -algebraic Element of E : verum } is Subset of E

proof end;

end;

:: deftheorem defines Alg_El FIELD_7:def 13 :
for F being Field
for E being FieldExtension of F holds Alg_El E = { a where a is b₁ -algebraic Element of E : verum } ;

definition

let F be Field;
let E be FieldExtension of F;

func Field_of_Algebraic_Elements E -> strict doubleLoopStr means :d: :: FIELD_7:def 14
( the carrier of it = Alg_El E & the addF of it = the addF of E || the carrier of it & the multF of it = the multF of E || the carrier of it & the OneF of it = 1. E & the ZeroF of it = 0. E );

existence
ex b₁ being strict doubleLoopStr st
( the carrier of b₁ = Alg_El E & the addF of b₁ = the addF of E || the carrier of b₁ & the multF of b₁ = the multF of E || the carrier of b₁ & the OneF of b₁ = 1. E & the ZeroF of b₁ = 0. E )

proof end;

uniqueness
for b₁, b₂ being strict doubleLoopStr st the carrier of b₁ = Alg_El E & the addF of b₁ = the addF of E || the carrier of b₁ & the multF of b₁ = the multF of E || the carrier of b₁ & the OneF of b₁ = 1. E & the ZeroF of b₁ = 0. E & the carrier of b₂ = Alg_El E & the addF of b₂ = the addF of E || the carrier of b₂ & the multF of b₂ = the multF of E || the carrier of b₂ & the OneF of b₂ = 1. E & the ZeroF of b₂ = 0. E holds
b₁ = b₂ ;

end;

:: deftheorem d defines Field_of_Algebraic_Elements FIELD_7:def 14 :
for F being Field
for E being FieldExtension of F
for b₃ being strict doubleLoopStr holds
( b₃ = Field_of_Algebraic_Elements E iff ( the carrier of b₃ = Alg_El E & the addF of b₃ = the addF of E || the carrier of b₃ & the multF of b₃ = the multF of E || the carrier of b₃ & the OneF of b₃ = 1. E & the ZeroF of b₃ = 0. E ) );

notation

let F be Field;
let E be FieldExtension of F;
synonym F_Alg E for Field_of_Algebraic_Elements E;

end;

registration

let F be Field;
let E be FieldExtension of F;

cluster Field_of_Algebraic_Elements E -> non degenerated strict ;

coherence
not F_Alg E is degenerated

proof end;

end;

Lm10: for R being Field
for E being FieldExtension of R
for x being Element of (F_Alg E) holds x is Element of E

proof end;

Lm11: for R being Field
for E being FieldExtension of R
for a, b being Element of E
for x, y being Element of (F_Alg E) st a = x & b = y holds
a + b = x + y

proof end;

Lm12: for R being Field
for S being FieldExtension of R
for a, b being Element of S
for x, y being Element of (F_Alg S) st a = x & b = y holds
a * b = x * y

proof end;

registration

let F be Field;
let E be FieldExtension of F;

cluster Field_of_Algebraic_Elements E -> right_complementable strict Abelian add-associative right_zeroed ;

coherence
( F_Alg E is Abelian & F_Alg E is add-associative & F_Alg E is right_zeroed & F_Alg E is right_complementable )

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;

cluster Field_of_Algebraic_Elements E -> almost_left_invertible strict well-unital distributive associative commutative ;

coherence
( F_Alg E is commutative & F_Alg E is associative & F_Alg E is well-unital & F_Alg E is distributive & F_Alg E is almost_left_invertible )

proof end;

end;

ee: for F being Field
for E being FieldExtension of F holds E is FieldExtension of F_Alg E

proof end;

registration

let F be Field;
let E be FieldExtension of F;

cluster Field_of_Algebraic_Elements E -> strict F -extending ;

coherence
F_Alg E is F -extending

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;

cluster Field_of_Algebraic_Elements E -> strict F -algebraic ;

coherence
F_Alg E is F -algebraic

proof end;

end;

theorem :: FIELD_7:41

for F being Field
for E being FieldExtension of F holds F_Alg E is FieldExtension of F ;

theorem :: FIELD_7:42

for F being Field
for E being FieldExtension of F holds E is FieldExtension of F_Alg E by ee;

t2: for F being Field
for E being b₁ -algebraic FieldExtension of F holds F_Alg E is FieldExtension of E

proof end;

theorem :: FIELD_7:43

for F being Field
for E being FieldExtension of F
for K being FieldExtension of E holds F_Alg K is FieldExtension of F_Alg E

proof end;

theorem :: FIELD_7:44

for F being Field
for E being b₁ -algebraic FieldExtension of F holds F_Alg E == E

proof end;