:: Introduction to {G}alois Theory
:: by Christoph Schwarzweller and Agnieszka Rowi\'nska-Schwarzweller
::
:: Received December 12, 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, ALGSTR_0, TARSKI, STRUCT_0, SUBSET_1, NAT_1,
SUPINF_2, MESFUNC1, C0SP1, POLYNOM1, RLVECT_5, HURWITZ, CARD_1, EC_PF_1,
FUNCT_1, RELAT_1, NUMBERS, FOMODEL1, YELLOW_8, FIELD_14, ZFMISC_1, CAT_1,
ARYTM_1, FIELD_4, AFINSQ_1, ALGNUM_1, POLYNOM5, WELLORD1, REALSET1,
INT_1, XBOOLE_0, XXREAL_0, COMPLFLD, GLIB_000, SIN_COS, SQUARE_1,
PYTHTRIP, MOD_4, XCMPLX_0, RING_2, RING_3, POLYNOM2, FUNCT_2, FIELD_6,
RING_5, COMPLEX1, FIELD_8, FIELD_9, RATFUNC1, GROUP_1, NEWTON, FINSET_1,
MSSUBFAM, BINOP_2, RLVECT_1, BINOP_1, LATTICES, CATALG_1, GROUP_4,
GRAPH_1, GROUP_2, FIELD_1, FIELD_16, AUTGROUP, GR_CY_1, PEPIN, ORDINAL1,
GROUP_6, GALOIS_0, GALOIS_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, FINSET_1, RELAT_1,
REALSET1, FUNCT_1, ORDINAL1, FUNCT_2, NUMBERS, CARD_1, PARTFUN1,
XCMPLX_0, XXREAL_0, SQUARE_1, NEWTON, INT_2, NAT_D, STRUCT_0, POLYNOM3,
ALGSTR_0, GROUP_1, O_RING_1, COMPLEX1, COMPLFLD, GROUP_2, GROUP_4,
GROUP_6, GR_CY_1, MOD_4, RLVECT_1, MATRLIN, HURWITZ, VECTSP_1, C0SP1,
EC_PF_1, RATFUNC1, ALGNUM_1, POLYNOM4, POLYNOM5, RING_2, RING_3, RING_4,
RING_5, REALALG1, FIELD_1, FIELD_4, FIELD_6, FIELD_8, FIELD_9, FIELD_13,
FIELD_14, FIELD_16, GALOIS_0;
constructors BINOP_1, REAL_1, FINSOP_1, BINARITH, VECTSP_2, POLYNOM3, NAT_6,
NAT_D, CARD_1, RING_3, REALSET1, ALGSTR_2, BINOM, UNIROOTS, MEMBERED,
RINGCAT1, RING_2, EC_PF_1, ALGSEQ_1, VECTSP_9, POLYNOM1, NEWTON, INT_2,
RLVECT_5, RING_4, FUNCOP_1, GROUP_4, ALGNUM_1, GROUP_1, FVSUM_1, RING_5,
SQUARE_1, COMPLEX1, COMPLFLD, BINOP_2, FIELD_7, GROUP_2, POLYDIFF,
REALALG1, POLYNOM4, GR_CY_1, FIELD_8, FIELD_9, FIELD_12, FIELD_13,
FIELD_14, FIELD_15, FIELD_16, GALOIS_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, SUBSET_1, STRUCT_0, VECTSP_1, FUNCT_2,
ALGSTR_1, EC_PF_1, FINSET_1, VECTSP_2, INT_3, ALGSTR_0, COMPLEX1,
COMPLFLD, GROUP_1, RLVECT_1, ALGNUM_1, FUNCT_1, CARD_1, REALSET1,
ALGSEQ_1, RELAT_1, GROUP_4, RING_2, RING_3, RING_4, RING_5, GROUP_2,
GR_CY_1, NEWTON, RINGCAT1, MOD_4, POLYNOM1, POLYNOM3, POLYNOM5, REALALG1,
REALALG3, FIELD_2, FIELD_4, FIELD_5, FIELD_6, FIELD_7, FIELD_8, FIELD_9,
FIELD_16, GALOIS_0;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, VECTSP_1, FIELD_9, FIELD_16,
GALOIS_0;
expansions STRUCT_0, GROUP_1, TARSKI, FUNCT_2, FIELD_7, FIELD_8, FIELD_9,
FIELD_16, GALOIS_0;
theorems GROUP_1, VECTSP_1, RLVECT_1, FUNCT_2, TARSKI, FUNCT_1, EC_PF_1,
RATFUNC1, RING_5, HURWITZ, XREAL_1, INT_1, ORDINAL1, XBOOLE_0, FIELD_4,
CARD_1, CARD_2, POLYNOM3, XCMPLX_1, ZFMISC_1, XXREAL_0, FIELD_6, FIELD_7,
SQUARE_1, XCMPLX_0, COMPLEX1, COMPLFLD, FIELD_1, FIELD_5, FIELD_9, NAT_1,
FIELD_10, FIELD_12, RING_2, RING_3, GROUP_6, RELAT_1, XBOOLE_1, GROUP_2,
NAT_D, GR_CY_1, FINSEQ_4, FIELD_8, FIELD_13, FIELD_14, FIELD_15,
FIELD_16, O_RING_1, GALOIS_0;
schemes NAT_1, FUNCT_2, BINOP_1;
begin :: Preliminaries
definition
let X be non empty set;
let x be Element of X;
redefine func {x} -> Subset of X; :: redefines { (TARSKI, definition)
coherence
proof
now let o be object;
assume o in {x};
then o = x by TARSKI:def 1;
hence o in X;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let F be non quadratic_complete Field;
let a be non square Element of F;
cluster X^2-a -> irreducible;
coherence
proof
set p = X^2-a;
now assume X^2-a is reducible; then
consider q being monic Element of the carrier of Polynom-Ring F such that
A: q divides p & 1 <= deg q & deg q < deg p by FIELD_15:19;
deg p = 2 by FIELD_9:def 4; then
deg q + 1 <= 2 by A,INT_1:7; then
deg q + 1 - 1 <= 2 - 1 by XREAL_1:9; then
consider x,b being Element of F such that
B: x <> 0.F & q = x * rpoly(1,b) by A,XXREAL_0:1,HURWITZ:28;
LC q = x * LC rpoly(1,b) by B,RATFUNC1:18 .= x * 1.F by RATFUNC1:def 7; then
x = 1.F by RATFUNC1:def 7; then
0.F = eval(p,b) by B,A,RING_5:11; then
-a + 0.F * b + 1.F * b^2 = 0.F by FIELD_9:20; then
b^2 - a = 0.F; then
a = b^2 by RLVECT_1:21;
hence contradiction by O_RING_1:def 2;
end;
hence thesis;
end;
end;
registration
let F be non quadratic_complete Field;
cluster F-quadratic for FieldExtension of F;
existence
proof
set a = the non square Element of F, p = X^2-a;
consider E being FieldExtension of F such that
A: X^2-a is_with_roots_in E by FIELD_5:30;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
consider b being Element of E such that
B: b is_a_root_of X^2-a,E by A,FIELD_4:def 3;
C: Ext_eval(X^2-a,b) = 0.E by B,FIELD_4:def 2; then
reconsider b as F-algebraic Element of E by FIELD_6:43;
D: X^2-a = MinPoly(b,F) by C,FIELD_6:52;
deg(FAdj(F,{b}),F) = deg MinPoly(b,F) by FIELD_6:67
.= 2 by D,FIELD_9:def 4;
hence thesis by FIELD_9:def 26;
end;
end;
registration
let F be Field;
cluster F-quadratic -> F-simple for FieldExtension of F;
coherence
proof
let E be FieldExtension of F;
assume Q: E is F-quadratic;
now assume for a being Element of the carrier of E
holds a in the carrier of F;
then H: the carrier of E c= the carrier of F;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1;
hence contradiction by Q,H,XBOOLE_0:def 10,FIELD_7:7;
end; then
consider b being Element of the carrier of E such that
A: not b in the carrier of F;
reconsider E1 = E as F-extending FieldExtension of FAdj(F,{b})
by FIELD_4:7;
E1 is FAdj(F,{b})-finite by Q,FIELD_7:31; then
B: deg(E1,F) = deg(E1,FAdj(F,{b})) * deg(FAdj(F,{b}),F) by Q,FIELD_7:30;
C: deg(FAdj(F,{b}),F) <= deg(E1,F) by Q,FIELD_7:31;
I: deg(FAdj(F,{b}),F) >= 0 + 1 by Q,INT_1:7;
now assume deg(FAdj(F,{b}),F) = 1; then
J: the carrier of FAdj(F,{b}) = the carrier of F by FIELD_7:7;
b in {b} & {b} is Subset of FAdj(F,{b}) by TARSKI:def 1,FIELD_6:35;
hence contradiction by J,A;
end; then
deg(FAdj(F,{b}),F) > 1 by I,XXREAL_0:1; then
deg(FAdj(F,{b}),F) >= 1 + 1 by INT_1:7; then
2 = deg(E1,FAdj(F,{b})) * 2 by B,Q,C,XXREAL_0:1;
hence thesis by FIELD_7:8,FIELD_14:def 7;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster Roots(FAdj(F,{a}),MinPoly(a,F)) -> non empty finite;
coherence by FIELD_16:13;
end;
theorem U0:
for z being Element of F_Complex holds z is Element of F_Real iff z*' = z
proof
let z be Element of F_Complex;
reconsider c = z as Complex; reconsider b = Re c as Complex;
now assume z*' = z; then
I: Im(z) = -Im(z) by COMPLEX1:27;
Re b = Re c & Im b = 0 by COMPLEX1:def 1;
hence z is Element of F_Real by I,COMPLEX1:def 3;
end;
hence thesis;
end;
registration
cluster F_Complex -> non 2-characteristic;
coherence
proof
Char F_Complex = 0 by RING_3:def 6;
hence thesis;
end;
end;
definition
redefine func <i> -> non zero (F_Real)-algebraic Element of F_Complex; :: redefines <i> (XCMPLX_0, definition)
coherence
proof
reconsider c = <i> as Element of F_Complex by COMPLFLD:def 1;
A: c is non zero by COMPLFLD:def 1;
reconsider p = X^2+(1.F_Real) as Polynomial of F_Complex by FIELD_4:8;
H: 1.F_Real = 1.F_Complex by COMPLFLD:def 1,COMPLEX1:def 4;
0.F_Real = 0.F_Complex by COMPLFLD:def 1; then
B: p = <%1.F_Complex,0.F_Complex,1.F_Complex%> by H,FIELD_9:23;
C: 1.F_Complex = 1r & 0.F_Complex = 0c by COMPLFLD:def 1;
p is Element of the carrier of Polynom-Ring F_Complex by POLYNOM3:def 10; then
Ext_eval(X^2+(1.F_Real),c)
= eval(p,c) by FIELD_4:26
.= 1.F_Complex + 0.F_Complex * c + 1.F_Complex * c^2 by B,FIELD_9:20
.= 1.F_Complex + c * c by O_RING_1:def 1
.= 0.F_Complex by C,COMPLEX1:18;
hence thesis by A,FIELD_6:43;
end;
end;
registration
cluster X^2+(1.F_Real) -> irreducible;
coherence
proof
now assume X^2+(1.F_Real) is reducible; then
X^2-(-1.F_Real) is reducible;
hence contradiction;
end;
hence thesis;
end;
end;
theorem lemma:
Roots(F_Complex,X^2+(1.F_Real)) = { <i>, -<i> }
proof
the carrier of Polynom-Ring F_Real c=
the carrier of Polynom-Ring F_Complex by FIELD_4:10; then
reconsider p = X^2+(1.F_Real) as
Element of the carrier of Polynom-Ring F_Complex;
reconsider p1 = p as Polynomial of F_Complex;
set c = 1.(F_Complex), b = 0.(F_Complex), a = 1.(F_Complex);
F_Real is Subfield of F_Complex by FIELD_4:7; then
A: 1.F_Complex = 1.F_Real & 0.F_Complex = 0.F_Real by EC_PF_1:def 1;
B: p = <%c,b,a%> by A,FIELD_9:23; then
reconsider p1 as monic purely_quadratic Polynomial of F_Complex;
reconsider i = <i> as Element of F_Complex;
set w = 2 '*' i;
D: 1.F_Complex = 1r & 0.F_Complex = 0c by COMPLFLD:def 1;
E: i^2 = i * i by O_RING_1:def 1 .= - 1.F_Complex by D,COMPLEX1:18;
(2 '*' i)^2
= 2^2 '*' i^2 by FIELD_9:4
.= (2*2) '*' i^2 by SQUARE_1:def 1
.= 4 '*' ((-1) '*' 1.F_Complex) by E,RING_3:61
.= (4 * (-1)) '*' 1.F_Complex by RING_3:65
.= (-4) '*' 1.F_Complex
.= b^2 - 4 '*' a * c by RING_3:63; then
F: Roots p = { (-b+w) * (2'*'a)", (-b-w) * (2'*'a)" } by B,FIELD_9:27;
I: 2 '*' i <> 0.F_Complex & 2 '*' 1.F_Complex <> 0.F_Complex by FIELD_9:5;
G: (-b+w) * (2'*'a)"
= i * (1.F_Complex)" by I,FIELD_9:3
.= i;
(-b-w) * (2'*'a)"
= -((2 '*' i) * (2 '*' 1.F_Complex)")
.= -i * (1.F_Complex)" by I,FIELD_9:3
.= -i;
hence thesis by F,G,FIELD_7:13;
end;
theorem lemMinPol:
MinPoly(<i>,F_Real) = X^2+(1.F_Real)
proof
A: Roots(F_Complex,X^2+(1.F_Real)) =
{a where a is Element of F_Complex :
a is_a_root_of X^2+(1.F_Real),F_Complex} by FIELD_4:def 4;
<i> in Roots(F_Complex,X^2+(1.F_Real)) by lemma,TARSKI:def 2; then
consider a being Element of F_Complex such that
B: <i> = a & a is_a_root_of X^2+(1.F_Real),F_Complex by A;
Ext_eval(X^2+(1.F_Real),<i>) = 0.F_Complex by B,FIELD_4:def 2;
hence thesis by FIELD_6:52;
end;
theorem lem5:
F_Complex is SplittingField of X^2+(1.F_Real)
proof
reconsider p = X^2+(1.F_Real) as Polynomial of F_Complex by FIELD_4:8;
p is Element of the carrier of Polynom-Ring F_Complex
by POLYNOM3:def 10; then
deg p = deg(X^2+(1.F_Real)) by FIELD_4:20 .= 2 by FIELD_9:def 4; then
reconsider p as non constant Polynomial of F_Complex by RATFUNC1:def 2;
consider a being non zero Element of F_Complex,
q being Ppoly of (F_Complex) such that
B: p = a * q by FIELD_12:22,FIELD_4:def 5;
A: X^2+(1.F_Real) splits_in F_Complex by B,FIELD_4:def 5;
now let E be FieldExtension of F_Real;
assume B: X^2+(1.F_Real) splits_in E & E is Subfield of F_Complex;
then H: E is Subring of F_Complex by FIELD_5:12;
then F_Complex is E-extending by FIELD_4:def 1;
then <i> in {<i>,-<i>} & {<i>,-<i>} c= the carrier of E
by B,A,FIELD_8:27,TARSKI:def 2,lemma;
then reconsider i = <i> as Element of E;
C: the carrier of F_Complex c= the carrier of E
proof
now let o be object;
assume o in the carrier of F_Complex; then
reconsider z = o as Element of F_Complex;
C1: z = Re(z) + <i> * Im(z) by COMPLEX1:13;
F_Real is Subfield of E by FIELD_4:7; then
the carrier of F_Real c= the carrier of E by EC_PF_1:def 1; then
reconsider a = Re(z), b = Im(z) as Element of E;
F_Real is Subfield of F_Complex by FIELD_4:7; then
the carrier of F_Real c= the carrier of F_Complex
by EC_PF_1:def 1; then
reconsider Rz = Re(z), Iz = Im(z), ii = <i> as Element of F_Complex;
i * b = ii * Iz by H,FIELD_6:16; then
a + i * b = Rz + ii * Iz by H,FIELD_6:15;
hence o in the carrier of E by C1;
end;
hence thesis;
end;
D: the carrier of E c= the carrier of F_Complex &
the addF of E = (the addF of F_Complex) || the carrier of E &
the multF of E = (the multF of F_Complex) || the carrier of E &
1.E = 1.F_Complex & 0.E = 0.F_Complex by B,EC_PF_1:def 1; then
the carrier of F_Complex = the carrier of E by C,XBOOLE_0:def 10;
hence E == F_Complex by D;
end;
hence thesis by B,FIELD_4:def 5,FIELD_8:def 1;
end;
main1b:
deg(F_Complex,F_Real) = 2
proof
FAdj(F_Real,{sqrt(-1.F_Real)}) is SplittingField of X^2-(-1.F_Real)
by FIELD_9:58; then
FAdj(F_Real,{sqrt(-1.F_Real)}),F_Complex are_isomorphic_over F_Real
by lem5,FIELD_8:58;
hence deg(F_Complex,F_Real)
= deg(FAdj(F_Real,{sqrt(-1.F_Real)}),F_Real) by FIELD_8:45
.= 2 by FIELD_9:55;
end;
theorem lem6:
F_Complex = FAdj(F_Real,{<i>})
proof
F_Complex == FAdj(F_Real,{<i>,-<i>}) by lem5,FIELD_8:34,lemma;
hence thesis by FIELD_9:9;
end;
registration
cluster F_Complex -> (F_Real)-quadratic;
coherence by main1b;
end;
begin :: Groups of Automorphims
definition
let F be Field;
func Auts F -> non empty set equals
the set of all f where f is Automorphism of F;
coherence
proof
id F in the set of all f where f is Automorphism of F;
hence thesis;
end;
end;
registration
let F be Field;
cluster Auts F -> F-functional;
coherence
proof
now let o be object;
assume o in Auts F; then
consider f being Automorphism of F such that A: o = f;
thus o is Function of F,F by A;
end;
hence thesis;
end;
end;
registration
let F be Field;
cluster -> additive multiplicative unity-preserving
isomorphism for Element of Auts F;
coherence
proof
let o be Element of Auts F;
o in the set of all f where f is Automorphism of F; then
consider f being Automorphism of F such that A: o = f;
thus thesis by A;
end;
end;
definition
let F be Field;
func AutComp F -> BinOp of Auts F means :defMult:
for f,g being Automorphism of F holds it.(f,g) = f * g;
existence
proof
set M = Auts F;
defpred P[object,object,object] means
ex f,g being Element of M st $1 = f & $2 = g & $3 = f * g;
A: now let x,y be object;
assume x in M & y in M; then
reconsider f = x, g = y as Element of M;
thus ex z being object st z in M & P[x,y,z]
proof
take z = f * g;
thus z in M;
thus thesis;
end;
end;
consider h being Function of [:M,M:],M such that
B: for x,y being object st x in M & y in M holds P[x,y,h.(x,y)]
from BINOP_1:sch 1(A);
take h;
now let x,y be Automorphism of F;
x in M & y in M; then
P[x,y,h.(x,y)] by B;
hence h.(x,y) = x * y;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be BinOp of Auts F;
assume A: for f,g being Automorphism of F holds f1.(f,g) = f * g;
assume B: for f,g being Automorphism of F holds f2.(f,g) = f * g;
now let o be object;
assume o in [:Auts(F),Auts(F):]; then
consider a,b being object such that
C: a in Auts F & b in Auts F & o = [a,b] by ZFMISC_1:def 2;
reconsider a,b as Element of Auts F by C;
f1.(a,b) = a * b by A .= f2.(a,b) by B;
hence f1.o = f2.o by C;
end;
hence f1 = f2;
end;
end;
definition
let F be Field;
func Aut F -> strict non empty multMagma equals
multMagma (# Auts F, AutComp F #);
coherence;
end;
registration
let F be Field;
cluster Aut F -> Group-like associative;
coherence
proof
set G = Aut F;
ex e being Element of G
st for h being Element of G holds h * e = h & e * h = h &
ex g being Element of G st h * g = e & g * h = e
proof
id F in the set of all f where f is Automorphism of F; then
reconsider e = id F as Element of G;
take e;
now let h be Element of G;
h in the set of all f where f is Automorphism of F; then
consider h1 being Automorphism of F such that A: h1 = h;
thus h * e = h1 * (id F) by A,defMult .= h by A,FUNCT_2:17;
thus e * h = (id F) * h1 by A,defMult .= h by A,FUNCT_2:17;
thus ex g being Element of G st h * g = e & g * h = e
proof
h1" in the set of all f where f is Automorphism of F; then
reconsider g = h1" as Element of G;
take g;
B: rng h1 = the carrier of F by FUNCT_2:def 3;
thus h * g = h1 * h1" by A,defMult .= e by B,FUNCT_2:29;
thus g * h = h1" * h1 by A,defMult .= e by B,FUNCT_2:29;
end;
end;
hence thesis;
end;
hence G is Group-like;
now let a,b,c be Element of G;
a in the set of all f where f is Automorphism of F; then
consider f being Automorphism of F such that A: f = a;
b in the set of all f where f is Automorphism of F; then
consider g being Automorphism of F such that B: g = b;
c in the set of all f where f is Automorphism of F; then
consider h being Automorphism of F such that C: h = c;
D: a * b = f * g & b * c = g * h by A,B,C,defMult;
thus (a * b) * c
= (f * g) * h by D,C,defMult
.= f * (g * h) by RELAT_1:36
.= a * (b * c) by A,D,defMult;
end;
hence thesis;
end;
end;
theorem Th1:
for F being Field holds 1_(Aut F) = id F
proof
let F be Field;
id F in the set of all f where f is Automorphism of F; then
reconsider e = id F as Element of Aut F;
now let h be Element of Aut F;
h in the set of all f where f is Automorphism of F; then
consider h1 being Automorphism of F such that A: h1 = h;
thus h * e = h1 * (id F) by A,defMult .= h by A,FUNCT_2:17;
thus e * h = (id F) * h1 by A,defMult .= h by A,FUNCT_2:17;
end;
hence thesis by GROUP_1:4;
end;
registration
let F be Field;
cluster Aut F -> F-functional;
coherence;
cluster the carrier of Aut F -> F-functional;
coherence;
cluster -> F-functional for Subset of Aut(F);
coherence;
end;
registration
let F be Field;
let G be Subgroup of Aut(F);
cluster the carrier of G -> F-functional;
coherence
proof
the carrier of G c= the carrier of Aut(F) by GROUP_2:def 5;
hence thesis;
end;
end;
registration
let F be Field;
cluster -> additive multiplicative unity-preserving
isomorphism for Element of the carrier of Aut F;
coherence;
end;
registration
let F be Field;
let G be non empty Subset of Aut(F);
cluster -> additive multiplicative unity-preserving
isomorphism for Element of G;
coherence
proof
let o be Element of G;
o in G; then
consider f being Automorphism of F such that A: o = f;
thus thesis by A;
end;
end;
registration
let F be Field;
let G be non empty Subgroup of Aut(F);
cluster -> additive multiplicative unity-preserving
isomorphism for Element of the carrier of G;
coherence
proof
let o be Element of G;
the carrier of G c= the carrier of Aut(F) by GROUP_2:def 5; then
reconsider f = o as Element of the carrier of Aut(F);
f is Automorphism of F;
hence thesis;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
func Auts(E,F) -> non empty Subset of Auts(E) equals
the set of all f where f is F-fixing Automorphism of E;
coherence
proof
A: id E in the set of all f where f is F-fixing Automorphism of E;
now let o be object;
assume o in the set of all f where f is F-fixing Automorphism of E;
then consider f being F-fixing Automorphism of E such that B: f = o;
thus o in Auts(E) by B;
end; then
the set of all f where f is F-fixing Automorphism of E c= Auts(E);
hence thesis by A;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster Auts(E,F) -> E-functional;
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster -> F-fixing additive multiplicative unity-preserving
isomorphism for Element of Auts(E,F);
coherence
proof
let o be Element of Auts(E,F);
o in the set of all f where f is F-fixing Automorphism of E; then
consider f being F-fixing Automorphism of E such that B: f = o;
thus thesis by B;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
func AutComp(E,F) -> BinOp of Auts(E,F) equals
(AutComp E) || Auts(E,F);
coherence
proof
set g = AutComp E, f = (AutComp E) || Auts(E,F);
I: dom g = [: Auts(E), Auts(E):] by FUNCT_2:def 1;
A: dom f = dom g /\ [: Auts(E,F), Auts(E,F):] by RELAT_1:61
.= [: Auts(E,F), Auts(E,F):] by I,XBOOLE_1:28,ZFMISC_1:96;
now let x be object;
assume AS: x in [: Auts(E,F), Auts(E,F):]; then
consider x1,x2 being object such that
B: x1 in Auts(E,F) & x2 in Auts(E,F) & x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1,x2 as Element of Auts(E,F) by B;
Auts(E,F) c= Auts(E); then
reconsider y1 = x1, y2 = x2 as Element of Auts(E);
f.x = g.(y1,y2) by AS,B,FUNCT_1:49 .= x1 * x2 by defMult;
hence f.x in Auts(E,F);
end;
hence thesis by A,FUNCT_2:3;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
func Aut(E,F) -> strict multMagma equals
multMagma (# Auts(E,F), AutComp(E,F) #);
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster Aut(E,F) -> non empty;
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster Aut(E,F) -> Group-like associative;
coherence
proof
set G = Aut(E,F);
ex e being Element of G st for h being Element of G holds
h * e = h & e * h = h &
ex g being Element of G st h * g = e & g * h = e
proof
id E in the set of all f where f is F-fixing Automorphism of E; then
reconsider e = id E as Element of G;
take e;
now let h be Element of G;
h in the set of all f where f is F-fixing Automorphism of E; then
consider h1 being F-fixing Automorphism of E such that A: h1 = h;
h1 in Auts(E,F) & id E in Auts(E,F); then
B: [h1,e] in [:Auts(E,F),Auts(E,F):] &
[e,h1] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
thus h * e = (AutComp E).(h1,e) by A,B,FUNCT_1:49
.= h1 * (id E) by defMult
.= h by A,FUNCT_2:17;
thus e * h = (AutComp E).(e,h1) by A,B,FUNCT_1:49
.= (id E) * h1 by defMult
.= h by A,FUNCT_2:17;
thus ex g being Element of G st h * g = e & g * h = e
proof
h1" in the set of all f where f is F-fixing Automorphism of E; then
reconsider g = h1" as Element of G;
take g;
B: rng h1 = the carrier of E by FUNCT_2:def 3;
C: [h,g] in [:Auts(E,F),Auts(E,F):] &
[g,h] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
thus h * g = (AutComp E).(h,g) by C,FUNCT_1:49
.= h1 * h1" by A,defMult .= e by B,FUNCT_2:29;
thus g * h = (AutComp E).(g,h) by C,FUNCT_1:49
.= h1" * h1 by A,defMult .= e by B,FUNCT_2:29;
end;
end;
hence thesis;
end;
hence G is Group-like;
now let a,b,c be Element of G;
a in the set of all f where f is F-fixing Automorphism of E; then
consider f being F-fixing Automorphism of E such that A: f = a;
b in the set of all f where f is F-fixing Automorphism of E; then
consider g being F-fixing Automorphism of E such that B: g = b;
c in the set of all f where f is F-fixing Automorphism of E; then
consider h being F-fixing Automorphism of E such that C: h = c;
H: f in Auts(E,F) & g in Auts(E,F) & h in Auts(E,F); then
I: [f,g] in [:Auts(E,F),Auts(E,F):] &
[g,h] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
D: a * b = (AutComp E).(f,g) by A,B,I,FUNCT_1:49
.= f * g by defMult;
E: b * c = (AutComp E).(g,h) by B,C,I,FUNCT_1:49
.= g * h by defMult; then
J: [f*g,h] in [:Auts(E,F),Auts(E,F):] &
[f,g*h] in [:Auts(E,F),Auts(E,F):] by H,D,ZFMISC_1:def 2;
thus (a * b) * c
= (AutComp E).(f*g,h) by C,D,J,FUNCT_1:49
.= (f * g) * h by defMult
.= f * (g * h) by RELAT_1:36
.= (AutComp E).(f,g*h) by defMult
.= a * (b * c) by A,E,J,FUNCT_1:49;
end;
hence G is associative;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
redefine func Aut(E,F) -> strict Subgroup of Aut(E); :: redefines Aut (GALOIS_1, definition)
coherence by GROUP_2:def 5;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster Aut(E,F) -> E-functional;
coherence;
cluster the carrier of Aut(E,F) -> E-functional;
coherence;
cluster -> E-functional for Subset of Aut(E,F);
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster -> F-fixing additive multiplicative unity-preserving
isomorphism for Element of the carrier of Aut(E,F);
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
let G be non empty Subset of Aut(E,F);
cluster -> F-fixing additive multiplicative unity-preserving
isomorphism for Element of G;
coherence
proof
let o be Element of G;
o in G; then
consider f being F-fixing Automorphism of E such that B: f = o;
thus thesis by B;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let G be Subgroup of Aut(E,F);
cluster -> F-fixing additive multiplicative unity-preserving
isomorphism for Element of the carrier of G;
coherence
proof
let o be Element of the carrier of G;
the carrier of G c= the carrier of Aut(E,F) by GROUP_2:def 5;
hence thesis;
end;
end;
definition
let E be Field;
let F be Subfield of E;
func Aut(E,F) -> strict Subgroup of Aut(E) equals
Aut(FieldExt(E,F),F);
coherence;
end;
definition
let F be Field;
let E be FieldExtension of F;
let K be IntermediateField of E,F;
func Aut(E,K) -> strict Subgroup of Aut(E) equals
Aut(FieldExt(E,K),K);
coherence;
end;
theorem
for F being Field
for E being FieldExtension of F
for K1 being IntermediateField of E,F
for K2 being Subfield of E st K2 = K1 holds Aut(E,K2) = Aut(E,K1);
begin :: Conjugates
definition
let F be Field;
let G be Subgroup of Aut(F);
let a be Element of F;
func Conjugates(a,G) -> non empty Subset of F equals
the set of all f.a where f is Element of the carrier of G;
coherence
proof
set M = the set of all f.a where f is Element of the carrier of G;
id F = 1_Aut(F) by Th1 .= 1_G by GROUP_2:44; then
A: (id F).a in M;
now let o be object;
assume o in M; then
consider f being Element of the carrier of G such that
B: o = f.a;
the carrier of G c= the carrier of Aut(F) by GROUP_2:def 5; then
reconsider f1 = f as Element of the carrier of Aut(F);
thus o in the carrier of F by B;
end;
hence thesis by A,TARSKI:def 3;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let a be Element of E;
func Conjugates a -> non empty Subset of E equals
Conjugates(a,Aut(E,F));
coherence;
end;
notation
let F be Field;
let G be Subgroup of Aut(F);
let a be Element of F;
synonym Conj(a,G) for Conjugates(a,G);
end;
notation
let F be Field;
let E be FieldExtension of F;
let a be Element of E;
synonym Conj a for Conjugates a;
end;
theorem ID2c:
for F being Field
for E being FieldExtension of F
for a being F-algebraic Element of E st E == FAdj(F,{a})
for b being Element of E st b in Roots(FAdj(F,{a}),MinPoly(a,F))
holds FAdj(F,{b}) = FAdj(F,{a})
proof
let F be Field, E be FieldExtension of F, a be F-algebraic Element of E;
assume AS1: E == FAdj(F,{a});
let b be Element of E;
assume AS2: b in Roots(FAdj(F,{a}),MinPoly(a,F));
set p = MinPoly(a,F), n = deg MinPoly(a,F);
U: E is FAdj(F,{a})-extending by FIELD_4:7;
Roots(FAdj(F,{a}),p) =
{c where c is Element of FAdj(F,{a}) : c is_a_root_of p,FAdj(F,{a})}
by FIELD_4:def 4; then
consider c being Element of FAdj(F,{a}) such that
B: c = b & c is_a_root_of p,FAdj(F,{a}) by AS2;
A: Ext_eval(p,b) = Ext_eval(p,c) by U,B,FIELD_6:11
.= 0.FAdj(F,{a}) by B,FIELD_4:def 2
.= 0.E by EC_PF_1:def 1; then
reconsider b1 = b as F-algebraic Element of E by FIELD_6:43;
reconsider E as FAdj(F,{b1})-extending FieldExtension of F by FIELD_4:7;
K: VecSp(FAdj(F,{a}),F) is finite-dimensional &
VecSp(FAdj(F,{a}),F) = VecSp(E,F) by AS1,FIELD_4:def 8,FIELD_7:4;
H: deg(E,F) = deg(FAdj(F,{a}),F) by AS1,FIELD_7:5;
E is F-finite by K,FIELD_4:def 8; then
E is FAdj(F,{b1})-finite by FIELD_7:31; then
G: deg(E,F) = deg(E,FAdj(F,{b1})) * deg(FAdj(F,{b1}),F) by FIELD_7:30;
MinPoly(b1,F) = MinPoly(a,F) by A,FIELD_6:52; then
n = deg(E,F) & n = deg(FAdj(F,{b1}),F) by H,FIELD_6:67; then
FAdj(F,{b1}) == E by G,XCMPLX_1:7,FIELD_7:8;
hence thesis by AS1;
end;
theorem ID2b:
for F being Field
for E being FieldExtension of F
for a being F-algebraic Element of E
for b being Element of E st b in Roots(FAdj(F,{a}),MinPoly(a,F))
ex f being F-fixing Automorphism of FAdj(F,{a}) st f.a = b
proof
let F be Field, E be FieldExtension of F, a be F-algebraic Element of E;
let b be Element of E;
assume A: b in Roots(FAdj(F,{a}),MinPoly(a,F));
set p = MinPoly(a,F);
id F is isomorphism; then
reconsider F1 = F as F-isomorphic F-homomorphic Field
by RING_2:def 4,RING_3:def 4;
reconsider h = id F as Isomorphism of F,F1;
now let i be Element of NAT;
thus ((PolyHom h).p).i = h.(p.i) by FIELD_1:def 2 .= p.i;
end; then
Q: (PolyHom h).p = p;
reconsider E1 = FAdj(F,{a}) as FieldExtension of F;
U: E is E1-extending by FIELD_4:7;
reconsider E2 = E as FieldExtension of F1;
{a} is Subset of the carrier of FAdj(F,{a}) by FIELD_6:35; then
a in {a} & {a} c= the carrier of FAdj(F,{a}) by TARSKI:def 1; then
reconsider a1 = a as F-algebraic Element of E1;
C: FAdj(F,{a1}) = FAdj(F,{a}) &
MinPoly(a,F) = MinPoly(a1,F) by U,FIELD_10:10,FIELD_10:9;
N: Roots(FAdj(F,{a}),p) =
{b where b is Element of FAdj(F,{a}) : b is_a_root_of p,FAdj(F,{a})}
by FIELD_4:def 4; then
consider c being Element of FAdj(F,{a}) such that
O: c = b & c is_a_root_of p,FAdj(F,{a}) by A;
Ext_eval(p,b) = Ext_eval(p,c) by U,O,FIELD_6:11
.= 0.E1 by O,FIELD_4:def 2
.= 0.E by EC_PF_1:def 1; then
reconsider b as F-algebraic Element of E by FIELD_6:43;
reconsider b1 = b as F1-algebraic Element of E2;
reconsider b2 = b1 as F-algebraic Element of E1 by A;
(id FAdj(F,{a})).a in Roots(FAdj(F,{a}),p) by FIELD_16:13; then
consider c being Element of FAdj(F,{a}) such that
O: c = a1 & c is_a_root_of p,FAdj(F,{a}) by N;
B: Ext_eval(p,a1) = 0.E1 by O,FIELD_4:def 2;
consider c being Element of FAdj(F,{a}) such that
O: c = b & c is_a_root_of p,FAdj(F,{a}) by A,N;
Ext_eval(p,b1) = Ext_eval(p,c) by U,O,FIELD_6:11
.= 0.E1 by O,FIELD_4:def 2; then
E: Ext_eval((PolyHom h).p,b1) = 0.E2 by Q,EC_PF_1:def 1; then
F: Psi(a1,b1,h,p) is h-extending isomorphism by B,FIELD_8:55;
b2 in Roots(FAdj(F,{a}),MinPoly(a,F)) by O,N; then
FAdj(F,{a1}) = FAdj(F,{b2}) by C,ID2c .= FAdj(F,{b}) by U,FIELD_10:9; then
reconsider f = Psi(a1,b1,h,p) as Automorphism of FAdj(F,{a})
by E,C,B,FIELD_8:55;
f is (id F)-extending by F; then
reconsider f as F-fixing Automorphism of FAdj(F,{a});
f.a1 = b1 by B,E,FIELD_13:26;
hence thesis;
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 by GROUP_6:def 6,VECTSP_1:def 20;
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;
lemBC:
for F being Field
for E1,E2 being FieldExtension of F
for p being Element of the carrier of Polynom-Ring F
st E1 == E2 holds Roots(E1,p) = Roots(E2,p)
proof
let F be Field, E1,E2 be FieldExtension of F,
p be Element of the carrier of Polynom-Ring F;
assume AS: E1 == E2;
H: Roots(E1,p) = {a where a is Element of E1 : a is_a_root_of p,E1} &
Roots(E2,p) = {a where a is Element of E2 : a is_a_root_of p,E2}
by FIELD_4:def 4;
A: now let o be object;
assume o in Roots(E1,p); then
consider a1 being Element of E1 such that
B: o = a1 & a1 is_a_root_of p,E1 by H;
reconsider a2 = a1 as Element of E2 by AS;
0.E2 = 0.E1 by AS
.= Ext_eval(p,a1) by B,FIELD_4:def 2
.= Ext_eval(p,a2) by AS,FIELD_12:42; then
a2 is_a_root_of p,E2 by FIELD_4:def 2;
hence o in Roots(E2,p) by B,H;
end;
now let o be object;
assume o in Roots(E2,p); then
consider a2 being Element of E2 such that
B: o = a2 & a2 is_a_root_of p,E2 by H;
reconsider a1 = a2 as Element of E1 by AS;
0.E1 = 0.E2 by AS
.= Ext_eval(p,a2) by B,FIELD_4:def 2
.= Ext_eval(p,a1) by AS,FIELD_12:42; then
a1 is_a_root_of p,E1 by FIELD_4:def 2;
hence o in Roots(E1,p) by B,H;
end;
hence thesis by A,TARSKI:2;
end;
theorem lemBA:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E,F)
for a being F-algebraic Element of E holds Conj(a,G) c= Roots(E,MinPoly(a,F))
proof
let F be Field, E be FieldExtension of F,
G be Subgroup of Aut(E,F), a be F-algebraic Element of E;
set p = MinPoly(a,F);
now let o be object;
assume o in Conj(a,G); then
consider f being Element of the carrier of G such that
B: o = f.a;
the carrier of G c= the carrier of Aut(E,F) by GROUP_2:def 5; then
reconsider f as Element of the carrier of Aut(E,F);
C: Roots(E,p) = {b where b is Element of E : b is_a_root_of p,E}
by FIELD_4:def 4;
0.E = Ext_eval(p,a) by FIELD_6:52; then
a is_a_root_of p,E by FIELD_4:def 2; then
a in Roots(E,p) by C;
hence o in Roots(E,MinPoly(a,F)) by B,FIELD_8:38;
end;
hence thesis;
end;
registration
let F be Field;
let E be FieldExtension of F;
let G be Subgroup of Aut(E,F);
let a be F-algebraic Element of E;
cluster Conj(a,G) -> finite;
coherence
proof
Conj(a,G) c= Roots(E,MinPoly(a,F)) by lemBA;
hence thesis;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster Conj a -> finite;
coherence
proof
Aut(E,F) is Subgroup of Aut(E,F) by GROUP_2:54;
hence thesis;
end;
end;
theorem
for F being Field
for E being FieldExtension of F
for a being F-algebraic Element of E
st E == FAdj(F,{a}) holds Conj a = Roots(E,MinPoly(a,F))
proof
let F be Field, E be FieldExtension of F, a be F-algebraic Element of E;
assume AS: E == FAdj(F,{a});
A: now let o be object;
assume B: o in Conj a;
Aut(E,F) is Subgroup of Aut(E,F) by GROUP_2:54; then
Conj(a,Aut(E,F)) c= Roots(E,MinPoly(a,F)) by lemBA;
hence o in Roots(E,MinPoly(a,F)) by B;
end;
now let o be object;
assume B: o in Roots(E,MinPoly(a,F)); then
reconsider b = o as Element of E;
b in Roots(FAdj(F,{a}),MinPoly(a,F)) by B,AS,lemBC; then
consider f being F-fixing Automorphism of FAdj(F,{a}) such that
C: f.a = b by ID2b;
f is F-fixing Automorphism of E by AS,lemBB; then
f in Auts(E,F);
hence o in Conj a by C;
end;
hence thesis by A,TARSKI:2;
end;
theorem ThBij:
for F being Field
for E being FieldExtension of F
for a being F-algebraic Element of E
ex f being Function of
Auts(FAdj(F,{a}),F),Roots(FAdj(F,{a}),MinPoly(a,F))
st f is bijective
proof
let F be Field, E be FieldExtension of F, a be F-algebraic Element of E;
set G = Auts(FAdj(F,{a}),F), R = Roots(FAdj(F,{a}),MinPoly(a,F)),
p = MinPoly(a,F);
defpred P[object,object] means
ex f being Element of G st $1 = f & $2 = f.a;
A: now let x be object;
assume x in G; then
reconsider f = x as Element of G;
f.a in R by FIELD_16:13;
hence ex y being object st y in R & P[x,y];
end;
consider h being Function of G,R such that
B: for x being object st x in G holds P[x,h.x] from FUNCT_2:sch 1(A);
now let x1,x2 be object;
assume B1: x1 in G & x2 in G & h.x1 = h.x2; then
reconsider f1 = x1, f2 = x2 as Element of G;
P[f1,h.f1] & P[f2,h.f2] by B;
hence x1 = x2 by B1,FIELD_16:16;
end; then
C: h is one-to-one by FUNCT_2:19;
D: rng h c= R by RELAT_1:def 19;
now let o be object;
assume C1: o in R;
Roots(FAdj(F,{a}),p) =
{b where b is Element of FAdj(F,{a}) : b is_a_root_of p,FAdj(F,{a})}
by FIELD_4:def 4; then
consider b being Element of FAdj(F,{a}) such that
C2: o = b & b is_a_root_of p,FAdj(F,{a}) by C1;
the carrier of FAdj(F,{a}) c= the carrier of E by EC_PF_1:def 1; then
reconsider b1 = b as Element of E;
consider f being F-fixing Automorphism of FAdj(F,{a}) such that
C3: f.a = b1 by C1,C2,ID2b;
C4: f in G & dom h = G by FUNCT_2:def 1; then
P[f,h.f] by B;
hence o in rng h by C2,C3,C4,FUNCT_1:3;
end; then
h is onto by D,TARSKI:2;
hence thesis by C;
end;
registration
let F be Field;
let E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster Aut(FAdj(F,{a}),F) -> finite;
coherence
proof
consider f being Function of
Auts(FAdj(F,{a}),F),Roots(FAdj(F,{a}),MinPoly(a,F)) such that
A: f is bijective by ThBij;
B: dom f = Auts(FAdj(F,{a}),F) by FUNCT_2:def 1;
C: rng f = Roots(FAdj(F,{a}),MinPoly(a,F)) by A,FUNCT_2:def 3;
card dom f = card rng f by A,CARD_1:70;
hence thesis by B,C;
end;
end;
lemZ0:
for F being Field, E being FieldExtension of F, S being Subset of E
holds (id E).:S = S
proof
let F be Field, E be FieldExtension of F, S be Subset of E;
A: now let o be object;
assume B: o in S; then
reconsider a = o as Element of E;
(id E).a = a & dom(id E) = the carrier of E;
hence o in (id E).:S by B,FUNCT_1:def 6;
end;
now let o be object;
assume o in (id E).:S; then
consider x being object such that
C: x in dom(id E) & x in S & o = (id E).x by FUNCT_1:def 6;
reconsider a = x as Element of E by C;
(id E).a = a;
hence o in S by C;
end;
hence thesis by A,TARSKI:2;
end;
lemZ1:
for F being Field, E being FieldExtension of F, S being Subset of E
holds id E in {f where f is F-fixing Automorphism of E : f.:S = S}
proof
let F be Field, E be FieldExtension of F, S be Subset of E;
(id E).:S = S by lemZ0;
hence thesis;
end;
definition
let F be Field;
let E be FieldExtension of F;
let S be Subset of E;
func Auts S -> non empty Subset of Auts(E,F) equals
{ f where f is F-fixing Automorphism of E : f.:S = S };
coherence
proof
now let o be object;
assume o in {f where f is F-fixing Automorphism of E : f.:S = S};
then consider f being F-fixing Automorphism of E such that
B: f = o & f.:S = S;
thus o in Auts(E,F) by B;
end; then
{f where f is F-fixing Automorphism of E : f.:S = S} c= Auts(E,F);
hence thesis by lemZ1;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let a be Element of E;
func Auts a -> non empty Subset of Auts(E,F) equals
Auts {a};
coherence;
end;
theorem lemZ2:
for F being Field
for E being FieldExtension of F
for a being Element of E
holds Auts a = { f where f is F-fixing Automorphism of E : f.a = a }
proof
let F be Field, E be FieldExtension of F, a be Element of E;
A: now let o be object;
assume o in Auts a; then
consider f being F-fixing Automorphism of E such that
A1: o = f & f.:{a} = {a};
A2: dom f = the carrier of E by FUNCT_2:def 1;
A3: f.:{a} = Im(f,a) by RELAT_1:def 16 .= {f.a} by A2,FUNCT_1:59;
a in {a} by TARSKI:def 1;
then f.a = a by A1,A3,TARSKI:def 1;
hence o in {f where f is F-fixing Automorphism of E : f.a = a} by A1;
end;
now let o be object;
assume o in {f where f is F-fixing Automorphism of E : f.a = a}; then
consider f being F-fixing Automorphism of E such that
A1: o = f & f.a = a;
A2: dom f = the carrier of E by FUNCT_2:def 1;
f.:{a} = Im(f,a) by RELAT_1:def 16 .= {a} by A1,A2,FUNCT_1:59;
hence o in Auts a by A1;
end;
hence thesis by A,TARSKI:2;
end;
definition
let F be Field;
let E be FieldExtension of F;
let S be Subset of E;
func AutComp S -> BinOp of Auts S equals
AutComp(E,F) || (Auts S);
coherence
proof
set g = AutComp(E,F), f = AutComp(E,F) || Auts S;
I: dom g = [: Auts(E,F), Auts(E,F):] by FUNCT_2:def 1;
A: dom f = dom g /\ [: Auts S, Auts S:] by RELAT_1:61
.= [: Auts S, Auts S:] by I,XBOOLE_1:28,ZFMISC_1:96;
now let x be object;
assume AS: x in [:Auts S, Auts S:]; then
consider x1,x2 being object such that
B: x1 in Auts S & x2 in Auts S & x = [x1,x2] by ZFMISC_1:def 2;
consider f1 being F-fixing Automorphism of E such that
C: x1 = f1 & f1.:S = S by B;
consider f2 being F-fixing Automorphism of E such that
D: x2 = f2 & f2.:S = S by B;
H: [:Auts S, Auts S:] c= [:Auts(E,F), Auts(E,F):] by ZFMISC_1:96;
E: f.x = g.(f1,f2) by AS,B,C,D,FUNCT_1:49
.= (AutComp E).(f1,f2) by AS,B,C,D,H,FUNCT_1:49
.= f1 * f2 by defMult;
(f1 * f2).:S = S by C,D,RELAT_1:126;
hence f.x in Auts S by E;
end;
hence thesis by A,FUNCT_2:3;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let S be Subset of E;
func Aut S -> strict non empty multMagma equals
multMagma (# Auts S, AutComp S #);
coherence;
end;
lemZ3:
for F being Field
for E being FieldExtension of F
for S being non empty Subset of E
for h being Automorphism of E st h.:S = S
holds dom(h|S) = S & rng(h|S) = S & dom(h"|S) = S & rng(h"|S) = S
proof
let F be Field, E be FieldExtension of F, S be non empty Subset of E;
let h be Automorphism of E;
assume AS: h.:S = S;
U: now let h be Automorphism of E;
assume A: h.:S = S;
dom h = the carrier of E by FUNCT_2:def 1;
hence dom(h|S) = S by RELAT_1:62;
B: now let o be object;
assume o in S; then
consider x being object such that
A1: x in dom h & x in S & o = h.x by A,FUNCT_1:def 6;
thus o in rng(h|S) by A1,FUNCT_1:50;
end;
now let o be object;
assume o in rng(h|S); then
consider x being object such that
A2: x in dom(h|S) & o = (h|S).x by FUNCT_1:def 3;
A3: o = h.x by A2,FUNCT_1:47;
x in dom h & x in S by A2,RELAT_1:57;
hence o in S by A,A3,FUNCT_1:def 6;
end;
hence rng(h|S) = S by B,TARSKI:2;
end;
hence dom(h|S) = S & rng(h|S) = S by AS;
dom(h") = the carrier of E by FUNCT_2:def 1;
hence dom(h"|S) = S by RELAT_1:62;
B: rng h = the carrier of E & h is one-to-one by FUNCT_2:def 3;
h".:S = (h"*h).:S by AS,RELAT_1:126
.= (id E).:S by B,FUNCT_2:29
.= S by lemZ0;
hence thesis by U;
end;
registration
let F be Field;
let E be FieldExtension of F;
let S be non empty Subset of E;
cluster Aut S -> Group-like associative;
coherence
proof
set G = Aut S;
ex e being Element of G
st for h being Element of G holds h * e = h & e * h = h &
ex g being Element of G st h * g = e & g * h = e
proof
reconsider e = id E as Element of the carrier of G by lemZ1;
take e;
now let h be Element of the carrier of G;
h in {f where f is F-fixing Automorphism of E : f.:S = S}; then
consider h1 being F-fixing Automorphism of E such that
A: h1 = h & h1.:S = S;
J: Auts S c= Auts(E,F);
H: [:Auts S, Auts S:] c= [:Auts(E,F), Auts(E,F):] by ZFMISC_1:96;
K: Auts(E,F) c= Auts(E);
B: [h,e] in [:Auts S, Auts S:] &
[e,h] in [:Auts S, Auts S:] by ZFMISC_1:def 2;
reconsider h3 = h1 as Automorphism of E;
id E in Auts(E); then
reconsider h2 = h, e2 = id E as Element of the carrier of Aut(E) by J,K;
thus h * e = AutComp(E,F).(h,e) by B,FUNCT_1:49
.= (AutComp E).(h2,e2) by B,H,FUNCT_1:49
.= h3 * (id E) by A,defMult
.= h by A,FUNCT_2:17;
thus e * h = AutComp(E,F).(e,h) by B,FUNCT_1:49
.= (AutComp E).(e2,h2) by B,H,FUNCT_1:49
.= (id E) * h3 by A,defMult
.= h by A,FUNCT_2:17;
thus ex g being Element of G st h * g = e & g * h = e
proof
F: dom(h1|S) = S & rng(h1|S) = S by A,lemZ3;
E: now let o be object;
assume o in S; then
reconsider y = o as Element of S;
E2: dom(h1") = the carrier of E by FUNCT_2:def 1;
E4: dom(h1) = the carrier of E by FUNCT_2:def 1; then
E3: h1.y in S by F,FUNCT_1:50;
h1".(h1.y) = y by E4,FUNCT_1:34;
hence o in (h1").:S by E2,E3,FUNCT_1:def 6;
end;
now let o be object;
assume o in (h1").:S; then
consider x being object such that
E1: x in dom(h1") & x in S & o = (h1").x by FUNCT_1:def 6;
E2: x in dom(h1"|S) by E1,RELAT_1:57; then
(h1"|S).x = h1".x by FUNCT_1:47; then
o in rng(h1"|S) by E1,E2,FUNCT_1:def 3;
hence o in S by A,lemZ3;
end; then
(h1").:S = S by E,TARSKI:2; then
h1" in {f where f is F-fixing Automorphism of E : f.:S = S}; then
reconsider g = h1" as Element of the carrier of G;
take g;
R: rng h1 = the carrier of E by FUNCT_2:def 3;
S: [h,g] in [:Auts S, Auts S:] &
[g,h] in [:Auts S, Auts S:] by ZFMISC_1:def 2;
reconsider g2 = g as Element of the carrier of Aut(E) by J,K;
thus h * g = AutComp(E,F).(h,g) by S,FUNCT_1:49
.= (AutComp E).(h2,g2) by S,H,FUNCT_1:49
.= h1 * h1" by A,defMult
.= e by R,FUNCT_2:29;
thus g * h = AutComp(E,F).(g,h) by S,FUNCT_1:49
.= (AutComp E).(g2,h2) by S,H,FUNCT_1:49
.= h1" * h1 by A,defMult
.= e by R,FUNCT_2:29;
end;
end;
hence thesis;
end;
hence G is Group-like;
now let x,y,z be Element of G;
x in {f where f is F-fixing Automorphism of E : f.:S = S}; then
consider f being F-fixing Automorphism of E such that
E1: x = f & f.:S = S;
y in {f where f is F-fixing Automorphism of E : f.:S = S}; then
consider g being F-fixing Automorphism of E such that
E2: y = g & g.:S = S;
z in {f where f is F-fixing Automorphism of E : f.:S = S}; then
consider h being F-fixing Automorphism of E such that
E3: z = h & h.:S = S;
H: [:Auts S, Auts S:] c= [:Auts(E,F), Auts(E,F):] by ZFMISC_1:96;
B: [f,g] in [:Auts S, Auts S:] &
[g,h] in [:Auts S, Auts S:] by E1,E2,E3,ZFMISC_1:def 2;
E4: x * y = AutComp(E,F).(x,y) by E1,E2,B,FUNCT_1:49
.= (AutComp E).(f,g) by E1,E2,B,H,FUNCT_1:49
.= f * g by defMult;
E5: y * z = AutComp(E,F).(y,z) by E2,E3,B,FUNCT_1:49
.= (AutComp E).(g,h) by E2,E3,B,H,FUNCT_1:49
.= g * h by defMult; then
D: [f*g,h] in [:Auts S, Auts S:] &
[f,g*h] in [:Auts S, Auts S:] by E1,E3,E4,ZFMISC_1:def 2;
thus (x * y) * z
= AutComp(E,F).(x*y,z) by E3,E4,D,FUNCT_1:49
.= (AutComp E).(f*g,h) by E3,E4,D,H,FUNCT_1:49
.= (f * g) * h by defMult
.= f * (g * h) by RELAT_1:36
.= (AutComp E).(f,g*h) by defMult
.= ((AutComp E) || Auts(E,F)).(x,y*z) by E1,E5,D,H,FUNCT_1:49
.= x * (y * z) by E1,E5,D,FUNCT_1:49;
end;
hence thesis;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let S be non empty Subset of E;
redefine func Aut S -> strict Subgroup of Aut(E,F); :: redefines Aut (GALOIS_1, definition)
coherence by GROUP_2:def 5;
end;
definition
let F be Field;
let E be FieldExtension of F;
let a be Element of E;
func Aut a -> strict Subgroup of Aut(E,F) equals
Aut {a};
coherence;
end;
theorem
for F being Field
for E being FieldExtension of F
for a being Element of E holds card(Conj a) = Index(Aut a)
proof
let F be Field, E be FieldExtension of F, a be Element of E;
set H = Aut a, G = Aut(E,F);
H: Auts a = {f where f is F-fixing Automorphism of E : f.a = a} &
the carrier of H = Auts a by lemZ2;
defpred P[object,object] means
for f being Element of the carrier of G st $1 = f.a holds $2 = f * H;
A: now let x be object;
assume x in Conj a; then
consider f being Element of the carrier of G such that
B: x = f.a;
A1: f is one-to-one & rng f = the carrier of E by FUNCT_2:def 3;
reconsider f1 = f as F-fixing Automorphism of E;
thus ex y being object st y in Left_Cosets H & P[x,y]
proof
take y = f * H;
thus y in Left_Cosets H by GROUP_2:def 15;
now let g be Element of the carrier of G;
reconsider g1 = g as F-fixing Automorphism of E;
f" is Element of the carrier of G; then
reconsider ff = f" as F-fixing Automorphism of E;
I: [f",g] in [:Auts(E,F),Auts(E,F):] &
[f",f] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
id E = 1_(Aut E) by Th1
.= 1_G by GROUP_2:44
.= f" * f by GROUP_1:def 5
.= (AutComp E).(f",f) by I,FUNCT_1:49
.= ff * f1 by defMult; then
f" = f1" by A1,FUNCT_2:30; then
A3: f1" * g1 = (AutComp E).(f",g) by defMult
.= f" * g by I,FUNCT_1:49;
assume x = g.a; then
(f1" * g1).a = (f1").(f1.a) by B,FUNCT_2:15 .= a by FUNCT_2:26; then
f" * g in H by H,A3;
hence y = g * H by GROUP_2:114;
end;
hence thesis;
end;
end;
consider h being Function of Conj a,Left_Cosets H such that
B: for x being object st x in Conj a holds P[x,h.x]
from FUNCT_2:sch 1(A);
C: dom h = Conj a by FUNCT_2:def 1;
now let x1,x2 be object;
assume C0: x1 in Conj a & x2 in Conj a & h.x1 = h.x2; then
consider f1 being Element of the carrier of G such that
C1: x1 = f1.a;
consider f2 being Element of the carrier of G such that
C2: x2 = f2.a by C0;
f1 * H = h.(f2.a) by C0,C1,C2,B .= f2 * H by C0,C2,B; then
consider g being Element of G such that
C3: f2 = f1 * g & g in H by GROUP_2:103,108;
g in Auts a by C3; then
g in {f where f is F-fixing Automorphism of E : f.a = a}
by lemZ2; then
consider g2 being F-fixing Automorphism of E such that
C5: g2 = g & g2.a = a;
f1 in Auts(E,F) & g2 in Auts(E,F); then
[f1,g2] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2; then
f2 = (AutComp E).(f1,g2) by C3,C5,FUNCT_1:49
.= f1 * g2 by defMult;
hence x1 = x2 by C1,C2,C5,FUNCT_2:15;
end; then
h is one-to-one by FUNCT_2:19; then
D: card(dom h) = card(rng h) by CARD_1:70;
rng h = Left_Cosets H
proof
D1: rng h c= Left_Cosets H by RELAT_1:def 19;
now let o be object;
assume o in Left_Cosets H; then
consider g being Element of the carrier of G such that
D2: o = g * H by GROUP_2:def 15;
D3: g.a in Conj a;
consider g1 being Element of the carrier of G such that
D4: g.a = g1.a;
h.(g1.a) = g * H by B,D3,D4;
hence o in rng h by C,D4,D3,D2,FUNCT_1:def 3;
end; then
Left_Cosets H c= rng h;
hence thesis by D1,XBOOLE_0:def 10;
end;
hence thesis by C,D,GROUP_2:def 17;
end;
begin :: Fixed Fields
definition
let F be Field;
let G be Subgroup of Aut(F);
func Fixed_Elements(F,G) -> non empty Subset of F equals
{ a where a is Element of F :
for f being Function of F,F st f in G holds f.a = a };
coherence
proof
set M = { a where a is Element of F :
for f being Function of F,F st f in G holds f.a = a };
H: the carrier of G c= the carrier of Aut(F) by GROUP_2:def 5;
now let f be Function of F,F;
assume f in G; then
reconsider h = f as Element of the carrier of Aut(F) by H;
h.(1_F) = 1_F by GROUP_1:def 13;
hence f.(1.F) = 1.F;
end; then
A: 1.F in M;
now let o be object;
assume o in M; then
consider a being Element of F such that
A: o = a & for f being Function of F,F st f in G holds f.a = a;
thus o in the carrier of F by A;
end;
then M c= the carrier of F;
hence thesis by A;
end;
end;
notation
let F be Field;
let G be Subgroup of Aut(F);
synonym Fixed_El(F,G) for Fixed_Elements(F,G);
end;
lemH:
for F being Field
for f being Automorphism of F, a being Element of F
st a <> 0.F holds f.(a") = (f.a)"
proof
let F be Field,f be Automorphism of F, x be Element of F;
assume AS: x <> 0.F;
A: f.(x") * f.x = f.(x"*x) by GROUP_6:def 6
.= f.(1_F) by AS,VECTSP_1:def 10
.= 1.F by GROUP_1:def 13;
now assume f.x = 0.F;
then f.x = f.(0.F) by RING_2:6;
hence x = 0.F by FUNCT_2:19;
end;
hence thesis by AS,A,VECTSP_1:def 10;
end;
registration
let F be Field;
let G be Subgroup of Aut(F);
cluster Fixed_El(F,G) -> inducing_subfield;
coherence
proof
set M = Fixed_El(F,G);
H: the carrier of G c= the carrier of Aut(F) by GROUP_2:def 5;
A: now let f be Function of F,F;
assume f in G; then
reconsider h = f as Element of the carrier of Aut(F) by H;
h.(1_F) = 1_F by GROUP_1:def 13;
hence f.(1.F) = 1.F;
end;
B: for f be Function of F,F st f in G holds f.(0.F) = 0.F by RING_2:6;
C: now let a,b be Element of F;
assume D0: a in M & b in M; then
consider x being Element of F such that
D1: x = a & for f being Function of F,F st f in G holds f.x = x;
consider y being Element of F such that
D2: y = b & for f being Function of F,F st f in G holds f.y = y by D0;
now let f be Function of F,F;
assume A: f in G; then
reconsider h = f as Element of the carrier of Aut(F) by H;
h.(a+b) = h.a + h.b by VECTSP_1:def 20
.= a + f.b by A,D1 .= a + b by A,D2;
hence f.(a+b) = a+b;
end;
hence a + b in M;
now let f be Function of F,F;
assume A: f in G; then
reconsider h = f as Element of the carrier of Aut(F) by H;
h.(a*b) = h.a * h.b by GROUP_6:def 6
.= a * f.b by A,D1 .= a * b by A,D2;
hence f.(a*b) = a*b;
end;
hence a * b in M;
now let f be Function of F,F;
assume A: f in G; then
reconsider h = f as Element of the carrier of Aut(F) by H;
h.(-a) = -(h.a) by RING_2:7 .= -a by A,D1;
hence f.(-a) = -a;
end;
hence -a in M;
end;
now let a be non zero Element of F;
assume a in M; then
consider x being Element of F such that
D1: x = a & for f being Function of F,F st f in G holds f.x = x;
now let f be Function of F,F;
assume A: f in G; then
reconsider h = f as Element of the carrier of Aut(F) by H;
h is Automorphism of F & a <> 0.F; then
h.(a") = (h.a)" by lemH .= a" by A,D1;
hence f.(a") = a";
end;
hence a" in M;
end;
hence thesis by A,B,C;
end;
end;
definition
let F be Field;
let G be Subgroup of Aut(F);
func Fix(F,G) -> strict doubleLoopStr means :df:
the carrier of it = Fixed_El(F,G) &
the addF of it = (the addF of F)||Fixed_El(F,G) &
the multF of it = (the multF of F)||Fixed_El(F,G) &
1.it = 1.F & 0.it = 0.F;
existence
proof
take InducedSubfield Fixed_El(F,G);
thus thesis by FIELD_16:def 3;
end;
uniqueness;
end;
lemFix:
for F being Field, G being Subgroup of Aut(F)
holds Fix(F,G) = InducedSubfield Fixed_El(F,G)
proof
let F be Field, G be Subgroup of Aut(F);
set I = InducedSubfield Fixed_El(F,G);
A: the carrier of I = Fixed_El(F,G) by FIELD_16:def 3;
B: the addF of I = (the addF of F)||Fixed_El(F,G) by FIELD_16:def 3
.= the addF of Fix(F,G) by df;
C: the multF of I = (the multF of F)||Fixed_El(F,G) by FIELD_16:def 3
.= the multF of Fix(F,G) by df;
D: 1.I = 1.F by FIELD_16:def 3 .= 1.Fix(F,G) by df;
0.I = 0.F by FIELD_16:def 3 .= 0.Fix(F,G) by df;
hence thesis by A,B,C,D,df;
end;
registration
let F be Field;
let G be Subgroup of Aut(F);
cluster Fix(F,G) -> non degenerated;
coherence
proof
InducedSubfield Fixed_El(F,G) is non degenerated;
hence thesis by lemFix;
end;
end;
registration
let F be Field;
let G be Subgroup of Aut(F);
cluster Fix(F,G) -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
InducedSubfield Fixed_El(F,G) is
Abelian add-associative right_zeroed right_complementable;
hence thesis by lemFix;
end;
end;
registration
let F be Field;
let G be Subgroup of Aut(F);
cluster Fix(F,G) -> commutative associative well-unital
distributive almost_left_invertible;
coherence
proof
InducedSubfield Fixed_El(F,G) is commutative associative well-unital
distributive almost_left_invertible;
hence thesis by lemFix;
end;
end;
definition
let F be Field;
let G be Subgroup of Aut(F);
redefine func Fix(F,G) -> strict Subfield of F; :: redefines Fix (GALOIS_1, definition)
coherence
proof
InducedSubfield Fixed_El(F,G) is strict Subfield of F;
hence thesis by lemFix;
end;
end;
G16:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E,F) holds Fix(E,G) is IntermediateField of E,F
proof
let F be Field, E being FieldExtension of F, G be Subgroup of Aut(E,F);
reconsider C = G as Subgroup of Aut(E);
H: Aut(E,F) = multMagma (# Auts(E,F), AutComp(E,F) #) &
Auts(E,F) = the set of all f where f is F-fixing Automorphism of E &
the carrier of G c= the carrier of Aut(E,F) &
F is Subfield of E
by FIELD_4:7,GROUP_2:def 5;
now let o be object;
assume A: o in the carrier of F;
the carrier of F c= the carrier of E by H,EC_PF_1:def 1; then
reconsider a = o as Element of E by A;
for f being Function of E,E st f in C holds f.a = a by A,FIELD_8:def 2;
then o in Fixed_Elements(E,C);
hence o in the carrier of Fix(E,G) by df;
end; then
B: the carrier of F c= the carrier of Fix(E,G); then
I: [:the carrier of F,the carrier of F:] c=
[:the carrier of Fix(E,G),the carrier of Fix(E,G):] by ZFMISC_1:96;
C: (the addF of Fix(E,G)) || the carrier of F
= (((the addF of E) || the carrier of Fix(E,G))) || the carrier of F
by EC_PF_1:def 1
.= (the addF of E) || the carrier of F by I,FUNCT_1:51
.= the addF of F by H,EC_PF_1:def 1;
D: (the multF of Fix(E,G)) || the carrier of F
= (((the multF of E) || the carrier of Fix(E,G))) || the carrier of F
by EC_PF_1:def 1
.= (the multF of E) || the carrier of F by I,FUNCT_1:51
.= the multF of F by H,EC_PF_1:def 1;
E: 1.F = 1.E by H,EC_PF_1:def 1 .= 1.Fix(E,G) by df;
0.F = 0.E by H,EC_PF_1:def 1 .= 0.Fix(E,G) by df; then
F is Subfield of Fix(E,G) by B,C,D,E,EC_PF_1:def 1; then
Fix(E,G) in IntermediateFields(E,F) by FIELD_14:4;
hence thesis by GALOIS_0:def 5;
end;
definition
let F be Field;
let E be FieldExtension of F;
let G be Subgroup of Aut(E,F);
redefine func Fix(E,G) -> IntermediateField of E,F; :: redefines Fix (GALOIS_1, definition)
coherence by G16;
end;
begin :: Some basic properties
theorem G1:
for F being Field
for E being FieldExtension of F holds F is Subfield of Fix(E,Aut(E,F))
proof
let F be Field, E be FieldExtension of F;
now let o be object;
assume B: o in the carrier of F;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1; then
reconsider a = o as Element of the carrier of E by B;
now let f be Function of E,E;
assume f in Aut(E,F);
then f is F-fixing isomorphism;
hence f.a = a by B;
end;
then a in Fixed_Elements(E,Aut(E,F));
hence o in the carrier of Fix(E,Aut(E,F)) by df;
end; then
B: the carrier of F c= the carrier of Fix(E,Aut(E,F)); then
H: [:the carrier of F,the carrier of F:] c=
[:the carrier of Fix(E,Aut(E,F)),the carrier of Fix(E,Aut(E,F)):]
by ZFMISC_1:96;
F is Subfield of E by FIELD_4:7; then
A: 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;
E: (the addF of Fix(E,Aut(E,F))) || the carrier of F
= ((the addF of E) || the carrier of Fix(E,Aut(E,F)))|| the carrier of F
by EC_PF_1:def 1
.= the addF of F by A,H,FUNCT_1:51;
F: (the multF of Fix(E,Aut(E,F))) || the carrier of F
= ((the multF of E) || the carrier of Fix(E,Aut(E,F)))|| the carrier of F
by EC_PF_1:def 1
.= the multF of F by A,H,FUNCT_1:51;
1.F = 1.Fix(E,Aut(E,F)) & 0.F = 0.Fix(E,Aut(E,F))
by A,EC_PF_1:def 1;
hence thesis by B,E,F,EC_PF_1:def 1;
end;
theorem
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds K is Subfield of Fix(E,Aut(E,K))
by G1;
theorem G2:
for F being Field
for G being Subgroup of Aut(F) holds G is Subgroup of Aut(F,Fix(F,G))
proof
let F be Field, G be Subgroup of Aut(F);
now let o be object;
assume B: o in the carrier of G;
the carrier of G c= the carrier of Aut(F) by GROUP_2:def 5; then
o in the set of all f where f is Automorphism of F by B; then
consider f being Automorphism of F such that E: o = f;
reconsider E = F as FieldExtension of Fix(F,G) by FIELD_4:7;
reconsider f as Automorphism of E;
now let a be Element of Fix(F,G);
the carrier of Fix(F,G) = Fixed_El(F,G) by df; then
a in Fixed_El(F,G); then
consider a1 being Element of F such that
G: a1 = a & for f being Function of F,F st f in G holds f.a1 = a1;
f in G by B,E;
hence f.a = a by G;
end; then
f is Fix(F,G)-fixing;
hence o in the carrier of Aut(F,Fix(F,G)) by E;
end; then
B: the carrier of G c= the carrier of Aut(F,Fix(F,G)); then
J: [:the carrier of G,the carrier of G:] c=
[:the carrier of Aut(F,Fix(F,G)),the carrier of Aut(F,Fix(F,G)):]
by ZFMISC_1:96;
the multF of G = (the multF of Aut(F))||the carrier of G by GROUP_2:def 5;
then (the multF of Aut(F,Fix(F,G)))||the carrier of G
= the multF of G by J,FUNCT_1:51;
hence thesis by B,GROUP_2:def 5;
end;
G3:
for F being Field
for K being FieldExtension of F
for E being K-extending FieldExtension of F
holds Aut(E,K) is Subgroup of Aut(E,F)
proof
let F be Field, K be FieldExtension of F;
let E be K-extending FieldExtension of F;
now let o be object;
assume o in the carrier of Aut(E,K); then
consider f being K-fixing Automorphism of E such that E: o = f;
now let a be Element of F;
F is Subfield of K by FIELD_4:7; then
the carrier of F c= the carrier of K by EC_PF_1:def 1; then
reconsider a1 = a as Element of K;
thus f.a = a1 by FIELD_8:def 2 .= a;
end; then
f is F-fixing;
hence o in the carrier of Aut(E,F) by E;
end; then
B: the carrier of Aut(E,K) c= the carrier of Aut(E,F); then
J: [:the carrier of Aut(E,K),the carrier of Aut(E,K):] c=
[:the carrier of Aut(E,F),the carrier of Aut(E,F):] by ZFMISC_1:96;
(the multF of Aut(E,F))||the carrier of Aut(E,K)
= the multF of Aut(E,K) by J,FUNCT_1:51;
hence thesis by B,GROUP_2:def 5;
end;
theorem
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds Aut(E,K) is Subgroup of Aut(E,F)
by G3;
theorem
for F being Field
for E being FieldExtension of F
for K1,K2 being IntermediateField of E,F
st K1 is Subfield of K2 holds Aut(E,K2) is Subgroup of Aut(E,K1)
proof
let F be Field, E be FieldExtension of F, K1,K2 be IntermediateField of E,F;
assume K1 is Subfield of K2; then
reconsider K3 = K2 as FieldExtension of K1 by FIELD_4:7;
K1 in IntermediateFields(E,F) by GALOIS_0:def 5; then
K1 is Subfield of E by FIELD_14:4; then
reconsider E1 = E as FieldExtension of K1 by FIELD_4:7;
K2 in IntermediateFields(E,F) by GALOIS_0:def 5; then
K2 is Subfield of E by FIELD_14:4; then
reconsider E1 as K3-extending FieldExtension of K1 by FIELD_4:7;
Aut(E1,K3) is Subgroup of Aut(E1,K1) by G3;
hence thesis;
end;
theorem G4:
for F being Field
for G1,G2 being Subgroup of Aut(F)
st G1 is Subgroup of G2 holds Fix(F,G2) is Subfield of Fix(F,G1)
proof
let F be Field, G1,G2 being Subgroup of Aut(F);
assume AS: G1 is Subgroup of G2;
now let o be object;
assume B: o in the carrier of Fix(F,G2);
the carrier of Fix(F,G2) = Fixed_El(F,G2) by df; then
consider a being Element of F such that
G: a = o & for f being Function of F,F st f in G2 holds f.a = a by B;
now let f be Function of F,F;
assume B: f in G1;
the carrier of G1 c= the carrier of G2 by AS,GROUP_2:def 5; then
f in G2 by B;
hence f.a = a by G;
end; then
a in Fixed_El(F,G1);
hence o in the carrier of Fix(F,G1) by G,df;
end; then
B: the carrier of Fix(F,G2) c= the carrier of Fix(F,G1); then
J: [:the carrier of Fix(F,G2),the carrier of Fix(F,G2):] c=
[:the carrier of Fix(F,G1),the carrier of Fix(F,G1):] by ZFMISC_1:96;
A: the addF of Fix(F,G2) = (the addF of F) || the carrier of Fix(F,G2)
& the multF of Fix(F,G2) = (the multF of F) || the carrier of Fix(F,G2)
& 1.F = 1.Fix(F,G2) & 0.F = 0.Fix(F,G2) by EC_PF_1:def 1;
E: (the addF of Fix(F,G1)) || the carrier of Fix(F,G2)
= ((the addF of F) || the carrier of Fix(F,G1))|| the carrier of Fix(F,G2)
by EC_PF_1:def 1
.= the addF of Fix(F,G2) by A,J,FUNCT_1:51;
F: (the multF of Fix(F,G1)) || the carrier of Fix(F,G2)
= ((the multF of F) || the carrier of Fix(F,G1))|| the carrier of Fix(F,G2)
by EC_PF_1:def 1
.= the multF of Fix(F,G2) by A,J,FUNCT_1:51;
1.Fix(F,G1) = 1.Fix(F,G2) & 0.Fix(F,G1) = 0.Fix(F,G2)
by A,EC_PF_1:def 1;
hence thesis by B,E,F,EC_PF_1:def 1;
end;
theorem
for F being Field
for E being FieldExtension of F holds Aut(E,F) = Aut(E,Fix(E,Aut(E,F)))
proof
let F be Field, E be FieldExtension of F;
A: Aut(E,F) is Subgroup of Aut(E,Fix(E,Aut(E,F))) by G2;
F is Subfield of Fix(E,Aut(E,F)) by G1; then
reconsider K = Fix(E,Aut(E,F)) as FieldExtension of F by FIELD_4:7;
reconsider E as K-extending FieldExtension of F by FIELD_4:7;
Aut(E,Fix(E,Aut(E,F))) is Subgroup of Aut(E,F) by G3;
hence thesis by A,GROUP_2:55;
end;
theorem
for F being Field
for G being Subgroup of Aut(F) holds Fix(F,G) = Fix(F,Aut(F,Fix(F,G)))
proof
let F be Field, G be Subgroup of Aut(F);
G is Subgroup of Aut(F,Fix(F,G)) by G2; then
Fix(F,G) == Fix(F,Aut(F,Fix(F,G))) by G4,G1;
hence thesis;
end;
begin :: Galois Extensions
definition
let F be Field;
let E be FieldExtension of F;
attr E is F-Galois means :defGalois:
Fix(E,Aut(E,F)) == F;
end;
lemG0:
for F being Field
for E being FieldExtension of F holds the carrier of (1).Aut(E,F) = {id E}
proof
let F be Field,E be FieldExtension of F;
id E = 1_(Aut E) by Th1;
then the carrier of (1).(Aut E) = {id E} by GROUP_2:def 7;
hence thesis by GROUP_2:63;
end;
lemG1:
for F being Field
for E being FieldExtension of F st E = F holds Aut(E,F) = (1).Aut(E)
proof
let F be Field, E be FieldExtension of F;
assume AS: E = F;
H: the carrier of (1).Aut(E,F) = {id E} by lemG0;
A: now let o be object;
assume o in the carrier of (1).Aut(E);
then o in the carrier of (1).Aut(E,F) by GROUP_2:63;
then o = id E by H,TARSKI:def 1;
hence o in the carrier of Aut(E,F);
end;
now let o be object;
assume o in the carrier of Aut(E,F); then
consider h being F-fixing Automorphism of E such that C: h = o;
h = id E by AS,FIELD_8:def 2;
then o in {id E} by C,TARSKI:def 1;
then o in the carrier of (1).Aut(E,F) by lemG0;
hence o in the carrier of (1).Aut(E) by GROUP_2:63;
end;
hence thesis by A,TARSKI:2,GROUP_2:59;
end;
lemG2:
for F being Field holds Fix(F,(1).Aut(F)) == F
proof
let F be Field;
reconsider E = F as FieldExtension of F by FIELD_4:6;
set A = (1).Aut(F);
(1).Aut(F) = (1).Aut(E,F) by GROUP_2:63; then
A: the carrier of (1).Aut(F) = {id F} by lemG0;
now let o be object;
assume o in the carrier of F; then
reconsider a = o as Element of F;
now let f be Function of F,F;
assume f in A;
then f = id F by A,TARSKI:def 1;
hence f.a = a;
end;
hence o in Fixed_El(F,A);
end; then
the carrier of F c= Fixed_El(F,A); then
B: Fixed_El(F,A) = the carrier of F by XBOOLE_0:def 10; then
the addF of Fix(F,A) = (the addF of F)||(the carrier of F) &
the multF of Fix(F,A) = (the multF of F)||(the carrier of F) &
1.Fix(F,A) = 1.F & 0.Fix(F,A) = 0.F by df;
hence thesis by B,df;
end;
lemG3:
for F being Field
for E being FieldExtension of F st E = F holds Fix(E,Aut(E,F)) == F
proof
let F be Field,E be FieldExtension of F;
assume AS: E = F;
then Fix(E,Aut(E,F)) = Fix(E,(1).Aut(E)) by lemG1;
hence thesis by AS,lemG2;
end;
registration
let F be Field;
cluster F-Galois for FieldExtension of F;
existence
proof
reconsider E = F as FieldExtension of F by FIELD_4:6;
take E;
thus thesis by lemG3;
end;
end;
definition
let F be Field;
mode GaloisExtension of F is F-Galois FieldExtension of F;
end;
registration
let F be Field;
cluster F-finite for GaloisExtension of F;
existence
proof
reconsider E = F as FieldExtension of F by FIELD_4:6;
Fix(E,Aut(E,F)) == F by lemG3; then
reconsider E as GaloisExtension of F by defGalois;
take E;
deg(E,F) = 1 by FIELD_7:8;
then VecSp(E,F) is finite-dimensional by FIELD_4:def 7;
hence thesis by FIELD_4:def 8;
end;
end;
theorem
for F being Field
for E being FieldExtension of F
holds E is F-Galois iff ex G being Subgroup of Aut(E) st Fix(E,G) == F
proof
let F be Field, E be FieldExtension of F;
now assume ex G being Subgroup of Aut(E) st F == Fix(E,G); then
consider G being Subgroup of Aut(E) such that A: F == Fix(E,G);
now let o be object;
assume A1: o in the carrier of G;
the carrier of G c= the carrier of Aut(E) by GROUP_2:def 5; then
reconsider f = o as Element of the carrier of Aut(E) by A1;
now let a be Element of F;
a in Fix(E,G) by A; then
a in Fixed_El(E,G) by df; then
consider a1 being Element of E such that
A2: a1 = a &
for f being Function of E,E st f in G holds f.a1 = a1;
f in G by A1;
hence f.a = a by A2;
end; then
f is F-fixing;
hence o in the carrier of Aut(E,F);
end; then
H: the carrier of G c= the carrier of Aut(E,F);
the multF of G
= (the multF of Aut(E))||the carrier of G by GROUP_2:def 5
.= (the multF of Aut(E,F))||the carrier of G by H,ZFMISC_1:96,RELAT_1:74;
then
G is Subgroup of Aut(E,F) by H,GROUP_2:def 5; then
Fix(E,Aut(E,F)) is Subfield of Fix(E,G) by G4; then
F == Fix(E,Aut(E,F)) by G1,A,EC_PF_1:5;
hence E is F-Galois;
end;
hence thesis;
end;
theorem
for F being Field holds F is GaloisExtension of F
proof
let F be Field;
reconsider E = F as FieldExtension of F by FIELD_4:6;
Fix(E,Aut(E,F)) == F by lemG3;
hence thesis by defGalois;
end;
definition
func *' -> Function of F_Complex,F_Complex means :di:
for z being Element of F_Complex holds it.z = z*';
existence
proof
set L = F_Complex;
defpred P[object,object] means ex c being Element of L st $1 = c & $2 = c*';
A: now let x be object;
assume x in the carrier of L; then
reconsider c = x as Element of L;
thus ex y being object st y in the carrier of L & P[x,y]
proof
take c*';
thus thesis;
end;
end;
consider f being Function of the carrier of L,the carrier of L such that
B: for x being object st x in the carrier of L holds P[x,f.x]
from FUNCT_2:sch 1(A);
take f;
now let z be Element of L;
P[z,f.z] by B;
hence f.z = z*';
end;
hence thesis;
end;
uniqueness
proof
set L = F_Complex;
let f1,f2 be Function of L,L;
assume A: for z being Element of L holds f1.z = z*';
assume B: for z being Element of L holds f2.z = z*';
now let z be Element of L;
thus f1.z = z*' by A .= f2.z by B;
end;
hence f1 = f2;
end;
end;
registration
cluster *' -> (F_Real)-fixing isomorphism;
coherence
proof
set f = *', L = F_Complex;
now let a be Element of F_Real;
F_Real is Subfield of L by FIELD_4:7; then
the carrier of F_Real c= the carrier of L by EC_PF_1:def 1; then
reconsider c = a as Element of L;
thus f.a = c*' by di .= a;
end;
hence *' is (F_Real)-fixing;
now let o be object;
assume o in the carrier of L; then
reconsider a = o as Element of L;
Re a - (Im a)*<i> in COMPLEX by XCMPLX_0:def 2; then
reconsider c = Re a + (-(Im a))*<i> as Element of L by COMPLFLD:def 1;
H: dom f = the carrier of L by FUNCT_2:def 1;
I: Re c = Re a & Im c = -(Im a) by COMPLEX1:12;
f.c = c*' by di
.= Re c - (Im c) * <i> by COMPLEX1:def 11
.= Re a + (Im a) * <i> by I
.= a by COMPLEX1:13;
hence o in rng f by H,FUNCT_1:def 3;
end; then
rng f c= the carrier of L & the carrier of L c= rng f
by RELAT_1:def 19; then
B: *' is onto by XBOOLE_0:def 10;
now let x,y be Element of L;
thus f.(x+y) = (x+y)*' by di
.= Re(x+y) - Im(x+y) * <i> by COMPLEX1:def 11
.= (Re x + Re y) - Im(x+y) * <i> by COMPLEX1:8
.= (Re x + Re y) - ((Im x + Im y) * <i>) by COMPLEX1:8
.= (Re x - Im x * <i>) + (Re y - Im y * <i>)
.= x*' + (Re y - Im y * <i>) by COMPLEX1:def 11
.= x*' + y*' by COMPLEX1:def 11
.= f.x + y*' by di
.= f.x + f.y by di;
end; then
C: *' is additive by VECTSP_1:def 20;
now let x,y be Element of L;
thus f.(x*y) = (x*y)*' by di
.= Re(x*y) - Im(x*y) * <i> by COMPLEX1:def 11
.= (Re x * Re y - Im x * Im y) - Im(x*y) * <i> by COMPLEX1:9
.= (Re x * Re y - Im x * Im y) -
(Re x * Im y + Re y * Im x) * <i> by COMPLEX1:9
.= (Re x - Im x * <i>) * (Re y - Im y * <i>)
.= x*' * (Re y - Im y * <i>) by COMPLEX1:def 11
.= x*' * y*' by COMPLEX1:def 11
.= f.x * y*' by di
.= f.x * f.y by di;
end; then
D: *' is multiplicative by GROUP_6:def 6;
*' is unity-preserving by di,COMPLFLD:49;
hence thesis by B,C,D;
end;
end;
definition
redefine func *' -> Element of the carrier of Aut(F_Complex,F_Real); :: redefines *' (GALOIS_1, definition)
coherence
proof
*' in the set of all f where f is (F_Real)-fixing Automorphism of F_Complex;
hence thesis;
end;
end;
theorem U1:
Auts(F_Complex,F_Real) = { id F_Complex, *' }
proof
A: now let o be object;
assume o in {id F_Complex, *'}; then
per cases by TARSKI:def 2;
suppose o = id F_Complex;
hence o in Auts(F_Complex,F_Real);
end;
suppose o = *';
hence o in Auts(F_Complex,F_Real);
end;
end;
H: <i>*' = -<i> by COMPLEX1:31;
now let o be object;
assume o in Auts(F_Complex,F_Real); then
consider f being (F_Real)-fixing Automorphism of F_Complex such that
A: o = f;
f.<i> in Roots(FAdj(F_Real,{<i>}),MinPoly(<i>,F_Real)) by lem6,FIELD_16:13;
then per cases by lem6,lemma,lemMinPol,TARSKI:def 2;
suppose f.<i> = <i>; then
f.<i> = (id F_Complex).<i>; then
f = id F_Complex by lem6,FIELD_16:16;
hence o in {id F_Complex, *'} by A,TARSKI:def 2;
end;
suppose f.<i> = -<i>; then
f.<i> = (*').<i> by H,di; then
f = *' by lem6,FIELD_16:16;
hence o in {id F_Complex, *'} by A,TARSKI:def 2;
end;
end;
hence thesis by A,TARSKI:2;
end;
lemAT3:
for F being Field
for E being FieldExtension of F
for f,g being Function of E,E
for a,b being Element of Aut(E,F)
st f = a & g = b holds f * g = a * b
proof
let F be Field, E be FieldExtension of F, f,g be Function of E,E;
let a,b be Element of Aut(E,F);
assume A: f = a & g = b;
[a,b] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
hence a * b = (AutComp E).(f,g) by A,FUNCT_1:49 .= f * g by A,defMult;
end;
lemAT2:
for F being Field
for E being FieldExtension of F
for f being Function of E,E
for a being Element of Aut(E,F)
for m being Nat st f = a holds f`^m = a|^m
proof
let F be Field, E be FieldExtension of F, f be Function of E,E;
let a be Element of Aut(E,F), m be Nat;
assume AS: f = a;
defpred P[Nat] means f`^($1) = a|^($1);
f`^0 = id E by FIELD_16:1 .= 1_Aut(E) by Th1
.= 1_Aut(E,F) by GROUP_2:44 .= a|^0 by GROUP_1:25; then
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
f`^(k+1) = (f`^k) * f by FIELD_16:2
.= a|^k * a by IV,AS,lemAT3
.= a|^(k+1) by GROUP_1:34;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
theorem U2:
Aut(F_Complex,F_Real) = gr { *' }
proof
set F = F_Real, E = F_Complex;
reconsider b = id F_Complex as Element of Aut(E,F) by U1,TARSKI:def 2;
now let o be object;
assume o in the carrier of Aut(E,F); then
per cases by U1,TARSKI:def 2;
suppose A: o = id F_Complex;
b = (*')`^0 by FIELD_16:1 .= (*')|^0 by lemAT2;
then b in gr{*'} by GR_CY_1:5;
hence o in the carrier of gr{*'} by A;
end;
suppose A: o = *';
*' = (*')`^1 .= (*')|^1 by lemAT2;
then *' in gr{*'} by GR_CY_1:5;
hence o in the carrier of gr{*'} by A;
end;
end; then
the carrier of Aut(E,F) c= the carrier of gr{*'};
hence thesis by GROUP_2:61;
end;
registration
cluster Aut(F_Complex,F_Real) -> finite cyclic;
coherence by U1,U2,GR_CY_1:def 7;
end;
theorem U3:
order Aut(F_Complex,F_Real) = 2
proof
reconsider c = <i> as Complex;
<i>*' = -<i> by COMPLEX1:31;
then
(*').<i> = -<i> by di; then
id F_Complex <> *';
hence thesis by U1,CARD_2:57;
end;
theorem
Aut(F_Complex,F_Real), INT.Group(2) are_isomorphic
proof
set E = F_Complex, F = F_Real;
defpred P[object,object] means
($1 = 0 & $2 = id E) or ($1 = 1 & $2 = *');
A2: INT.Group(2) = multMagma(#Segm(2),addint(2)#) by GR_CY_1:def 5;
A: now let x1 be object;
assume A1: x1 in the carrier of INT.Group(2); then
reconsider x = x1 as natural Number by A2;
x in Segm(1+1) by A1,A2; then
B: x = 0 or ... or x = 1 by NAT_1:61;
thus ex y being object st y in the carrier of Aut(E,F) & P[x1,y]
proof
per cases by B;
suppose C: x = 0;
take id E;
thus thesis by C;
end;
suppose C: x = 1;
take *';
thus thesis by C;
end;
end;
end;
consider f being Function of the carrier of INT.Group(2),
the carrier of Aut(E,F) such that
B: for x being object st x in the carrier of INT.Group(2) holds P[x,f.x]
from FUNCT_2:sch 1(A);
reconsider f as Function of INT.Group(2), Aut(E,F);
H: id F_Complex <> *'
proof
reconsider c = <i> as Complex;
A: <i>*' = -<i> by COMPLEX1:31;
(*').<i> = -<i> by A,di;
hence thesis;
end;
reconsider g = id E as Element of the carrier of Aut(E,F) by U1,TARSKI:def 2;
reconsider g as F-fixing Automorphism of E;
now let x,y be Element of INT.Group(2);
reconsider n = x, m = y as Element of Segm(2) by A2;
dom f = Segm(2) by A2,FUNCT_2:def 1; then
f.m in rng f & rng f c= the carrier of Aut(E,F)
by FUNCT_1:3,RELAT_1:def 19; then
reconsider g1 = f.m as Element of the carrier of Aut(E,F);
reconsider g1 as F-fixing Automorphism of E;
J: [g,g1] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
n in Segm(1+1); then
n = 0 or ... or n = 1 by NAT_1:61; then
per cases;
suppose D: n = 0; then
(addint(2)).(n,m) = (0+m) mod 2 by GR_CY_1:def 4
.= m by NAT_1:44,NAT_D:24;
hence f.(x*y) = (id E) * g1 by A2,FUNCT_2:17
.= (AutComp E).(g,g1) by defMult
.= AutComp(E,F).(g,g1) by J,FUNCT_1:49
.= f.x * f.y by B,D;
end;
suppose D: n = 1;
dom f = Segm(2) by A2,FUNCT_2:def 1;
then f.n in rng f & rng f c= the carrier of Aut(E,F)
by FUNCT_1:3,RELAT_1:def 19; then
reconsider g2 = f.n as Element of the carrier of Aut(E,F);
reconsider g2 as F-fixing Automorphism of E;
J: [g2,g] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
m in Segm(1+1); then
m = 0 or ... or m = 1 by NAT_1:61; then
per cases;
suppose D1: m = 0; then
(addint(2)).(n,m) = (n+0) mod 2 by GR_CY_1:def 4
.= n by NAT_1:44,NAT_D:24;
hence f.(x*y) = g2 * (id E) by A2,FUNCT_2:17
.= (AutComp E).(g2,g) by defMult
.= AutComp(E,F).(g2,g) by J,FUNCT_1:49
.= f.x * f.y by B,D1;
end;
suppose D1: m = 1; then
D2: (addint(2)).(n,m) = (1+1) mod 2 by D,GR_CY_1:def 4
.= 0 by NAT_D:25;
D3: f.m = *' & f.n = *' by D1,D,B;
J: [*',*'] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
reconsider g3 = *' as F-fixing Automorphism of E;
K: g3 * g3 = id E
proof
set h = g3 * g3;
now let o be object;
assume o in the carrier of F_Complex; then
reconsider a = o as Element of the carrier of F_Complex;
dom g3 = the carrier of E by FUNCT_2:def 1; then
a in dom g3 & g3.a in dom g3; then
a in dom h by FUNCT_1:11; then
h.a = g3.(g3.a) by FUNCT_1:12 .= g3.(a*') by di
.= (a*')*' by di .= (id E).a;
hence h.o = (id E).o;
end;
hence thesis;
end;
thus f.(x*y) = id E by A2,B,D2
.= (AutComp E).(g3,g3) by K,defMult
.= f.x * f.y by D3,J,FUNCT_1:49;
end;
end;
end; then
reconsider f as Homomorphism of INT.Group(2), Aut(E,F) by GROUP_6:def 6;
C: card(the carrier of INT.Group(2))
= card(the carrier of Aut(E,F)) by U3,A2,ORDINAL1:def 17;
now let x1,x2 be object;
assume C: x1 in the carrier of INT.Group(2) &
x2 in the carrier of INT.Group(2) & f.x1 = f.x2;
then reconsider n = x1, m = x2 as natural Number by A2;
n in Segm(1+1) by C,A2; then
n = 0 or ... or n = 1 by NAT_1:61; then
per cases;
suppose D: n = 0;
then f.n = id E by C,B;
hence x1 = x2 by C,H,B,D;
end;
suppose D: n = 1;
then f.n = *' by C,B;
hence x1 = x2 by C,H,B,D;
end;
end; then
D: f is one-to-one by FUNCT_2:19; then
f is onto by C,FINSEQ_4:63;
hence thesis by D,GROUP_6:def 11;
end;
registration
cluster F_Complex -> (F_Real)-Galois;
coherence
proof
set E = F_Complex, F = F_Real, K = Fix(E,Aut(E,F));
Fixed_Elements(E,Aut(E,F)) = {a where a is Element of E :
for f being Function of E,E st f in Aut(E,F) holds f.a = a}; then
A: the carrier of K = {a where a is Element of E :
for f being Function of E,E st f in Aut(E,F) holds f.a = a} by df;
B: now let o be object;
assume o in the carrier of F; then
reconsider a = o as Element of F;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
for f being Function of E,E st f in Aut(E,F) holds f.a1 = a1
by FIELD_8:def 2;
hence o in the carrier of K by A;
end;
now let o be object;
assume o in the carrier of K; then
consider a being Element of E such that
D: a = o &
for f being Function of E,E st f in Aut(E,F) holds f.a = a by A;
(*') in Aut(E,F); then
(*').a = a by D; then
a*' = a by di; then
a is Element of F_Real by U0;
hence o in the carrier of F by D;
end; then
C: the carrier of F = the carrier of K by B,TARSKI:2;
F is Subfield of E by FIELD_4:7; then
D: 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;
the carrier of K = Fixed_El(E,Aut(E,F)) by df;
hence thesis by C,D,df;
end;
end;
theorem
F_Complex is GaloisExtension of F_Real;
definition
let p be Prime;
let n be non zero Nat;
let F be GaloisField of p|^n;
redefine func Frob F -> Element of the carrier of Aut(F,Z/p); :: redefines Frob (FIELD_16, synonym) → FrobeniusMorphism (FIELD_16, definition)
coherence
proof
Frob F in the set of all f where f is (Z/p)-fixing Automorphism of F;
hence thesis;
end;
end;
registration
let p be Prime;
let n be non zero Nat;
let F be GaloisField of p|^n;
let m be Nat;
cluster (Frob F)`^m -> (Z/p)-fixing isomorphism;
coherence;
end;
theorem AT0:
for p being Prime, n being non zero Nat
for F being GaloisField of p|^n holds Aut(F,Z/p) = Aut(F)
proof
let p be Prime, n be non zero Nat, F be GaloisField of p|^n;
card F = p|^n by FIELD_16:def 8; then
A: the set of all f where f is Automorphism of F =
{ (Frob F)`^m where m is Nat : 0 <= m & m <= n-1 } by FIELD_16:65;
now let o be object;
assume o in the carrier of Aut(F); then
consider m being Nat such that
B: o = (Frob F)`^m & 0 <= m & m <= n - 1 by A;
thus o in the carrier of Aut(F,Z/p) by B;
end; then
the carrier of Aut(F) c= the carrier of Aut(F,Z/p);
hence thesis by GROUP_2:61;
end;
theorem AT1:
for p being Prime, n being non zero Nat
for F being GaloisField of p|^n holds
Auts(F,Z/p) = { (Frob F)`^m where m is Nat : 0 <= m & m <= n-1 }
proof
let p be Prime, n be non zero Nat, F be GaloisField of p|^n;
card F = p|^n by FIELD_16:def 8; then
the set of all f where f is Automorphism of F =
{ (Frob F)`^m where m is Nat : 0 <= m & m <= n-1 } by FIELD_16:65;
hence Auts(F,Z/p)
= {(Frob F)`^m where m is Nat : 0 <= m & m <= n-1} by AT0;
end;
theorem AT2:
for p being Prime, n being non zero Nat
for F being GaloisField of p|^n holds Aut(F,Z/p) = gr { Frob F }
proof
let p be Prime, n be non zero Nat, F be GaloisField of p|^n;
card F = p|^n by FIELD_16:def 8; then
A: the set of all f where f is Automorphism of F =
{ (Frob F)`^m where m is Nat : 0 <= m & m <= n-1 } by FIELD_16:65;
now let o be object;
assume o in the carrier of Aut(F,Z/p);
then o in the carrier of Aut(F);
then consider m being Nat such that
B: o = (Frob F)`^m & 0 <= m & m <= n - 1 by A;
(Frob F)`^m = (Frob F)|^m by lemAT2; then
(Frob F)`^m in gr{Frob F} by GR_CY_1:5;
hence o in the carrier of gr{Frob F} by B;
end; then
the carrier of Aut(F,Z/p) c= the carrier of gr{Frob F};
hence thesis by GROUP_2:61;
end;
AT3:
for p being Prime, n being non zero Nat
for F being GaloisField of p|^n holds card(the carrier of Aut(F,Z/p)) = n
proof
let p be Prime, n be non zero Nat, F be GaloisField of p|^n;
card F = p|^n by FIELD_16:def 8; then
card{(Frob F)`^m where m is Nat : 0 <= m & m <= n-1} = n by FIELD_16:64;
hence thesis by AT1;
end;
registration
let p be Prime;
let n be non zero Nat;
let F be GaloisField of p|^n;
cluster Aut(F,Z/p) -> finite cyclic;
coherence
proof
card(the carrier of Aut(F,Z/p)) = n by AT3;
hence Aut(F,Z/p) is finite;
Aut(F,Z/p) = gr { Frob F } by AT2;
hence Aut(F,Z/p) is cyclic by GR_CY_1:def 7;
end;
end;
theorem
for p being Prime, n being non zero Nat
for F being GaloisField of p|^n holds order Aut(F,Z/p) = n by AT3;
theorem
for p being Prime, n being non zero Nat
for F being GaloisField of p|^n
holds Aut(F,Z/p), INT.Group(n) are_isomorphic
proof
let p be Prime, n be non zero Nat, F be GaloisField of p|^n;
set a = Frob F;
defpred P[object,object] means ex m being Nat st $1 = m & $2 = a|^m;
A2: INT.Group(n) = multMagma(#Segm(n),addint(n)#) by GR_CY_1:def 5;
A: now let x be object;
assume A1: x in the carrier of INT.Group(n); then
reconsider m = x as natural Number by A2;
thus ex y being object st y in the carrier of Aut(F,Z/p) & P[x,y]
proof
take a|^m;
thus thesis by A1;
end;
end;
consider f being Function of the carrier of INT.Group(n),
the carrier of Aut(F,Z/p) such that
B: for x being object st x in the carrier of INT.Group(n) holds P[x,f.x]
from FUNCT_2:sch 1(A);
reconsider f as Function of INT.Group(n), Aut(F,Z/p);
now let x,y be Element of INT.Group(n);
reconsider x1 = x, y1 = y as Element of Segm(n) by A2;
reconsider m1 = x, m2 = y as Nat by A2;
reconsider m = (x1+y1) mod n as Nat;
E: x * y = (x1+y1) mod n by A2,GR_CY_1:def 4; then
C: P[m,f.m] & P[m1,f.m1] & P[m2,f.m2] by B;
D: ((Frob F)`^m1) * ((Frob F)`^m2) = (Frob F)`^m
proof
D0: m1 + m2 = n * ((x1+y1) div n) + m by NAT_D:2;
card F = p|^n by FIELD_16:def 8; then
D1: (Frob F)`^n = id F by FIELD_16:61;
D2: (Frob F)`^(n * ((x1+y1) div n)) =
((Frob F)`^n)`^((x1+y1) div n) by FIELD_16:4;
thus ((Frob F)`^m1) * ((Frob F)`^m2)
= (Frob F)`^(n * ((x1+y1) div n) + m) by D0,FIELD_16:3
.= ((Frob F)`^(n*((x1+y1) div n)))*((Frob F)`^m) by FIELD_16:3
.= (Frob F)`^m by D2,D1,FUNCT_2:17;
end;
F: a|^m1 = (Frob F)`^m1 & a|^m2 = (Frob F)`^m2 by lemAT2;
thus f.(x*y)
= ((Frob F)`^m1) * ((Frob F)`^m2) by D,E,C,lemAT2
.= f.x * f.y by C,F,lemAT3;
end; then
reconsider f as Homomorphism of INT.Group(n), Aut(F,Z/p) by GROUP_6:def 6;
P: card F = p|^n by FIELD_16:def 8;
C: card(the carrier of INT.Group(n))
= card n by A2,ORDINAL1:def 17
.= card(the carrier of Aut(F,Z/p)) by AT3;
now let x1,x2 be object;
assume C1: x1 in the carrier of INT.Group(n) &
x2 in the carrier of INT.Group(n) & f.x1 = f.x2;
reconsider y1 = x1, y2 = x2 as Element of Segm(n) by C1,A2;
reconsider m1 = x1, m2 = x2 as Nat by C1,A2;
C2: P[m1,f.m1] & P[m2,f.m2] by C1,B; then
C3: (Frob F)`^m1 = f.m2 by C1,lemAT2 .= (Frob F)`^m2 by C2,lemAT2;
m1 < n & m2 < n by C1,A2,NAT_1:44; then
m1 + 1 <= n & m2 + 1 <= n by INT_1:7; then
0 <= m1 & m1+1-1 <= n-1 & 0 <= m2 & m2+1-1 <= n-1 by XREAL_1:9;
hence x1 = x2 by P,C3,FIELD_16:63;
end; then
D: f is one-to-one by FUNCT_2:19; then
f is onto by C,FINSEQ_4:63;
hence thesis by D,GROUP_6:def 11;
end;
registration
let p be Prime;
let n be non zero Nat;
cluster -> (Z/p)-Galois for GaloisField of p|^n;
coherence
proof
let E be GaloisField of p|^n;
set F = Z/p, K = Fix(E,Aut(E,F));
Fixed_Elements(E,Aut(E,F)) = {a where a is Element of E :
for f being Function of E,E st f in Aut(E,F) holds f.a = a}; then
A: the carrier of K = {a where a is Element of E :
for f being Function of E,E st f in Aut(E,F) holds f.a = a} by df;
B: now let o be object;
assume o in the carrier of F; then
reconsider a = o as Element of F;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
for f being Function of E,E st f in Aut(E,F) holds f.a1 = a1
by FIELD_8:def 2;
hence o in the carrier of K by A;
end;
now let o be object;
assume o in the carrier of K; then
consider a being Element of E such that
D: a = o &
for f being Function of E,E st f in Aut(E,F) holds f.a = a by A;
(Frob E) in Aut(E,F); then
(Frob E).a = a by D; then
a in PrimeField E by FIELD_16:45;
hence o in the carrier of F by D,FIELD_16:70;
end; then
C: the carrier of F = the carrier of K by B,TARSKI:2;
F is Subfield of E by FIELD_4:7; then
D: 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;
the carrier of K = Fixed_El(E,Aut(E,F)) by df;
hence thesis by C,D,df;
end;
end;
theorem
for p being Prime
for n being non zero Nat
for G being GaloisField of p|^n holds G is GaloisExtension of Z/p;