FIELD_14: Simple Extensions

end;

registration

let n be Element of NAT ;

cluster n -' 1 -> natural ;

proof end;

end;

registration

let R be Ring;
let n be Nat;

reduce n * (0. R) to 0. R;

reducibility

proof end;

end;

registration

cluster -> nonnegative-yielding for FinSequence of NAT ;

proof end;

end;

theorem lembag2b: :: FIELD_14:1

for f being FinSequence of NAT
for i, j being Nat st i in dom f & j in dom f & i <> j holds
Sum f >= (f . i) + (f . j)

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;
:: original: {
redefine func {a,b} -> F -algebraic Subset of E;
coherence

proof end;

end;

registration

let F be Field;
let K be FieldExtension of F;
let E be K -extending FieldExtension of F;

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

proof end;

end;

registration

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

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

end;

registration

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

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID Euclidian F -homomorphic factorial F -monomorphic F -extending K -extending F -finite gcd-like for doubleLoopStr ;

proof end;

end;

registration

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

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 unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID Euclidian F -homomorphic factorial F -monomorphic F -extending E -extending K -extending gcd-like for doubleLoopStr ;

proof end;

end;

theorem simp1: :: FIELD_14:2

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

proof end;

theorem mm5a: :: FIELD_14:3

for R being Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S
for n being Element of NAT st a = b holds
n * a = n * b

proof end;

definition

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

func IntermediateFields (E,F) -> set means :defY: :: FIELD_14:def 1
for x being object holds
( x in it iff ex K being strict Field st
( K = x & F is Subfield of K & K is Subfield of E ) );

proof end;

uniqueness

proof end;

end;

:: deftheorem defY defines IntermediateFields FIELD_14:def 1 :

registration

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

cluster IntermediateFields (E,F) -> non empty Field-membered ;

proof end;

end;

theorem simp3: :: FIELD_14:4

for F being Field
for E being FieldExtension of F
for K being strict Field holds
( K in IntermediateFields (E,F) iff ( F is Subfield of K & K is Subfield of E ) )

proof end;

theorem simp2: :: FIELD_14:5

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F holds IntermediateFields (E,F) c= IntermediateFields (K,F)

proof end;

definition

let Z be non empty set ;
let B be bag of Z;
:: original: Sum
redefine func card B -> Element of NAT ;
coherence

proof end;

end;

theorem bag1a: :: FIELD_14:6

for Z being non empty set
for B1, B2 being bag of Z holds
( B1 divides B2 iff ex B3 being bag of Z st B2 = B1 + B3 )

proof end;

theorem bag1: :: FIELD_14:7

for Z being non empty set
for B1, B2 being bag of Z st B1 divides B2 holds
card B1 <= card B2

proof end;

theorem bag2a: :: FIELD_14:8

for Z being non empty set
for B being bag of Z
for o being object holds B . o <= card B

proof end;

theorem bag2b: :: FIELD_14:9

for Z being non empty set
for B being bag of Z
for o1, o2 being object st B . o1 = card B & o2 <> o1 holds
B . o2 = 0

proof end;

theorem bag2: :: FIELD_14:10

for R being domRing
for B1 being bag of the carrier of R holds
( card B1 = 1 iff ex a being Element of R st B1 = Bag {a} )

proof end;

theorem :: FIELD_14:11

for F being Field
for B1, B2 being non zero bag of the carrier of F st B2 divides B1 & card B1 = 1 holds
B2 = B1

proof end;

theorem bag6: :: FIELD_14:12

for Z being non empty set
for B1, B2 being bag of Z st B2 divides B1 & B1 -' B2 is zero holds
B2 = B1

proof end;

theorem bagset1: :: FIELD_14:13

for F being Field
for S1, S2 being non empty finite Subset of F holds
( Bag S1 divides Bag S2 iff S1 c= S2 )

proof end;

theorem bagset2: :: FIELD_14:14

for F being Field
for B being non zero bag of the carrier of F
for S1 being non empty finite Subset of F holds
( B divides Bag S1 iff ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) )

proof end;

registration

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

cluster p * q -> non constant ;

proof end;

end;

theorem ZZ3y: :: FIELD_14:15

for F being Field
for p being monic Polynomial of F
for r being Polynomial of F st p *' r is monic holds
r is monic

proof end;

theorem lemconst: :: FIELD_14:16

for R being domRing
for p being Polynomial of R holds
( ( p is monic & p is constant ) iff p = 1_. R )

proof end;

theorem lemrpoly: :: FIELD_14:17

for R being domRing
for a being Element of R
for m being non zero Nat holds (rpoly (1,a)) `^ m is Ppoly of R

proof end;

theorem multi00: :: FIELD_14:18

for F being Field
for p being Polynomial of F
for E being FieldExtension of F
for q being Polynomial of E
for n being Element of NAT st q = p holds
q `^ n = p `^ n

proof end;

theorem multi0: :: FIELD_14:19

for F being Field
for p being Polynomial of F
for i, j being Element of NAT holds p `^ (i + j) = (p `^ i) *' (p `^ j)

proof end;

theorem simpAgcd2: :: FIELD_14:20

for F being Field
for a being Element of F
for p being Ppoly of F,{a} holds p = rpoly (1,a)

proof end;

theorem bag5: :: FIELD_14:21

for F being Field
for B1, B2 being non zero bag of the carrier of F
for p being Ppoly of F,B1
for q being Ppoly of F,B2 st B1 = B2 holds
p = q

proof end;

theorem co: :: FIELD_14:22

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 q = p holds
Coeff q = Coeff p

proof end;

theorem ZZ7: :: FIELD_14:23

for F being Field
for p, q being non zero Polynomial of F
for a being Element of F holds multiplicity (p,a) <= multiplicity ((p *' q),a)

proof end;

theorem extsubst: :: FIELD_14:24

for F being Field
for E being FieldExtension of F
for p, q being Polynomial of F
for p1, q1 being Polynomial of E st p1 = p & q1 = q holds
Subst (p1,q1) = Subst (p,q)

proof end;

theorem extevalsubst: :: FIELD_14:25

for F being Field
for p, q being Polynomial of F
for E being FieldExtension of F
for a being Element of E holds Ext_eval ((Subst (p,q)),a) = Ext_eval (p,(Ext_eval (q,a)))

proof end;

theorem exteval2: :: FIELD_14:26

for F being Field
for a, b being Element of F
for E being FieldExtension of F
for x being Element of E holds Ext_eval (<%a,b%>,x) = (@ (a,E)) + ((@ (b,E)) * x)

proof end;

ro1: for R being non degenerated comRing
for p, q being Polynomial of R
for a being Element of R st a is_a_root_of p holds
a is_a_root_of p *' q

proof end;

theorem ZZ1f: :: FIELD_14:27

for R being non degenerated comRing
for p, q being Polynomial of R holds Roots p c= Roots (p *' q)

proof end;

ZZ1e: for F being Field
for p, q being non zero Polynomial of F
for a being Element of F st a is_a_root_of p *' q & not a is_a_root_of p holds
a is_a_root_of q

proof end;

theorem r58: :: FIELD_14:28

for R being domRing
for S1, S2 being non empty finite Subset of R
for p being Ppoly of R,S1
for q being Ppoly of R,S2 st S1 /\ S2 = {} holds
p *' q is Ppoly of R,(S1 \/ S2)

proof end;

theorem ZZ1d: :: FIELD_14:29

for F being Field
for p, q being non zero Polynomial of F st ( for a being Element of F st a is_a_root_of p *' q holds
multiplicity ((p *' q),a) = 1 ) holds
(Roots p) /\ (Roots q) = {}

proof end;

theorem ZZ1: :: FIELD_14:30

for F being Field
for p being Ppoly of F holds
( p is Ppoly of F,(Roots p) iff for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 )

proof end;

theorem ZZ1a: :: FIELD_14:31

for F being Field
for S being non empty finite Subset of F
for p being Ppoly of F,S
for q being non zero with_roots Polynomial of F st p *' q is Ppoly of F,(S \/ (Roots q)) holds
q is Ppoly of F,(Roots q)

proof end;

theorem r59a: :: FIELD_14:32

for F being Field
for S being non empty finite Subset of F
for a being Element of F
for p being Ppoly of F,(S \/ {a})
for q being non constant Polynomial of F st p = (rpoly (1,a)) *' q & not a in S holds
q is Ppoly of F,S

proof end;

ZZ3b: for R being domRing
for p, q being Polynomial of R st q divides p holds
Roots q c= Roots p

proof end;

theorem r59: :: FIELD_14:33

for F being Field
for S1, S2 being non empty finite Subset of F
for p being Ppoly of F,S1
for a being Element of F
for q being non constant Polynomial of F st p = (rpoly (1,a)) *' q & S2 = S1 \ {a} holds
q is Ppoly of F,S2

proof end;

definition

let R, S be non degenerated comRing;
let p be Polynomial of R;

pred p is_square-free_over S means :: FIELD_14:def 2
for q1 being non constant Polynomial of S
for q2 being Polynomial of S holds
( not q2 = p or not q1 `^ 2 divides q2 );

end;

:: deftheorem defines is_square-free_over FIELD_14:def 2 :

definition

let R be non degenerated comRing;
let p be Polynomial of R;

attr p is square-free means :: FIELD_14:def 3
p is_square-free_over R;

end;

:: deftheorem defines square-free FIELD_14:def 3 :

lemsq: for R being non degenerated comRing
for p being Polynomial of R holds
( p is square-free iff for q being non constant Polynomial of R holds not q `^ 2 divides p )

proof end;

registration

let R be domRing;

cluster Relation-like -defined -valued Function-like quasi_total finite-Support non zero non constant square-free for Element of bool [:omega, the carrier of R:];

proof end;

cluster Relation-like -defined -valued Function-like quasi_total finite-Support non zero non constant non square-free for Element of bool [:omega, the carrier of R:];

proof end;

end;

theorem :: FIELD_14:34

for R being non degenerated comRing
for p being Polynomial of R holds
( p is square-free iff for q being non constant Polynomial of R holds not q `^ 2 divides p ) by lemsq;

theorem ZZ3x: :: FIELD_14:35

for F being Field
for p being monic Polynomial of F st p divides 1_. F holds
p = 1_. F

proof end;

theorem ZZ1fB: :: FIELD_14:36

for F being Field
for p, q being non zero Polynomial of F holds BRoots p divides BRoots (p *' q)

proof end;

theorem :: FIELD_14:37

for R being domRing
for p, q being Polynomial of R st q divides p holds
Roots q c= Roots p by ZZ3b;

theorem ZZ3z: :: FIELD_14:38

for F being Field
for p, q being Polynomial of F
for r being non zero Polynomial of F st r *' q divides r *' p holds
q divides p

proof end;

theorem ZZ2: :: FIELD_14:39

for F being Field
for p, q being Polynomial of F
for r being monic Polynomial of F holds (r *' p) gcd (r *' q) = r *' (p gcd q)

proof end;

theorem multi1: :: FIELD_14:40

for F being Field
for p, q being Polynomial of F
for n, k being Element of NAT st q `^ n divides p & k <= n holds
q `^ k divides p

proof end;

theorem hirr: :: FIELD_14:41

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 q = p & q is irreducible holds
p is irreducible

proof end;

theorem lemgcd0a: :: FIELD_14:42

for R being gcdDomain
for a being Element of R holds a is a_gcd of a, 0. R

proof end;

lemgcd0: for R being gcdDomain
for a being Element of R
for g being a_gcd of a, 0. R holds g is_associated_to a

proof end;

theorem lemgcdii: :: FIELD_14:43

for R being EuclidianRing
for a, b being Element of R
for g being a_gcd of a,b ex r, s being Element of R st g = (a * r) + (b * s)

proof end;

theorem lemgcdi: :: FIELD_14:44

for R being EuclidianRing
for a, b being Element of R
for g being a_gcd of a,b holds {g} -Ideal = {a,b} -Ideal

proof end;

lemgcdh: for F being Field
for p, q being Element of (Polynom-Ring F) ex a, b being Element of (Polynom-Ring F) st p gcd q = (a * p) + (b * q)

proof end;

theorem lemgcd: :: FIELD_14:45

for F being Field
for E being FieldExtension of F
for p, q being Element of the carrier of (Polynom-Ring F)
for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
p1 gcd q1 = p gcd q

proof end;

theorem :: FIELD_14:46

for F being Field
for p being Element of the carrier of (Polynom-Ring F) holds p gcd (0_. F) = NormPolynomial p

proof end;

theorem lemgcdn: :: FIELD_14:47

for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for q being non zero Element of the carrier of (Polynom-Ring F) st q divides p holds
p gcd q = NormPolynomial q

proof end;

theorem :: FIELD_14:48

proof end;

theorem ppolydiv: :: FIELD_14:49

for F being Field
for B1 being non zero bag of the carrier of F
for p being Ppoly of F,B1
for q being non constant monic Polynomial of F holds
( q divides p iff ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) )

proof end;

theorem simpAgcd1: :: FIELD_14:50

for F being Field
for S1 being non empty finite Subset of F
for p being Ppoly of F,S1
for q being non constant monic Polynomial of F holds
( q divides p iff ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) )

proof end;

theorem r59Bag: :: FIELD_14:51

for F being Field
for p being Ppoly of F
for q being monic Polynomial of F
for a being Element of F holds
( q divides (rpoly (1,a)) *' p iff ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) )

proof end;

theorem ZZ3: :: FIELD_14:52

for F being Field
for p being Ppoly of F
for q being Polynomial of F holds
( (Roots p) /\ (Roots q) = {} iff p gcd q = 1_. F )

proof end;

theorem simpAgcd: :: FIELD_14:53

for F being Field
for S1, S2 being non empty finite Subset of F
for p1 being Ppoly of F,S1
for p2 being Polynomial of F st S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2

proof end;

definition

let R be domRing;
let p be Polynomial of R;

func Divisors p -> non empty Subset of the carrier of (Polynom-Ring R) equals :: FIELD_14:def 4
{ q where q is Element of the carrier of (Polynom-Ring R) : q divides p } ;

proof end;

func MonicDivisors p -> non empty Subset of the carrier of (Polynom-Ring R) equals :: FIELD_14:def 5
{ q where q is monic Element of the carrier of (Polynom-Ring R) : q divides p } ;

proof end;

end;

:: deftheorem defines Divisors FIELD_14:def 4 :

:: deftheorem defines MonicDivisors FIELD_14:def 5 :

theorem divfin2h: :: FIELD_14:54

for F being Field
for a being Element of F holds MonicDivisors (rpoly (1,a)) = {(1_. F),(rpoly (1,a))}

proof end;

divfin2: for F being Field
for p being Ppoly of F ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) )

proof end;

theorem diveq: :: FIELD_14:55

for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F)
for a being non zero Element of F holds MonicDivisors p = MonicDivisors (a * p)

proof end;

theorem divfin1: :: FIELD_14:56

for F being Field
for E being FieldExtension of F
for p being Polynomial of F
for q being Polynomial of E st q = p holds
MonicDivisors p c= MonicDivisors q

proof end;

registration

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

cluster MonicDivisors p -> non empty finite ;

proof end;

end;

theorem :: FIELD_14:57

for F being Field
for p being non zero Polynomial of F holds card (MonicDivisors p) <= 2 |^ (deg p)

proof end;

notation

let R be Ring;
synonym Deriv R for Der1 R;

end;

registration

let R be domRing;

cluster Deriv R -> derivation ;

end;

theorem der1: :: FIELD_14:58

for R being non degenerated comRing holds
( (Deriv R) . (1_. R) = 0_. R & (Deriv R) . (0_. R) = 0_. R )

proof end;

theorem der3: :: FIELD_14:59

for R being Ring
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds (Deriv R) . (a * p) = a * ((Deriv R) . p)

proof end;

theorem der4: :: FIELD_14:60

for R being non degenerated comRing
for p being constant Element of the carrier of (Polynom-Ring R) holds (Deriv R) . p = 0_. R

proof end;

theorem :: FIELD_14:61

for R being Ring
for a being Element of R holds (Deriv R) . (X- a) = 1_. R

proof end;

theorem :: FIELD_14:62

for R being non degenerated comRing
for p being Element of the carrier of (Polynom-Ring R) holds (Deriv R) . (p |^ 0) = 0_. R

proof end;

theorem :: FIELD_14:63

for R being domRing
for p being Element of the carrier of (Polynom-Ring R)
for n being non zero Element of NAT holds (Deriv R) . (p |^ n) = n * ((p |^ (n - 1)) * ((Deriv R) . p))

proof end;

theorem mm6a: :: FIELD_14:64

for R being non degenerated comRing
for p being non zero Element of the carrier of (Polynom-Ring R) holds deg ((Deriv R) . p) < deg p

proof end;

theorem mm4i: :: FIELD_14:65

for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F) st p gcd ((Deriv F) . p) = 1_. F holds
p is square-free

proof end;

theorem mm5: :: FIELD_14:66

for R being non degenerated comRing
for p being Element of the carrier of (Polynom-Ring R)
for S being comRingExtension of R
for q being Element of the carrier of (Polynom-Ring S) st q = p holds
(Deriv S) . q = (Deriv R) . p

proof end;

definition

let R be non degenerated comRing;
let S be comRingExtension of R;
let p be non zero Polynomial of R;
let a be Element of S;

func multiplicity (p,a) -> Element of NAT means :defM: :: FIELD_14:def 6
ex q being non zero Polynomial of S st
( q = p & it = multiplicity (q,a) );

proof end;

uniqueness ;

end;

:: deftheorem defM defines multiplicity FIELD_14:def 6 :

theorem multi2: :: FIELD_14:67

for F being Field
for p being non zero Polynomial of F
for a being Element of F
for n being Element of NAT holds
( n = multiplicity (p,a) iff ( (X- a) `^ n divides p & not (X- a) `^ (n + 1) divides p ) )

proof end;

theorem mm6c: :: FIELD_14:68

for F being 0 -characteristic Field
for p being non zero Element of the carrier of (Polynom-Ring F) holds deg ((Deriv F) . p) = (deg p) - 1

proof end;

theorem mm6b: :: FIELD_14:69

for F being 0 -characteristic Field
for p being Element of the carrier of (Polynom-Ring F) holds
( (Deriv F) . p = 0_. F iff p is constant )

proof end;

theorem mm6: :: FIELD_14:70

for F being 0 -characteristic Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds p gcd ((Deriv F) . p) = 1_. F

proof end;

theorem mpa1: :: FIELD_14:71

for F being 0 -characteristic Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1

proof end;

definition

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

attr E is F -simple means :defsimp: :: FIELD_14:def 7
ex a being Element of E st E == FAdj (F,{a});

end;

:: deftheorem defsimp defines -simple FIELD_14:def 7 :

definition

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

attr a is F -primitive means :: FIELD_14:def 8
E == FAdj (F,{a});

end;

:: deftheorem defines -primitive FIELD_14:def 8 :

registration end;

registration

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

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non irreducible F -primitive for Element of the carrier of E;

proof end;

end;

definition

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

func deg (a,F) -> Integer equals :: FIELD_14:def 9
deg ((FAdj (F,{a})),F);

end;

:: deftheorem defines deg FIELD_14:def 9 :

theorem :: FIELD_14:72

for F being Field
for E being b₁ -finite FieldExtension of F
for a being Element of E holds deg (a,F) divides deg (E,F)

proof end;

theorem :: FIELD_14:73

for F being Field
for E being b₁ -finite FieldExtension of F holds
( E is F -simple iff ex a being Element of E st deg (a,F) = deg (E,F) )

proof end;

theorem :: FIELD_14:74

for F being Field
for E being b₁ -finite FieldExtension of F
for a being Element of E holds
( a is F -primitive iff deg (a,F) = deg (E,F) )

proof end;

theorem simpmainhelp: :: FIELD_14:75

for F being Field
for K being b₁ -finite FieldExtension of F
for E being b₁ -extending b₁ -finite FieldExtension of F
for a being b₂ -algebraic Element of E st E == FAdj (F,{a}) holds
( E == FAdj (K,{a}) & K == FAdj (F,(Coeff (MinPoly (a,K)))) )

proof end;

theorem :: FIELD_14:76

for F being infinite Field
for E being b₁ -finite FieldExtension of F holds
( E is F -simple iff IntermediateFields (E,F) is finite )

proof end;

theorem simpA: :: FIELD_14:77

for F being 0 -characteristic Field
for E being FieldExtension of F
for a, b being b₁ -algebraic Element of E ex x being Element of F st FAdj (F,{a,b}) = FAdj (F,{(a + ((@ (x,E)) * b))})

proof end;

registration

let F be 0 -characteristic Field;

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