:: 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 b₁ being Ring st b₁ 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 b₁ being Field st b₁ is Subring of R by deffc;

end;

:: deftheorem defsubfr defines Subfield FIELD_6:def 2 :
for R being field-containing Ring
for b₂ being Field holds
( b₂ is Subfield of R iff b₂ 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 b₃ -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 b₁ being sequence of L st b₁ = f +* ((x,y) --> (a,b)) holds
b₁ 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 b₁ being strict doubleLoopStr st
( the carrier of b₁ = carrierRA T & the addF of b₁ = the addF of S || (carrierRA T) & the multF of b₁ = the multF of S || (carrierRA T) & the OneF of b₁ = 1. S & the ZeroF of b₁ = 0. S )

proof end;

uniqueness
for b₁, b₂ being strict doubleLoopStr st the carrier of b₁ = carrierRA T & the addF of b₁ = the addF of S || (carrierRA T) & the multF of b₁ = the multF of S || (carrierRA T) & the OneF of b₁ = 1. S & the ZeroF of b₁ = 0. S & the carrier of b₂ = carrierRA T & the addF of b₂ = the addF of S || (carrierRA T) & the multF of b₂ = the multF of S || (carrierRA T) & the OneF of b₂ = 1. S & the ZeroF of b₂ = 0. S holds
b₁ = b₂ ;

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 b₄ being strict doubleLoopStr holds
( b₄ = RingAdjunction (R,T) iff ( the carrier of b₄ = carrierRA T & the addF of b₄ = the addF of S || (carrierRA T) & the multF of b₄ = the multF of S || (carrierRA T) & the OneF of b₄ = 1. S & the ZeroF of b₄ = 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 b₁ being strict doubleLoopStr st
( the carrier of b₁ = carrierFA T & the addF of b₁ = the addF of E || (carrierFA T) & the multF of b₁ = the multF of E || (carrierFA T) & 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₁ = carrierFA T & the addF of b₁ = the addF of E || (carrierFA T) & the multF of b₁ = the multF of E || (carrierFA T) & the OneF of b₁ = 1. E & the ZeroF of b₁ = 0. E & the carrier of b₂ = carrierFA T & the addF of b₂ = the addF of E || (carrierFA T) & the multF of b₂ = the multF of E || (carrierFA T) & the OneF of b₂ = 1. E & the ZeroF of b₂ = 0. E holds
b₁ = b₂ ;

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 b₄ being strict doubleLoopStr holds
( b₄ = FieldAdjunction (F,T) iff ( the carrier of b₄ = carrierFA T & the addF of b₄ = the addF of E || (carrierFA T) & the multF of b₄ = the multF of E || (carrierFA T) & the OneF of b₄ = 1. E & the ZeroF of b₄ = 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 b₁ being comRingExtension of R holds b₁ 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 b₁ being FieldExtension of F st b₁ 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 b₁ being Element of E st b₁ 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 b₁ -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 b₁ -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 b₁ -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 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;

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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -homomorphic FieldExtension of F
for a being b₁ -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 b₁ -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 b₁ -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 b₁ -homomorphic FieldExtension of F
for a being b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -homomorphic FieldExtension of F
for a being b₁ -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 b₁ -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 b₁ -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;