:: Characterization of Finite {G}alois Extensions
:: by Christoph Schwarzweller
::
:: Received December 21, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies ARYTM_3, VECTSP_1, TARSKI, STRUCT_0, SUBSET_1, SUPINF_2, CAT_1,
POLYNOM1, TOPGEN_1, MESFUNC1, FDIFF_1, FUNCSDOM, EC_PF_1, HURWITZ,
CARD_1, RING_2, FUNCT_1, RELAT_1, NUMBERS, POLYNOM5, FOMODEL1, FIELD_14,
SIN_COS, XCMPLX_0, FIELD_9, POLYNOM3, FINSEQ_1, YELLOW_8, ARYTM_1,
FIELD_4, C0SP1, FINSET_1, XBOOLE_0, XXREAL_0, GLIB_000, POLYNOM2,
REALSET1, FIELD_6, NAT_1, RING_5, VECTSP_2, UPROOTS, FIELD_8, GROUP_1,
ALGNUM_1, ALGSTR_0, RATFUNC1, CARD_3, RFINSEQ, GROUP_2, RING_3, CATALG_1,
ORDINAL4, AUTGROUP, MSSUBFAM, MOD_4, PARTFUN1, ZFMISC_1, FIELD_1,
FIELD_13, FIELD_15, RLSUB_1, GALOIS_0, GALOIS_1, GALOIS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FINSET_1, REALSET1,
FUNCT_1, FUNCT_2, BINOP_1, ORDINAL1, NUMBERS, CARD_1, PARTFUN1, XCMPLX_0,
XXREAL_0, NAT_1, FINSEQ_1, RFINSEQ, POLYNOM3, POLYNOM4, POLYNOM5,
ALGNUM_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_4, GROUP_6, MOD_4,
VECTSP_2, HURWITZ, VECTSP_1, C0SP1, EC_PF_1, RATFUNC1, RING_2, RING_3,
RING_4, RING_5, FIELD_1, FIELD_4, FIELD_5, FIELD_6, FIELD_7, FIELD_8,
FIELD_9, FIELD_13, FIELD_14, FIELD_15, GALOIS_0, GALOIS_1;
constructors ABIAN, POLYNOM4, REALSET1, GROUP_4, RINGCAT1, ALGNUM_1, RFINSEQ,
RING_5, FIELD_8, FIELD_9, FIELD_13, FIELD_15, GALOIS_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XXREAL_0, XREAL_0,
NAT_1, INT_1, MEMBERED, SUBSET_1, STRUCT_0, VECTSP_1, FINSET_1, VECTSP_2,
FUNCT_2, FUNCT_1, CARD_1, RATFUNC1, MOD_4, FINSEQ_1, RELAT_1, RINGCAT1,
UPROOTS, RING_4, RING_5, GROUP_2, POLYNOM3, FIELD_1, FIELD_4, FIELD_5,
FIELD_6, FIELD_7, FIELD_8, FIELD_9, FIELD_12, FIELD_13, FIELD_14,
FIELD_15, FIELD_16, GALOIS_0, GALOIS_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, POLYNOM3, FINSEQ_1, RING_4,
FIELD_9, GALOIS_1;
expansions STRUCT_0, GROUP_1, VECTSP_1, TARSKI, GROUP_6, FUNCT_1, FUNCT_2,
FIELD_7, FIELD_8, GALOIS_1;
theorems GROUP_1, VECTSP_1, VECTSP_2, RLVECT_1, C0SP1, FIELD_10, REALALG3,
FUNCT_2, TARSKI, FUNCT_1, EC_PF_1, RING_3, RATFUNC1, POLYNOM5, UPROOTS,
RING_4, RING_5, HURWITZ, XREAL_1, INT_1, XBOOLE_0, FIELD_4, POLYNOM3,
FUNCT_7, NIVEN, ZFMISC_1, XXREAL_0, FIELD_6, CARD_2, FINSEQ_2, FIELD_7,
FINSEQ_1, GROUP_4, FIELD_5, FIELD_14, FIELD_8, POLYNOM4, NAT_1, RING_2,
GROUP_6, FIELD_1, PARTFUN1, RELAT_1, XBOOLE_1, FIELD_13, GROUP_2,
FINSEQ_5, FIELD_15, FIELD_16, STRUCT_0, ALGNUM_1, FINSEQ_6, RFINSEQ,
GALOIS_0, GALOIS_1;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
definition
let X,Y be non empty set;
let f be Function of X,Y;
let S be non empty finite Subset of X;
redefine func f.:S -> non empty finite Subset of Y; :: redefines .: (FUNCT_1, redefinition) → .: (RELAT_1, definition)
coherence
proof
reconsider M = f.:S as Subset of Y;
set x = the Element of S;
f.x in Y & dom f = X by FUNCT_2:def 1;
then f.x in M by FUNCT_1:def 6;
hence thesis;
end;
end;
theorem
for F being Field
for g1,g2 being Element of Aut(F)
for f1,f2 being Automorphism of F
st g1 = f1 & g2 = f2 holds g1 * g2 = f1 * f2 by GALOIS_1:def 2;
theorem
for F being Field
for g being Element of Aut(F)
for f being Automorphism of F st g = f holds g" = f"
proof
let F be Field, g be Element of Aut(F), f be Automorphism of F;
assume A: g = f;
f" in the set of all f where f is Automorphism of F; then
reconsider g1 = f" as Element of Aut(F);
H: rng f = the carrier of F by FUNCT_2:def 3;
B: g1 * g = f" * f by A,GALOIS_1:def 2
.= id F by H,FUNCT_2:29
.= 1_Aut(F) by GALOIS_1:6;
g * g1 = f * f" by A,GALOIS_1:def 2
.= id F by H,FUNCT_2:29
.= 1_Aut(F) by GALOIS_1:6;
hence thesis by B,GROUP_1:def 5;
end;
theorem G3b:
for F being Field
for E being FieldExtension of F
for g1,g2 being Element of Aut(E,F)
for f1,f2 being F-fixing Automorphism of E
st g1 = f1 & g2 = f2 holds g1 * g2 = f1 * f2
proof
let F be Field, E be FieldExtension of F, g1,g2 be Element of Aut(E,F);
let f1,f2 be F-fixing Automorphism of E;
assume A: g1 = f1 & g2 = f2;
C: [g1,g2] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
thus g1 * g2 = (AutComp E).(g1,g2) by C,FUNCT_1:49
.= f1 * f2 by A,GALOIS_1:def 2;
end;
theorem G3a:
for F being Field
for E being FieldExtension of F
for g being Element of Aut(E,F)
for f being F-fixing Automorphism of E st g = f holds g" = f"
proof
let F be Field, E be FieldExtension of F, g be Element of Aut(E,F);
let f be F-fixing Automorphism of E;
assume A: g = f;
f" in the set of all f where f is F-fixing Automorphism of E; then
reconsider g1 = f" as Element of Aut(E,F);
H: rng f = the carrier of E by FUNCT_2:def 3;
B: g1 * g = f" * f by A,G3b
.= id E by H,FUNCT_2:29
.= 1_Aut(E) by GALOIS_1:6
.= 1_Aut(E,F) by GROUP_2:44;
g * g1 = f * f" by A,G3b
.= id E by H,FUNCT_2:29
.= 1_Aut(E) by GALOIS_1:6
.= 1_Aut(E,F) by GROUP_2:44;
hence thesis by B,GROUP_1:def 5;
end;
theorem rot:
for R being comRing
for S being comRingExtension of R
for p,q being Element of the carrier of Polynom-Ring R
holds q divides p implies Roots(S,q) c= Roots(S,p)
proof
let F be comRing, E be comRingExtension of F,
p,q be Element of the carrier of Polynom-Ring F;
assume q divides p; then
consider u being Polynomial of F such that AS: p = q *'u by RING_4:1;
H: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E} &
Roots(E,q) = {a where a is Element of E : a is_a_root_of q,E}
by FIELD_4:def 4;
now let o be object;
assume o in Roots(E,q); then
consider a being Element of E such that
B: o = a & a is_a_root_of q,E by H;
F is Subring of E by FIELD_4:def 1; then
Ext_eval(p,a) = Ext_eval(q,a) * Ext_eval(u,a) by AS,ALGNUM_1:20
.= 0.E * Ext_eval(u,a) by B,FIELD_4:def 2;
then a is_a_root_of p,E by FIELD_4:def 2;
hence o in Roots(E,p) by H,B;
end;
hence thesis;
end;
registration
let R be domRing;
let p be non zero Polynomial of R;
let q be non constant Polynomial of R;
cluster p *' q -> non constant;
coherence
proof
A: deg q > 0 by RATFUNC1:def 2;
p <> 0_.R & q <> 0_.R; then
deg(p *' q) = deg p + deg q by HURWITZ:23;
hence thesis by A,RATFUNC1:def 2;
end;
end;
registration
let R be domRing;
let p be non zero Element of the carrier of Polynom-Ring R;
let q be non constant Element of the carrier of Polynom-Ring R;
cluster p * q -> non constant;
coherence
proof
reconsider p1 = p as non zero Polynomial of R;
deg q > 0 by RING_4:def 4; then
reconsider q1 = q as non constant Polynomial of R by RATFUNC1:def 2;
H: p * q = p1 *' q1 by POLYNOM3:def 10;
deg(p1 *' q1) > 0 by RATFUNC1:def 2;
hence thesis by H,RING_4:def 4;
end;
end;
theorem R58:
for R being Ring
for S being RingExtension of R
for a being Element of R, b being Element of S holds Ext_eval(a|R,b) = a
proof
let R be Ring, S be RingExtension of R;
let a be Element of R, b be Element of S;
R is Subring of S by FIELD_4:def 1; then
the carrier of R c= the carrier of S by C0SP1:def 3; then
reconsider aS = a as Element of S;
H: a|R is Element of the carrier of Polynom-Ring R &
aS|S is Element of the carrier of Polynom-Ring S by POLYNOM3:def 10;
Ext_eval(a|R,b) = eval(aS|S,b) by H,FIELD_6:23,FIELD_4:26
.= aS by RING_5:8;
hence thesis;
end;
lemsepprodA:
for F being Field,
E being FieldExtension of F
for f being non empty FinSequence of the carrier of Polynom-Ring F
for q being Polynomial of F
for a being Element of E
st q = Product f &
for i being Element of dom f,
p being Polynomial of F st p = f.i holds Ext_eval(p,a) <> 0.E
holds Ext_eval(q,a) <> 0.E
proof
let F be Field, E be FieldExtension of F;
let f be non empty FinSequence of the carrier of Polynom-Ring F;
let q be Polynomial of F; let a be Element of E;
assume AS: q = Product f &
for i being Element of dom f,
p being Polynomial of F st p = f.i holds Ext_eval(p,a) <> 0.E;
defpred P[Nat] means
for f being non empty FinSequence of the carrier of Polynom-Ring F
for q being Polynomial of F for a being Element of E
st q = Product f & len f = $1 &
for i being Element of dom f,
p being Polynomial of F st p = f.i holds Ext_eval(p,a) <> 0.E
holds Ext_eval(q,a) <> 0.E;
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
now let f be non empty FinSequence of Polynom-Ring F;
let p be Element of the carrier of Polynom-Ring F;
let a be Element of E;
assume A1: p = Product f & len f = k+1 &
for i being Element of dom f,
q being Polynomial of F st q = f.i holds Ext_eval(q,a) <> 0.E;
consider g being FinSequence of the carrier of Polynom-Ring F,
r1 being Element of the carrier of Polynom-Ring F such that
A3: f = g ^ <*r1*> by A1,FINSEQ_2:19;
A4: len f = len g + 1 by A3,FINSEQ_2:16;
reconsider q = Product g, r2 = r1
as Polynomial of F by POLYNOM3:def 10;
A5: p = (Product g) * r1 by A1,A3,GROUP_4:6
.= q *' r2 by POLYNOM3:def 10;
F is Subring of E by FIELD_4:def 1; then
A8: Ext_eval(p,a) = Ext_eval(q,a) * Ext_eval(r2,a) by A5,ALGNUM_1:20;
A6: f.(len f) = r2 & 1 <= len f by A3,A4,FINSEQ_1:42,FINSEQ_1:20;
then len f in Seg(len f);
then A7: len f in dom f by FINSEQ_1:def 3; then
A9: Ext_eval(r2,a) <> 0.E by A6,A1;
per cases;
suppose g = {}; then
g = <*>(the carrier of Polynom-Ring F); then
q = 1_(Polynom-Ring F) by GROUP_4:8 .= 1_.F by POLYNOM3:def 10;
hence Ext_eval(p,a) <> 0.E by A5,A7,A6,A1;
end;
suppose g <> {}; then
reconsider g as non empty FinSequence of the carrier of Polynom-Ring F;
now let i be Element of dom g, r be Polynomial of F;
assume B1: r = g.i;
i in dom g; then
i in Seg(len g) by FINSEQ_1:def 3; then
B3: 1 <= i & i <= len g by FINSEQ_1:1; then
i + 0 < len f by A4,XREAL_1:8; then
i in Seg(len f) by B3; then
B4: i in dom f by FINSEQ_1:def 3;
r = f.i by A3,B1,FINSEQ_1:def 7;
hence Ext_eval(r,a) <> 0.E by B4,A1;
end;
then Ext_eval(q,a) <> 0.E by A4,A1,IV;
hence Ext_eval(p,a) <> 0.E by A9,A8,VECTSP_2:def 1;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: len f = n;
thus thesis by I,H,AS;
end;
theorem
for F being Field,
E being FieldExtension of F
for f being non empty FinSequence of the carrier of Polynom-Ring F
for q being Polynomial of F st q = Product f
for a being Element of E
holds Ext_eval(q,a) = 0.E iff
ex i being Element of dom f,
p being Polynomial of F st p = f.i & Ext_eval(p,a) = 0.E
by FIELD_13:4,lemsepprodA;
theorem sepprodB:
for F being Field
for f being FinSequence of Polynom-Ring F
for p,q being Element of the carrier of Polynom-Ring F
st p = Product f & ex i being Nat st 1 <= i & i <= len f & f.i = q
holds q divides p
proof
let F be Field, f be FinSequence of Polynom-Ring F;
let p,q be Element of the carrier of Polynom-Ring F;
assume A: p = Product f & ex i being Nat st 1 <= i & i <= len f & f.i = q;
then consider i being Nat such that
B: 1 <= i & i <= len f & f.i = q;
reconsider i1 = i - 1 as Element of NAT by B,INT_1:3;
reconsider r1 = Product (f|i1),
r2 = Product (f/^i) as Element of the carrier of Polynom-Ring F;
i in Seg(len f) by B; then
C: i1 + 1 = i & i in dom f by FINSEQ_1:def 3; then
D: f/.i = f.i by PARTFUN1:def 6;
E: r1 * r2 = r1 *' r2 by POLYNOM3:def 10;
f = f|i1 ^ (f/^i1) by RFINSEQ:8
.= f|i1 ^ (<*f/.i*>^(f/^i)) by C,FINSEQ_5:31; then
p = Product(f|i1) * Product (<*f/.i*>^(f/^i)) by A,GROUP_4:5
.= r1 * (q * r2) by B,D,GROUP_4:7
.= q * (r1 * r2) by GROUP_1:def 3
.= q *' (r1 *' r2) by E,POLYNOM3:def 10;
hence thesis by RING_4:1;
end;
theorem sepprodC:
for F being Field
for f being FinSequence of Polynom-Ring F
for p,q1,q2 being Element of the carrier of Polynom-Ring F
st p = Product f &
ex i,j being Nat st j <> i & 1 <= i & i <= len f & f.i = q1 &
1 <= j & j <= len f & f.j = q2
holds q1 *' q2 divides p
proof
let F be Field, f be FinSequence of Polynom-Ring F;
let p,q1,q2 being Element of the carrier of Polynom-Ring F;
assume A: p = Product f &
ex i,j being Nat st j <> i & 1 <= i & i <= len f & f.i = q1 &
1 <= j & j <= len f & f.j = q2; then
consider i,j being Nat such that
B: j <> i & 1 <= i & i <= len f & f.i = q1 &
1 <= j & j <= len f & f.j = q2;
reconsider i1 = i - 1 as Element of NAT by B,INT_1:3;
i in Seg(len f) by B; then
C: i1 + 1 = i & i in dom f by FINSEQ_1:def 3; then
D: f/.i = f.i by PARTFUN1:def 6;
set g = (f|i1)^(f/^i);
reconsider r = Product g,
r1 = Product (f|i1),
r2 = Product (f/^i) as Element of the carrier of Polynom-Ring F;
H1: f = f|i1 ^ (f/^i1) by RFINSEQ:8
.= f|i1 ^ (<*f/.i*>^(f/^i)) by C,FINSEQ_5:31; then
E: p = Product(f|i1) * Product (<*f/.i*>^(f/^i)) by A,GROUP_4:5
.= r1 * (q1 * r2) by B,D,GROUP_4:7
.= q1 * (r1 * r2) by GROUP_1:def 3
.= q1 * r by GROUP_4:5
.= q1 *' r by POLYNOM3:def 10;
F: len f = len(f|i1) + len(<*f/.i*>^(f/^i)) by H1,FINSEQ_1:22
.= len(f|i1) + (len(<*f/.i*>) + len(f/^i)) by FINSEQ_1:22
.= len(f|i1) + (1 + len(f/^i)) by FINSEQ_1:40
.= 1 + (len(f|i1) + len(f/^i))
.= 1 + len g by FINSEQ_1:22;
ex k being Nat st 1 <= k & k <= len g & g.k = q2
proof
i1 + 1 = i; then
KK: i1 <= i by NAT_1:11; then
K0: i1 <= len f by B,XXREAL_0:2;
K1: len(f|i1) = i1 by KK,B,XXREAL_0:2,FINSEQ_1:59;
per cases by B,XXREAL_0:1;
suppose H3: j < i; then
j < len f by B,XXREAL_0:1; then
H4: j - 1 + 1 <= len g by F,INT_1:7;
j + 1 <= i by H3,INT_1:7; then
j + 1 - 1 <= i - 1 by XREAL_1:9; then
K2: j in Seg len(f|i1) by B,K1; then
H5: j in dom(f|i1) by FINSEQ_1:def 3;
now assume 1 > i1; then
1 >= i1 + 1 by INT_1:7;
hence contradiction by H3,B,XXREAL_0:1;
end; then
i1 in Seg(len f) by K0; then
i1 in dom f by FINSEQ_1:def 3; then
q2 = (f|i1).j by K1,K2,B,RFINSEQ:6 .= g.j by H5,FINSEQ_1:def 7;
hence thesis by B,H4;
end;
suppose HH: j > i; then
j - i > i - i by XREAL_1:9; then
reconsider k1 = j - i as Element of NAT by INT_1:3;
set k = i1 + k1;
k1 > i - i by HH,XREAL_1:9; then
H0: 0 + 1 <= k1 by INT_1:7; then
H1: (f/^i).k1 = f.(k1+i) by B,FINSEQ_6:114;
k1 <= k by NAT_1:11; then
H2: 1 <= k by H0,XXREAL_0:2;
k + 0 < j - 1 + 1 by XREAL_1:6; then
k < len f by B,XXREAL_0:2; then
H3: k <= len g by F,INT_1:7;
H4: len(f/^i) = len f - i by B,RFINSEQ:def 1;
k1 <= len f - i by B,XREAL_1:9; then
k1 in Seg(len(f/^i)) by H4,H0; then
k1 in dom(f/^i) by FINSEQ_1:def 3; then
g.k = q2 by B,H1,K1,FINSEQ_1:def 7;
hence thesis by H2,H3;
end;
end; then
consider s being Polynomial of F such that
F: q2 *' s = r by RING_4:1,sepprodB;
(q1 *' q2) *' s = q1 *' r by F,POLYNOM3:33;
hence thesis by E,RING_4:1;
end;
theorem mon:
for F being Field
for f being FinSequence of the carrier of Polynom-Ring F
st for i being Element of dom f, q being Polynomial of F
st q = f.i holds q is monic
for p being Polynomial of F st p = Product f holds p is monic
proof
let F be Field, f be FinSequence of the carrier of Polynom-Ring F;
assume AS1: for i being Element of dom f, q be Polynomial of F
st q = f.i holds q is monic;
let p be Polynomial of F;
assume AS2: p = Product f;
defpred P[Nat] means
for f being FinSequence of the carrier of Polynom-Ring F
st len f = $1 & for i being Element of dom f, q be Polynomial of F
st q = f.i holds q is monic
for p being Polynomial of F st p = Product f holds p is monic;
IA: P[0]
proof
now let f be FinSequence of the carrier of Polynom-Ring F;
assume AS1: len f = 0 & for i being Element of dom f,
q be Polynomial of F st q = f.i holds q is monic;
let p be Polynomial of F;
assume AS2: p = Product f;
f = <*>(the carrier of Polynom-Ring F) by AS1; then
Product f = 1_(Polynom-Ring F) by GROUP_4:8
.= 1_.(F) by POLYNOM3:def 10;
hence p is monic by AS2;
end;
hence thesis;
end;
IS: now let k be Nat;
assume IV: P[k];
now let f be FinSequence of the carrier of Polynom-Ring F;
assume AS1: len f = k+1 &
for i being Element of dom f, q be Polynomial of F
st q = f.i holds q is monic;
let p be Polynomial of F;
assume AS2: p = Product f;
consider g being FinSequence of the carrier of Polynom-Ring F,
x being Element of Polynom-Ring F such that
A1: f = g ^ <*x*> by AS1,FINSEQ_2:19;
reconsider q = Product g as Polynomial of F by POLYNOM3:def 10;
A4: len f = len g + 1 by A1,FINSEQ_2:16;
A5: x = f.(len f) by A1,A4,FINSEQ_1:42;
len f in Seg(len f) by AS1,FINSEQ_1:3; then
reconsider i = len f as Element of dom f by FINSEQ_1:def 3;
reconsider q = f.i as Polynomial of F by A5,POLYNOM3:def 10;
reconsider q as monic Polynomial of F by AS1;
per cases;
suppose g = {};
then f = <*x*> by A1,FINSEQ_1:34;
then Product f = q by A5,GROUP_4:9;
hence p is monic by AS2;
end;
suppose B1: g is non empty;
reconsider r = Product g as Polynomial of F by POLYNOM3:def 10;
now let i be Element of dom g, q be Polynomial of F;
assume C1: q = g.i;
C2: dom g c= dom f by A1,FINSEQ_1:26;
C3: g.i = f.i by B1,A1,FINSEQ_1:def 7;
i in dom f by B1,C2;
hence q is monic by C1,C3,AS1;
end; then
reconsider r as monic Polynomial of F by AS1,A4,IV;
Product f = Product g * Product<*x*> by A1,GROUP_4:5
.= (Product g) * x by GROUP_4:9
.= r *' q by A5,POLYNOM3:def 10;
hence p is monic by AS2;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider k being Nat such that K: len f = k;
thus thesis by I,K,AS1,AS2;
end;
spl1:
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
for E being SplittingField of p
for a being Element of E
for q being non constant Element of the carrier of Polynom-Ring FAdj(F,{a})
st q = p holds E is SplittingField of q
proof
let F be Field, p be non constant Element of the carrier of Polynom-Ring F;
let E be SplittingField of p, a be Element of E;
let q be non constant Element of the carrier of Polynom-Ring FAdj(F,{a});
assume AS: q = p;
E is FAdj(F,{a})-extending by FIELD_4:7;
hence thesis by AS,FIELD_8:53;
end;
theorem splitE:
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
let F be Field, E be FieldExtension of F;
let p be non constant Polynomial of F; let q be non zero Polynomial of F;
assume p *' q splits_in E; then
consider a being non zero Element of E, r being Ppoly of E such that
A1: p *' q = a * r by FIELD_4:def 5;
reconsider p1 = p as Polynomial of E by FIELD_4:8;
p1 is Element of the carrier of Polynom-Ring E &
p is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10; then
deg p > 0 & deg p1 = deg p by RATFUNC1:def 2,FIELD_4:20; then
reconsider p1 as non constant Polynomial of E by RATFUNC1:def 2;
reconsider q1 = q as Polynomial of E by FIELD_4:8;
q <> 0_.(F) & 0_.(E) = 0_.(F) by FIELD_4:12; then
reconsider q1 as non zero Polynomial of E by UPROOTS:def 5;
p1 *' q1 = p *' q by FIELD_4:17; then
p1 *' q1 splits_in E by A1,FIELD_4:def 5; then
consider b being non zero Element of E, s being Ppoly of E such that
A2: p1 = b * s by FIELD_8:11,FIELD_4:def 5;
thus thesis by A2,FIELD_4:def 5;
end;
lemBB:
for F being Field
for E1,E2 being FieldExtension of F
for f being F-fixing Automorphism of E1
st E1 == E2 holds f is F-fixing Automorphism of E2
proof
let F be Field, E1,E2 be FieldExtension of F,
f be F-fixing Automorphism of E1;
assume AS: E1 == E2; then
reconsider g = f as Function of E2,E2;
A: g is F-fixing by FIELD_8:def 2;
now let a2,b2 be Element of E2;
reconsider a1 = a2, b1 = b2 as Element of E1 by AS;
a1 + b1 = a2 + b2 by AS;
hence g.(a2+b2) = f.a1 + f.b1 by VECTSP_1:def 20
.= g.a2 + g.b2 by AS;
a1 * b1 = a2 * b2 by AS;
hence g.(a2*b2) = f.a1 * f.b1 by GROUP_6:def 6
.= g.a2 * g.b2 by AS;
end; then
B: g is additive multiplicative;
g.(1_E2) = 1_E1 by AS,GROUP_1:def 13 .= 1_E2 by AS; then
g is unity-preserving;
hence thesis by A,B,AS;
end;
lemBF:
for F being Field
for E1,E2 being FieldExtension of F
for f being Automorphism of E1 st E1 == E2 holds f is Automorphism of E2
proof
let F be Field, E1,E2 be FieldExtension of F,
f be Automorphism of E1;
assume AS: E1 == E2; then
reconsider g = f as Function of E2,E2;
now let a2,b2 be Element of E2;
reconsider a1 = a2, b1 = b2 as Element of E1 by AS;
a1 + b1 = a2 + b2 by AS;
hence g.(a2+b2) = f.a1 + f.b1 by VECTSP_1:def 20
.= g.a2 + g.b2 by AS;
a1 * b1 = a2 * b2 by AS;
hence g.(a2*b2) = f.a1 * f.b1 by GROUP_6:def 6
.= g.a2 * g.b2 by AS;
end; then
B: g is additive multiplicative;
g.(1_E2) = 1_E1 by AS,GROUP_1:def 13 .= 1_E2 by AS; then
g is unity-preserving;
hence thesis by B,AS;
end;
theorem lemBE:
for F being Field
for E1,E2 being FieldExtension of F st E1 == E2 holds Aut(E1) = Aut(E2)
proof
let F be Field, E1,E2 be FieldExtension of F;
assume A: E1 == E2;
B: now let o be object;
assume o in Auts(E1);
then consider f being Automorphism of E1 such that C: o = f;
f is Automorphism of E2 by A,lemBF;
hence o in Auts(E2) by C;
end;
G: now let o be object;
assume o in Auts(E2);
then consider f being Automorphism of E2 such that C: o = f;
f is Automorphism of E1 by A,lemBF;
hence o in Auts(E1) by C;
end;
then C: Auts(E1) = Auts(E2) by B,TARSKI:2;
now let o be object;
assume o in [:Auts(E1),Auts(E1):]; then
consider x,y being object such that
D: x in Auts(E1) & y in Auts(E1) & o = [x,y] by ZFMISC_1:def 2;
consider f1 being Automorphism of E1 such that E: x = f1 by D;
consider g1 being Automorphism of E1 such that F: y = g1 by D;
consider f2 being Automorphism of E2 such that G: x = f2 by C,D;
consider g2 being Automorphism of E2 such that H: y = g2 by C,D;
thus (AutComp E1).o = (AutComp E1).(f1,g1) by D,E,F
.= f2 * g2 by E,F,G,H,GALOIS_1:def 2
.= (AutComp E2).(f2,g2) by GALOIS_1:def 2
.= (AutComp E2).o by D,G,H;
end;
then AutComp E1 = AutComp E2 by C;
hence Aut(E1) = Aut(E2) by G,B,TARSKI:2;
end;
theorem lemBC:
for F being Field
for E1,E2 being FieldExtension of F st E1 == E2 holds Aut(E1,F) = Aut(E2,F)
proof
let F be Field, E1,E2 be FieldExtension of F;
assume A: E1 == E2;
B: now let o be object;
assume o in Auts(E1,F);
then consider f being F-fixing Automorphism of E1 such that C: o = f;
f is F-fixing Automorphism of E2 by A,lemBB;
hence o in Auts(E2,F) by C;
end;
C: now let o be object;
assume o in Auts(E2,F);
then consider f being F-fixing Automorphism of E2 such that C: o = f;
f is F-fixing Automorphism of E1 by A,lemBB;
hence o in Auts(E1,F) by C;
end;
Aut(E2,F) is Subgroup of Aut(E1) by A,lemBE;
hence Aut(E1,F) = Aut(E2,F) by C,B,TARSKI:2,GROUP_2:59;
end;
theorem lemBD:
for F being Field
for E1,E2 being FieldExtension of F
st E1 == E2 holds Fix(E1,Aut(E1,F)) = Fix(E2,Aut(E2,F))
proof
let F be Field, E1,E2 be FieldExtension of F;
assume A: E1 == E2;
set G1 = Aut(E1,F), G2 = Aut(E2,F);
G1 = G2 by A,lemBC; then
Fixed_El(E1,G1) = Fixed_El(E2,G2) by A; then
B: the carrier of Fix(E1,G1) = Fixed_El(E2,G2) by GALOIS_1:def 17
.= the carrier of Fix(E2,G2) by GALOIS_1:def 17;
Fix(E2,G2) is Subfield of E1 by A,EC_PF_1:5;
hence thesis by B,EC_PF_1:8;
end;
theorem
for F being Field
for E1 being GaloisExtension of F
for E2 being FieldExtension of F st E2 == E1 holds E2 is GaloisExtension of F
proof
let F be Field, E1 be GaloisExtension of F, E2 be FieldExtension of F;
assume E2 == E1; then
A: Fix(E1,Aut(E1,F)) = Fix(E2,Aut(E2,F)) by lemBD;
Fix(E1,Aut(E1,F)) == F by GALOIS_1:def 18;
hence thesis by A,GALOIS_1:def 18;
end;
begin :: More on Separability
definition
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
attr T is F-separable means :defT:
for a being Element of E st a in T holds a is F-separable;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster finite F-separable non empty for Subset of E;
existence
proof
set a = the F-separable Element of E;
take T = {a};
thus T is finite;
thus T is F-separable by TARSKI:def 1;
thus T is non empty;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster -> F-algebraic for F-separable Subset of E;
coherence
proof
let T be F-separable Subset of E;
now let a be Element of E;
assume a in T;
then a is F-separable by defT;
hence a is F-algebraic;
end;
hence thesis;
end;
end;
registration
let F be Field;
let E be F-separable FieldExtension of F;
cluster -> F-separable for Subset of E;
coherence;
end;
theorem separ:
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
holds p is separable iff
for E being FieldExtension of F
st p splits_in E holds card Roots(E,p) = deg p
proof
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
A: now assume A1: p is separable;
now assume ex E being FieldExtension of F
st p splits_in E & card Roots(E,p) <> deg p; then
consider E being FieldExtension of F such that
A2: p splits_in E & card Roots(E,p) <> deg p;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E
by FIELD_4:10; then
reconsider p1 = p as Element of the carrier of Polynom-Ring E;
deg p > 0 & deg p1 = deg p by FIELD_4:20,RING_4:def 4; then
reconsider p1 as non constant
Element of the carrier of Polynom-Ring E by RING_4:def 4;
reconsider p1 as separable non constant
Element of the carrier of Polynom-Ring E by A1,FIELD_15:88;
consider a being non zero Element of E, q being Ppoly of E such that
A4: p = a * q by A2,FIELD_4:def 5;
deg p1 = card(Roots p1) by A4,FIELD_4:def 5,FIELD_15:79
.= card Roots(E,p) by FIELD_7:13;
hence contradiction by A2,FIELD_4:20;
end;
hence for E being FieldExtension of F
st p splits_in E holds card Roots(E,p) = deg p;
end;
now assume B: for E being FieldExtension of F
st p splits_in E holds card Roots(E,p) = deg p;
set K = the SplittingField of p;
p splits_in K by FIELD_8:def 1;
then card Roots(K,p) = deg p by B;
hence p is separable by FIELD_15:85;
end;
hence thesis by A;
end;
definition
let F be Field;
let p,q be Element of the carrier of Polynom-Ring F;
pred p,q have_common_roots_in_some_extension means
ex E being FieldExtension of F st Roots(E,p) /\ Roots(E,q) <> {};
end;
notation
let F be Field;
let p,q be Element of the carrier of Polynom-Ring F;
antonym p,q have_nowhere_common_roots
for p,q have_common_roots_in_some_extension;
end;
theorem irrm:
for F being Field
for p,q being monic irreducible Element of the carrier of Polynom-Ring F
st p,q have_common_roots_in_some_extension holds p = q
proof
let F be Field;
let p,q be monic irreducible Element of the carrier of Polynom-Ring F;
assume p,q have_common_roots_in_some_extension; then
consider E being FieldExtension of F such that
AS: Roots(E,p) /\ Roots(E,q) <> {};
set o = the Element of Roots(E,p) /\ Roots(E,q);
H: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E} &
Roots(E,q) = {a where a is Element of E : a is_a_root_of q,E}
by FIELD_4:def 4;
o in Roots(E,p) by AS,XBOOLE_0:def 4; then
consider a being Element of E such that
A: o = a & a is_a_root_of p,E by H;
o in Roots(E,q) by AS,XBOOLE_0:def 4; then
consider b being Element of E such that
B: o = b & b is_a_root_of q,E by H;
C: Ext_eval(p,a) = 0.E & Ext_eval(q,b) = 0.E by A,B,FIELD_4:def 2; then
reconsider b as F-algebraic Element of E by FIELD_6:43;
thus p = MinPoly(b,F) by A,B,C,FIELD_6:52 .= q by C,FIELD_6:52;
end;
theorem sepmult:
for F being Field
for p,q being non constant Element of the carrier of Polynom-Ring F
st p is separable & q is separable
holds p * q is separable iff p,q have_nowhere_common_roots
proof
let F be Field, p,q be non constant Element of the carrier of Polynom-Ring F;
assume AS: p is separable & q is separable;
reconsider r = p*q as non constant Element of the carrier of Polynom-Ring F;
deg p > 0 by RING_4:def 4; then
reconsider p1 = p as non constant Polynomial of F by RATFUNC1:def 2;
deg q > 0 by RING_4:def 4; then
reconsider q1 = q as non constant Polynomial of F by RATFUNC1:def 2;
H: p * q = p1 *' q1 by POLYNOM3:def 10;
Z: now assume AS1: p,q have_nowhere_common_roots;
now let E be FieldExtension of F;
assume r splits_in E; then
A: p *' q splits_in E & F is Subring of E by POLYNOM3:def 10,FIELD_4:def 1;
let a be Element of E;
assume a is_a_root_of p*q,E; then
B: 0.E = Ext_eval(p1*'q1,a) by H,FIELD_4:def 2
.= Ext_eval(p1,a) * Ext_eval(q1,a) by A,ALGNUM_1:20;
C: p1 splits_in E & q1 splits_in E by A,FIELD_13:7;
D: multiplicity(p1*'q1,a) = multiplicity(p1,a) + multiplicity(q1,a)
by FIELD_15:62;
per cases by B,VECTSP_2:def 1;
suppose S: Ext_eval(p1,a) = 0.E; then
E: a is_a_root_of p,E by FIELD_4:def 2;
F: multiplicity(p,a) = 1 by S,AS,C,FIELD_15:75,FIELD_4:def 2;
G: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E} &
Roots(E,q) = {a where a is Element of E : a is_a_root_of q,E}
by FIELD_4:def 4;
now assume multiplicity(q,a) > 0;
then multiplicity(q,a) >= 0 + 1 by INT_1:7;
then a is_a_root_of q,E by FIELD_15:57;
then a in Roots(E,p) & a in Roots(E,q) by G,E;
then Roots(E,p) /\ Roots(E,q) <> {} by XBOOLE_0:def 4;
hence contradiction by AS1;
end;
hence multiplicity(r,a) = 1 + 0 by D,H,F .= 1;
end;
suppose S: Ext_eval(q1,a) = 0.E; then
E: a is_a_root_of q,E by FIELD_4:def 2;
F: multiplicity(q,a) = 1 by S,AS,C,FIELD_15:75,FIELD_4:def 2;
G: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E} &
Roots(E,q) = {a where a is Element of E : a is_a_root_of q,E}
by FIELD_4:def 4;
now assume multiplicity(p,a) > 0;
then multiplicity(p,a) >= 0 + 1 by INT_1:7;
then a is_a_root_of p,E by FIELD_15:57;
then a in Roots(E,p) & a in Roots(E,q) by G,E;
then Roots(E,p) /\ Roots(E,q) <> {} by XBOOLE_0:def 4;
hence contradiction by AS1;
end;
hence multiplicity(r,a) = 0 + 1 by D,H,F .= 1;
end;
end;
hence p * q is separable by FIELD_15:75;
end;
now assume A: p * q is separable;
now assume p,q have_common_roots_in_some_extension; then
consider E being FieldExtension of F such that
B: Roots(E,p) /\ Roots(E,q) <> {};
G: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E} &
Roots(E,q) = {a where a is Element of E : a is_a_root_of q,E}
by FIELD_4:def 4;
set o = the Element of Roots(E,p) /\ Roots(E,q);
o in Roots(E,p) by B,XBOOLE_0:def 4; then
consider a1 being Element of E such that
C: o = a1 & a1 is_a_root_of p,E by G;
o in Roots(E,q) by B,XBOOLE_0:def 4; then
consider a2 being Element of E such that
D: o = a2 & a2 is_a_root_of q,E by G;
E: multiplicity(p,a1) >= 1 & multiplicity(q,a1) >= 1 by D,C,FIELD_15:57;
multiplicity(p1*'q1,a1) = multiplicity(p,a1) + multiplicity(q,a1)
by FIELD_15:62; then
multiplicity(p1*'q1,a1) >= 1 + 1 by E,XREAL_1:7; then
multiplicity(p1*'q1,a1) - 0 > 1 + 1 - 1 by XREAL_1:15;
hence contradiction by H,A,FIELD_15:77;
end;
hence p,q have_nowhere_common_roots;
end;
hence thesis by Z;
end;
theorem sepirr:
for F being Field
for p,q being monic irreducible Element of the carrier of Polynom-Ring F
st p is separable & q is separable
holds p * q is separable iff p <> q
proof
let F be Field;
let p,q be monic irreducible Element of the carrier of Polynom-Ring F;
assume AS: p is separable & q is separable;
deg p > 0 by RING_4:def 4; then
reconsider p1 = p as non constant Polynomial of F by RATFUNC1:def 2;
A: now assume B: p * q is separable;
now assume C: p = q;
set E = the SplittingField of p;
set a = the Element of Roots(E,p);
Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E}
& a in Roots(E,p) by FIELD_4:def 4; then
consider a1 being Element of E such that
D: a1 = a & a1 is_a_root_of p,E;
E: multiplicity(p,a) >= 1 by D,FIELD_15:57;
multiplicity(p1*'p1,a) = multiplicity(p1,a) + multiplicity(p1,a)
by FIELD_15:62; then
multiplicity(p1*'p1,a) >= 1 + 1 by E,XREAL_1:7; then
F: multiplicity(p1*'p1,a) - 0 > (1 + 1) - 1 by XREAL_1:15;
p1 *' p1 = p * q by C,POLYNOM3:def 10;
hence contradiction by B,F,FIELD_15:77;
end;
hence p <> q;
end;
now assume p <> q;
then p,q have_nowhere_common_roots by irrm;
hence p * q is separable by AS,sepmult;
end;
hence thesis by A;
end;
sepprodE1:
for F being Field
for E being FieldExtension of F
for f being FinSequence of Polynom-Ring F
for p being non zero Element of the carrier of Polynom-Ring F
for a being Element of E
st p = Product f &
for i being Nat st 1 <= i & i <= len f
for r being non zero Element of the carrier of Polynom-Ring F
st r = f.i holds multiplicity(r,a) = 0
holds multiplicity(p,a) = 0
proof
let F be Field, E be FieldExtension of F, f be FinSequence of Polynom-Ring F;
let p be non zero Element of the carrier of Polynom-Ring F, a be Element of E;
assume AS: p = Product f &
for i being Nat st 1 <= i & i <= len f
for r being non zero Element of the carrier of Polynom-Ring F
st r = f.i holds multiplicity(r,a) = 0;
defpred P[Nat] means
for f being FinSequence of Polynom-Ring F
for p being non zero Element of the carrier of Polynom-Ring F
for a being Element of E
st p = Product f & len f = $1 &
for i being Nat st 1 <= i & i <= len f
for r being non zero Element of the carrier of Polynom-Ring F
st r = f.i holds multiplicity(r,a) = 0
holds multiplicity(p,a) = 0;
IA: P[0]
proof
now let f be FinSequence of Polynom-Ring F;
let p be non zero Element of the carrier of Polynom-Ring F;
let a be Element of E;
assume A1: p = Product f & len f = 0 &
for i being Nat st 1 <= i & i <= len f
for r being non zero Element of the carrier of Polynom-Ring F
st r = f.i holds multiplicity(r,a) = 0; then
f = <*>(the carrier of Polynom-Ring F); then
A2: p = 1_(Polynom-Ring F) by A1,GROUP_4:8 .= 1_.F by POLYNOM3:def 10;
now assume multiplicity(p,a) > 0;
then multiplicity(p,a) >= 0 + 1 by INT_1:7;
then 0.E = Ext_eval(p,a) by FIELD_15:57,FIELD_4:def 2
.= 1.E by A2,FIELD_4:23;
hence contradiction;
end;
hence multiplicity(p,a) = 0;
end;
hence thesis;
end;
IS: now let k be Nat;
assume IV: P[k];
now let f be FinSequence of Polynom-Ring F;
let p be non zero Element of the carrier of Polynom-Ring F;
let a be Element of E;
assume A1: p = Product f & len f = k+1 &
for i being Nat st 1 <= i & i <= len f
for r being non zero Element of the carrier of Polynom-Ring F
st r = f.i holds multiplicity(r,a) = 0;
consider g being FinSequence of the carrier of Polynom-Ring F,
r1 being Element of the carrier of Polynom-Ring F such that
A3: f = g ^ <*r1*> by A1,FINSEQ_2:19;
A4: len f = len g + 1 by A3,FINSEQ_2:16;
reconsider q = Product g, r2 = r1
as Polynomial of F by POLYNOM3:def 10;
A5: p = (Product g) * r1 by A1,A3,GROUP_4:6
.= q *' r2 by POLYNOM3:def 10; then
reconsider q,r2 as non zero Polynomial of F;
A6: multiplicity(p,a) = multiplicity(q,a) + multiplicity(r2,a)
by A5,FIELD_15:62;
f.(len f) = r2 & 1 <= len f by A3,A4,FINSEQ_1:42,FINSEQ_1:20; then
A8: multiplicity(p,a) = multiplicity(q,a) + 0 by A6,A1;
now let i be Nat;
assume B1: 1 <= i & i <= len g;
let r be non zero Element of the carrier of Polynom-Ring F;
assume B2: r = g.i;
i in Seg(len g) by B1; then
i in dom g by FINSEQ_1:def 3; then
B3: g.i = f.i by A3,FINSEQ_1:def 7;
i + 0 < len f by A4,B1,XREAL_1:8;
hence multiplicity(r,a) = 0 by B1,B2,B3,A1;
end;
hence multiplicity(p,a) = 0 by A8,A4,A1,IV;
end;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis by AS;
end;
sepprodE:
for F being Field
for E being FieldExtension of F
for f being FinSequence of Polynom-Ring F
for p,r being non zero Element of the carrier of Polynom-Ring F
for a being Element of E
st p = Product f &
ex i being Nat st 1 <= i & i <= len f & r = f.i &
for j being Nat st j <> i & 1 <= j & j <= len f
for q being non zero Element of the carrier of Polynom-Ring F
st q = f.j holds multiplicity(q,a) = 0
holds multiplicity(p,a) = multiplicity(r,a)
proof
let F be Field, E be FieldExtension of F, f be FinSequence of Polynom-Ring F;
let p,r be non zero Element of the carrier of Polynom-Ring F;
let a be Element of E;
assume AS: p = Product f &
ex i being Nat st 1 <= i & i <= len f & r = f.i &
for j being Nat st j <> i & 1 <= j & j <= len f
for q being non zero Element of the carrier of Polynom-Ring F
st q = f.j holds multiplicity(q,a) = 0;
defpred P[Nat] means
for f being FinSequence of Polynom-Ring F
for p,r being non zero Element of the carrier of Polynom-Ring F
for a being Element of E
st p = Product f & len f = $1 &
ex i being Nat st 1 <= i & i <= len f & r = f.i &
for j being Nat st j <> i & 1 <= j & j <= len f
for q being non zero Element of the carrier of Polynom-Ring F
st q = f.j holds multiplicity(q,a) = 0
holds multiplicity(p,a) = multiplicity(r,a);
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
now let f be FinSequence of Polynom-Ring F;
let p,r be non zero Element of the carrier of Polynom-Ring F;
let a be Element of E;
assume A1: p = Product f & len f = k + 1 &
ex i being Nat st 1 <= i & i <= len f & r = f.i &
for j being Nat st j <> i & 1 <= j & j <= len f
for q being non zero Element of the carrier of Polynom-Ring F
st q = f.j holds multiplicity(q,a) = 0; then
consider i being Nat such that
A2: 1 <= i & i <= len f & r = f.i &
for j being Nat st j <> i & 1 <= j & j <= len f
for q being non zero Element of the carrier of Polynom-Ring F
st q = f.j holds multiplicity(q,a) = 0;
consider g being FinSequence of the carrier of Polynom-Ring F,
r1 being Element of the carrier of Polynom-Ring F such that
A3: f = g ^ <*r1*> by A1,FINSEQ_2:19;
A4: len f = len g + 1 by A3,FINSEQ_2:16;
reconsider q = Product g, r2 = r1
as Polynomial of F by POLYNOM3:def 10;
A5: p = (Product g) * r1 by A1,A3,GROUP_4:6
.= q *' r2 by POLYNOM3:def 10; then
reconsider q,r2 as non zero Polynomial of F;
A6: multiplicity(p,a) = multiplicity(q,a) + multiplicity(r2,a)
by A5,FIELD_15:62;
A7: f.(len f) = r2 by A3,A4,FINSEQ_1:42;
per cases by A2,XXREAL_0:1;
suppose B0: i = len f;
now let j be Nat;
assume B2: 1 <= j & j <= len g;
let r be non zero Element of the carrier of Polynom-Ring F;
assume B3: r = g.j;
B4: j + 0 < len f by A4,B2,XREAL_1:8;
j in Seg(len g) by B2;
then j in dom g by FINSEQ_1:def 3;
then g.j = f.j by A3,FINSEQ_1:def 7;
hence multiplicity(r,a) = 0 by B0,B2,B3,B4,A2;
end;
then multiplicity(q,a) = 0 by sepprodE1;
hence multiplicity(p,a)
= multiplicity(r,a) by A6,B0,A2,A3,A4,FINSEQ_1:42;
end;
suppose B1: i < len f;
1 <= len f by A1,NAT_1:11; then
B2: multiplicity(r2,a) = 0 by B1,A2,A7;
B3: i <= len g by B1,A4,INT_1:7; then
i in Seg(len g) by A2; then
i in dom g by FINSEQ_1:def 3; then
B4: r = g.i by A2,A3,FINSEQ_1:def 7;
now let j be Nat;
assume B4: j <> i & 1 <= j & j <= len g;
let q be non zero Element of the carrier of Polynom-Ring F;
assume B5: q = g.j;
j in Seg(len g) by B4; then
j in dom g by FINSEQ_1:def 3; then
B6: q = f.j by A3,B5,FINSEQ_1:def 7;
j + 0 < len f by A4,B4,XREAL_1:8;
hence multiplicity(q,a) = 0 by B6,B4,A2;
end;
hence multiplicity(p,a) = multiplicity(r,a) by A6,B2,B3,B4,A1,A2,A4,IV;
end;
end;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis by AS;
end;
theorem sepprod:
for F being Field
for E being FieldExtension of F
for f being non empty FinSequence of Polynom-Ring F
st for i being Nat st 1 <= i & i <= len f
ex q being monic irreducible Element of the carrier of Polynom-Ring F
st f.i = q & q is separable
for p being non constant Element of the carrier of Polynom-Ring F
st p = Product f holds p is separable iff f is one-to-one
proof
let F be Field, E be FieldExtension of F,
f be non empty FinSequence of Polynom-Ring F;
assume AS1:
for i being Nat st 1 <= i & i <= len f
ex q being monic irreducible Element of the carrier of Polynom-Ring F
st f.i = q & q is separable;
let p be non constant Element of the carrier of Polynom-Ring F;
assume AS2: p = Product f;
A: now assume AS3: p is separable;
A5: now let i,j be Nat;
assume A0: j <> i &
1 <= i & i <= len f & 1 <= j & j <= len f & f.i = f.j; then
consider qi being monic irreducible Element of the carrier of Polynom-Ring F
such that A1: f.i = qi & qi is separable by AS1;
consider qj being monic irreducible Element of the carrier of Polynom-Ring F
such that A2: f.j = qj & qj is separable by A0,AS1;
reconsider r = qi * qj
as non constant Element of the carrier of Polynom-Ring F;
qi *' qj divides p by AS2,A0,A1,A2,sepprodC; then
r divides p by POLYNOM3:def 10; then
consider s being Polynomial of F such that A4: p = r *' s by RING_4:1;
A3: s is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
r is non separable by A0,A1,A2,sepirr;
hence contradiction by A4,A3,AS3,FIELD_15:87;
end;
now let x1,x2 be object;
assume A7: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
reconsider i = x1, j = x2 as Element of NAT;
i in Seg(len f) & j in Seg(len f) by A7,FINSEQ_1:def 3; then
1 <= i & i <= len f & 1 <= j & j <= len f by FINSEQ_1:1;
hence x1 = x2 by A5,A7;
end;
hence f is one-to-one;
end;
now assume A1: f is one-to-one;
AS3: now let i,j be Nat;
assume B: j <> i & 1 <= i & i <= len f & 1 <= j & j <= len f;
then i in Seg(len f) & j in Seg(len f);
then i in dom f & j in dom f by FINSEQ_1:def 3;
hence f.i <> f.j by A1,B;
end;
now let E be FieldExtension of F;
assume A0: p splits_in E;
let a be Element of E;
assume a is_a_root_of p,E; then
Ext_eval(p,a) = 0.E by FIELD_4:def 2; then
consider i being Element of dom f,
q1 being Polynomial of F such that
A2: q1 = f.i & Ext_eval(q1,a) = 0.E by AS2,lemsepprodA;
dom f = Seg(len f) by FINSEQ_1:def 3; then
H4: 1 <= i & i <= len f by FINSEQ_1:1; then
consider qi being monic irreducible Element of the carrier of Polynom-Ring F
such that A3: f.i = qi & qi is separable by AS1;
consider s being Polynomial of F such that
H2: p = qi *' s by AS2,H4,A3,sepprodB,RING_4:1;
reconsider s as non zero Polynomial of F by H2;
deg qi > 0 by RING_4:def 4; then
H0: qi is non constant Polynomial of F by RATFUNC1:def 2;
qi *' s splits_in E by A0,H2; then
H1: qi splits_in E by H0,FIELD_13:7;
H2: a is_a_root_of qi,E by A3,A2,FIELD_4:def 2;
A4: multiplicity(qi,a) = 1 by H1,A3,A2,FIELD_4:def 2,FIELD_15:75;
now let j be Nat;
assume B0: j <> i & 1 <= j & j <= len f;
let q be non zero Element of the carrier of Polynom-Ring F;
assume B1: q = f.j;
consider q1 being monic irreducible
Element of the carrier of Polynom-Ring F such that
B2: f.j = q1 & q1 is separable by B0,AS1;
B3: Roots(E,qi) = {a where a is Element of E : a is_a_root_of qi,E} &
Roots(E,q) = {a where a is Element of E : a is_a_root_of q,E}
by FIELD_4:def 4;
now assume multiplicity(q,a) > 0; then
multiplicity(q,a) >= 0 + 1 by INT_1:7; then
a is_a_root_of q,E by FIELD_15:57; then
a in Roots(E,qi) & a in Roots(E,q) by H2,B3; then
a in Roots(E,qi) /\ Roots(E,q) by XBOOLE_0:def 4; then
qi,q have_common_roots_in_some_extension;
hence contradiction by H4,A3,AS3,B2,B1,B0,irrm;
end;
hence multiplicity(q,a) = 0;
end;
hence multiplicity(p,a) = 1 by AS2,A3,A4,H4,sepprodE;
end;
hence p is separable by FIELD_15:75;
end;
hence thesis by A;
end;
begin :: The Product of Minimal Polynomials of a given Finite Algebraic Set
definition
let F be Field;
let E be FieldExtension of F;
let T be F-algebraic Subset of E;
func MinPolys T -> Subset of the carrier of Polynom-Ring F equals
{ MinPoly(a,F) where a is F-algebraic Element of E : a in T };
coherence
proof
set S = {MinPoly(a,F) where a is F-algebraic Element of E : a in T};
now let o be object;
assume o in S; then
consider a being F-algebraic Element of E such that
A: o = MinPoly(a,F) & a in T;
thus o in the carrier of Polynom-Ring F by A;
end;
then S c= the carrier of Polynom-Ring F;
hence thesis;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let T be non empty F-algebraic Subset of E;
cluster MinPolys T -> non empty;
coherence
proof
set a = the Element of T;
set p = MinPoly(a,F);
p in {MinPoly(a,F) where a is F-algebraic Element of E : a in T};
hence thesis;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let T be finite F-algebraic Subset of E;
cluster MinPolys T -> finite;
coherence
proof
per cases;
suppose A: T = {};
now assume B: MinPolys T <> {};
set p = the Element of MinPolys T;
p in MinPolys T by B; then
consider a being F-algebraic Element of E such that
C: p = MinPoly(a,F) & a in T;
thus contradiction by A,C;
end;
hence MinPolys T is finite;
end;
suppose T <> {}; then
reconsider T1 = T as non empty finite F-algebraic Subset of E;
set S = MinPolys T1;
defpred P[object,object] means
ex a being F-algebraic Element of E st a in T1 & $1 = a & $2 = MinPoly(a,F);
A1: now let x be object;
assume A2: x in T; then
consider a being F-algebraic Element of E such that A3: x = a;
thus ex y being object st y in S & P[x,y]
proof
take y = MinPoly(a,F);
thus y in S by A2,A3;
thus thesis by A2,A3;
end;
end;
consider h being Function of T,S such that
A2: for o being object st o in T holds P[o,h.o] from FUNCT_2:sch 1(A1);
A3: dom h = T by FUNCT_2:def 1;
now let o be object;
assume o in S; then
consider a being F-algebraic Element of E such that
A5: o = MinPoly(a,F) & a in T;
P[a,h.a] by A2,A5;
hence o in rng h by A3,A5,FUNCT_1:def 3;
end;
then S c= rng h;
hence MinPolys T is finite;
end;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let T be finite F-algebraic Subset of E;
func FinSeq_MinPolys T -> FinSequence of the carrier of Polynom-Ring F equals
canFS(MinPolys T);
coherence
proof
set S = MinPolys T, f = canFS S;
H: rng f c= S by FINSEQ_1:def 4;
now let o be object;
assume o in rng f; then
o in S by H; then
consider a being F-algebraic Element of E such that
C1: o = MinPoly(a,F) & a in T;
thus o in the carrier of Polynom-Ring F by C1;
end; then
rng f c= the carrier of Polynom-Ring F;
hence thesis by FINSEQ_1:def 4;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E;
cluster FinSeq_MinPolys T -> non empty;
coherence;
end;
definition
let F be Field;
let E be FieldExtension of F;
let T be finite F-algebraic Subset of E;
func ProductMinPolys T -> Element of the carrier of Polynom-Ring F equals
Product(FinSeq_MinPolys T);
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E;
cluster ProductMinPolys T -> non constant monic;
coherence
proof
set S = MinPolys T, f = FinSeq_MinPolys T,
p = ProductMinPolys T, a = the Element of T;
H: rng f c= S by FINSEQ_1:def 4;
now assume C0: deg p < 1;
C1: now let i be Element of dom f;
f.i in S by H,FUNCT_1:3; then
consider a being F-algebraic Element of E such that
C2: MinPoly(a,F) = f.i & a in T;
thus f.i <> 0_.(F) by C2;
end;
rng f = S by FUNCT_2:def 3; then
MinPoly(a,F) in rng f; then
consider i being object such that
C2: i in dom f & MinPoly(a,F) = f.i by FUNCT_1:def 3;
reconsider i as Element of dom f by C2;
deg MinPoly(a,F) <= deg p by C1,C2,FIELD_13:3; then
deg MinPoly(a,F) < 1 by C0,XXREAL_0:2; then
deg MinPoly(a,F) + 1 <= 1 by INT_1:7; then
deg MinPoly(a,F) + 1 - 1 <= 1 - 1 by XREAL_1:9;
hence contradiction by RING_4:def 4;
end;
hence p is non constant by RING_4:def 4;
now let i be Element of dom f, q be Polynomial of F;
assume C3: q = f.i;
f.i in S by H,FUNCT_1:3; then
consider b being F-algebraic Element of E such that
C4: MinPoly(b,F) = f.i & b in T;
thus q is monic by C3,C4;
end;
hence thesis by mon;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E;
cluster Roots(E,ProductMinPolys T) -> non empty;
coherence
proof
set S = MinPolys T, f = FinSeq_MinPolys T,
p = ProductMinPolys T, i = the Element of dom f;
H: rng f c= S by FINSEQ_1:def 4;
f.i in S by H,FUNCT_1:3; then
consider a being F-algebraic Element of E such that
C4: f.i = MinPoly(a,F) & a in T;
Ext_eval(MinPoly(a,F),a) = 0.E by FIELD_6:52;
then Ext_eval(p,a) = 0.E by C4,FIELD_13:4;
then a is_a_root_of p,E by FIELD_4:def 2;
then a in {a where a is Element of E : a is_a_root_of p,E};
hence thesis by FIELD_4:def 4;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let T be non empty finite F-separable Subset of E;
cluster ProductMinPolys T -> separable;
coherence
proof
set S = MinPolys T, f = FinSeq_MinPolys T, p = ProductMinPolys T;
H: rng f c= S by FINSEQ_1:def 4;
now let i be Nat;
assume 1 <= i & i <= len f; then
i in Seg(len f); then
i in dom f by FINSEQ_1:def 3; then
f.i in S by H,FUNCT_1:3; then
consider a being F-algebraic Element of E such that
C1: f.i = MinPoly(a,F) & a in T;
reconsider a1 = a as F-separable Element of E by C1,defT;
MinPoly(a1,F) is separable;
hence ex q being monic irreducible Element of the carrier of Polynom-Ring F
st f.i = q & q is separable by C1;
end;
hence thesis by sepprod;
end;
end;
theorem
for F being Field
for E being FieldExtension of F
for T being non empty finite F-algebraic Subset of E st E == FAdj(F,T)
holds E == FAdj(F,Roots(E,ProductMinPolys T))
proof
let F be Field, E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E;
assume AS: E == FAdj(F,T);
set S = MinPolys T, f = canFS S, p = ProductMinPolys T;
now let o be object;
assume C0: o in T; then
reconsider a = o as F-algebraic Element of E;
MinPoly(a,F) in S & rng f = S by C0,FUNCT_2:def 3; then
consider i being object such that
C2: i in dom f & MinPoly(a,F) = f.i by FUNCT_1:def 3;
reconsider i as Element of dom f by C2;
Ext_eval(MinPoly(a,F),a) = 0.E by FIELD_6:52;
then Ext_eval(p,a) = 0.E by C2,FIELD_13:4;
then a is_a_root_of p,E by FIELD_4:def 2;
then a in {a where a is Element of E : a is_a_root_of p,E};
hence o in Roots(E,ProductMinPolys T) by FIELD_4:def 4;
end; then
T c= Roots(E,ProductMinPolys T); then
FAdj(F,T) is Subfield of FAdj(F,Roots(E,ProductMinPolys T)) by FIELD_7:10;
hence thesis by AS,EC_PF_1:5;
end;
theorem
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
for E being FieldExtension of F holds
E is SplittingField of p iff (p splits_in E & E == FAdj(F,Roots(E,p)))
proof
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F;
now assume A: p splits_in E & E == FAdj(F,Roots(E,p));
now let K be FieldExtension of F;
assume B: p splits_in K & K is Subfield of E; then
E is K-extending by FIELD_4:7; then
Roots(E,p) is Subset of K & F is Subfield of K
by A,B,FIELD_8:27,FIELD_4:7; then
FAdj(F,Roots(E,p)) is Subfield of K by B,FIELD_6:37;
hence K == E by A,B,EC_PF_1:5;
end;
hence E is SplittingField of p by A,FIELD_8:def 1;
end;
hence thesis by FIELD_8:34,FIELD_8:def 1;
end;
begin :: Minimal Polynomials in Galois Extensions
G0: for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E) st Fix(E,G) == F
for g being Element of G holds g in Auts(E,F)
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E);
assume AS: Fix(E,G) == F;
let g be Element of G;
the carrier of G c= the carrier of Aut(E) by GROUP_2:def 5; then
reconsider g1 = g as Element of the carrier of Aut E;
now let a be Element of F;
a in Fix(E,G) by AS; then
a in Fixed_El(E,G) by GALOIS_1:def 17; then
consider a1 being Element of E such that
A: a1 = a & for f being Function of E,E st f in G holds f.a1 = a1;
g1 in G;
hence g1.a = a by A;
end;
then g1 is F-fixing;
hence thesis;
end;
theorem mainG1:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E) st Fix(E,G) == F holds G is Subgroup of Aut(E,F)
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E);
assume AS: Fix(E,G) == F;
reconsider G1 = the carrier of G as non empty Subset of Aut(E)
by GROUP_2:def 5;
C: the carrier of G c= the carrier of Aut(E,F) by AS,G0;
the multF of G = (the multF of Aut(E))||the carrier of G &
the multF of Aut(E,F) = (the multF of Aut(E))||the carrier of Aut(E,F)
by GROUP_2:def 5; then
the multF of G = (the multF of Aut(E,F))||the carrier of G
by C,ZFMISC_1:96,RELAT_1:74;
hence thesis by C,GROUP_2:def 5;
end;
theorem G1:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E) st Fix(E,G) == F
for p being Polynomial of E
st for g being Element of the carrier of G holds (PolyHom g).p = p
holds p is Polynomial of F
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E);
assume AS1: Fix(E,G) == F;
let p be Polynomial of E;
assume AS2: for f being Element of the carrier of G holds (PolyHom f).p = p;
now let o be object;
assume A: o in Coeff p;
Coeff p = {p.i where i is Element of NAT : p.i <> 0.E} by FIELD_7:def 3; then
consider i being Element of NAT such that
B: o = p.i & p.i <> 0.E by A;
now let g be Function of E,E;
assume C: g in G; then
reconsider g1 = g as additive Function of E,E;
reconsider p1 = p as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
thus p.i = ((PolyHom g1).p1).i by C,AS2 .= g.(p.i) by GALOIS_0:def 27;
end;
then p.i in Fixed_El(E,G);
hence o in the carrier of F by B,AS1,GALOIS_1:def 17;
end;
then Coeff p c= the carrier of F;
hence thesis by FIELD_7:11;
end;
theorem G3:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E) st Fix(E,G) == F
for g being Element of the carrier of G
for a being Element of E st Conj(a,G) is finite
holds g .: Conj(a,G) = Conj(a,G)
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E);
assume AS: Fix(E,G) == F;
let g be Element of the carrier of G, a be Element of E;
assume Conj(a,G) is finite; then
reconsider Z = Conj(a,G) as finite Subset of E;
reconsider G1 = the carrier of G as non empty Subset of Aut(E)
by GROUP_2:def 5;
M: G is Subgroup of Aut(E,F) by AS,mainG1; then
N: the carrier of G c= the carrier of Aut(E,F) by GROUP_2:def 5;
A: now let o be object;
assume o in Z; then
consider f being Element of the carrier of G such that
B: o = f.a;
reconsider g1 = g as F-fixing Automorphism of E by M;
reconsider f1 = f as F-fixing Automorphism of E by M;
reconsider h = (g1") * f1 as F-fixing Automorphism of E;
reconsider x = g, y = f as Element of Aut(E,F) by N;
x" = g" by M,GROUP_2:48; then
B3: x" * y = g" * f by M,GROUP_2:43;
g1" = x" by G3a; then
g1" * f1 = x" * y by G3b; then
C: h.a in Z by B3;
D: dom g = the carrier of E by FUNCT_2:def 1;
F: rng g1 = the carrier of E by FUNCT_2:def 3;
g.(h.a)
= g1.((g1").(f.a)) by FUNCT_2:15
.= (g1*(g1")).(f.a) by FUNCT_2:15
.= (id the carrier of E).(f.a) by F,FUNCT_2:29;
hence o in g.:Z by B,C,D,FUNCT_1:def 6;
end;
now let o be object;
assume o in g.:Z; then
consider x being object such that
B: x in dom g & x in Z & o = g.x by FUNCT_1:def 6;
consider f being Element of the carrier of G such that
C: x = f.a by B;
reconsider g1 = g as F-fixing Automorphism of E by M;
reconsider f1 = f as F-fixing Automorphism of E by M;
reconsider x = g, y = f as Element of Aut(E,F) by N;
E: g1 * f1 = x * y by G3b .= g * f by M,GROUP_2:43;
o = (g1*f1).a by B,C,FUNCT_2:15;
hence o in Z by E;
end;
hence thesis by A,TARSKI:2;
end;
theorem GG:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E) st Fix(E,G) == F
for a being F-algebraic Element of E
for Z being non empty finite Subset of E st Z = Conj(a,G)
for p being Ppoly of E,Z holds p = MinPoly(a,F)
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E);
assume AS: Fix(E,G) == F;
let a be F-algebraic Element of E, Z be non empty finite Subset of E;
assume AS1: Z = Conj(a,G);
let p be Ppoly of E,Z;
reconsider p1 = p as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
deg p1 > 0 by RATFUNC1:def 2; then
reconsider p1 = p as non constant Element of the carrier of Polynom-Ring E
by RING_4:def 4;
now let f be Element of the carrier of G;
Z = f.:Z by AS,AS1,G3; then
(PolyHom f).p is Ppoly of E,Z by GALOIS_0:44;
hence (PolyHom f).p = p by FIELD_14:21;
end; then
reconsider q = p as Polynomial of F by AS,G1;
reconsider q as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
deg p1 > 0 by RATFUNC1:def 2; then
deg q > 0 by FIELD_4:20; then
reconsider q as non constant Element of the carrier of Polynom-Ring F
by RING_4:def 4;
I: F is Subfield of E by FIELD_4:7; then
1.F = 1.E by EC_PF_1:def 1 .= LC p by RATFUNC1:def 7
.= LC q by FIELD_8:5; then
H: q is monic &
(Omega).Aut(E,F) = Aut(E,F) by GROUP_2:def 8,RATFUNC1:def 7;
id E = 1_Aut(E) by GALOIS_1:6 .= 1_G by GROUP_2:44; then
(id E).a in the set of all f.a
where f is Element of the carrier of G; then
A: 0.E = eval(p1,a) by AS1,RING_5:62 .= Ext_eval(q,a) by FIELD_4:26;
now assume q is reducible; then
consider r being monic Element of the carrier of Polynom-Ring F such that
A1: r divides q & 1 <= deg r & deg r < deg q by FIELD_15:19;
consider s1 being Polynomial of F such that
A2: r *' s1 = q by A1,RING_4:1;
reconsider s = s1 as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider s as non zero Element of the carrier of Polynom-Ring F by A2;
A3: now assume A4: deg s >= deg q;
A5: r <> 0_.(F) & s <> 0_.(F);
deg s + deg r >= deg q + 1 by A1,A4,XREAL_1:7; then
deg s + deg r - 0 > deg q + 1 - 1 by XREAL_1:15;
hence contradiction by A5,A2,HURWITZ:23;
end;
F is Subring of E by I,FIELD_5:12; then
0.E = Ext_eval(r,a) * Ext_eval(s,a) by A,A2,ALGNUM_1:20; then
per cases by VECTSP_2:def 1;
suppose A5: 0.E = Ext_eval(r,a);
now let o be object;
assume A6: o in Z; then
reconsider b = o as Element of E;
consider f1 being Element of the carrier of G such that
A8: b = f1.a by AS1,A6;
G is Subgroup of Aut(E,F) by AS,mainG1; then
f1 in the carrier of Aut(E,F); then
consider g being Element of the carrier of Aut(E,F) such that
A4: b = g.a by A8;
A7: Roots(E,r) ={a where a is Element of E : a is_a_root_of r,E}
by FIELD_4:def 4;
Ext_eval(r,b) = g.(Ext_eval(r,a)) by A4,GALOIS_0:40 .= 0.E by A5;
then b is_a_root_of r,E by FIELD_4:def 2;
hence o in Roots(E,r) by A7;
end; then
Z c= Roots(E,r); then
card Z <= card Roots(E,r) by NAT_1:43; then
deg p1 <= card Roots(E,r) by RING_5:60; then
deg q <= card Roots(E,r) &
card Roots(E,r) <= deg r by FIELD_16:11,FIELD_4:20;
hence contradiction by A1,XXREAL_0:2;
end;
suppose A5: 0.E = Ext_eval(s,a);
now let o be object;
assume A6: o in Z; then
reconsider b = o as Element of E;
consider f1 being Element of the carrier of G such that
A8: b = f1.a by AS1,A6;
G is Subgroup of Aut(E,F) by AS,mainG1; then
f1 in the carrier of Aut(E,F); then
consider g being Element of the carrier of Aut(E,F) such that
A4: b = g.a by A8;
A7: Roots(E,s) ={a where a is Element of E : a is_a_root_of s,E}
by FIELD_4:def 4;
Ext_eval(s,b) = g.(Ext_eval(s,a)) by A4,GALOIS_0:40 .= 0.E by A5;
then b is_a_root_of s,E by FIELD_4:def 2;
hence o in Roots(E,s) by A7;
end; then
Z c= Roots(E,s); then
card Z <= card Roots(E,s) by NAT_1:43; then
deg p1 <= card Roots(E,s) by RING_5:60; then
deg q <= card Roots(E,s) &
card Roots(E,s) <= deg s by FIELD_16:11,FIELD_4:20;
hence contradiction by A3,XXREAL_0:2;
end;
end;
hence thesis by H,A,FIELD_6:52;
end;
theorem Gv:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E) st Fix(E,G) == F
for a being F-algebraic Element of E st Conj(a,G) is finite
holds MinPoly(a,F) is separable & MinPoly(a,F) splits_in E &
Roots(E,MinPoly(a,F)) = Conj(a,G) & deg MinPoly(a,F) = card Conj(a,G)
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E);
assume AS: Fix(E,G) == F;
let a be F-algebraic Element of E;
assume Conj(a,G) is finite; then
reconsider Z = Conj(a,G) as non empty finite Subset of E;
set p = the Ppoly of E,Z;
B: p = MinPoly(a,F) by AS,GG; then
reconsider p1 = p as non constant Element of the carrier of Polynom-Ring F;
H: p is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10; then
C: deg p1 = deg p by FIELD_4:20
.= card Z by RING_5:60
.= card Roots(p) by RING_5:63
.= card Roots(E,p1) by H,FIELD_7:13;
hence MinPoly(a,F) is separable by B,FIELD_15:85;
p = 1.E * p; then
consider b being non zero Element of E, q being Ppoly of E such that
D: MinPoly(a,F) = b * q by B;
thus MinPoly(a,F) splits_in E by D,FIELD_4:def 5;
thus Conj(a,G) = Roots p by RING_5:63
.= Roots(E,MinPoly(a,F)) by B,H,FIELD_7:13;
hence deg MinPoly(a,F) = card Conj(a,G) by B,C;
end;
theorem lem18a:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E) st Fix(E,G) == F
for a being Element of E st Conj(a,G) is finite holds a is F-algebraic
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E);
assume AS: Fix(E,G) == F;
let a be Element of E;
assume Conj(a,G) is finite; then
reconsider Z = Conj(a,G) as non empty finite Subset of E;
set p = the Ppoly of E,Z;
reconsider p1 = p as non zero Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
now let f be Element of the carrier of G;
Z = f.:Z by AS,G3; then
(PolyHom f).p is Ppoly of E,Z by GALOIS_0:44;
hence (PolyHom f).p = p by FIELD_14:21;
end; then
reconsider q = p as Polynomial of F by AS,G1;
reconsider q as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
p <> 0_.(E); then
p <> 0_.(F) by FIELD_4:12; then
reconsider q as non zero Element of the carrier of Polynom-Ring F
by UPROOTS:def 5;
1_G = 1_(Aut E) by GROUP_2:44 .= id E by GALOIS_1:6; then
(id E).a in the set of all f.a where f is Element of the carrier of G;
then 0.E = eval(p1,a) by RING_5:62 .= Ext_eval(q,a) by FIELD_4:26;
hence a is F-algebraic by FIELD_6:43;
end;
registration
let F be Field;
let E be GaloisExtension of F;
let a be F-algebraic Element of E;
cluster MinPoly(a,F) -> separable;
coherence
proof
A: Conj a = Conj(a,Aut(E,F));
F == Fix(E,Aut(E,F)) by GALOIS_1:def 18;
hence thesis by A,Gv;
end;
end;
theorem
for F being Field
for E being GaloisExtension of F
for a being F-algebraic Element of E
holds MinPoly(a,F) splits_in E &
Roots(E,MinPoly(a,F)) = Conj a & deg MinPoly(a,F) = card(Conj a)
proof
let F be Field, E be GaloisExtension of F, a be F-algebraic Element of E;
A: Conj a = Conj(a,Aut(E,F));
F == Fix(E,Aut(E,F)) by GALOIS_1:def 18;
hence thesis by A,Gv;
end;
theorem
for F being Field
for E being GaloisExtension of F
for a being Element of E holds a is F-algebraic iff Conj a is finite
proof
let F be Field, E be GaloisExtension of F;
let a be Element of E;
Fix(E,Aut(E,F)) == F by GALOIS_1:def 18;
hence thesis by lem18a;
end;
begin :: Main Characterization of finite Galois Extensions
mainA:
for F being Field
for E being F-finite GaloisExtension of F holds E is F-normal F-separable
proof
let F be Field, E be F-finite GaloisExtension of F;
consider T being finite F-algebraic Subset of E such that
A: E == FAdj(F,T) by FIELD_7:37;
per cases;
suppose T = {}; then
T c= the carrier of F; then
A3: FAdj(F,T) == F by FIELD_7:3; then
A4: E == F by A;
set p = the linear Element of the carrier of Polynom-Ring F;
F is SplittingField of p by FIELD_13:17;
hence E is F-normal by A4,FIELD_13:16;
now let a be Element of E;
reconsider a1 = a as Element of F by A,A3;
MinPoly(a,F) = X-a by A,A3,FIELD_6:54 .= X-a1 by FIELD_4:21;
hence a is F-separable by FIELD_15:def 5;
end;
hence E is F-separable by FIELD_15:def 6;
end;
suppose T <> {};
then reconsider T as non empty finite Subset of E;
now let a be Element of T;
set p = the Ppoly of E,Conj a;
p = 1.E * p; then
consider b being non zero Element of E, q being Ppoly of E
such that C: p = b * q;
reconsider q1 = q as Ppoly of FAdj(F,T) by A,FIELD_13:12;
reconsider b1 = b as Element of FAdj(F,T) by A;
0.E = 0.FAdj(F,T) & b <> 0.E by A; then
reconsider b1 as non zero Element of FAdj(F,T) by STRUCT_0:def 12;
b * q = b1 * q1 by A,FIELD_13:14; then
consider b being non zero Element of FAdj(F,T), q being Ppoly of FAdj(F,T)
such that D: p = b * q by C;
F == Fix(E,Aut(E,F)) by GALOIS_1:def 18; then
p = MinPoly(a,F) by GG;
hence MinPoly(a,F) splits_in FAdj(F,T) by D,FIELD_4:def 5;
end; then
FAdj(F,T) is F-normal by FIELD_13:58; then
consider p being non constant Element of the carrier of Polynom-Ring F
such that C: FAdj(F,T) is SplittingField of p by FIELD_13:55;
thus E is F-normal by C,A,FIELD_13:16;
now let a be Element of E;
MinPoly(a,F) is separable;
hence a is F-separable by FIELD_15:def 5;
end;
hence E is F-separable by FIELD_15:def 6;
end;
end;
mainB:
for F being Field
for E being F-finite FieldExtension of F
st E is F-normal F-separable holds
ex p being separable non constant Element of Polynom-Ring F
st E is SplittingField of p
proof
let F be Field, E be F-finite FieldExtension of F;
assume AS: E is F-normal F-separable;
consider T being finite F-algebraic Subset of E such that
A: E == FAdj(F,T) by FIELD_7:37;
consider u being non constant Element of the carrier of Polynom-Ring F
such that A0: E is SplittingField of u by AS,FIELD_13:55;
A1: FAdj(F,T) is F-normal by A,A0,FIELD_13:16;
per cases;
suppose T = {}; then
T c= the carrier of F; then
FAdj(F,T) == F by FIELD_7:3; then
A2: E == F by A;
set a = the Element of F;
set p = X-a;
F is SplittingField of p by FIELD_13:17; then
E is SplittingField of p by A2,FIELD_13:16;
hence thesis;
end;
suppose T <> {}; then
reconsider T as non empty finite F-separable Subset of E by AS;
set p = ProductMinPolys T, f = FinSeq_MinPolys T, S = MinPolys T;
deg p > 0 by RING_4:def 4; then
I: p is non constant Polynomial of F by RATFUNC1:def 2;
now let i be Element of dom f, q be Polynomial of F;
assume C3: q = f.i;
rng f c= S by FINSEQ_1:def 4; then
f.i in S by FUNCT_1:3; then
consider a being F-algebraic Element of E such that
C4: f.i = MinPoly(a,F) & a in T;
T is Subset of FAdj(F,T) by FIELD_6:35; then
reconsider a1 = a as Element of FAdj(F,T) by C4;
E is FAdj(F,T)-extending by FIELD_4:7; then
Ext_eval(MinPoly(a,F),a1) = Ext_eval(MinPoly(a,F),a) by FIELD_6:11
.= 0.E by FIELD_6:52 .= 0.FAdj(F,T) by EC_PF_1:def 1; then
a1 is_a_root_of MinPoly(a,F),FAdj(F,T) by FIELD_4:def 2;
hence q is constant or q splits_in FAdj(F,T)
by A1,C3,C4,FIELD_13:def 5,FIELD_4:def 3;
end; then
E: p splits_in FAdj(F,T) by I,FIELD_13:6;
now let K be FieldExtension of F;
assume E1: p splits_in K & K is Subfield of FAdj(F,T); then
FAdj(F,T) is K-extending by FIELD_4:7; then
E2: Roots(FAdj(F,T),p) c= the carrier of K by E,E1,FIELD_8:27;
E3: K is Subfield of E & F is Subfield of K by E1,EC_PF_1:5,FIELD_4:7;
now let o be object;
assume E4: o in T; then
reconsider a = o as F-algebraic Element of E;
T is Subset of FAdj(F,T) by FIELD_6:35; then
reconsider a1 = a as Element of FAdj(F,T) by E4;
E is FAdj(F,T)-extending by FIELD_4:7; then
E5: Ext_eval(MinPoly(a,F),a1) = Ext_eval(MinPoly(a,F),a) by FIELD_6:11
.= 0.E by FIELD_6:52 .= 0.FAdj(F,T) by EC_PF_1:def 1;
rng f = S by FUNCT_2:def 3; then
MinPoly(a,F) in rng f by E4; then
consider i being object such that
E6: i in dom f & MinPoly(a,F) = f.i by FUNCT_1:def 3;
reconsider i as Element of dom f by E6;
Ext_eval(p,a1) = 0.FAdj(F,T) by E5,E6,FIELD_13:4; then
E7: a1 is_a_root_of p,FAdj(F,T) by FIELD_4:def 2;
Roots(FAdj(F,T),p) = {a where a is Element of FAdj(F,T) :
a is_a_root_of p,FAdj(F,T)} by FIELD_4:def 4;
hence o in Roots(FAdj(F,T),p) by E7;
end; then
T c= the carrier of K by E2;
hence K == FAdj(F,T) by E1,E3,FIELD_6:37;
end; then
FAdj(F,T) is SplittingField of p by E,FIELD_8:def 1; then
E is SplittingField of p by A,FIELD_13:16;
hence ex p being separable non constant Element of Polynom-Ring F
st E is SplittingField of p;
end;
end;
theorem
for F being Field
for p being irreducible Element of the carrier of Polynom-Ring F
for E being SplittingField of p
for a,b being Element of E st a in Roots(E,p) & b in Roots(E,p)
ex h being F-fixing Automorphism of E st h.a = b
proof
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
let E be SplittingField of p, a,b be Element of E;
assume AS: a in Roots(E,p) & b in Roots(E,p);
id F is isomorphism; then
reconsider F1 = F as F-isomorphic F-homomorphic Field
by RING_3:def 4,RING_2:def 4;
reconsider h = id F as Isomorphism of F,F1;
reconsider E1 = E as FieldExtension of F1;
reconsider b1 = b as Element of E1;
H: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E}
by FIELD_4:def 4; then
consider a1 being Element of E such that
I: a = a1 & a1 is_a_root_of p,E by AS;
A: Ext_eval(p,a) = 0.E by I,FIELD_4:def 2;
now let i be Nat;
thus ((PolyHom h).p).i = h.(p.i) by FIELD_1:def 2 .= p.i;
end; then
J: (PolyHom h).p = p;
consider b2 being Element of E such that
K: b = b2 & b2 is_a_root_of p,E by H,AS;
B: Ext_eval((PolyHom h).p,b) = 0.E1 by K,J,FIELD_4:def 2; then
C: Psi(a,b1,h,p) is h-extending isomorphism by A,FIELD_8:55; then
reconsider K1 = FAdj(F,{b}) as
FAdj(F,{a})-isomorphic FAdj(F,{a})-homomorphic Field
by RING_3:def 4,RING_2:def 4;
reconsider g = Psi(a,b1,h,p) as Isomorphism of FAdj(F,{a}),K1 by C;
the carrier of Polynom-Ring F c=
the carrier of Polynom-Ring FAdj(F,{a}) by FIELD_4:10; then
reconsider p1 = p as Element of the carrier of Polynom-Ring FAdj(F,{a});
deg p > 0 & deg p = deg p1 by RING_4:def 4,FIELD_4:20; then
reconsider p1 as non constant
Element of the carrier of Polynom-Ring FAdj(F,{a})
by RING_4:def 4;
E is FAdj(F,{a})-extending by FIELD_4:7; then
reconsider E2 = E as SplittingField of p1 by FIELD_8:53;
now let i be Nat;
thus ((PolyHom g).p1).i = g.(p.i) by FIELD_1:def 2
.= h.(p.i) by C
.= p1.i;
end; then
(PolyHom g).p1 = p1; then
reconsider E3 = E as SplittingField of (PolyHom g).p1 by spl1;
consider f being Function of E2,E3 such that
D: f is g-extending isomorphism by FIELD_8:57;
reconsider f as Automorphism of E by D;
now let b be Element of F;
F is Subfield of FAdj(F,{a}) by FIELD_4:7;
then the carrier of F c= the carrier of FAdj(F,{a}) by EC_PF_1:def 1;
then b in FAdj(F,{a});
hence f.b = g.b by D .= h.b by C .= b;
end; then
f is F-fixing; then
reconsider f as F-fixing Automorphism of E;
take f;
a in {a} & {a} is Subset of FAdj(F,{a}) by TARSKI:def 1,FIELD_6:35;
hence f.a = g.a by D .= b by A,B,FIELD_13:26;
end;
theorem FixAut:
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
for E being SplittingField of p
for a,b being Element of E
st a in Roots(E,p) & b in Roots(E,p) & MinPoly(a,F) = MinPoly(b,F)
ex h being F-fixing Automorphism of E st h.a = b
proof
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
let E be SplittingField of p, a,b be Element of E;
assume AS: a in Roots(E,p) & b in Roots(E,p) & MinPoly(a,F) = MinPoly(b,F);
set q = MinPoly(a,F);
id F is isomorphism; then
reconsider F1 = F as F-isomorphic F-homomorphic Field
by RING_3:def 4,RING_2:def 4;
reconsider h = id F as Isomorphism of F,F1;
reconsider E1 = E as FieldExtension of F1;
reconsider b1 = b as Element of E1;
A: Ext_eval(q,a) = 0.E by FIELD_6:52;
now let i be Nat;
thus ((PolyHom h).q).i = h.(q.i) by FIELD_1:def 2 .= q.i;
end; then
(PolyHom h).q = q; then
B: Ext_eval((PolyHom h).q,b) = 0.E1 by AS,FIELD_6:52; then
C: Psi(a,b1,h,q) is h-extending isomorphism by A,FIELD_8:55; then
reconsider K1 = FAdj(F,{b}) as
FAdj(F,{a})-isomorphic FAdj(F,{a})-homomorphic Field
by RING_3:def 4,RING_2:def 4;
reconsider g = Psi(a,b1,h,q) as Isomorphism of FAdj(F,{a}),K1 by C;
the carrier of Polynom-Ring F c=
the carrier of Polynom-Ring FAdj(F,{a}) by FIELD_4:10; then
reconsider p1 = p as Element of the carrier of Polynom-Ring FAdj(F,{a});
deg p > 0 & deg p = deg p1 by RING_4:def 4,FIELD_4:20; then
reconsider p1 as non constant
Element of the carrier of Polynom-Ring FAdj(F,{a})
by RING_4:def 4;
E is FAdj(F,{a})-extending by FIELD_4:7; then
reconsider E2 = E as SplittingField of p1 by FIELD_8:53;
now let i be Nat;
thus ((PolyHom g).p1).i = g.(p.i) by FIELD_1:def 2
.= h.(p.i) by C
.= p1.i;
end; then
(PolyHom g).p1 = p1; then
reconsider E3 = E as SplittingField of (PolyHom g).p1 by spl1;
consider f being Function of E2,E3 such that
D: f is g-extending isomorphism by FIELD_8:57;
reconsider f as Automorphism of E by D;
now let c be Element of F;
F is Subfield of FAdj(F,{a}) by FIELD_4:7;
then the carrier of F c= the carrier of FAdj(F,{a}) by EC_PF_1:def 1;
then c in FAdj(F,{a});
hence f.c = g.c by D .= h.c by C .= c;
end; then
f is F-fixing; then
reconsider f as F-fixing Automorphism of E;
take f;
a in {a} & {a} is Subset of FAdj(F,{a}) by TARSKI:def 1,FIELD_6:35;
hence f.a = g.a by D .= b by A,B,FIELD_13:26;
end;
Th28:
for L be non empty ZeroStr, a be Element of L holds (a|L).0 = a
proof
let L be non empty ZeroStr, a be Element of L;
0 in dom 0_.(L);
hence (a|L).0 = a by FUNCT_7:31;
end;
mainC:
for F being Field
for E being F-finite FieldExtension of F
st ex p being separable non constant Element of Polynom-Ring F
st E is SplittingField of p holds E is F-Galois
proof
let F be Field, E be F-finite FieldExtension of F;
assume AS: ex p being separable non constant Element of Polynom-Ring F
st E is SplittingField of p;
defpred P[Nat] means
for F being Field
for E being F-finite FieldExtension of F
for p being separable non constant Element of Polynom-Ring F
st card(Roots(E,p)\(the carrier of F)) = $1 & E is SplittingField of p
holds the carrier of Fix(E,Aut(E,F)) c= the carrier of F;
IS: now let k be Nat;
assume IV: for n being Nat st n < k holds P[n];
per cases;
suppose AS: k = 0;
now let F be Field, E be F-finite FieldExtension of F;
let p be separable non constant Element of Polynom-Ring F;
assume A: card(Roots(E,p)\(the carrier of F)) = 0 &
E is SplittingField of p; then
B: E == FAdj(F,Roots(E,p)) by FIELD_8:34;
Roots(E,p)\(the carrier of F) = {} by A;
then Roots(E,p) c= the carrier of F by XBOOLE_1:37;
then FAdj(F,Roots(E,p)) == F by FIELD_7:3; then
C: E == F by B;
reconsider E1 = F as FieldExtension of F by FIELD_4:6;
E1 is F-Galois by GALOIS_1:24;
then Fix(E,Aut(E,F)) == F by C,lemBD;
hence the carrier of Fix(E,Aut(E,F)) c= the carrier of F;
end;
hence P[k] by AS;
end;
suppose AS1: k > 0;
now let F be Field, E be F-finite FieldExtension of F;
let p be separable non constant Element of Polynom-Ring F;
assume AS: card(Roots(E,p)\(the carrier of F)) = k &
E is SplittingField of p;
reconsider p1 = p as Polynomial of F by POLYNOM3:def 10;
now let o be object;
assume H1: o in the carrier of Fix(E,Aut(E,F));
the carrier of Fix(E,Aut(E,F)) c= the carrier of E by EC_PF_1:def 1;
then reconsider a = o as Element of E by H1;
per cases;
suppose Z: not a in the carrier of F;
set b = the Element of Roots(E,p)\(the carrier of F);
A0: Roots(E,p)\(the carrier of F) <> {} by AS1,AS; then
A1: b in Roots(E,p) & not b in the carrier of F
by XBOOLE_0:def 5; then
reconsider b as Element of E;
Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E}
by FIELD_4:def 4; then
consider b1 being Element of E such that
A2: b1 = b & b1 is_a_root_of p,E by A1;
A: Ext_eval(p1,b) = 0.E & not b in the carrier of F
by A0,A2,FIELD_4:def 2,XBOOLE_0:def 5; then
N: Roots(E,MinPoly(b,F)) c= Roots(E,p) by rot,FIELD_6:53;
set m = deg MinPoly(b,F);
reconsider E1 = E as FieldExtension of FAdj(F,{b}) by FIELD_4:7;
reconsider E1 as FAdj(F,{b})-finite FieldExtension of FAdj(F,{b})
by FIELD_7:31;
the carrier of Polynom-Ring F c=
the carrier of Polynom-Ring FAdj(F,{b}) by FIELD_4:10; then
reconsider p2 = p as
Element of the carrier of Polynom-Ring FAdj(F,{b});
deg p1 > 0 & deg p1 = deg p2 by RING_4:def 4,FIELD_4:20; then
reconsider p2 as non constant Element of Polynom-Ring FAdj(F,{b})
by RING_4:def 4;
reconsider p2 as separable non constant
Element of Polynom-Ring FAdj(F,{b}) by FIELD_15:88;
B: E1 is SplittingField of p2 by AS,spl1;
reconsider k1 = card(Roots(E1,p2)\(the carrier of FAdj(F,{b})))
as Element of NAT;
B1: Roots(E1,p2) = Roots(E,p) by FIELD_8:7;
F is Subfield of FAdj(F,{b}) by FIELD_4:7; then
B2: the carrier of F c= the carrier of FAdj(F,{b})
by EC_PF_1:def 1;
B3: b in Roots(E,p)\(the carrier of F) by A0;
b in {b} & {b} is Subset of FAdj(F,{b})
by TARSKI:def 1,FIELD_6:35; then
not b in Roots(E1,p2)\(the carrier of FAdj(F,{b}))
by XBOOLE_0:def 5; then
Roots(E1,p2)\(the carrier of FAdj(F,{b})) c<
Roots(E,p)\(the carrier of F)
by B3,B2,B1,XBOOLE_1:35,XBOOLE_0:def 8;
then k1 < k by AS,CARD_2:48; then
C: the carrier of Fix(E1,Aut(E1,FAdj(F,{b})))
c= the carrier of FAdj(F,{b}) by B,IV;
a in the carrier of FAdj(F,{b})
proof
F is Subfield of FAdj(F,{b}) & FAdj(F,{b}) is Subfield of E
by FIELD_4:7; then
FAdj(F,{b}) in IntermediateFields(E,F) by FIELD_14:4; then
reconsider Fb = FAdj(F,{b}) as IntermediateField of E,F
by GALOIS_0:def 5;
D: the carrier of Fix(E,Aut(E,Fb)) c=
the carrier of Fix(E1,Aut(E1,FAdj(F,{b})))
by GALOIS_0:def 6;
Aut(E,Fb) is Subgroup of Aut(E,F) by GALOIS_1:18; then
Fix(E,Aut(E,F)) is Subfield of Fix(E,Aut(E,Fb)) by GALOIS_1:20;
then the carrier of Fix(E,Aut(E,F)) c=
the carrier of Fix(E,Aut(E,Fb)) by EC_PF_1:def 1;
hence thesis by H1,D,C;
end; then
consider q being Polynomial of F such that
E: deg q < m & a = Ext_eval(q,b) by REALALG3:23;
now assume E0: q is constant;
reconsider q1 = q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
deg q <= 0 by E0,RATFUNC1:def 2; then
consider c being Element of F such that
E1: q1 = c|F by RING_4:20,RING_4:def 4;
Ext_eval(q,b) = c by E1,R58;
hence contradiction by E,Z;
end; then
reconsider q as non constant Polynomial of F;
reconsider qE = q as Polynomial of E by FIELD_4:8;
q is Element of the carrier of Polynom-Ring F &
qE is Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10; then
deg q > 0 & deg qE = deg q by RATFUNC1:def 2,FIELD_4:20; then
reconsider qE as non constant Polynomial of E by RATFUNC1:def 2;
Ext_eval(MinPoly(b,F),b) = 0.E by FIELD_6:52; then
F1: b is_a_root_of MinPoly(b,F),E by FIELD_4:def 2;
Roots(E,MinPoly(b,F)) = {a where a is Element of E :
a is_a_root_of MinPoly(b,F),E} by FIELD_4:def 4; then
F: b in Roots(E,MinPoly(b,F)) by F1;
G: for c being Element of E st c in Roots(E,MinPoly(b,F))
ex f being F-fixing Automorphism of E st f.b = c
proof
let c be Element of E;
assume G1: c in Roots(E,MinPoly(b,F));
Roots(E,MinPoly(b,F)) = {a where a is Element of E :
a is_a_root_of MinPoly(b,F),E} by FIELD_4:def 4; then
consider c1 being Element of E such that
G4: c1 = c & c1 is_a_root_of MinPoly(b,F),E by G1;
Ext_eval(MinPoly(b,F),c) = 0.E by G4,FIELD_4:def 2; then
MinPoly(c,F) = MinPoly(b,F) by FIELD_6:52;
hence thesis by AS,F,G1,N,FixAut;
end;
set r = qE - (a|E);
H: deg r = deg q
proof
F is Subfield of E by FIELD_4:7; then
0.F = 0.E by EC_PF_1:def 1; then
a <> 0.E by Z; then
deg(a|E) = 0 by RING_4:21; then
H2: deg(qE - (a|E)) = deg qE by RATFUNC1:def 2,NIVEN:43;
q is Element of the carrier of Polynom-Ring F &
qE is Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
hence thesis by H2,FIELD_4:20;
end;
now let o be object;
assume H0: o in Roots(E,MinPoly(b,F)); then
reconsider c = o as Element of E;
consider f being F-fixing Automorphism of E such that
H2: f.b = c by H0,G;
H4: qE is Element of the carrier of Polynom-Ring E &
q is Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
f.a = a
proof
a in Fixed_El(E,Aut(E,F)) by H1,GALOIS_1:def 17; then
consider a1 being Element of E such that
H6: a1 = a & for g being Function of E,E
st g in Aut(E,F) holds g.a1 = a1;
f in Aut(E,F);
hence thesis by H6;
end; then
H3: Ext_eval(q,c) = a by E,H2,H4,GALOIS_0:40;
eval(r,c) = eval(qE,c) - eval(a|E,c) by POLYNOM4:21
.= eval(qE,c) - a by RING_5:8
.= Ext_eval(q,c) - a by H4,FIELD_4:26
.= 0.E by H3,RLVECT_1:15;
then c is_a_root_of r by POLYNOM5:def 7;
hence o in Roots r by POLYNOM5:def 10;
end; then
I: Roots(E,MinPoly(b,F)) c= Roots r;
reconsider p3 = p as separable non constant
Element of the carrier of Polynom-Ring F;
consider t being Polynomial of F such that
I1: MinPoly(b,F) *' t = p3 by A,FIELD_6:53,RING_4:1;
reconsider t as non zero Polynomial of F by I1;
t is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
then I2: MinPoly(b,F) is separable by I1,FIELD_15:87;
reconsider p4 = MinPoly(b,F) as Polynomial of F;
deg MinPoly(b,F) > 0 by RING_4:def 4; then
reconsider p4 as non constant Polynomial of F by RATFUNC1:def 2;
I4: p4 *' t = p3 by I1;
p3 splits_in E by AS,FIELD_8:def 1; then
J: card Roots(E,MinPoly(b,F)) = m by I2,I4,splitE,separ;
now assume r <> 0_.(E); then
reconsider r as non zero Polynomial of E by UPROOTS:def 5;
J1: card(Roots r) <= deg q by H,RING_5:22;
card(Roots r) >= m by I,J,NAT_1:43;
hence contradiction by E,J1,XXREAL_0:2;
end;
then 0.E = r.0
.= qE.0 - (a|E).0 by POLYNOM3:27
.= qE.0 - a by Th28;
then a = q.0 by RLVECT_1:21;
hence o in the carrier of F;
end;
suppose a in the carrier of F;
hence o in the carrier of F;
end;
end;
hence the carrier of Fix(E,Aut(E,F)) c= the carrier of F;
end;
hence P[k];
end;
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(IS);
consider p being separable non constant Element of Polynom-Ring F such that
K0: E is SplittingField of p by AS;
consider n being Element of NAT such that
H: card(Roots(E,p)\(the carrier of F)) = n;
J: the carrier of Fix(E,Aut(E,F)) c= the carrier of F by H,I,K0;
F is Subfield of Fix(E,Aut(E,F)) by GALOIS_1:15; then
the carrier of F c= the carrier of Fix(E,Aut(E,F)) by EC_PF_1:def 1; then
K1: the carrier of F
= the carrier of Fix(E,Aut(E,F)) by J,XBOOLE_0:def 10
.= Fixed_El(E,Aut(E,F)) by GALOIS_1:def 17;
K2: the carrier of Fix(E,Aut(E,F)) = Fixed_El(E,Aut(E,F)) &
the addF of Fix(E,Aut(E,F))
= (the addF of E)||Fixed_El(E,Aut(E,F)) &
the multF of Fix(E,Aut(E,F))
= (the multF of E)||Fixed_El(E,Aut(E,F)) &
1.Fix(E,Aut(E,F)) = 1.E &
0.Fix(E,Aut(E,F)) = 0.E by GALOIS_1:def 17;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E &
the addF of F = (the addF of E) || the carrier of F &
the multF of F = (the multF of E) || the carrier of F &
1.F = 1.E & 0.F = 0.E by EC_PF_1:def 1; then
Fix(E,Aut(E,F)) == F by K1,K2;
hence thesis;
end;
theorem main1:
for F being Field
for E being F-finite FieldExtension of F holds
E is GaloisExtension of F iff E is F-normal F-separable
proof
let F be Field, E be F-finite FieldExtension of F;
now assume E is F-normal F-separable;
then ex p being separable non constant Element of Polynom-Ring F
st E is SplittingField of p by mainB;
hence E is F-Galois by mainC;
end;
hence thesis by mainA;
end;
theorem main2:
for F being Field
for E being F-finite FieldExtension of F
holds E is GaloisExtension of F iff
ex p being separable non constant Element of Polynom-Ring F
st E is SplittingField of p
proof
let F be Field, E be F-finite FieldExtension of F;
now assume E is F-Galois;
then E is F-normal F-separable by mainA;
hence ex p being separable non constant Element of Polynom-Ring F
st E is SplittingField of p by mainB;
end;
hence thesis by mainC;
end;
registration
let F be Field;
cluster -> F-normal F-separable for F-finite GaloisExtension of F;
coherence by main1;
cluster F-normal F-separable -> F-Galois for F-finite FieldExtension of F;
coherence by main1;
end;
registration
let F be Field;
let p be separable non constant Element of the carrier of Polynom-Ring F;
cluster -> F-Galois for SplittingField of p;
coherence by mainC;
end;
begin :: Some Corollaries
col:
for F being Field
for K being F-finite FieldExtension of F
for E being K-extending F-finite FieldExtension of F
st E is GaloisExtension of F holds E is GaloisExtension of K
proof
let F be Field, K be F-finite FieldExtension of F;
let E be K-extending F-finite FieldExtension of F;
assume E is GaloisExtension of F; then
consider p being separable non constant Element of Polynom-Ring F
such that A: E is SplittingField of p by main2;
reconsider p1 = p as Polynomial of F by POLYNOM3:def 10;
the carrier of Polynom-Ring F c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p2 = p as Element of the carrier of Polynom-Ring K;
deg p1 > 0 & deg p1 = deg p2 by RING_4:def 4,FIELD_4:20; then
reconsider p2 as non constant Element of Polynom-Ring K by RING_4:def 4;
reconsider p2 as separable non constant
Element of Polynom-Ring K by FIELD_15:88;
E is SplittingField of p2 by A,FIELD_8:53;
hence thesis;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F holds E is GaloisExtension of K
proof
let F be Field, E be F-finite GaloisExtension of F;
let K be IntermediateField of E,F;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
A: F is Subfield of K & K is Subfield of E by FIELD_14:4;
reconsider K1 = K as FieldExtension of F;
reconsider E1 = E as K1-extending FieldExtension of F by A,FIELD_4:7;
reconsider K1 as F-finite FieldExtension of F;
reconsider E1 = E as K1-extending F-finite FieldExtension of F
by A,FIELD_4:7;
E1 is GaloisExtension of K1 by col;
hence thesis;
end;
theorem
for F being Field
for E being F-finite FieldExtension of F holds
E is GaloisExtension of F iff
for a being Element of E holds card Roots(E,MinPoly(a,F)) = deg(FAdj(F,{a}),F)
proof
let F be Field, E be F-finite FieldExtension of F;
A: now assume A1: E is GaloisExtension of F;
now let a be Element of E;
thus card Roots(E,MinPoly(a,F))
= deg MinPoly(a,F) by A1,FIELD_13:54,separ
.= deg(FAdj(F,{a}),F) by FIELD_6:67;
end;
hence for a being Element of E
holds card Roots(E,MinPoly(a,F)) = deg(FAdj(F,{a}),F);
end;
now assume B1: for a being Element of E
holds card Roots(E,MinPoly(a,F)) = deg(FAdj(F,{a}),F);
now let a be Element of E;
card Roots(E,MinPoly(a,F))
= deg(FAdj(F,{a}),F) by B1
.= deg MinPoly(a,F) by FIELD_6:67;
then MinPoly(a,F) splits_in E &
MinPoly(a,F) is separable by FIELD_16:19;
hence MinPoly(a,F) splits_in E & a is F-separable by FIELD_15:def 5;
end; then
E is F-normal F-separable by FIELD_13:54,FIELD_15:def 6;
hence E is F-Galois;
end;
hence thesis by A;
end;
theorem
for F being Field
for E being FieldExtension of F
for T being finite Subset of E
holds FAdj(F,T) is F-separable iff
for a being Element of E st a in T holds a is F-separable
proof
let F be Field, E be FieldExtension of F, T be finite Subset of E;
I: now assume
A: for a being Element of E st a in T holds a is F-separable;
per cases;
suppose T = {}; then
T c= the carrier of F; then
A1: FAdj(F,T) == F by FIELD_7:3;
set a = the Element of F;
set p = X-a;
F is SplittingField of p by FIELD_13:17; then
reconsider K = FAdj(F,T) as SplittingField of p by A1,FIELD_13:16;
K is F-Galois;
hence FAdj(F,T) is F-separable;
end;
suppose T <> {}; then
reconsider T1 = T as non empty finite F-separable Subset of E by A,defT;
set p = ProductMinPolys T1, f = FinSeq_MinPolys T1, S = MinPolys T1;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring FAdj(F,T)
by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring FAdj(F,T);
deg p > 0 & deg p1 = deg p by FIELD_4:20,RING_4:def 4; then
reconsider p1 as non constant Element of the carrier of Polynom-Ring FAdj(F,T)
by RING_4:def 4;
set K = the SplittingField of p1;
reconsider K as FAdj(F,T)-extending FieldExtension of F;
reconsider T2 = T1 as finite F-algebraic Subset of FAdj(F,T) by FIELD_6:35;
H: E is FAdj(F,T)-extending by FIELD_4:7;
E0: FAdj(F,T) is Subfield of K & FAdj(F,T) is Subfield of E by FIELD_4:7;
now let o be object;
assume E1: o in T2; then
reconsider a = o as F-algebraic Element of FAdj(F,T);
reconsider a1 = a as F-algebraic Element of E by E1;
the carrier of FAdj(F,T) c= the carrier of K by E0,EC_PF_1:def 1; then
reconsider a2 = a1 as Element of K;
MinPoly(a1,F) in S & rng f = S by E1,FUNCT_2:def 3; then
consider i being object such that
E2: i in dom f & MinPoly(a1,F) = f.i by FUNCT_1:def 3;
reconsider i as Element of dom f by E2;
Ext_eval(MinPoly(a1,F),a1) = 0.E by FIELD_6:52; then
0.E = Ext_eval(p,a1) by E2,FIELD_13:4
.= Ext_eval(p,a) by H,FIELD_7:14
.= Ext_eval(p,a2) by FIELD_7:14
.= Ext_eval(p1,a2) by FIELD_7:15; then
Ext_eval(p1,a2) = 0.FAdj(F,T) by EC_PF_1:def 1; then
Ext_eval(p1,a2) = 0.K by E0,EC_PF_1:def 1; then
E3: a2 is_a_root_of p1,K by FIELD_4:def 2;
Roots(K,p1) = {a where a is Element of K : a is_a_root_of p1,K}
by FIELD_4:def 4;
hence o in Roots(K,p1) by E3;
end; then
T2 c= Roots(K,p1) & FAdj(F,T2) == FAdj(F,T) by H,FIELD_13:19; then
reconsider K as SplittingField of p by FIELD_13:23;
K is F-Galois;
hence FAdj(F,T) is F-separable by FIELD_15:94;
end;
end;
now assume A: FAdj(F,T) is F-separable;
now let a be Element of E;
assume B: a in T;
T is Subset of FAdj(F,T) by FIELD_6:35; then
reconsider a1 = a as F-algebraic Element of FAdj(F,T) by A,B;
consider q being non zero Polynomial of F such that
H: Ext_eval(q,a1) = 0.FAdj(F,T) by FIELD_6:43;
E is FAdj(F,T)-extending & q is Element of the carrier of
Polynom-Ring F by POLYNOM3:def 10,FIELD_4:7; then
Ext_eval(q,a) = Ext_eval(q,a1) & 0.FAdj(F,T) = 0.E
by FIELD_6:11,EC_PF_1:def 1; then
reconsider a2 = a as F-algebraic Element of E by H,FIELD_6:43;
E is FAdj(F,T)-extending by FIELD_4:7; then
MinPoly(a1,F) = MinPoly(a2,F) by FIELD_10:10;
hence a is F-separable by A,FIELD_15:def 5;
end;
hence for a being Element of E st a in T holds a is F-separable;
end;
hence thesis by I;
end;
theorem coll:
for F being Field
for E being F-finite FieldExtension of F
ex p being non constant Element of the carrier of Polynom-Ring F,
K being SplittingField of p st K is E-extending
proof
let F be Field, E be F-finite FieldExtension of F;
consider T being finite F-algebraic Subset of E such that
A: E == FAdj(F,T) by FIELD_7:37;
per cases;
suppose T = {}; then
T c= the carrier of F; then
FAdj(F,T) == F by FIELD_7:3; then
A2: E == F by A;
set a = the Element of F;
set p = X-a;
F is SplittingField of p by FIELD_13:17; then
reconsider K = E as SplittingField of p by A2,FIELD_13:16;
take p,K;
E is Subfield of E by FIELD_4:1;
hence thesis by FIELD_4:7;
end;
suppose T <> {}; then
reconsider T as non empty finite F-algebraic Subset of E;
set p = ProductMinPolys T, f = FinSeq_MinPolys T, S = MinPolys T;
take p;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring E;
deg p > 0 & deg p1 = deg p by FIELD_4:20,RING_4:def 4; then
reconsider p1 as non constant Element of the carrier of Polynom-Ring E
by RING_4:def 4;
set K = the SplittingField of p1;
reconsider K as E-extending FieldExtension of F;
E0: E is Subfield of K by FIELD_4:7;
now let o be object;
assume E1: o in T; then
reconsider a = o as Element of E;
the carrier of E c= the carrier of K by E0,EC_PF_1:def 1; then
reconsider a1 = a as Element of K;
MinPoly(a,F) in S & rng f = S by E1,FUNCT_2:def 3; then
consider i being object such that
E2: i in dom f & MinPoly(a,F) = f.i by FUNCT_1:def 3;
reconsider i as Element of dom f by E2;
Ext_eval(MinPoly(a,F),a) = 0.E by FIELD_6:52; then
0.E = Ext_eval(p,a) by E2,FIELD_13:4
.= Ext_eval(p,a1) by FIELD_7:14
.= Ext_eval(p1,a1) by FIELD_7:15; then
Ext_eval(p1,a1) = 0.K by E0,EC_PF_1:def 1; then
E3: a1 is_a_root_of p1,K by FIELD_4:def 2;
Roots(K,p1) = {a where a is Element of K : a is_a_root_of p1,K}
by FIELD_4:def 4;
hence o in Roots(K,p1) by E3;
end; then
T c= Roots(K,p1); then
reconsider K as SplittingField of p by A,FIELD_13:23;
take K;
thus thesis;
end;
end;
coll1:
for F being Field
for E being F-finite FieldExtension of F
ex K being F-finite F-normal FieldExtension of F st K is E-extending
proof
let F be Field, E be F-finite FieldExtension of F;
consider p being non constant Element of the carrier of Polynom-Ring F,
K being SplittingField of p such that
A: K is E-extending by coll;
take K;
thus thesis by A;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
cluster F-normal E-extending for FieldExtension of F;
existence
proof
consider K being F-finite F-normal FieldExtension of F such that
A: K is E-extending by coll1;
take K;
thus thesis by A;
end;
end;
theorem colls:
for F being Field
for E being F-finite F-separable FieldExtension of F
ex p being separable non constant Element of the carrier of Polynom-Ring F,
K being SplittingField of p st K is E-extending
proof
let F be Field, E be F-finite F-separable FieldExtension of F;
consider T being finite F-algebraic Subset of E such that
A: E == FAdj(F,T) by FIELD_7:37;
per cases;
suppose T = {}; then
T c= the carrier of F; then
FAdj(F,T) == F by FIELD_7:3; then
A2: E == F by A;
set a = the Element of F;
set p = X-a;
F is SplittingField of p by FIELD_13:17; then
reconsider K = E as SplittingField of p by A2,FIELD_13:16;
take p,K;
E is Subfield of E by FIELD_4:1;
hence thesis by FIELD_4:7;
end;
suppose T <> {}; then
reconsider T as non empty finite F-separable Subset of E;
set p = ProductMinPolys T, f = FinSeq_MinPolys T, S = MinPolys T;
take p;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring E;
deg p > 0 & deg p1 = deg p by FIELD_4:20,RING_4:def 4; then
reconsider p1 as non constant Element of the carrier of Polynom-Ring E
by RING_4:def 4;
set K = the SplittingField of p1;
reconsider K as E-extending FieldExtension of F;
E0: E is Subfield of K by FIELD_4:7;
now let o be object;
assume E1: o in T; then
reconsider a = o as Element of E;
the carrier of E c= the carrier of K by E0,EC_PF_1:def 1; then
reconsider a1 = a as Element of K;
MinPoly(a,F) in S & rng f = S by E1,FUNCT_2:def 3; then
consider i being object such that
E2: i in dom f & MinPoly(a,F) = f.i by FUNCT_1:def 3;
reconsider i as Element of dom f by E2;
Ext_eval(MinPoly(a,F),a) = 0.E by FIELD_6:52; then
0.E = Ext_eval(p,a) by E2,FIELD_13:4
.= Ext_eval(p,a1) by FIELD_7:14
.= Ext_eval(p1,a1) by FIELD_7:15; then
Ext_eval(p1,a1) = 0.K by E0,EC_PF_1:def 1; then
E3: a1 is_a_root_of p1,K by FIELD_4:def 2;
Roots(K,p1) = {a where a is Element of K : a is_a_root_of p1,K}
by FIELD_4:def 4;
hence o in Roots(K,p1) by E3;
end; then
T c= Roots(K,p1); then
reconsider K as SplittingField of p by A,FIELD_13:23;
take K;
thus thesis;
end;
end;
colls1:
for F being Field
for E being F-finite F-separable FieldExtension of F
ex K being F-finite GaloisExtension of F st K is E-extending
proof
let F be Field, E be F-finite F-separable FieldExtension of F;
consider
p being separable non constant Element of the carrier of Polynom-Ring F,
K being SplittingField of p such that
A: K is E-extending by colls;
take K;
thus thesis by A;
end;
registration
let F be Field;
let E be F-finite F-separable FieldExtension of F;
cluster F-finite E-extending for GaloisExtension of F;
existence
proof
consider K being F-finite GaloisExtension of F such that
A: K is E-extending by colls1;
take K;
thus thesis by A;
end;
end;