:: Normal Extensions
:: by Christoph Schwarzweller
::
:: Received June 30, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

definition

let Y be non empty set ;
let y1, y2, y3 be Element of Y;
:: original: {
redefine func {y1,y2,y3} -> Subset of Y;
coherence
{y1,y2,y3} is Subset of Y

proof end;

end;

T8: for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )

proof end;

registration

let R be domRing;
let p, q be constant Polynomial of R;

cluster p *' q -> constant ;

coherence
p *' q is constant

proof end;

end;

registration

let R be Ring;

cluster non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative R -extending -> R -homomorphic R -monomorphic for doubleLoopStr ;

coherence
for b₁ being RingExtension of R holds
( b₁ is R -homomorphic & b₁ is R -monomorphic )

proof end;

end;

registration

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

cluster Roots (E,p) -> non empty ;

coherence
not Roots (E,p) is empty

proof end;

end;

registration

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

cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty total quasi_total additive unity-preserving RingHomomorphism multiplicative R -fixing for Element of bool [: the carrier of S, the carrier of T:];

existence
ex b₁ being Homomorphism of S,T st b₁ is R -fixing

proof end;

cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like one-to-one non empty total quasi_total additive unity-preserving RingHomomorphism monomorphism multiplicative R -fixing for Element of bool [: the carrier of S, the carrier of T:];

existence
ex b₁ being Monomorphism of S,T st b₁ is R -fixing

proof end;

end;

theorem Eprod: :: FIELD_13:1

for R being Ring
for S being Subring of R
for F being non empty FinSequence of the carrier of R
for G being non empty FinSequence of the carrier of S st F = G holds
Product F = Product G

proof end;

theorem lemNor1dega: :: FIELD_13:2

for F being Field
for G being non empty FinSequence of the carrier of (Polynom-Ring F) holds
( Product G = 0_. F iff ex i being Element of dom G st G . i = 0_. F )

proof end;

theorem lemNor1deg: :: FIELD_13:3

for F being Field
for G being non empty FinSequence of the carrier of (Polynom-Ring F) st ( for i being Element of dom G holds G . i <> 0_. F ) holds
for q being Polynomial of F st q = Product G holds
for i being Element of dom G
for p being Polynomial of F st p = G . i holds
deg p <= deg q

proof end;

theorem lemNor1b: :: FIELD_13:4

for F being Field
for E being FieldExtension of F
for G being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being Polynomial of F st q = Product G holds
for a being Element of E st ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) holds
Ext_eval (q,a) = 0. E

proof end;

theorem lemNor1ah: :: FIELD_13:5

for F being Field
for G being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being non constant Polynomial of F st q = Product G holds
( q splits_in F iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in F ) )

proof end;

theorem lemNor1a: :: FIELD_13:6

for F being Field
for E being FieldExtension of F
for G being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being non constant Polynomial of F st q = Product G holds
( q splits_in E iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) )

proof end;

theorem F811: :: FIELD_13:7

for F being Field
for E being FieldExtension of F
for p being non constant Polynomial of F
for q being non zero Polynomial of F st p *' q splits_in E holds
p splits_in E

proof end;

theorem field426a: :: FIELD_13:8

for n being Nat
for F being Field
for E being FieldExtension of F
for p being Polynomial of n,F
for q being Polynomial of n,E st p = q holds
Support q = Support p

proof end;

theorem field426: :: FIELD_13:9

for n being Nat
for F being Field
for E being FieldExtension of F
for p being Polynomial of n,F
for q being Polynomial of n,E
for x being Function of n,E st p = q holds
Ext_eval (p,x) = eval (q,x)

proof end;

theorem field427: :: FIELD_13:10

for n being Nat
for F being Field
for E being FieldExtension of F
for a being Element of F
for b being Element of E st a = b holds
a | (n,F) = b | (n,E)

proof end;

theorem lemNor1cu: :: FIELD_13:11

for F being Field
for E1 being FieldExtension of F
for E2 being Field st E1 == E2 holds
E2 is FieldExtension of F

proof end;

theorem lemNor1cx: :: FIELD_13:12

for F1, F2 being Field
for p being Ppoly of F1 st F1 == F2 holds
p is Ppoly of F2

proof end;

theorem lemNor1cv: :: FIELD_13:13

for F being Field
for E being FieldExtension of F
for p being Polynomial of F
for q being Polynomial of E
for a being Element of F
for b being Element of E st p = q & a = b holds
a * p = b * q

proof end;

theorem lemNor1cy: :: FIELD_13:14

for F1, F2 being Field
for p being Polynomial of F1
for a being Element of F1
for q being Polynomial of F2
for b being Element of F2 st F1 == F2 & p = q & a = b holds
a * p = b * q

proof end;

theorem lemNor1c: :: FIELD_13:15

for F being Field
for E1, E2 being FieldExtension of F
for p being Polynomial of F st E1 == E2 & p splits_in E1 holds
p splits_in E2

proof end;

helpb: for R1, R2, R3 being Ring st R1 == R2 & R2 == R3 holds
R1 == R3

proof end;

theorem lemNor1d: :: FIELD_13:16

for F being Field
for E1, E2 being FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) st E1 == E2 & E1 is SplittingField of p holds
E2 is SplittingField of p

proof end;

theorem lemNor1e: :: FIELD_13:17

for F being Field
for p being linear Element of the carrier of (Polynom-Ring F) holds F is SplittingField of p

proof end;

registration

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

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

existence
ex b₁ being Subset of E st
( not b₁ is empty & b₁ is finite & 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 for Subset of E;

coherence
for b₁ being Subset of E st b₁ = {a} holds
b₁ is F -algebraic

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let T1, T2 be F -algebraic Subset of E;

cluster T1 \/ T2 -> F -algebraic for Subset of E;

coherence
for b₁ being Subset of E st b₁ = T1 \/ T2 holds
b₁ is F -algebraic

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let T1 be F -algebraic Subset of E;
let T2 be Subset of E;

cluster T1 /\ T2 -> F -algebraic for Subset of E;

coherence
for b₁ being Subset of E st b₁ = T1 /\ T2 holds
b₁ is F -algebraic

proof end;

cluster T1 \ T2 -> F -algebraic for Subset of E;

coherence
for b₁ being Subset of E st b₁ = T1 \ T2 holds
b₁ is F -algebraic

proof end;

end;

definition

let F be Field;
let E be FieldExtension of F;
let T be non empty F -algebraic Subset of E;
:: original: Element
redefine mode Element of T -> Element of E;
coherence
for b₁ being Element of T holds b₁ is Element of E by TARSKI:def 3;

end;

registration

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

cluster -> F -algebraic for Element of T;

coherence
for b₁ being Element of T holds b₁ is F -algebraic by FIELD_7:def 12;

end;

definition

let F be Field;
let E1, E2 be FieldExtension of F;
let h be Function of E1,E2;
let T be Subset of E1;
:: original: .:
redefine func h .: T -> Subset of E2;
coherence
h .: T is Subset of E2

proof end;

end;

theorem ug1: :: FIELD_13:18

for F being Field
for E being FieldExtension of F
for T1, T2 being Subset of E
for E1 being FieldExtension of FAdj (F,T2)
for T3 being Subset of E1 st E1 = E & T1 = T3 holds
FAdj (F,(T1 \/ T2)) = FAdj ((FAdj (F,T2)),T3)

proof end;

theorem lemh1: :: FIELD_13:19

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for T1 being finite b₁ -algebraic Subset of E
for T2 being Subset of K st T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)

proof end;

theorem lemNor3z: :: FIELD_13:20

for F1, F2 being Field
for p1 being Element of the carrier of (Polynom-Ring F1)
for p2 being Element of the carrier of (Polynom-Ring F2)
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2 st E1 = E2 & p1 = p2 holds
Roots (E1,p1) = Roots (E2,p2)

proof end;

theorem lemNor3xx: :: FIELD_13:21

for F being Field
for E, K being FieldExtension of F
for U1 being FieldExtension of E
for U2 being FieldExtension of K
for T1 being Subset of U1
for T2 being Subset of U2 st U1 = U2 & T1 = T2 & E == K holds
FAdj (E,T1) = FAdj (K,T2)

proof end;

theorem :: FIELD_13:22

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for T1 being Subset of K
for T2 being finite Subset of K st T1 c= T2 & E == FAdj (F,T1) holds
FAdj (E,T2) = FAdj (F,T2)

proof end;

theorem lemNor32: :: FIELD_13:23

for F1 being Field
for p1 being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being FieldExtension of F1
for p2 being non constant Element of the carrier of (Polynom-Ring F2)
for E being SplittingField of p2
for T being b₁ -algebraic Subset of F2 st T c= Roots (E,p2) & F2 == FAdj (F1,T) & p1 = p2 holds
E is SplittingField of p1

proof end;

theorem lemNor2bb: :: FIELD_13:24

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
Roots (K,p) = Roots (E,p)

proof end;

theorem lemNor3d: :: FIELD_13:25

for F1 being Field
for F2 being b₁ -homomorphic Field
for h being Homomorphism of F1,F2
for a being Element of F1 holds (PolyHom h) . (X- a) = X- (h . a)

proof end;

theorem lemNor3e: :: FIELD_13:26

for F1 being Field
for F2 being b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b

proof end;

definition

let R1, R2 be Ring;

redefine pred R1 == R2 means :: FIELD_13:def 1
( R1 is Subring of R2 & R2 is Subring of R1 );

correctness
compatibility
( R1 == R2 iff ( R1 is Subring of R2 & R2 is Subring of R1 ) );

proof end;

end;

:: deftheorem defines == FIELD_13:def 1 :
for R1, R2 being Ring holds
( R1 == R2 iff ( R1 is Subring of R2 & R2 is Subring of R1 ) );

theorem :: FIELD_13:27

for R being Ring holds R == R ;

theorem :: FIELD_13:28

for R1, R2 being Ring st R1 == R2 holds
R2 == R1 ;

theorem :: FIELD_13:29

for R1, R2, R3 being Ring st R1 == R2 & R2 == R3 holds
R1 == R3 by helpb;

theorem ext0: :: FIELD_13:30

for R being Ring
for S being RingExtension of R
for T1, T2 being Subset of S st T1 c= T2 holds
RAdj (R,T1) is Subring of RAdj (R,T2)

proof end;

theorem ug: :: FIELD_13:31

for R being Ring
for S being RingExtension of R
for T1, T2 being Subset of S
for S1 being RingExtension of RAdj (R,T2)
for T3 being Subset of S1 st S1 = S & T1 = T3 holds
RAdj (R,(T1 \/ T2)) = RAdj ((RAdj (R,T2)),T3)

proof end;

theorem helpa: :: FIELD_13:32

for R being 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 n be Nat;
let R, S be non degenerated comRing;
let x be Function of n,S;

func hom_Ext_eval (x,R) -> Function of (Polynom-Ring (n,R)),S means :dh: :: FIELD_13:def 2
for p being Polynomial of n,R holds it . p = Ext_eval (p,x);

existence
ex b₁ being Function of (Polynom-Ring (n,R)),S st
for p being Polynomial of n,R holds b₁ . p = Ext_eval (p,x)

proof end;

uniqueness
for b₁, b₂ being Function of (Polynom-Ring (n,R)),S st ( for p being Polynomial of n,R holds b₁ . p = Ext_eval (p,x) ) & ( for p being Polynomial of n,R holds b₂ . p = Ext_eval (p,x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem dh defines hom_Ext_eval FIELD_13:def 2 :
for n being Nat
for R, S being non degenerated comRing
for x being Function of n,S
for b₅ being Function of (Polynom-Ring (n,R)),S holds
( b₅ = hom_Ext_eval (x,R) iff for p being Polynomial of n,R holds b₅ . p = Ext_eval (p,x) );

registration

let n be Nat;
let R be non degenerated comRing;
let S be comRingExtension of R;
let x be Function of n,S;

cluster hom_Ext_eval (x,R) -> additive unity-preserving multiplicative ;

coherence
( hom_Ext_eval (x,R) is additive & hom_Ext_eval (x,R) is multiplicative & hom_Ext_eval (x,R) is unity-preserving )

proof end;

end;

theorem helpp: :: FIELD_13:33

for n being Nat
for F being Field
for E being FieldExtension of F holds E is Polynom-Ring (n,F) -homomorphic

proof end;

registration

let n be Nat;
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 zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID F -homomorphic Polynom-Ring (n,F) -homomorphic Polynom-Ring F -homomorphic factorial F -monomorphic F -extending gcd-like for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ is Polynom-Ring (n,F) -homomorphic

proof end;

end;

theorem lemphi1: :: FIELD_13:34

for n being Nat
for F, E being Field
for x being Function of n,E holds rng (hom_Ext_eval (x,F)) = { (Ext_eval (p,x)) where p is Polynomial of n,F : verum }

proof end;

T0: for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E holds 0. E in rng (hom_Ext_eval (x,F))

proof end;

T1: for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E holds 1. E in rng (hom_Ext_eval (x,F))

proof end;

T3: for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E holds rng (hom_Ext_eval (x,F)) is Preserv of the addF of E

proof end;

T4: for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E holds rng (hom_Ext_eval (x,F)) is Preserv of the multF of E

proof end;

definition

let n be Nat;
let F be Field;
let E be FieldExtension of F;
let x be Function of n,E;

func Image_hom_Ext_eval (x,F) -> strict doubleLoopStr means :defIm: :: FIELD_13:def 3
( the carrier of it = rng (hom_Ext_eval (x,F)) & the addF of it = the addF of E || (rng (hom_Ext_eval (x,F))) & the multF of it = the multF of E || (rng (hom_Ext_eval (x,F))) & the OneF of it = 1. E & the ZeroF of it = 0. E );

existence
ex b₁ being strict doubleLoopStr st
( the carrier of b₁ = rng (hom_Ext_eval (x,F)) & the addF of b₁ = the addF of E || (rng (hom_Ext_eval (x,F))) & the multF of b₁ = the multF of E || (rng (hom_Ext_eval (x,F))) & 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₁ = rng (hom_Ext_eval (x,F)) & the addF of b₁ = the addF of E || (rng (hom_Ext_eval (x,F))) & the multF of b₁ = the multF of E || (rng (hom_Ext_eval (x,F))) & the OneF of b₁ = 1. E & the ZeroF of b₁ = 0. E & the carrier of b₂ = rng (hom_Ext_eval (x,F)) & the addF of b₂ = the addF of E || (rng (hom_Ext_eval (x,F))) & the multF of b₂ = the multF of E || (rng (hom_Ext_eval (x,F))) & the OneF of b₂ = 1. E & the ZeroF of b₂ = 0. E holds
b₁ = b₂ ;

end;

:: deftheorem defIm defines Image_hom_Ext_eval FIELD_13:def 3 :
for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E
for b₅ being strict doubleLoopStr holds
( b₅ = Image_hom_Ext_eval (x,F) iff ( the carrier of b₅ = rng (hom_Ext_eval (x,F)) & the addF of b₅ = the addF of E || (rng (hom_Ext_eval (x,F))) & the multF of b₅ = the multF of E || (rng (hom_Ext_eval (x,F))) & the OneF of b₅ = 1. E & the ZeroF of b₅ = 0. E ) );

registration

let n be Nat;
let F be Field;
let E be FieldExtension of F;
let x be Function of n,E;

cluster Image_hom_Ext_eval (x,F) -> non degenerated strict ;

coherence
not Image_hom_Ext_eval (x,F) is degenerated

proof end;

end;

T5: for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E
for a, b being Element of (Image_hom_Ext_eval (x,F))
for x1, x2 being Element of E st a = x1 & b = x2 holds
( a + b = x1 + x2 & a * b = x1 * x2 )

proof end;

T6: for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E
for a being Element of (Image_hom_Ext_eval (x,F)) ex y being Element of the carrier of (Polynom-Ring (n,F)) st (hom_Ext_eval (x,F)) . y = a

proof end;

registration

let n be Nat;
let F be Field;
let E be FieldExtension of F;
let x be Function of n,E;

cluster Image_hom_Ext_eval (x,F) -> right_complementable strict Abelian add-associative right_zeroed ;

coherence
( Image_hom_Ext_eval (x,F) is Abelian & Image_hom_Ext_eval (x,F) is add-associative & Image_hom_Ext_eval (x,F) is right_zeroed & Image_hom_Ext_eval (x,F) is right_complementable )

proof end;

end;

registration

let n be Nat;
let F be Field;
let E be FieldExtension of F;
let x be Function of n,E;

cluster Image_hom_Ext_eval (x,F) -> strict well-unital distributive associative commutative ;

coherence
( Image_hom_Ext_eval (x,F) is commutative & Image_hom_Ext_eval (x,F) is associative & Image_hom_Ext_eval (x,F) is well-unital & Image_hom_Ext_eval (x,F) is distributive )

proof end;

end;

theorem lemphi3: :: FIELD_13:35

for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E holds F is Subring of Image_hom_Ext_eval (x,F)

proof end;

definition

let F be Field;
let T be finite Subset of F;
let x be Function of (card T),F;

attr x is T -evaluating means :tev: :: FIELD_13:def 4
( x is one-to-one & rng x = T );

end;

:: deftheorem tev defines -evaluating FIELD_13:def 4 :
for F being Field
for T being finite Subset of F
for x being Function of (card T),F holds
( x is T -evaluating iff ( x is one-to-one & rng x = T ) );

registration

let F be Field;
let T be finite Subset of F;

cluster Relation-like card T -defined the carrier of F -valued Function-like total quasi_total finite finite-support T -evaluating for Element of bool [:(card T), the carrier of F:];

existence
ex b₁ being Function of (card T),F st b₁ is T -evaluating

proof end;

end;

registration

let F be Field;
let T be finite Subset of F;

cluster Function-like quasi_total T -evaluating -> T -valued one-to-one for Element of bool [:(card T), the carrier of F:];

coherence
for b₁ being Function of (card T),F st b₁ is T -evaluating holds
( b₁ is T -valued & b₁ is one-to-one ) by RELAT_1:def 19;

end;

lemphi2ax: for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for b being bag of card T st ex o being set st support b = {o} holds
for x being b₃ -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))

proof end;

theorem lemphi2a: :: FIELD_13:36

for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for b being bag of card T
for x being b₃ -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))

proof end;

Lm7: for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for p being Polynomial of (card T),F st ex b being bag of card T st Support p = {b} holds
for x being b₃ -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T))

proof end;

theorem lemphi2b: :: FIELD_13:37

for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for p being Polynomial of (card T),F
for x being b₃ -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T))

proof end;

lemphi2: for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for x being b₃ -evaluating Function of (card T),E holds rng (hom_Ext_eval (x,F)) c= the carrier of (RAdj (F,T))

proof end;

lemphi4aa: for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for x being b₃ -evaluating Function of (card T),E holds Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T)

proof end;

lemphi4ab: for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for x being b₃ -evaluating Function of (card T),E holds T is Subset of the carrier of (Image_hom_Ext_eval (x,F))

proof end;

lemring: now :: thesis: for R, S, T being Ring st R is Subring of S & S is Subring of T holds
R is Subring of T

let R, S, T be Ring; :: thesis: ( R is Subring of S & S is Subring of T implies R is Subring of T )
assume AS: ( R is Subring of S & S is Subring of T ) ; :: thesis: R is Subring of T
then H: ( the carrier of R c= the carrier of S & the carrier of S c= the carrier of T ) by C0SP1:def 3;
then J: [: the carrier of R, the carrier of R:] c= [: the carrier of S, the carrier of S:] by ZFMISC_1:96;
A: the carrier of R c= the carrier of T by H;
B: the addF of R = the addF of S || the carrier of R by AS, C0SP1:def 3
.= ( the addF of T || the carrier of S) || the carrier of R by AS, C0SP1:def 3
.= the addF of T || the carrier of R by J, FUNCT_1:51 ;
C: the multF of R = the multF of S || the carrier of R by AS, C0SP1:def 3
.= ( the multF of T || the carrier of S) || the carrier of R by AS, C0SP1:def 3
.= the multF of T || the carrier of R by J, FUNCT_1:51 ;
D: 1. R = 1. S by AS, C0SP1:def 3
.= 1. T by AS, C0SP1:def 3 ;
0. R = 0. S by AS, C0SP1:def 3
.= 0. T by AS, C0SP1:def 3 ;
hence R is Subring of T by A, B, C, D, C0SP1:def 3; :: thesis: verum

end;

theorem lemphi4: :: FIELD_13:38

for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for x being b₃ -evaluating Function of (card T),E holds RAdj (F,T) = Image_hom_Ext_eval (x,F)

proof end;

theorem help2m: :: FIELD_13:39

for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for x being b₃ -evaluating Function of (card T),E holds the carrier of (RAdj (F,T)) = { (Ext_eval (p,x)) where p is Polynomial of (card T),F : verum }

proof end;

help2: for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for o being object st o in the carrier of (RAdj (F,T)) holds
ex p being Polynomial of (card T),F ex x being b₃ -evaluating Function of (card T),E st o = Ext_eval (p,x)

proof end;

theorem help1: :: FIELD_13:40

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

proof end;

registration

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

cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty total quasi_total additive unity-preserving RingHomomorphism endomorphism multiplicative R -fixing for Element of bool [: the carrier of S, the carrier of S:];

existence
ex b₁ being Homomorphism of S st b₁ is R -fixing

proof end;

cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total quasi_total additive unity-preserving RingHomomorphism monomorphism endomorphism multiplicative R -fixing for Element of bool [: the carrier of S, the carrier of S:];

existence
ex b₁ being Monomorphism of S st b₁ is R -fixing

proof end;

cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total quasi_total onto bijective additive unity-preserving RingHomomorphism monomorphism epimorphism isomorphism endomorphism multiplicative R -fixing for Element of bool [: the carrier of S, the carrier of S:];

existence
ex b₁ being Automorphism of S st b₁ is R -fixing

proof end;

end;

theorem fixp: :: FIELD_13:41

for F being Field
for E being FieldExtension of F
for K being FieldExtension of E
for p being Element of the carrier of (Polynom-Ring F)
for h being b₁ -fixing Homomorphism of E,K holds (PolyHom h) . p = p

proof end;

theorem fixeval: :: FIELD_13:42

for F being Field
for E being FieldExtension of F
for K being FieldExtension of E
for p being Element of the carrier of (Polynom-Ring F)
for a being Element of E
for h being b₁ -fixing Homomorphism of E,K holds h . (Ext_eval (p,a)) = Ext_eval (p,(h . a))

proof end;

theorem fixrr: :: FIELD_13:43

for F being Field
for E being FieldExtension of F
for h being b₁ -fixing Monomorphism of E
for p being non zero Element of the carrier of (Polynom-Ring F) holds h .: (Roots (E,p)) = Roots (E,p)

proof end;

theorem fixr: :: FIELD_13:44

for F being Field
for E being b₁ -algebraic FieldExtension of F
for h being b₁ -fixing Monomorphism of E holds the carrier of E c= rng h

proof end;

theorem iso: :: FIELD_13:45

for F being Field
for E being b₁ -algebraic FieldExtension of F
for h being b₁ -fixing Monomorphism of E holds h is Automorphism of E

proof end;

registration

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

cluster Function-like quasi_total monomorphism F -fixing -> isomorphism F -fixing for Element of bool [: the carrier of E, the carrier of E:];

coherence
for b₁ being F -fixing Monomorphism of E holds b₁ is isomorphism by iso;

end;

theorem ll: :: FIELD_13:46

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for T being b₁ -algebraic Subset of E holds h .: T is F -algebraic

proof end;

Lm10: for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for T being non empty finite Subset of E
for b being bag of card T st ex o being set st support b = {o} holds
for x being b₅ -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))

proof end;

theorem Lm9: :: FIELD_13:47

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for T being non empty finite Subset of E
for b being bag of card T
for x being b₅ -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))

proof end;

Lm8: for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for T being non empty finite Subset of E
for p being Polynomial of (card T),F st ex b being bag of card T st Support p = {b} holds
for x being b₅ -evaluating Function of (card T),E holds h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T)))

proof end;

theorem help3: :: FIELD_13:48

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for T being non empty finite Subset of E
for p being Polynomial of (card T),F
for x being b₅ -evaluating Function of (card T),E holds h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T)))

proof end;

theorem lemNor2ch: :: FIELD_13:49

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for T being non empty finite b₁ -algebraic Subset of E holds h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T)))

proof end;

theorem :: FIELD_13:50

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for T being finite b₁ -algebraic Subset of K st T c= the carrier of E holds
FAdj (F,T) is Subfield of E

proof end;

theorem lemh: :: FIELD_13:51

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for h being b₁ -fixing Homomorphism of E,K
for T being finite b₁ -algebraic Subset of E st h .: T c= the carrier of E holds
FAdj (F,(h .: T)) is Subfield of E

proof end;

theorem lemNor2c: :: FIELD_13:52

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for T being non empty finite b₁ -algebraic Subset of E st h .: T c= the carrier of E holds
h .: the carrier of (FAdj (F,T)) c= the carrier of E

proof end;

theorem lemNor2b: :: FIELD_13:53

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
for p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
h .: (Roots (E,p)) c= the carrier of E

proof end;

definition

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

attr E is F -normal means :: FIELD_13:def 5
( E is F -algebraic & ( for p being irreducible Element of the carrier of (Polynom-Ring F) st p is_with_roots_in E holds
p splits_in E ) );

end;

:: deftheorem defines -normal FIELD_13:def 5 :
for F being Field
for E being FieldExtension of F holds
( E is F -normal iff ( E is F -algebraic & ( for p being irreducible Element of the carrier of (Polynom-Ring F) st p is_with_roots_in E holds
p splits_in E ) ) );

registration

let F be Field;

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

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

end;

lemmin: for F being Field
for E being b₁ -algebraic FieldExtension of F holds
( E is F -normal iff for a being Element of E holds MinPoly (a,F) splits_in E )

proof end;

registration

let F be Field;

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

coherence
for b₁ being FieldExtension of F st b₁ is F -quadratic holds
b₁ is F -normal

proof end;

cluster -> F -normal for AlgebraicClosure of F;

coherence
for b₁ being AlgebraicClosure of F holds b₁ is F -normal

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 zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID F -homomorphic Polynom-Ring F -homomorphic factorial F -monomorphic F -extending F -algebraic gcd-like F -normal for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st
( b₁ is F -algebraic & b₁ is F -normal )

proof end;

end;

registration

cluster FieldAdjunction (F_Rat,{3-Root(2)}) -> non F_Rat -normal ;

coherence
not FAdj (F_Rat,{3-Root(2)}) is F_Rat -normal

proof end;

end;

theorem :: FIELD_13:54

for F being Field
for E being b₁ -algebraic FieldExtension of F holds
( E is F -normal iff for a being Element of E holds MinPoly (a,F) splits_in E ) by lemmin;

lemNor1: for F being Field
for E being b₁ -finite FieldExtension of F st E is F -normal holds
ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p

proof end;

lemNor2: for F being Field
for E being b₁ -finite FieldExtension of F st ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p holds
for K being FieldExtension of E
for h being b₁ -fixing Monomorphism of E,K holds h is Automorphism of E

proof end;

lemNor31: for F being Field
for E being FieldExtension of F
for T being Subset of E
for a being Element of E st a in the carrier of (FAdj (F,T)) holds
FAdj (F,(T \/ {a})) = FAdj (F,T)

proof end;

lemNor3: for F being Field
for E being b₁ -finite FieldExtension of F st ( for K being FieldExtension of E
for h being b₁ -fixing Monomorphism of E,K holds h is Automorphism of E ) holds
E is F -normal

proof end;

theorem main1: :: FIELD_13:55

for F being Field
for E being b₁ -finite FieldExtension of F holds
( E is F -normal iff ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p )

proof end;

theorem :: FIELD_13:56

for F being Field
for E being b₁ -finite FieldExtension of F holds
( E is F -normal iff for K being FieldExtension of E
for h being b₁ -fixing Monomorphism of E,K holds h is Automorphism of E )

proof end;

registration

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

cluster -> F -normal for SplittingField of p;

coherence
for b₁ being SplittingField of p holds b₁ is F -normal by main1;

end;

theorem :: FIELD_13:57

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

proof end;

theorem :: FIELD_13:58

for F being Field
for E being FieldExtension of F
for T being non empty finite b₁ -algebraic Subset of E holds
( FAdj (F,T) is F -normal iff for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) )

proof end;