:: Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials
:: by Christoph Schwarzweller
::
:: Received October 25, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


theorem degen: :: FIELD_6:1
for R being Ring holds
( R is degenerated iff the carrier of R = {(0. R)} )
proof end;

registration
let F be Field;
cluster {(0. F)} -Ideal -> maximal ;
coherence
{(0. F)} -Ideal is maximal
proof end;
end;

registration
let R be non degenerated non almost_left_invertible comRing;
cluster {(0. R)} -Ideal -> non maximal ;
coherence
not {(0. R)} -Ideal is maximal
proof end;
end;

definition
let R be Ring;
attr R is field-containing means :deffc: :: FIELD_6:def 1
 ex F being Field st F is Subring of R;
end;

:: deftheorem deffc defines field-containing FIELD_6:def 1 :
for R being Ring holds
( R is field-containing iff ex F being Field st F is Subring of R );

registration
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Abelian add-associative right_zeroed V123() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative V254() V255() V256() V257() K745() -homomorphic field-containing for doubleLoopStr ;
existence
ex b1 being Ring st b1 is field-containing
proof end;
end;

definition
let R be field-containing Ring;
mode Subfield of R -> Field means :defsubfr: :: FIELD_6:def 2
it is Subring of R;
existence
ex b1 being Field st b1 is Subring of R by deffc;
end;

:: deftheorem defsubfr defines Subfield FIELD_6:def 2 :
for R being field-containing Ring
for b2 being Field holds
( b2 is Subfield of R iff b2 is Subring of R );

theorem thLC: :: FIELD_6:2
for R being non degenerated Ring
for p being non zero Polynomial of R holds p . (deg p) = LC p
proof end;

registration
let R be non degenerated Ring;
let p be non zero Polynomial of R;
cluster Leading-Monomial p -> non zero ;
coherence
not LM p is zero
proof end;
end;

theorem thdegLM: :: FIELD_6:3
for R being Ring
for p being Polynomial of R holds deg (LM p) = deg p
proof end;

theorem thdegLC: :: FIELD_6:4
for R being Ring
for p being Polynomial of R holds LC (LM p) = LC p
proof end;

theorem thdLM: :: FIELD_6:5
for R being non degenerated Ring
for p being non zero Polynomial of R holds deg (p - (LM p)) < deg p
proof end;

theorem thE1: :: FIELD_6:6
for R being Ring
for p being Polynomial of R
for i being Nat holds (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i
proof end;

theorem thE2: :: FIELD_6:7
for R being Ring
for p being Polynomial of R holds (<%(0. R),(1. R)%> *' p) . 0 = 0. R
proof end;

theorem :: FIELD_6:8
for R being domRing
for p being non zero Polynomial of R holds deg (<%(0. R),(1. R)%> *' p) = (deg p) + 1
proof 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;

help3a: for R being domRing
for n being Element of NAT st n <> 0 holds
for a being Element of R holds eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
proof end;

theorem :: FIELD_6:9
for R being comRing
for p being Polynomial of R
for a being Element of R holds eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))
proof end;

ThR1: for R being Ring holds R is Subring of R
by LIOUVIL2:18;

theorem FIELD427: :: FIELD_6:10
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R
for b being Element of S st b = a holds
Ext_eval (p,b) = eval (p,a)
proof end;

theorem lemma7: :: FIELD_6:11
for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for K being b3 -extending FieldExtension of F
for a being Element of E
for b being Element of K st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)
proof end;

registration
let L be non empty ZeroStr ;
let a, b be Element of L;
let f be the carrier of L -valued Function;
let x, y be object ;
cluster f +* ((x,y) --> (a,b)) -> the carrier of L -valued ;
coherence
f +* ((x,y) --> (a,b)) is the carrier of L -valued
proof end;
end;

registration
let L be non empty ZeroStr ;
let a, b be Element of L;
let f be finite-Support sequence of L;
let x, y be object ;
cluster f +* ((x,y) --> (a,b)) -> finite-Support for sequence of L;
coherence
for b1 being sequence of L st b1 = f +* ((x,y) --> (a,b)) holds
b1 is finite-Support
proof end;
end;

theorem RE: :: FIELD_6:12
for R1, R2 being strict Ring st R1 is Subring of R2 & R2 is Subring of R1 holds
R1 = R2
proof end;

theorem Th6: :: FIELD_6:13
for S being Ring
for R1, R2 being Subring of S holds
( R1 is Subring of R2 iff the carrier of R1 c= the carrier of R2 )
proof end;

theorem RE1: :: FIELD_6:14
for S being Ring
for R1, R2 being strict Subring of S holds
( R1 = R2 iff the carrier of R1 = the carrier of R2 )
proof end;

theorem Th17: :: FIELD_6:15
for S being Ring
for R being Subring of S
for x, y being Element of S
for x1, y1 being Element of R st x = x1 & y = y1 holds
x + y = x1 + y1
proof end;

theorem Th18: :: FIELD_6:16
for S being Ring
for R being Subring of S
for x, y being Element of S
for x1, y1 being Element of R st x = x1 & y = y1 holds
x * y = x1 * y1
proof end;

theorem Th19: :: FIELD_6:17
for S being Ring
for R being Subring of S
for x being Element of S
for x1 being Element of R st x = x1 holds
- x = - x1
proof end;

theorem Th19f: :: FIELD_6:18
for E being Field
for F being Subfield of E
for x being non zero Element of E
for x1 being Element of F st x = x1 holds
x " = x1 "
proof end;

theorem pr5: :: FIELD_6:19
for S being Ring
for R being Subring of S
for x being Element of S
for x1 being Element of R
for n being Element of NAT st x = x1 holds
x |^ n = x1 |^ n
proof end;

theorem pr20: :: FIELD_6:20
for S being Ring
for R being Subring of S
for x1, x2 being Element of S
for y1, y2 being Element of R st x1 = y1 & x2 = y2 holds
<%x1,x2%> = <%y1,y2%>
proof end;

theorem helpp: :: FIELD_6:21
for R being comRing
for S being comRingExtension of R
for x1, x2 being Element of S
for y1, y2 being Element of R
for n being Element of NAT st x1 = y1 & x2 = y2 holds
<%x1,x2%> `^ n = <%y1,y2%> `^ n
proof end;

theorem help3: :: FIELD_6:22
for R being domRing
for S being domRingExtension of R
for n being non zero Element of NAT
for a being Element of S holds Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
proof end;

Th28: for L being non empty ZeroStr
for a being Element of L holds
( (a | L) . 0 = a & ( for n being Nat st n <> 0 holds
(a | L) . n = 0. L ) )
proof end;

theorem constpol: :: FIELD_6:23
for R being Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S st a = b holds
a | R = b | S
proof end;

theorem pr0: :: FIELD_6:24
for F being Field
for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
NormPolynomial p = NormPolynomial q
proof end;

theorem pr1: :: FIELD_6:25
for F being Field
for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for a being Element of E holds
( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )
proof end;

theorem exevalminus: :: FIELD_6:26
for R being Ring
for S being RingExtension of R
for a being Element of S
for p being Polynomial of R holds Ext_eval ((- p),a) = - (Ext_eval (p,a))
proof end;

theorem exevalminus2: :: FIELD_6:27
for R being Ring
for S being RingExtension of R
for a being Element of S
for p, q being Polynomial of R holds Ext_eval ((p - q),a) = (Ext_eval (p,a)) - (Ext_eval (q,a))
proof end;

theorem exevalconst: :: FIELD_6:28
for R being Ring
for S being RingExtension of R
for a being Element of S
for p being constant Polynomial of R holds Ext_eval (p,a) = LC p
proof end;

theorem exevalLM: :: FIELD_6:29
for R being non degenerated Ring
for S being RingExtension of R
for a, b being Element of S
for p being non zero Polynomial of R st b = LC p holds
Ext_eval ((Leading-Monomial p),a) = b * (a |^ (deg p))
proof end;

definition
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
func carrierRA T -> non empty Subset of S equals :: FIELD_6:def 3
 { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } ;
coherence
{ x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } is non empty Subset of S
proof end;
end;

:: deftheorem defines carrierRA FIELD_6:def 3 :
for R being Ring
for S being RingExtension of R
for T being Subset of S holds carrierRA T = { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } ;

definition
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
func RingAdjunction (R,T) -> strict doubleLoopStr means :dRA: :: FIELD_6:def 4
( the carrier of it = carrierRA T & the addF of it = the addF of S || (carrierRA T) & the multF of it = the multF of S || (carrierRA T) & the OneF of it = 1. S & the ZeroF of it = 0. S );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = carrierRA T & the addF of b1 = the addF of S || (carrierRA T) & the multF of b1 = the multF of S || (carrierRA T) & the OneF of b1 = 1. S & the ZeroF of b1 = 0. S )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = carrierRA T & the addF of b1 = the addF of S || (carrierRA T) & the multF of b1 = the multF of S || (carrierRA T) & the OneF of b1 = 1. S & the ZeroF of b1 = 0. S & the carrier of b2 = carrierRA T & the addF of b2 = the addF of S || (carrierRA T) & the multF of b2 = the multF of S || (carrierRA T) & the OneF of b2 = 1. S & the ZeroF of b2 = 0. S holds
b1 = b2 ;
end;

:: deftheorem dRA defines RingAdjunction FIELD_6:def 4 :
for R being Ring
for S being RingExtension of R
for T being Subset of S
for b4 being strict doubleLoopStr holds
( b4 = RingAdjunction (R,T) iff ( the carrier of b4 = carrierRA T & the addF of b4 = the addF of S || (carrierRA T) & the multF of b4 = the multF of S || (carrierRA T) & the OneF of b4 = 1. S & the ZeroF of b4 = 0. S ) );

notation
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
synonym RAdj (R,T) for RingAdjunction (R,T);
end;

registration
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
cluster RingAdjunction (R,T) -> non empty strict ;
coherence
not RAdj (R,T) is empty
proof end;
end;

registration
let R be non degenerated Ring;
let S be RingExtension of R;
let T be Subset of S;
cluster RingAdjunction (R,T) -> non degenerated strict ;
coherence
not RAdj (R,T) is degenerated
proof end;
end;

Lm10: for R being Ring
for S being RingExtension of R
for T being Subset of S
for x being Element of (RAdj (R,T)) holds x is Element of S
proof end;

Lm11: for R being Ring
for S being RingExtension of R
for T being Subset of S
for a, b being Element of S
for x, y being Element of (RAdj (R,T)) st a = x & b = y holds
a + b = x + y
proof end;

Lm12: for R being Ring
for S being RingExtension of R
for T being Subset of S
for a, b being Element of S
for x, y being Element of (RAdj (R,T)) st a = x & b = y holds
a * b = x * y
proof end;

registration
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
cluster RingAdjunction (R,T) -> right_complementable strict Abelian add-associative right_zeroed ;
coherence
( RAdj (R,T) is Abelian & RAdj (R,T) is add-associative & RAdj (R,T) is right_zeroed & RAdj (R,T) is right_complementable )
proof end;
end;

registration
let R be comRing;
let S be comRingExtension of R;
let T be Subset of S;
cluster RingAdjunction (R,T) -> strict commutative ;
coherence
RAdj (R,T) is commutative
proof end;
end;

registration
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
cluster RingAdjunction (R,T) -> strict well-unital distributive associative ;
coherence
( RAdj (R,T) is associative & RAdj (R,T) is well-unital & RAdj (R,T) is distributive )
proof end;
end;

theorem RAt: :: FIELD_6:30
for R being Ring
for S being RingExtension of R
for T being Subset of S holds T is Subset of (RAdj (R,T))
proof end;

theorem RAsub: :: FIELD_6:31
for R being Ring
for S being RingExtension of R
for T being Subset of S holds R is Subring of RAdj (R,T)
proof end;

theorem RAsub2: :: FIELD_6:32
for R being Ring
for S being RingExtension of R
for T being Subset of S
for U being Subring of S st R is Subring of U & T is Subset of U holds
RAdj (R,T) is Subring of U
proof end;

theorem :: FIELD_6:33
for R being strict Ring
for S being RingExtension of R
for T being Subset of S holds
( RAdj (R,T) = R iff T is Subset of R )
proof end;

definition
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
:: original: RingAdjunction
redefine func RAdj (R,T) -> strict Subring of S;
coherence
RingAdjunction (R,T) is strict Subring of S
proof end;
end;

registration
let R be Ring;
let S be RingExtension of R;
let T be Subset of S;
cluster RingAdjunction (R,T) -> strict R -extending ;
coherence
RAdj (R,T) is R -extending
proof end;
end;

registration
let F be Field;
let R be RingExtension of F;
let T be Subset of R;
cluster RingAdjunction (F,T) -> strict field-containing ;
coherence
RAdj (F,T) is field-containing
proof end;
end;

theorem :: FIELD_6:34
for F being Field
for R being RingExtension of F
for T being Subset of R holds F is Subfield of RAdj (F,T)
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
func carrierFA T -> non empty Subset of E equals :: FIELD_6:def 5
 { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } ;
coherence
{ x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } is non empty Subset of E
proof end;
end;

:: deftheorem defines carrierFA FIELD_6:def 5 :
for F being Field
for E being FieldExtension of F
for T being Subset of E holds carrierFA T = { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U } ;

definition
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
func FieldAdjunction (F,T) -> strict doubleLoopStr means :dFA: :: FIELD_6:def 6
( the carrier of it = carrierFA T & the addF of it = the addF of E || (carrierFA T) & the multF of it = the multF of E || (carrierFA T) & the OneF of it = 1. E & the ZeroF of it = 0. E );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = carrierFA T & the addF of b1 = the addF of E || (carrierFA T) & the multF of b1 = the multF of E || (carrierFA T) & the OneF of b1 = 1. E & the ZeroF of b1 = 0. E )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = carrierFA T & the addF of b1 = the addF of E || (carrierFA T) & the multF of b1 = the multF of E || (carrierFA T) & the OneF of b1 = 1. E & the ZeroF of b1 = 0. E & the carrier of b2 = carrierFA T & the addF of b2 = the addF of E || (carrierFA T) & the multF of b2 = the multF of E || (carrierFA T) & the OneF of b2 = 1. E & the ZeroF of b2 = 0. E holds
b1 = b2 ;
end;

:: deftheorem dFA defines FieldAdjunction FIELD_6:def 6 :
for F being Field
for E being FieldExtension of F
for T being Subset of E
for b4 being strict doubleLoopStr holds
( b4 = FieldAdjunction (F,T) iff ( the carrier of b4 = carrierFA T & the addF of b4 = the addF of E || (carrierFA T) & the multF of b4 = the multF of E || (carrierFA T) & the OneF of b4 = 1. E & the ZeroF of b4 = 0. E ) );

notation
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
synonym FAdj (F,T) for FieldAdjunction (F,T);
end;

registration
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
cluster FieldAdjunction (F,T) -> non degenerated strict ;
coherence
not FAdj (F,T) is degenerated
proof end;
end;

Lm10f: for R being Field
for S being FieldExtension of R
for T being Subset of S
for x being Element of (FAdj (R,T)) holds x is Element of S
proof end;

Lm11f: for R being Field
for S being FieldExtension of R
for T being Subset of S
for a, b being Element of S
for x, y being Element of (FAdj (R,T)) st a = x & b = y holds
a + b = x + y
proof end;

Lm12f: for R being Field
for S being FieldExtension of R
for T being Subset of S
for a, b being Element of S
for x, y being Element of (FAdj (R,T)) st a = x & b = y holds
a * b = x * y
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
cluster FieldAdjunction (F,T) -> right_complementable strict Abelian add-associative right_zeroed ;
coherence
( FAdj (F,T) is Abelian & FAdj (F,T) is add-associative & FAdj (F,T) is right_zeroed & FAdj (F,T) is right_complementable )
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
cluster FieldAdjunction (F,T) -> almost_left_invertible strict well-unital distributive associative commutative ;
coherence
( FieldAdjunction (F,T) is commutative & FieldAdjunction (F,T) is associative & FieldAdjunction (F,T) is well-unital & FieldAdjunction (F,T) is distributive & FieldAdjunction (F,T) is almost_left_invertible )
proof end;
end;

theorem FAt: :: FIELD_6:35
for F being Field
for E being FieldExtension of F
for T being Subset of E holds T is Subset of (FAdj (F,T))
proof end;

theorem FAsub: :: FIELD_6:36
for F being Field
for E being FieldExtension of F
for T being Subset of E holds F is Subfield of FAdj (F,T)
proof end;

theorem FAsub2: :: FIELD_6:37
for F being Field
for E being FieldExtension of F
for T being Subset of E
for U being Subfield of E st F is Subfield of U & T is Subset of U holds
FAdj (F,T) is Subfield of U
proof end;

theorem :: FIELD_6:38
for F being strict 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;

definition
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
:: original: FieldAdjunction
redefine func FAdj (F,T) -> strict Subfield of E;
coherence
FieldAdjunction (F,T) is strict Subfield of E
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
cluster FieldAdjunction (F,T) -> strict F -extending ;
coherence
FAdj (F,T) is F -extending
proof end;
end;

theorem RF: :: FIELD_6:39
for F being Field
for E being FieldExtension of F
for T being Subset of E holds RAdj (F,T) is Subring of FAdj (F,T)
proof end;

theorem RF2: :: FIELD_6:40
for F being Field
for E being FieldExtension of F
for T being Subset of E holds
( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
proof end;

lcsub1: for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Element of NAT holds a |^ n in the carrier of (FAdj (F,{a}))
proof end;

registration
let R be non degenerated comRing;
let S be comRingExtension of R;
let a be Element of S;
cluster hom_Ext_eval (a,R) -> additive unity-preserving multiplicative ;
coherence
( hom_Ext_eval (a,R) is additive & hom_Ext_eval (a,R) is multiplicative & hom_Ext_eval (a,R) is unity-preserving )
proof end;
end;

registration
let R be non degenerated comRing;
cluster non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative R -extending -> Polynom-Ring R -homomorphic for doubleLoopStr ;
coherence
for b1 being comRingExtension of R holds b1 is Polynom-Ring R -homomorphic
proof end;
end;

registration
let F be Field;
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 Abelian add-associative right_zeroed V123() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V254() V255() V256() V257() PID Polynom-Ring F -homomorphic K745() -homomorphic factorial F -extending for doubleLoopStr ;
existence
ex b1 being FieldExtension of F st b1 is Polynom-Ring F -homomorphic
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
let a be Element of E;
attr a is F -algebraic means :: FIELD_6:def 7
 ker (hom_Ext_eval (a,F)) <> {(0. (Polynom-Ring F))};
end;

:: deftheorem defines -algebraic FIELD_6:def 7 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ker (hom_Ext_eval (a,F)) <> {(0. (Polynom-Ring F))} );

notation
let F be Field;
let E be FieldExtension of F;
let a be Element of E;
antonym F -transcendental a for F -algebraic ;
end;

theorem alg0: :: FIELD_6:41
for R being Ring
for S being RingExtension of R
for a being Element of S holds Ann_Poly (a,R) = ker (hom_Ext_eval (a,R))
proof end;

theorem alg1: :: FIELD_6:42
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff a is_integral_over F )
proof end;

theorem alg00: :: FIELD_6:43
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )
proof end;

registration
let F be Field;
let E be FieldExtension of F;
cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non irreducible F -algebraic for Element of the carrier of E;
existence
ex b1 being Element of E st b1 is F -algebraic
proof end;
end;

lemphi1: for F being Field
for E being FieldExtension of F
for a being Element of E holds rng (hom_Ext_eval (a,F)) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
proof end;

lemphi2: for F being Field
for E being FieldExtension of F
for a being Element of E holds rng (hom_Ext_eval (a,F)) c= the carrier of (RAdj (F,{a}))
proof end;

lemphi3: for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being Element of E holds F is Subring of Image (hom_Ext_eval (a,F))
proof end;

theorem lemphi4: :: FIELD_6:44
for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
proof end;

theorem lemphi5: :: FIELD_6:45
for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being Element of E holds the carrier of (RAdj (F,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
proof end;

lemlin: for F being Field
for E being b1 -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;

Lm12a: for F being Ring
for E being RingExtension of F
for a, b being Element of E
for s being Element of F
for v being Element of (VecSp (E,F)) st a = s & b = v holds
a * b = s * v
proof end;

Lm12b: for F being Ring
for E being RingExtension of F
for a, b being Element of E
for x, y being Element of F st a = x & b = y holds
a * b = x * y
proof end;

theorem lcsub: :: FIELD_6:46
for F being Field
for V being VectSp of F
for W being Subspace of V
for l1 being Linear_Combination of W ex l2 being Linear_Combination of V st
( Carrier l2 = Carrier l1 & ( for v being Element of V st v in Carrier l2 holds
l2 . v = l1 . v ) )
proof end;

theorem lembasx2: :: FIELD_6:47
for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp (E,F) ex p being Polynomial of F st
( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) )
proof end;

theorem lembasx1a: :: FIELD_6:48
for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp (E,F)
for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds
Sum l = Ext_eval ((LM p),a)
proof end;

theorem lembasx1: :: FIELD_6:49
for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for M being Subset of (VecSp (E,F)) st M = { (a |^ i) where i is Element of NAT : i <= n } & ( for i, j being Element of NAT st i < j & j <= n holds
a |^ i <> a |^ j ) holds
for l being Linear_Combination of M
for p being Polynomial of F st deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) holds
Ext_eval (p,a) = Sum l
proof end;

notation
let F be Field;
let E be FieldExtension of F;
let a be F -algebraic Element of E;
synonym MinPoly (a,F) for minimal_polynom (a,F);
end;

lemminirred: for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds MinPoly (a,F) is irreducible
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let a be F -algebraic Element of E;
cluster MinPoly (a,F) -> monic irreducible ;
coherence
( MinPoly (a,F) is monic & MinPoly (a,F) is irreducible )
proof end;
end;

theorem mpol1: :: FIELD_6:50
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )
proof end;

theorem mpol2: :: FIELD_6:51
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & Ext_eval (p,a) = 0. E & ( for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds
deg p <= deg q ) ) )
proof end;

theorem mpol3: :: FIELD_6:52
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )
proof end;

theorem mpol4: :: FIELD_6:53
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p )
proof end;

theorem :: FIELD_6:54
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds
( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F )
proof end;

theorem mpol5: :: FIELD_6:55
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for i, j being Element of NAT st i < j & j < deg (MinPoly (a,F)) holds
a |^ i <> a |^ j
proof end;

theorem ch1: :: FIELD_6:56
for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff FAdj (F,{a}) = RAdj (F,{a}) )
proof end;

theorem :: FIELD_6:57
for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being non zero Element of E holds
( a is F -algebraic iff a " in RAdj (F,{a}) )
proof end;

theorem :: FIELD_6:58
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
proof end;

theorem :: FIELD_6:59
for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being b1 -algebraic Element of E holds (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), FAdj (F,{a}) are_isomorphic
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let a be F -algebraic Element of E;
func Base a -> non empty Subset of (VecSp ((FAdj (F,{a})),F)) equals :: FIELD_6:def 8
 { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } ;
coherence
{ (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } is non empty Subset of (VecSp ((FAdj (F,{a})),F))
proof end;
end;

:: deftheorem defines Base FIELD_6:def 8 :
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds Base a = { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } ;

registration
let F be Field;
let E be FieldExtension of F;
let a be F -algebraic Element of E;
cluster Base a -> non empty finite ;
coherence
Base a is finite
proof end;
end;

lembas1b: for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for p being Polynomial of F st deg p < deg (MinPoly (a,F)) holds
Ext_eval ((Leading-Monomial p),a) in Lin (Base a)
proof end;

lembas1a: for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being b1 -algebraic Element of E
for p being Polynomial of F st deg p < deg (MinPoly (a,F)) holds
Ext_eval (p,a) in Lin (Base a)
proof end;

theorem lembas1: :: FIELD_6:60
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for p being Polynomial of F holds Ext_eval (p,a) in Lin (Base a)
proof end;

theorem lembas2a: :: FIELD_6:61
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for l being Linear_Combination of Base a ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
proof end;

theorem lembas2bb: :: FIELD_6:62
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for l being Linear_Combination of Base a
for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds
Sum l = Ext_eval ((LM p),a)
proof end;

theorem lembas2b: :: FIELD_6:63
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for l being Linear_Combination of Base a
for p being Polynomial of F st deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) holds
Sum l = Ext_eval (p,a)
proof end;

theorem lembas2: :: FIELD_6:64
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for l being Linear_Combination of Base a st Sum l = 0. F holds
l = ZeroLC (VecSp ((FAdj (F,{a})),F))
proof end;

theorem lembas: :: FIELD_6:65
for F being Field
for E being Polynom-Ring b1 -homomorphic FieldExtension of F
for a being b1 -algebraic Element of E holds Base a is Basis of (VecSp ((FAdj (F,{a})),F))
proof end;

theorem lembascard: :: FIELD_6:66
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds card (Base a) = deg (MinPoly (a,F))
proof end;

theorem :: FIELD_6:67
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F))
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let a be F -algebraic Element of E;
cluster FieldAdjunction (F,{a}) -> strict F -finite ;
coherence
FAdj (F,{a}) is F -finite
proof end;
end;

theorem :: FIELD_6:68
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff FAdj (F,{a}) is F -finite )
proof end;