:: The Fundamental Theorem of {G}alois Theory
:: by Christoph Schwarzweller
::
:: Received January 24, 2026
:: Copyright (c) 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, C0SP1,
RLSUB_2, EC_PF_1, HURWITZ, CARD_1, WELLORD1, RING_2, FUNCT_1, FUNCT_2,
RELAT_1, NUMBERS, POLYNOM5, FOMODEL1, FIELD_14, XCMPLX_0, FIELD_12,
MOD_4, ARYTM_1, FIELD_4, MESFUNC1, CONLAT_1, XBOOLE_0, XXREAL_0,
GLIB_000, PRE_TOPC, REALSET1, GROUP_4, POLYNOM1, SIN_COS, FIELD_6,
RING_5, MCART_1, FIELD_8, GROUP_1, ALGSTR_0, LATTICE3, FINSET_1, EQREL_1,
CQC_SIM1, PEPIN, WAYBEL_0, GROUP_2, CATALG_1, FIELD_16, FIELD_13,
FIELD_15, AUTGROUP, ALGNUM_1, FIELD_1, MSSUBFAM, GROUP_3, GROUP_6,
GALOIS_0, ORDERS_2, LATTICES, FILTER_1, RING_3, NEWTON, ZFMISC_1,
GALOIS_1, GALOIS_3, GALOIS_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, FINSET_1,
REALSET1, XTUPLE_0, FUNCT_1, FUNCT_2, BINOP_1, NUMBERS, CARD_1, PARTFUN1,
XCMPLX_0, XXREAL_0, ORDERS_2, POLYNOM3, POLYNOM5, WAYBEL_0, LATTICE3,
CONLAT_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4,
GROUP_6, MOD_4, MATRLIN2, LATTICES, VECTSP_1, C0SP1, EC_PF_1, HURWITZ,
RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_4, FIELD_6,
FIELD_8, FIELD_12, FIELD_13, FIELD_14, FIELD_15, FIELD_16, GALOIS_0,
GALOIS_1, GALOIS_3;
constructors RINGCAT1, CONLAT_1, REALSET1, ALGNUM_1, GROUP_4, RING_5, FIELD_2,
FIELD_8, FIELD_13, FIELD_15, MATRLIN2, GALOIS_3;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, INT_1, SUBSET_1,
STRUCT_0, VECTSP_1, FINSET_1, VECTSP_2, FUNCT_2, LATTICE3, FUNCT_1,
REALSET1, MOD_4, RELAT_1, XTUPLE_0, GROUP_1, GROUP_2, GROUP_3, GROUP_6,
RING_2, RING_4, RINGCAT1, FIELD_6, FIELD_7, FIELD_8, FIELD_13, FIELD_16,
GALOIS_0, GALOIS_1, GALOIS_2, GALOIS_3;
requirements SUBSET, BOOLE;
definitions TARSKI;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, GALOIS_0, GALOIS_3;
expansions STRUCT_0, GROUP_1, VECTSP_1, TARSKI, GROUP_6, FUNCT_1, FUNCT_2,
RING_2, FIELD_7, FIELD_8, FIELD_16;
theorems GROUP_1, VECTSP_1, FUNCT_2, TARSKI, FUNCT_1, EC_PF_1, RING_5,
ZFMISC_1, FIELD_6, FIELD_8, GROUP_4, FIELD_5, FIELD_14, GROUP_6, RELAT_1,
XBOOLE_1, FIELD_13, FIELD_7, GROUP_2, LATTICE3, WAYBEL_0, CONLAT_1,
GROUP_3, GALOIS_0, GALOIS_1, GALOIS_2, FIELD_4, FIELD_15, RING_2, RING_3,
FIELD_16, FIELD_12, GALOIS_3, ORDERS_2, XCMPLX_1, MATRLIN2, XBOOLE_0,
RING_4, FIELD_10, FIELD_1;
schemes FUNCT_2;
begin :: On Normal Subgroups
theorem ThN1:
for G being Group
for H being Subgroup of G holds
H is normal iff for g,h being Element of G st h in H holds h |^ g in H
proof
let G be Group, H be Subgroup of G;
hereby assume H is normal; then
A1: for a being Element of G holds H |^ a = the multMagma of H
by GROUP_3:def 13;
thus for g,h being Element of G st h in H holds h |^ g in H
proof
let g,h be Element of G;
assume h in H;
then g" * (h * g) in g" * (H * g) by GROUP_2:104,GROUP_2:27;
then g" * h * g in g" * (H * g) by GROUP_1:def 3;
then g" * h * g in g" * H * g by GROUP_2:106;
then g" * h * g in H |^ g by GROUP_3:59;
then g" * h * g in H by A1;
hence thesis by GROUP_3:def 2;
end;
end;
assume B: for g,h being Element of G st h in H holds h |^ g in H;
now let a be Element of G;
B2: now let o be object;
assume o in the carrier of (H |^ a); then
o in H |^ a; then
consider b being Element of G such that
B3: o = b |^ a & b in H by GROUP_3:58;
b |^ a in H by B,B3;
hence o in the carrier of H by B3;
end;
now let o be object;
assume C1: o in the carrier of H;
the carrier of H c= the carrier of G by GROUP_2:def 5; then
reconsider b = o as Element of G by C1;
b in H by C1; then
b |^ (a") in H by B; then
a"" * b * a" in H by GROUP_3:def 2; then
(a * b * a") * a in H * a by GROUP_2:104; then
(a * b) * (a" * a) in H * a by GROUP_1:def 3; then
(a * b) * (1_G) in H * a by GROUP_1:def 5; then
a * b in H * a by GROUP_1:def 4; then
a" * (a * b) in a" * (H * a) by GROUP_2:27; then
(a" * a) * b in a" * (H * a) by GROUP_1:def 3; then
(1_G) * b in a" * (H * a) by GROUP_1:def 5; then
b in a" * (H * a) by GROUP_1:def 4; then
b in a" * H * a by GROUP_2:106;
hence o in the carrier of (H |^ a) by GROUP_3:59;
end;
hence H |^ a = the multMagma of H by B2,TARSKI:2,GROUP_2:59;
end;
hence H is normal by GROUP_3:def 13;
end;
theorem N3:
for G being Group
for H being strict Subgroup of G holds
H is normal iff for g being Element of G holds H |^ g = H
proof
let G be Group, H be strict Subgroup of G;
hereby assume A1: H is normal;
thus for g being Element of G holds H |^ g = H
proof
let a be Element of G;
A3: now let o be object;
assume o in the carrier of (H|^a); then
o in H |^ a; then
consider b being Element of G such that
A4: o = b |^ a & b in H by GROUP_3:58;
b |^ a in H by A4,A1,ThN1;
hence o in the carrier of H by A4;
end;
now let o be object;
assume A5: o in the carrier of H;
the carrier of H c= the carrier of G by GROUP_2:def 5; then
reconsider b = o as Element of G by A5;
b in H by A5; then
b |^ (a") in H by A1,ThN1; then
a"" * b * a" in H by GROUP_3:def 2; then
(a * b * a") * a in H * a by GROUP_2:104; then
(a * b) * (a" * a) in H * a by GROUP_1:def 3; then
(a * b) * (1_G) in H * a by GROUP_1:def 5; then
a * b in H * a by GROUP_1:def 4; then
a" * (a * b) in a" * (H * a) by GROUP_2:27; then
(a" * a) * b in a" * (H * a) by GROUP_1:def 3; then
(1_G) * b in a" * (H * a) by GROUP_1:def 5; then
b in a" * (H * a) by GROUP_1:def 4; then
b in a" * H * a by GROUP_2:106;
hence o in the carrier of (H |^ a) by GROUP_3:59;
end;
hence thesis by A3,TARSKI:2,GROUP_2:59;
end;
end;
assume B: for g being Element of G holds H |^ g = H;
now let g,h be Element of G;
assume h in H;
then h |^ g in H |^ g by GROUP_3:58;
hence h |^ g in H by B;
end;
hence H is normal by ThN1;
end;
theorem
for G being Group
for H being strict Subgroup of G holds
H is normal iff ex G1 being Group, f being Homomorphism of G,G1 st Ker f = H
proof
let G be Group, H be strict Subgroup of G;
hereby assume H is normal; then
reconsider N = H as normal Subgroup of G;
thus ex G1 being Group, f being Homomorphism of G,G1 st Ker f = H
proof
take G./.N, nat_hom N;
thus Ker nat_hom N = H by GROUP_6:43;
end;
end;
thus thesis;
end;
definition
let G,H be Group;
assume AS:H is Subgroup of G;
func Index(H,G) -> Cardinal means :di:
ex H1 being Subgroup of G st H1 = H & it = Index H1;
existence
proof
reconsider H1 = H as Subgroup of G by AS;
take Index H1;
thus thesis;
end;
uniqueness;
end;
definition
let G,H1,H2 be Group;
pred H1,H2 are_conjugated_in G means
ex H3,H4 being Subgroup of G st H3 = H1 & H4 = H2 & H3,H4 are_conjugated;
end;
lemT2:
for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut(E,F)
for f being Element of the carrier of Aut(E,F)
for f1 being Element of the carrier of Aut(E)
st f1 = f holds G |^ f = G |^ f1
proof
let F be Field, E be FieldExtension of F, G be Subgroup of Aut(E,F);
let f be Element of the carrier of Aut(E,F),
f1 be Element of the carrier of Aut(E);
assume AS: f1 = f;
H: G |^ f is Subgroup of Aut(E) by GROUP_2:56;
A: now let o be object;
assume o in the carrier of G |^ f; then
o in G |^ f; then
consider g being Element of Aut(E,F) such that
A1: o = g |^ f & g in G by GROUP_3:58;
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) by A1;
reconsider h = f as F-fixing Automorphism of E;
H3: [f",g] in [:the carrier of Aut(E,F),the carrier of Aut(E,F):];
H4: [f"*g,f] in [:the carrier of Aut(E,F),the carrier of Aut(E,F):];
A2: f" = h" by GALOIS_2:4 .= f1" by AS,GALOIS_2:2;
A3: f" * g
= ((the multF of Aut(E))||the carrier of Aut(E,F)).(f",g)
by GROUP_2:def 5
.= f1" * g1 by A2,H3,FUNCT_1:49;
f" * g * f
= ((the multF of Aut(E))||the carrier of Aut(E,F)).(f"*g,f)
by GROUP_2:def 5
.= f1" * g1 * f1 by A3,AS,H4,FUNCT_1:49;
then o = f1" * g1 * f1 by A1,GROUP_3:def 2
.= g1 |^ f1 by GROUP_3:def 2;
then o in G |^ f1 by A1,GROUP_3:58;
hence o in the carrier of G |^ f1;
end;
now let o be object;
assume o in the carrier of G |^ f1; then
o in G |^ f1; then
consider g1 being Element of Aut(E) such that
A1: o = g1 |^ f1 & g1 in G by GROUP_3:58;
the carrier of G c= the carrier of Aut(E,F) by GROUP_2:def 5; then
reconsider g = g1 as Element of the carrier of Aut(E,F) by A1;
reconsider h = f as F-fixing Automorphism of E;
H3: [f",g] in [:the carrier of Aut(E,F),the carrier of Aut(E,F):];
H4: [f"*g,f] in [:the carrier of Aut(E,F),the carrier of Aut(E,F):];
A2: f" = h" by GALOIS_2:4 .= f1" by AS,GALOIS_2:2;
A3: f" * g
= ((the multF of Aut(E))||the carrier of Aut(E,F)).(f",g)
by GROUP_2:def 5
.= f1" * g1 by A2,H3,FUNCT_1:49;
f" * g * f
= ((the multF of Aut(E))||the carrier of Aut(E,F)).(f"*g,f)
by GROUP_2:def 5
.= f1" * g1 * f1 by A3,AS,H4,FUNCT_1:49;
then o = f" * g * f by A1,GROUP_3:def 2
.= g |^ f by GROUP_3:def 2;
then o in G |^ f by A1,GROUP_3:58;
hence o in the carrier of G |^ f;
end;
hence thesis by H,A,TARSKI:2,GROUP_2:59;
end;
begin :: On Normal Extensions
definition
let F be Field;
let E be FieldExtension of F;
let h be Homomorphism of E;
let K be IntermediateField of E,F;
func rng(h,K) -> Subset of E equals
rng(h|the carrier of K);
coherence
proof
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
the carrier of K c= the carrier of E by EC_PF_1:def 1; then
reconsider f = h|(the carrier of K) as Function of K,E by FUNCT_2:32;
now let o be object;
assume o in rng(h|the carrier of K);
then o in rng f & rng f c= the carrier of E by RELAT_1:def 19;
hence o in the carrier of E;
end; then
rng(h|the carrier of K) c= the carrier of E;
hence thesis;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let h be Homomorphism of E;
let K be IntermediateField of E,F;
cluster rng(h,K) -> inducing_subfield;
coherence
proof
set f = h|(the carrier of K);
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
the carrier of K c= the carrier of E by EC_PF_1:def 1; then
reconsider f = h|(the carrier of K) as Function of K,E by FUNCT_2:32;
K in IntermediateFields(E,F) & id E is Homomorphism of E by GALOIS_0:def 5;
then V: K is Subfield of E & E is E-homomorphic by FIELD_14:4;
then U: f is additive multiplicative unity-preserving by RING_3:54,55,56;
set S = rng(h,K);
H: dom f = the carrier of K by FUNCT_2:def 1;
A: f.(0.K) = 0.E by U,RING_2:6;
B: now let a,b be Element of E;
assume C1: a in S & b in S; then
consider x being object such that
C2: x in dom f & a = f.x by FUNCT_1:def 3;
consider y being object such that
C3: y in dom f & b = f.y by C1,FUNCT_1:def 3;
reconsider x,y as Element of K by C2,C3;
a + b = f.(x+y) by U,C2,C3;
hence a + b in S by H,FUNCT_1:def 3;
a * b = f.(x*y) by U,C2,C3;
hence a * b in S by H,FUNCT_1:def 3;
-a = f.(-x) by U,C2,RING_2:7;
hence -a in S by H,FUNCT_1:def 3;
end;
now let a be non zero Element of E;
assume a in S; then
consider x being object such that
D1: x in dom f & a = f.x by FUNCT_1:def 3;
reconsider x as Element of K by D1;
D2: a <> 0.E & 0.E = 0.K by V,EC_PF_1:def 1;
D3: now assume x = 0.K;
then f.x = 0.E by U,RING_2:6;
hence contradiction by D1;
end;
f.(x") * f.x = f.(x"*x) by U .= 1.E by U,D3,VECTSP_1:def 10;
then a" = f.(x") by D1,D2,VECTSP_1:def 10;
hence a" in S by H,FUNCT_1:def 3;
end;
hence thesis by A,B,U,H,FUNCT_1:def 3;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let K be IntermediateField of E,F;
let h be Homomorphism of E;
func h.:K -> Subfield of E equals
InducedSubfield rng(h,K);
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
let f be F-fixing Automorphism of E;
let K be IntermediateField of E,F;
cluster f.:K -> F-extending;
coherence
proof
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
H1: F is Subfield of K & K is Subfield of E &
F is Subfield of E by FIELD_14:4,FIELD_4:7; then
H2: the carrier of F c= the carrier of K &
the carrier of K c= the carrier of E by EC_PF_1:def 1;
H3: the addF of f.:K = (the addF of E) || the carrier of f.:K &
the multF of f.:K = (the multF of E) || the carrier of f.:K
by EC_PF_1:def 1;
now let o be object;
assume o in the carrier of F; then
reconsider a = o as Element of F;
f.a = a by FIELD_8:def 2; then
H3: (f|(the carrier of K)).a = a by H2,FUNCT_1:49;
dom (f|the carrier of K)
= dom f /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by H2,XBOOLE_1:28; then
a in rng(f,K) by H2,H3,FUNCT_1:3;
hence o in the carrier of f.:K by FIELD_16:def 3;
end; then
A: the carrier of F c= the carrier of f.:K;
B: (the addF of f.:K) || the carrier of F
= (the addF of E) || the carrier of F by H3,A,ZFMISC_1:96,RELAT_1:74
.= the addF of F by H1,EC_PF_1:def 1;
C: (the multF of f.:K) || the carrier of F
= (the multF of E) || the carrier of F by H3,A,ZFMISC_1:96,RELAT_1:74
.= the multF of F by H1,EC_PF_1:def 1;
D: 1.F = 1.E by H1,EC_PF_1:def 1 .= 1.(f.:K) by EC_PF_1:def 1;
0.F = 0.E by H1,EC_PF_1:def 1 .= 0.(f.:K) by EC_PF_1:def 1; then
F is Subfield of f.:K by A,B,C,D,EC_PF_1:def 1;
hence thesis by FIELD_4:7;
end;
end;
theorem T4a:
for F being Field
for E being F-finite FieldExtension of F
for K being IntermediateField of E,F
for f being F-fixing Automorphism of E
st K is F-normal holds f|(the carrier of K) is F-fixing Automorphism of K
proof
let F be Field, E be F-finite FieldExtension of F;
let K be IntermediateField of E,F;
let f be F-fixing Automorphism of E;
assume A: K is F-normal;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
H: K is Subfield of E by FIELD_14:4; then
reconsider E1 = E as FieldExtension of K by FIELD_4:7;
set h = f|(the carrier of K);
A4: the carrier of K c= the carrier of E by H,EC_PF_1:def 1;
A3: dom h = dom f /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by A4,XBOOLE_1:28;
rng h c= the carrier of E by RELAT_1:def 19; then
reconsider h as Function of K,E by A3,FUNCT_2:2;
now let a,b be Element of K;
reconsider a1 = a, b1 = b as Element of E by A4;
K is Subring of E by H,FIELD_5:12; then
a1 + b1 = a + b by FIELD_6:15;
hence h.(a+b) = f.(a1+b1) by FUNCT_1:49
.= f.a1 + f.b1 by VECTSP_1:def 20
.= h.a + f.b1 by FUNCT_1:49
.= h.a + h.b by FUNCT_1:49;
end; then
B1: h is additive;
now let a,b be Element of K;
reconsider a1 = a, b1 = b as Element of E by A4;
K is Subring of E by H,FIELD_5:12; then
a1 * b1 = a * b by FIELD_6:16;
hence h.(a*b) = f.(a1*b1) by FUNCT_1:49
.= f.a1 * f.b1 by GROUP_6:def 6
.= h.a * f.b1 by FUNCT_1:49
.= h.a * h.b by FUNCT_1:49;
end; then
B2: h is multiplicative;
h.(1_K) = f.(1_K) by FUNCT_1:49
.= f.(1_E) by H,EC_PF_1:def 1
.= 1_E by GROUP_1:def 13; then
h is unity-preserving; then
reconsider h as Homomorphism of K,E1 by B1,B2;
B: 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;
reconsider a2 = a1 as Element of E by A4;
thus h.a = f.a2 by FUNCT_1:49 .= a by FIELD_8:def 2;
end; then
h is F-fixing; then
reconsider h as Automorphism of K by A,FIELD_13:56;
h is F-fixing by B;
hence thesis;
end;
theorem lemT5:
for F being Field
for E being F-finite FieldExtension of F
for K being IntermediateField of E,F st K is F-normal
for f1,f2 being F-fixing Automorphism of E holds
(f1 * f2)|(the carrier of K) = f1|(the carrier of K) * f2|(the carrier of K)
proof
let F be Field, E be F-finite FieldExtension of F,
K be IntermediateField of E,F;
assume AS: K is F-normal;
let f1,f2 be F-fixing Automorphism of E;
reconsider g1 = f1|(the carrier of K), g2 = f2|(the carrier of K),
g = (f1 * f2)|(the carrier of K)
as F-fixing Automorphism of K by AS,T4a;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
H3: the carrier of K c= the carrier of E by EC_PF_1:def 1;
H4: dom f2 = the carrier of E by FUNCT_2:def 1;
H5: dom g2 = dom f2 /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by H3,XBOOLE_1:28;
H6: dom g1 = dom f1 /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by H3,XBOOLE_1:28;
dom g = dom(f1 * f2) /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by H3,XBOOLE_1:28; then
B: for o being object st o in dom(g1 * g2) holds o in dom g;
A: now let o be object;
H: rng g2 c= the carrier of K by RELAT_1:def 19;
assume o in dom g;
then o in dom g2 & g2.o in rng g2 by H5,FUNCT_1:3;
hence o in dom(g1 * g2) by H,H6,FUNCT_1:11;
end;
now let o be object;
assume o in dom g; then
reconsider a = o as Element of K;
reconsider a1 = a as Element of E by H3;
thus g.o = (f1 * f2).a by FUNCT_1:49
.= f1.(f2.a1) by H4,FUNCT_1:13
.= f1.(g2.a) by FUNCT_1:49
.= g1.(g2.a) by FUNCT_1:49
.= (g1 * g2).o by H5,FUNCT_1:13;
end;
hence thesis by A,B,TARSKI:2;
end;
lemSubF:
for E being Field, F being Subfield of E
st the carrier of F = the carrier of E holds F == E
proof
let E be Field, F be Subfield of E;
assume A: the carrier of F = the carrier of E; then
B: the addF of F = (the addF of E) || the carrier of E &
the multF of F = (the multF of E) || the carrier of E
by EC_PF_1:def 1;
1.F = 1.E & 0.F = 0.E by EC_PF_1:def 1;
hence thesis by A,B;
end;
theorem T4x:
for F being Field
for E being F-finite FieldExtension of F
for K being IntermediateField of E,F st K is F-normal
for f being Element of the carrier of Aut(E,F) holds f.:K = K
proof
let F be Field, E be F-finite FieldExtension of F;
let K be IntermediateField of E,F;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
H: K is Subfield of E by FIELD_14:4;
assume A1: K is F-normal;
reconsider E1 = E as FieldExtension of K by H,FIELD_4:7;
now let f be Element of the carrier of Aut(E,F);
reconsider f1 = f as F-fixing Automorphism of E;
set h = f1|(the carrier of K);
reconsider h as F-fixing Automorphism of K by A1,T4a;
B: the carrier of K = rng h by FUNCT_2:def 3
.= the carrier of f1.:K by FIELD_16:def 3;
f1.:K is Subfield of K
proof
D: the addF of f1.:K
= (the addF of E) || the carrier of f1.:K by EC_PF_1:def 1
.= (the addF of K) || the carrier of f1.:K by B,H,EC_PF_1:def 1;
E: the multF of f1.:K
= (the multF of E) || the carrier of f1.:K by EC_PF_1:def 1
.= (the multF of K) || the carrier of f1.:K by B,H,EC_PF_1:def 1;
F: 1.f1.:K = 1.E by EC_PF_1:def 1 .= 1.K by H,EC_PF_1:def 1;
0.(f1.:K) = 0.E by EC_PF_1:def 1 .= 0.K by H,EC_PF_1:def 1;
hence thesis by B,D,E,F,EC_PF_1:def 1;
end;
then f1.:K == K by B,lemSubF;
hence f.:K = K;
end;
hence for f being Element of the carrier of Aut(E,F) holds f.:K = K;
end;
theorem
for F being Field
for E being F-finite FieldExtension of F
for K being IntermediateField of E,F st K is F-normal
holds Fix(K,Aut(K,F)) is Subfield of Fix(E,Aut(E,F))
proof
let F be Field, E be F-finite FieldExtension of F;
let K be IntermediateField of E,F;
assume AS: K is F-normal;
set G = Aut(K,F);
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
I: K is Subfield of E by FIELD_14:4; then
H: Fix(K,G) is Subfield of E by EC_PF_1:5;
set fG = Fixed_Elements(K,G), fE = Fixed_Elements(E,Aut(E,F));
J: fG = {a where a is Element of K :
for f being Function of K,K st f in G holds f.a = a} &
fE = {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 GALOIS_1:def 16;
K: Aut(K,F) = multMagma (# Auts(K,F), AutComp(K,F) #) by GALOIS_1:def 6;
now let o be object;
assume o in fG; then
consider a being Element of K such that
A: o = a & for f being Function of K,K st f in G holds f.a = a by J;
the carrier of K c= the carrier of E by I,EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
now let f be Function of E,E;
assume f in Aut(E,F); then
reconsider f1 = f as F-fixing Automorphism of E;
reconsider g = f1|(the carrier of K)
as F-fixing Automorphism of K by AS,T4a;
g in the set of all f where f is F-fixing Automorphism of K; then
B1: g in G by K,GALOIS_1:def 4;
thus f.a1 = g.a by FUNCT_1:49 .= a1 by A,B1;
end;
hence o in fE by A,J;
end; then
fG c= fE; then
the carrier of Fix(K,G) c= fE by GALOIS_1:def 17; then
C: the carrier of Fix(K,G) c= the carrier of Fix(E,Aut(E,F))
by GALOIS_1:def 17; then
C1: [:the carrier of Fix(K,G),the carrier of Fix(K,G):] c=
[:the carrier of Fix(E,Aut(E,F)),the carrier of Fix(E,Aut(E,F)):]
by ZFMISC_1:96;
D: the addF of Fix(K,G)
= (the addF of E) || the carrier of Fix(K,G) by H,EC_PF_1:def 1
.= ((the addF of E) || the carrier of Fix(E,Aut(E,F)))
|| the carrier of Fix(K,G) by C1,FUNCT_1:51
.= (the addF of Fix(E,Aut(E,F))) || the carrier of Fix(K,G)
by EC_PF_1:def 1;
E: the multF of Fix(K,G)
= (the multF of E) || the carrier of Fix(K,G) by H,EC_PF_1:def 1
.= ((the multF of E) || the carrier of Fix(E,Aut(E,F)))
|| the carrier of Fix(K,G) by C1,FUNCT_1:51
.= (the multF of Fix(E,Aut(E,F))) || the carrier of Fix(K,G)
by EC_PF_1:def 1;
F: 1.Fix(K,G) = 1.E by H,EC_PF_1:def 1 .= 1.Fix(E,Aut(E,F)) by EC_PF_1:def 1;
0.Fix(K,G) = 0.E by H,EC_PF_1:def 1 .= 0.Fix(E,Aut(E,F)) by EC_PF_1:def 1;
hence thesis by C,D,E,F,EC_PF_1:def 1;
end;
theorem Conj0:
for F being Field
for E being F-normal FieldExtension of F
for a being F-algebraic Element of E
st E == FAdj(F,{a}) holds E is SplittingField of MinPoly(a,F)
proof
let F being Field, E be F-normal FieldExtension of F;
let a be F-algebraic Element of E;
assume A: E == FAdj(F,{a});
set p = MinPoly(a,F);
Ext_eval(p,a) = 0.E by FIELD_6:52; then
H0: 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}; then
H1: a in Roots(E,p) by FIELD_4:def 4;
B: p splits_in E by H0,FIELD_4:def 3,FIELD_13:def 5;
now let L be FieldExtension of F;
assume B1: p splits_in L & L is Subfield of E; then
B2: E is L-extending by FIELD_4:7; then
Roots(E,p) = Roots(L,p) by B,B1,FIELD_8:29; then
reconsider a1 = a as F-algebraic Element of L by H1;
FAdj(F,{a1}) is Subfield of L; then
FAdj(F,{a}) is Subfield of L & E is Subfield of FAdj(F,{a})
by A,B2,FIELD_10:9;
hence L == E by B1,EC_PF_1:5;
end;
hence thesis by B,FIELD_8:def 1;
end;
theorem Conj1:
for F being Field
for E being F-finite GaloisExtension of F
for K1,K2 being IntermediateField of E,F
for h being Function of K1,K2 st h is F-fixing isomorphism
ex f being F-fixing Automorphism of E st f|K1 = h
proof
let F be Field, E be F-finite GaloisExtension of F;
let K1,K2 be IntermediateField of E,F, h be Function of K1,K2;
assume AS: h is F-fixing isomorphism;
consider a being Element of E such that
A: E == FAdj(F,{a}) by FIELD_14:def 7;
set p = MinPoly(a,F);
K1 in IntermediateFields(E,F) by GALOIS_0:def 5; then
H3: F is Subfield of K1 & K1 is Subfield of E by FIELD_14:4; then
reconsider E1 = E as F-finite F-extending FieldExtension of K1
by FIELD_4:7;
the carrier of Polynom-Ring F c=
the carrier of Polynom-Ring K1 by FIELD_4:10; then
reconsider p1 = p as Element of the carrier of Polynom-Ring K1;
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 K1
by RING_4:def 4;
E is SplittingField of p & E is K1-extending by H3,FIELD_4:7,A,Conj0; then
reconsider L = E as SplittingField of p1 by FIELD_8:53;
reconsider K3 = K2 as K1-isomorphic K1-homomorphic Field
by AS,RING_3:def 4,RING_2:def 4;
reconsider h1 = h as Isomorphism of K1,K3 by AS;
E: (PolyHom h1).p1 = p1
proof
now let i be Element of NAT;
thus ((PolyHom h1).p1).i = h1.(p.i) by FIELD_1:def 2 .= p1.i by AS;
end;
hence thesis;
end;
L is SplittingField of (PolyHom h1).p1
proof
K2 in IntermediateFields(E,F) by GALOIS_0:def 5; then
K2 is Subfield of E by FIELD_14:4; then
reconsider L2 = L as F-extending FieldExtension of K2 by FIELD_4:7;
reconsider q = (PolyHom h1).p1 as
non constant Element of the carrier of Polynom-Ring K2;
E is SplittingField of p by A,Conj0; then
p splits_in L by FIELD_8:def 1; then
consider x being non zero Element of L, r being Ppoly of L such that
H5: q = x * r by E,FIELD_4:def 5;
E0: q splits_in L by H5,FIELD_4:def 5;
now let L1 be FieldExtension of K2;
assume E1: q splits_in L1 & L1 is Subfield of L2; then
L is L1-extending by FIELD_4:7; then
E3: Roots(L1,q) = Roots(L2,q) by E0,E1,FIELD_8:29;
a in Roots(L2,q)
proof
Ext_eval(p,a) = 0.E by FIELD_6:52; then
consider x being Element of E such that
E6: x = a & x is_a_root_of p,E by FIELD_4:def 2;
reconsider y = x as Element of L2;
0.E = Ext_eval(p,x) by E6,FIELD_4:def 2
.= Ext_eval(q,y) by E,FIELD_7:15; then
y is_a_root_of q,L2 by FIELD_4:def 2; then
y in {a where a is Element of L2 : a is_a_root_of q,L2};
hence a in Roots(L2,q) by E6,FIELD_4:def 4;
end; then
reconsider a1 = a as K2-algebraic Element of L1 by E3;
FAdj(K2,{a1}) == E
proof
reconsider K3 = K2 as F-finite FieldExtension of F;
K2 in IntermediateFields(E,F) by GALOIS_0:def 5; then
H: F is Subfield of K2 & K2 is Subfield of E by FIELD_14:4; then
reconsider E2 = E as F-finite F-extending FieldExtension of K3
by FIELD_4:7;
reconsider a2 = a1 as Element of E2;
E2 is K3-finite by FIELD_7:31; then
reconsider a2 as K3-algebraic Element of E2;
J: FAdj(K2,{a1}) is Subfield of E by E1,EC_PF_1:5;
K2 is Subfield of FAdj(K2,{a1}) by FIELD_6:36; then
K: F is Subfield of FAdj(K2,{a1}) by H,EC_PF_1:5;
{a2} is Subset of FAdj(K2,{a1}) by FIELD_6:35; then
FAdj(F,{a2}) is Subfield of FAdj(K2,{a1}) &
E is Subfield of FAdj(F,{a2}) by A,J,K,FIELD_6:37;
hence thesis by E1,EC_PF_1:5;
end;
hence L1 == L2 by E1,EC_PF_1:5;
end;
hence thesis by H5,FIELD_4:def 5,FIELD_8:def 1;
end; then
consider f being Function of L,L such that
F: f is h1-extending isomorphism by FIELD_8:57;
now let x being Element of F;
the carrier of F c= the carrier of K1 by H3,EC_PF_1:def 1; then
reconsider y = x as Element of K1;
thus f.x = h1.y by F .= x by AS;
end; then
reconsider f as F-fixing Automorphism of E by F,FIELD_8:def 2;
take f;
thus f|K1 = h by F,FIELD_8:40;
end;
theorem T7:
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F
for f being Element of the carrier of Aut E
holds Aut(E,f.:K) |^ f = Aut(E,K) & Aut(E,K) |^ f" = Aut(E,f.:K)
proof
let F be Field, E be FieldExtension of F,
K be IntermediateField of E,F, f be Element of the carrier of Aut E;
reconsider E1 = E as FieldExtension of f.:K by FIELD_4:7;
H1: Aut(E,f.:K) = Aut(FieldExt(E,f.:K),f.:K) by GALOIS_1:def 7 .= Aut(E1,f.:K);
H2: Aut(E1,f.:K) = multMagma(# Auts(E1,f.:K), AutComp(E1,f.:K) #) &
Aut(FieldExt(E,K),K) = multMagma(# Auts(FieldExt(E,K),K),
AutComp(FieldExt(E,K),K) #) by GALOIS_1:def 6;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
H3: the carrier of K c= the carrier of E by EC_PF_1:def 1;
H4: Aut(E,K) = Aut(FieldExt(E,K),K) by GALOIS_1:def 8;
H5: the carrier of Aut(E,K) c= the carrier of Aut(E) by GROUP_2:def 5;
reconsider f1 = f as Automorphism of E;
A: now let o be object;
assume o in the carrier of Aut(E,K) |^ f"; then
o in Aut(E,K) |^ f"; then
consider g being Element of the carrier of Aut(E) such that
A1: o = g |^ f" & g in Aut(E,K) by GROUP_3:58;
reconsider g1 = g as K-fixing Automorphism of FieldExt(E,K) by A1,H4;
A2: o = f1 * g1 * f1"
proof
B: f1" = f" by GALOIS_2:2; then
f1"" = f"" by GALOIS_2:2; then
f1"" * g1 = f"" * g by GALOIS_2:1; then
f1"" * g1 * f1" = f"" * g * f" by B,GALOIS_2:1; then
f1 * g1 * f1" = f"" * g * f" by FUNCT_1:43;
hence thesis by A1,GROUP_3:def 2;
end;
reconsider h = f1 * g1 * f1" as Automorphism of E1;
now let a be Element of f.:K;
a in the carrier of f.:K; then
a in rng(f1,K) by FIELD_16:def 3; then
consider x being object such that
A3: x in dom(f|(the carrier of K)) & (f|(the carrier of K)).x = a
by FUNCT_1:def 3;
dom(f|(the carrier of K))
= dom f /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by H3,XBOOLE_1:28; then
reconsider x as Element of K by A3;
A5: f1.x = a by A3,FUNCT_1:49;
A7: dom(f1") = the carrier of E & dom g1 = the carrier of E &
dom f1 = the carrier of E by FUNCT_2:def 1; then
x in dom f1 by H3; then
A6: f1".a = x by A5,FUNCT_1:34;
A8: the carrier of f.:K c= the carrier of E by EC_PF_1:def 1;
thus (f1 * g1 * f1").a
= (f1 * g1).x by A6,A7,A8,FUNCT_1:13
.= f1.(g1.x) by A7,A3,FUNCT_1:13
.= a by A5,FIELD_8:def 2;
end; then
h is (f.:K)-fixing; then
o in the set of all h where
h is (f.:K)-fixing Automorphism of E1 by A2;
hence o in the carrier of Aut(E,f.:K) by H1,H2,GALOIS_1:def 4;
end;
now let o be object;
assume o in the carrier of Aut(E,f.:K); then
o in the set of all h where
h is (f.:K)-fixing Automorphism of E1 by H1,H2,GALOIS_1:def 4;
then consider g1 being (f.:K)-fixing Automorphism of E1 such that
B0: o = g1;
reconsider h1 = f1" * g1 * f1 as Automorphism of FieldExt(E,K);
B2: dom(f1") = the carrier of E & dom g1 = the carrier of E &
dom f1 = the carrier of E by FUNCT_2:def 1;
now let a be Element of K;
dom(f|(the carrier of K))
= dom f /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by H3,XBOOLE_1:28; then
(f1|(the carrier of K)).a in rng(f1|(the carrier of K)) by FUNCT_1:3;
then f1.a in rng(f,K) by FUNCT_1:49; then
B1: f1.a in f.:K by FIELD_16:def 3;
B3: rng f1 c= the carrier of E &
a in dom f1 by B2,H3,RELAT_1:def 19; then
B4: f1.a in the carrier of E by FUNCT_1:3;
thus (f1" * g1 * f1).a
= (f1" * g1).(f1.a) by H3,B2,FUNCT_1:13
.= (f1").(g1.(f1.a)) by B4,B2,FUNCT_1:13
.= (f1").(f1.a) by B1,FIELD_8:def 2
.= a by B3,FUNCT_1:34;
end; then
h1 is K-fixing; then
h1 in the set of all h where
h is K-fixing Automorphism of FieldExt(E,K); then
h1 in Auts(FieldExt(E,K),K) by GALOIS_1:def 4; then
C: h1 in Aut(E,K) by H2,GALOIS_1:def 8; then
reconsider h = h1 as Element of Aut(E) by H5;
D: f1"" * h1 * f1" = f"" * h * f"
proof
B: f1" = f" by GALOIS_2:2; then
f1"" = f"" by GALOIS_2:2; then
f1"" * h1 = f"" * h by GALOIS_2:1;
hence f1"" * h1 * f1" = f"" *h * f" by B,GALOIS_2:1;
end;
E: rng(f1) = the carrier of E by FUNCT_2:def 3;
f1"" * h1 * f1"
= f1 * (f1" * g1 * f1) * f1" by FUNCT_1:43
.= (f1 * (f1" * (g1 * f1))) * f1" by RELAT_1:36
.= ((f1 * f1") * (g1 * f1)) * f1" by RELAT_1:36
.= ((id E) * (g1 * f1)) * f1" by E,FUNCT_2:29
.= (g1 * f1) * f1" by FUNCT_2:17
.= g1 * (f1 * f1") by RELAT_1:36
.= g1 * (id E) by E,FUNCT_2:29
.= g1 by FUNCT_2:17; then
g1 = h |^ f" by D,GROUP_3:def 2;
then g1 in Aut(E,K) |^ f" by C,GROUP_3:58;
hence o in the carrier of Aut(E,K) |^ f" by B0;
end; then
Aut(E,K) |^ f" = Aut(E,f.:K) by A,TARSKI:2,GROUP_2:59;
hence thesis by GROUP_3:62;
end;
theorem Conj2:
for F being Field
for E being FieldExtension of F
for H being Subgroup of Aut(E,F)
for f being Element of the carrier of Aut(E,F) holds f.:Fix(E,H) = Fix(E,H|^f")
proof
let F be Field, E be FieldExtension of F;
let H be Subgroup of Aut(E,F), f be Element of the carrier of Aut(E,F);
reconsider G = H |^ (f"), H1 = H as Subgroup of Aut(E) by GROUP_2:56;
A: the carrier of Fix(E,G) = Fixed_Elements(E,G) by GALOIS_1:def 17
.= {a where a is Element of E :
for f being Function of E,E st f in G holds f.a = a}
by GALOIS_1:def 16;
B: the carrier of f.:Fix(E,H) = rng(f,Fix(E,H)) by FIELD_16:def 3;
reconsider f1 = f as F-fixing Automorphism of E;
H1: dom f1 = the carrier of E &
rng f1 = the carrier of E by FUNCT_2:def 1,FUNCT_2:def 3;
C: now let o be object;
assume o in the carrier of Fix(E,G); then
consider a being Element of E such that
C1: o = a & for g being Function of E,E st g in G holds g.a = a by A;
set b = (f1").a;
now let g be Function of E,E;
assume D1: g in H;
the carrier of H c= the carrier of Aut(E,F) by GROUP_2:def 5; then
reconsider g1 = g as Element of Aut(E,F) by D1;
g1 |^ (f") in G by D1,GROUP_3:58; then
D2: (f"")*g1*(f") in G by GROUP_3:def 2;
f*g1 = f1*g & f" = f1" by GALOIS_2:3,4; then
f*g1*(f") = f1*g*(f1") by GALOIS_2:3; then
D3: (f1*g*(f1")).a = a by D2,C1;
D4: dom(f1") = the carrier of E &
dom(g*(f1")) = the carrier of E by FUNCT_2:def 1;
thus g.b
= (id the carrier of E).(g.((f1").a))
.= ((f1")*f1).(g.((f1").a)) by FUNCT_2:61
.= (f1").(f1.(g.((f1").a))) by H1,FUNCT_1:13
.= (f1").(f1.((g*(f1")).a)) by D4,FUNCT_1:13
.= (f1").((f1*(g*(f1"))).a) by D4,FUNCT_1:13
.= b by D3,RELAT_1:36;
end; then
b in {a where a is Element of E :
for f being Function of E,E st f in H holds f.a = a}; then
b in Fixed_El(E,H1) by GALOIS_1:def 16; then
C2: b in the carrier of Fix(E,H) by GALOIS_1:def 17; then
b in (dom f) /\ (the carrier of Fix(E,H)) by H1,XBOOLE_0:def 4; then
C3: b in dom(f|the carrier of Fix(E,H)) by RELAT_1:61;
(f|the carrier of Fix(E,H)).b
= f.b by C2,FUNCT_1:49 .= a by H1,FUNCT_1:35;
hence o in the carrier of f.:Fix(E,H) by B,C1,C3,FUNCT_1:def 3;
end;
now let o be object;
set h = f|the carrier of Fix(E,H);
Fix(E,H1) is Subfield of E; then
H0: the carrier of Fix(E,H) c= the carrier of E by EC_PF_1:def 1;
dom f = the carrier of E by FUNCT_2:def 1; then
(dom f) /\ (the carrier of Fix(E,H)) = the carrier of Fix(E,H)
by H0,XBOOLE_1:28; then
H1: dom h = the carrier of Fix(E,H) by RELAT_1:61;
assume o in the carrier of f.:Fix(E,H); then
D0: o in rng(f,Fix(E,H)) by FIELD_16:def 3;
consider y being object such that
D1: y in dom h & h.y = o by D0,FUNCT_1:def 3;
reconsider a = y, b = o as Element of E by D1,D0;
D2: now let g be Function of E,E;
a in Fixed_El(E,H1) by D1,H1,GALOIS_1:def 17; then
a in {a where a is Element of E :
for f being Function of E,E st f in H holds f.a = a}
by GALOIS_1:def 16; then
consider a1 being Element of E such that
D3: a1 = a & for f being Function of E,E st f in H holds f.a1 = a1;
assume g in H;
hence g.a = a by D3;
end;
now let g be Function of E,E;
assume g in G; then
consider g1 being Element of the carrier of Aut(E,F) such that
D3: g = g1|^(f") & g1 in H by GROUP_3:58;
D4: g = (f"") * g1 * (f") by D3,GROUP_3:def 2;
f * g1 = f1 * g1 & f" = f1" by GALOIS_2:3,4; then
D5: f * g1 * (f") = f1 * g1 * (f1") by GALOIS_2:3;
D6: dom f = the carrier of E &
dom g1 = the carrier of E &
dom(f1") = the carrier of E by FUNCT_2:def 1;
thus g.b
= (f1 * g1 * (f1")).(f.a) by D5,D4,D1,H1,FUNCT_1:49
.= (f1 * g1).((f1").(f.a)) by D6,FUNCT_1:13
.= (f1 * g1).a by D6,FUNCT_1:34
.= f1.(g1.a) by D6,FUNCT_1:13
.= f1.a by D2,D3
.= b by D1,H1,FUNCT_1:49;
end; then
b in {a where a is Element of E :
for f being Function of E,E st f in G holds f.a = a}; then
b in Fixed_El(E,G) by GALOIS_1:def 16;
hence o in the carrier of Fix(E,G) by GALOIS_1:def 17;
end;
hence thesis by C,TARSKI:2,EC_PF_1:8;
end;
begin :: The Theorem
theorem
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds (Psi E).K = Aut(E,K)
by GALOIS_3:def 14;
theorem
for F being Field
for E being FieldExtension of F
for G being SubGroup of Aut(E,F) holds (Phi E).G = Fix(E,G)
by GALOIS_3:def 15;
mainA:
for S,T being non empty RelStr
for g being Function of S,T, d being Function of T,S holds
g|(Closed d) is Function of (Closed d),(Closed g) &
d|(Closed g) is Function of (Closed g),(Closed d)
proof
let S,T be non empty RelStr, g be Function of S,T, d be Function of T,S;
reconsider g1 = g|(Closed d) as Function of (Closed d),the carrier of T
by FUNCT_2:32;
D: dom g1 = Closed d by FUNCT_2:def 1;
now let o be object;
assume o in rng g1; then
consider x being object such that
D1: x in dom g1 & g1.x = o by FUNCT_1:def 3;
reconsider x as Element of S by D,D1;
g.x = g1.x by D1,FUNCT_1:49;
hence o in Closed g by D1;
end; then
rng g1 c= Closed g; then
reconsider g1 as Function of (Closed d),(Closed g) by D,FUNCT_2:2;
g1 = g|(Closed d);
hence g|(Closed d) is Function of (Closed d),(Closed g);
reconsider d1 = d|(Closed g) as Function of (Closed g),the carrier of S
by FUNCT_2:32;
E: dom d1 = Closed g by FUNCT_2:def 1;
rng d1 c= Closed d
proof let o be object;
assume o in rng d1; then
consider x being object such that
E1: x in dom d1 & d1.x = o by FUNCT_1:def 3;
reconsider x as Element of T by E,E1;
d.x = d1.x by E1,FUNCT_1:49;
hence o in Closed d by E1;
end; then
reconsider d1 as Function of (Closed g),(Closed d) by E,FUNCT_2:2;
d1 = d|(Closed g);
hence d|(Closed g) is Function of (Closed g),(Closed d);
end;
lemCl:
for S,T being non empty Poset
for g being Function of S,T, d being Function of T,S
st [g,d] is co-Galois holds
Restr(g,d) is bijective & Restr(d,g) is bijective
proof
let S,T be non empty Poset, g be Function of S,T, d be Function of T,S;
assume [g,d] is co-Galois; then
consider f1 being Function of S,T,
f2 being Function of T,S such that
A: [f1,f2] = [g,d] & f1 is antitone & f2 is antitone &
for p1,p2 being Element of S, r1,r2 being Element of T
holds p1 <= f2.(f1.p1) & r1 <= f1.(f2.r1) by CONLAT_1:def 7;
B: f1 = [g,d]`1 by A .= g;
C: f2 = [g,d]`2 by A .= d;
reconsider g1 = g|(Closed d) as Function of (Closed d),(Closed g)
by mainA;
reconsider d1 = d|(Closed g) as Function of (Closed g),(Closed d)
by mainA;
K: now let s be Element of S;
now assume s in Closed d; then
consider t being Element of T such that F1: s = d.t;
F2: s <= d.(g.s) by A,B,C;
d.(g.(d.t)) <= d.t by A,B,C,WAYBEL_0:def 5;
hence d.(g.s) = s by F1,F2,ORDERS_2:2;
end;
hence s in Closed d iff d.(g.s) = s;
end;
E: now let t be Element of T;
now assume t in Closed g; then
consider s being Element of S such that F1: t = g.s;
F2: t <= g.(d.t) by A,B,C;
g.(d.(g.s)) <= g.s by A,B,C,WAYBEL_0:def 5;
hence g.(d.t) = t by F1,F2,ORDERS_2:2;
end;
hence t in Closed g iff g.(d.t) = t;
end;
now let o be object;
assume E1: o in Closed g; then
reconsider t = o as Element of T;
E2: d1.t = d.t by E1,FUNCT_1:49;
dom d1 = Closed g by FUNCT_2:def 1; then
E3: d1.t in rng d1 & rng d1 c= Closed d by E1,FUNCT_1:3,RELAT_1:def 19;
thus (g1 * d1).o
= g1.(d1.t) by E1,FUNCT_2:15
.= g.(d.t) by E2,E3,FUNCT_1:49
.= t by E1,E
.= (id (Closed g)).o by E1,FUNCT_1:18;
end; then
G1: g1 * d1 = id(Closed g);
now let o be object;
assume E1: o in Closed d; then
reconsider s = o as Element of S;
E2: g1.s = g.s by E1,FUNCT_1:49;
dom g1 = Closed d by FUNCT_2:def 1; then
E3: g1.s in rng g1 & rng g1 c= Closed g by E1,FUNCT_1:3,RELAT_1:def 19;
thus (d1 * g1).o
= d1.(g1.s) by E1,FUNCT_2:15
.= d.(g.s) by E2,E3,FUNCT_1:49
.= s by E1,K
.= (id (Closed d)).o by E1,FUNCT_1:18;
end; then
d1 * g1 = id(Closed d);
hence thesis by G1,FUNCT_2:23;
end;
theorem BIJ1:
for F being Field
for E being F-finite GaloisExtension of F
holds Psi E is a_Bijection of IntermediateFields(E,F), Subgroups Aut(E,F)
proof
let F be Field, E be F-finite GaloisExtension of F;
set f = Restr(Psi E,Phi E);
GalCon E is co-Galois; then
A: f is bijective by lemCl;
F: ClosedFields E = IntermediateFields(E,F) by GALOIS_3:27;
C: ClosedGroups E = Subgroups Aut(E,F) by GALOIS_3:37;
set P = LattPOSet(IntermediateFields E), L = IntermediateFields E;
L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
P = RelStr(#the carrier of L,LattRel L#) by LATTICE3:def 2;
hence thesis by F,C,A,GALOIS_0:def 2;
end;
theorem BIJ:
for F being Field
for E being F-finite GaloisExtension of F
holds Phi E is a_Bijection of Subgroups Aut(E,F), IntermediateFields(E,F)
proof
let F be Field, E be F-finite GaloisExtension of F;
set f = Restr(Phi E,Psi E);
GalCon E is co-Galois; then
A: f is bijective by lemCl;
F: ClosedGroups E = Subgroups Aut(E,F) by GALOIS_3:37;
C: ClosedFields E = IntermediateFields(E,F) by GALOIS_3:27;
set L2 = LattPOSet(SubgroupsAut E), L4 = SubgroupsAut E;
L4 = LattStr(#Subgroups Aut(E,F),SubJoin Aut(E,F),SubMeet Aut(E,F)#) &
L2 = RelStr(#the carrier of L4,LattRel L4#)
by LATTICE3:def 2,GROUP_4:def 12;
hence thesis by F,A,C,GALOIS_0:def 2;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
holds (Psi E)" = Phi E & (Phi E)" = Psi E
proof
let F be Field, E be F-finite GaloisExtension of F;
F: ClosedFields E = IntermediateFields(E,F) by GALOIS_3:27;
GalCon E is co-Galois; then
C: (Restr(Psi E,Phi E))" = Restr(Phi E,Psi E) by GALOIS_0:2;
set P = LattPOSet(IntermediateFields E), L = IntermediateFields E;
D: L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
P = RelStr(#the carrier of L,LattRel L#) by LATTICE3:def 2; then
B: Restr(Psi E,Phi E) = Psi E by F;
G: ClosedGroups E = Subgroups Aut(E,F) by GALOIS_3:37;
set L2 = LattPOSet(SubgroupsAut E), L4 = SubgroupsAut E;
E: L4 = LattStr(#Subgroups Aut(E,F),SubJoin Aut(E,F),SubMeet Aut(E,F)#) &
L2 = RelStr(#the carrier of L4,LattRel L4#)
by LATTICE3:def 2,GROUP_4:def 12;
hence (Psi E)" = Phi E by D,C,F,G;
H: Restr(Phi E,Psi E) = Phi E by E,G;
GalCon E is co-Galois;
hence thesis by B,H,GALOIS_0:3;
end;
registration
let F be Field;
let E be F-finite GaloisExtension of F;
cluster IntermediateFields(E,F) -> (Subgroups Aut(E,F))-bijective;
coherence
proof
ClosedGroups E = Subgroups Aut(E,F) by GALOIS_3:37;
hence thesis by GALOIS_3:27;
end;
cluster Subgroups Aut(E,F) -> IntermediateFields(E,F)-bijective;
coherence
proof
ClosedFields E = IntermediateFields(E,F) by GALOIS_3:27;
hence thesis by GALOIS_3:37;
end;
end;
theorem G1:
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F holds K = Fix(E,Aut(E,K))
proof
let F be Field, E be F-finite GaloisExtension of F;
let K be IntermediateField of E,F;
ClosedFields E = IntermediateFields(E,F) by GALOIS_3:27;
hence thesis by GALOIS_3:22,GALOIS_0:def 5;
end;
theorem G2:
for F being Field
for E being F-finite GaloisExtension of F
for G being SubGroup of Aut(E,F) holds G = Aut(E,Fix(E,G))
proof
let F be Field, E be F-finite GaloisExtension of F;
let G being SubGroup of Aut(E,F);
ClosedGroups E = Subgroups Aut(E,F) by GALOIS_3:37;
then G in ClosedGroups E by GROUP_3:def 1;
hence thesis by GALOIS_3:24;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for K1,K2 being IntermediateField of E,F
holds K1 is Subfield of K2 iff Aut(E,K2) is Subgroup of Aut(E,K1)
proof
let F be Field, E be F-finite GaloisExtension of F,
K1,K2 be IntermediateField of E,F;
set L = IntermediateFields E, P = LattPOSet(IntermediateFields E);
M: L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
P = RelStr(#the carrier of L,LattRel L#) by LATTICE3:def 2;
reconsider K3 = K1, K4 = K2 as
Element of the carrier of LattPOSet(IntermediateFields E)
by M,GALOIS_0:def 5;
set L = SubgroupsAut E, G = Aut(E,F), R = LattPOSet(SubgroupsAut E);
M: L = LattStr(# Subgroups G, SubJoin G, SubMeet G #) &
R = RelStr(#the carrier of L,LattRel L#) by GROUP_4:def 12,LATTICE3:def 2;
Aut(E,K1) is Subgroup of Aut(E,F) &
Aut(E,K2) is Subgroup of Aut(E,F) by GALOIS_1:18; then
reconsider G1 = Aut(E,K1), G2 = Aut(E,K2) as
Element of the carrier of LattPOSet(SubgroupsAut E) by M,GROUP_3:def 1;
N: Aut(E,K1) is Subgroup of Aut(E,F) by GALOIS_1:18; then
Aut(E,K1) in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G3 = Aut(E,K1) as SubGroup of Aut(E,F) by N,GALOIS_0:def 10;
N: Aut(E,K2) is Subgroup of Aut(E,F) by GALOIS_1:18; then
Aut(E,K2) in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G4 = Aut(E,K2) as SubGroup of Aut(E,F) by N,GALOIS_0:def 10;
H1: (Psi E).K3 = G1 & (Psi E).K4 = G2 by GALOIS_3:def 14;
H2: (Phi E).G3 = Fix(E,G3) by GALOIS_3:def 15 .= K1 by G1;
H3: (Phi E).G4 = Fix(E,G4) by GALOIS_3:def 15 .= K2 by G1;
A: now assume K1 is Subfield of K2;
then K3 <= K4 by GALOIS_0:32;
hence Aut(E,K2) is Subgroup of Aut(E,K1) by H1,GALOIS_0:15,WAYBEL_0:def 5;
end;
now assume Aut(E,K2) is Subgroup of Aut(E,K1);
then (Phi E).G2 >= (Phi E).G1 by GALOIS_0:15,WAYBEL_0:def 5;
hence K1 is Subfield of K2 by H2,H3,GALOIS_0:32;
end;
hence thesis by A;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for G1,G2 being SubGroup of Aut(E,F)
holds G1 is Subgroup of G2 iff Fix(E,G2) is Subfield of Fix(E,G1)
proof
let F be Field, E be F-finite GaloisExtension of F,
G1,G2 be SubGroup of Aut(E,F);
set L = IntermediateFields E, P = LattPOSet(IntermediateFields E);
M: L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
P = RelStr(#the carrier of L,LattRel L#) by LATTICE3:def 2;
reconsider H1 = G1, H2 = G2 as Subgroup of Aut(E,F);
reconsider K1 = Fix(E,G1), K2 = Fix(E,G2) as
Element of the carrier of LattPOSet(IntermediateFields E)
by M,GALOIS_0:def 5;
reconsider K3 = K1, K4 = K2 as IntermediateField of E,F;
set L = SubgroupsAut E, G = Aut(E,F), R = LattPOSet(SubgroupsAut E);
M: L = LattStr(# Subgroups G, SubJoin G, SubMeet G #) &
R = RelStr(#the carrier of L,LattRel L#) by GROUP_4:def 12,LATTICE3:def 2;
reconsider G3 = G1, G4 = G2 as
Element of the carrier of LattPOSet(SubgroupsAut E)
by M,GROUP_3:def 1;
H1: (Phi E).G3 = K1 & (Phi E).G4 = K2 by GALOIS_3:def 15;
H2: (Psi E).K1 = Aut(E,Fix(E,G1)) by GALOIS_3:def 14 .= G1 by G2;
H3: (Psi E).K2 = Aut(E,Fix(E,G2)) by GALOIS_3:def 14 .= G2 by G2;
A: now assume G1 is Subgroup of G2;
then G3 <= G4 by GALOIS_0:15;
hence Fix(E,G2) is Subfield of Fix(E,G1) by H1,GALOIS_0:32,WAYBEL_0:def 5;
end;
now assume Fix(E,G2) is Subfield of Fix(E,G1);
then K2 <= K1 by GALOIS_0:32;
hence G1 is Subgroup of G2 by H2,H3,GALOIS_0:15,WAYBEL_0:def 5;
end;
hence thesis by A;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F
holds deg(E,K) = order Aut(E,K) & deg(K,F) = Index(Aut(E,K),Aut(E,F))
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
K is Subfield of E by FIELD_14:4; then
reconsider E1 = E as FieldExtension of K by FIELD_4:7;
reconsider E1 as K-finite FieldExtension of K by FIELD_7:31;
reconsider E1 as K-finite GaloisExtension of K by GALOIS_2:35;
Aut(E,K) = Aut(FieldExt(E,K),K) by GALOIS_1:def 8 .= Aut(E1,K);
hence B: deg(E,K) = order Aut(E,K) by GALOIS_3:33;
reconsider G = Aut(E,K) as finite Subgroup of Aut(E,F) by GALOIS_1:18;
deg(E,K) * deg(K,F)
= deg(E,F) by FIELD_7:30
.= card Aut(E,F) by GALOIS_3:33
.= deg(E,K) * index G by B,GROUP_2:147;
hence deg(K,F) = index G by XCMPLX_1:5
.= card(Left_Cosets G) by GROUP_2:def 18
.= Index G by GROUP_2:145
.= Index(Aut(E,K),Aut(E,F)) by di;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for K1,K2 being IntermediateField of E,F holds
K1,K2 are_isomorphic_over F iff Aut(E,K1),Aut(E,K2) are_conjugated_in Aut(E,F)
proof
let F be Field, E be F-finite GaloisExtension of F;
let K1,K2 be IntermediateField of E,F;
reconsider H1 = Aut(E,K1),
H2 = Aut(E,K2) as Subgroup of Aut(E,F) by GALOIS_1:18;
H1 in Subgroups Aut(E,F) & H2 in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider H1,H2 as SubGroup of Aut(E,F) by GALOIS_0:def 10;
H1: Aut(E,F) = multMagma(#Auts(E,F),AutComp(E,F)#) by GALOIS_1:def 6;
set L1 = FieldExt(E,K1), L2 = FieldExt(E,K2);
H2: Aut(E,K1) = Aut(L1,K1) by GALOIS_1:def 8
.= multMagma(#Auts(L1,K1),AutComp(L1,K1)#) by GALOIS_1:def 6;
H3: Aut(E,K2) = Aut(L2,K2) by GALOIS_1:def 8
.= multMagma(#Auts(L2,K2),AutComp(L2,K2)#) by GALOIS_1:def 6;
A: now assume K1,K2 are_isomorphic_over F; then
consider h being Function of K1,K2 such that
A1: h is F-isomorphism;
consider f1 being F-fixing Automorphism of E such that
A2: f1|K1 = h by A1,Conj1;
f1 in the set of all f where f is F-fixing Automorphism of E; then
reconsider f = f1 as Element of the carrier of Aut(E,F)
by H1,GALOIS_1:def 4;
A3: now let o be object;
assume o in the carrier of H2; then
reconsider g = o as Element of H2;
the carrier of H2 c= the carrier of Aut(E,F) by GROUP_2:def 5; then
reconsider g1 = g as Element of the carrier of Aut(E,F);
set t = (f") * g1 * f;
f * t = f * ((f") * (g1 * f)) by GROUP_1:def 3
.= (f * (f")) * (g1 * f) by GROUP_1:def 3
.= (1_Aut(E,F)) * (g1 * f) by GROUP_1:def 5
.= g1 * f by GROUP_1:def 4; then
(f * t) * (f")
= g1 * (f * (f")) by GROUP_1:def 3
.= g1 * (1_Aut(E,F)) by GROUP_1:def 5; then
B1: g1 = (f"") * t * (f") by GROUP_1:def 4
.= t |^ (f") by GROUP_3:def 2;
f1" = f" by GALOIS_2:4; then
(f1") * g1 = (f") * g1 by GALOIS_2:3; then
B2: (f1") * g1 * f1 = t by GALOIS_2:3; then
reconsider t1 = t as Automorphism of L1;
now let a be Element of K1;
K1 in IntermediateFields(E,F) by GALOIS_0:def 5; then
K1 is Subfield of E by FIELD_14:4; then
the carrier of K1 c= the carrier of E by EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
h = f1|(the carrier of K1) by A2,MATRLIN2:def 1; then
B5: h.a1 = f1.a1 by FUNCT_1:49;
dom h = the carrier of K1 by FUNCT_2:def 1; then
B6: h.a in rng h &
rng h c= the carrier of K2 by FUNCT_1:3,RELAT_1:def 19;
B7: dom f1 = the carrier of E &
dom(g1 * f1) = the carrier of E by FUNCT_2:def 1;
thus t1.a
= ((f1") * (g1 * f1)).a1 by B2,RELAT_1:36
.= (f1").((g1 * f1).a1) by B7,FUNCT_1:13
.= (f1").(g1.(f1.a1)) by B7,FUNCT_1:13
.= (f1").(f1.a1) by B6,B5,H3,FIELD_8:def 2
.= (f1"*f1).a1 by B7,FUNCT_1:13
.= (id the carrier of E).a1 by FUNCT_2:61 .= a;
end; then
t1 is K1-fixing; then
t1 in the set of all f where f is K1-fixing Automorphism of L1;
then t1 in H1 by H2,GALOIS_1:def 4;
then o in H1 |^ f" by B1,GROUP_3:58;
hence o in the carrier of (H1|^f");
end;
now let o be object;
assume o in the carrier of (H1|^f"); then
o in H1 |^ f"; then
consider g being Element of the carrier of Aut(E,F) such that
B1: o = g |^ f" & g in H1 by GROUP_3:58;
reconsider f1, g1 = g as F-fixing Automorphism of L2;
B2: g |^ f" = (f"") * g * f" by GROUP_3:def 2;
f1 * g1 = f * g & f1" = f" by GALOIS_2:3,4; then
B3: f1 * g1 * f1" = f * g * f" by GALOIS_2:3;
now let a be Element of K2;
K2 in IntermediateFields(E,F) by GALOIS_0:def 5; then
K2 is Subfield of E by FIELD_14:4; then
the carrier of K2 c= the carrier of E by EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
h is onto by A1; then
consider b being object such that
C1: b in dom h & h.b = a by FUNCT_1:def 3;
reconsider b as Element of K1 by C1;
h = f1|(the carrier of K1) by A2,MATRLIN2:def 1; then
C2: f1.b = a by C1,FUNCT_1:49;
C3: dom f1 = the carrier of E &
dom(f1") = the carrier of E &
dom(g1 * (f1")) = the carrier of E by FUNCT_2:def 1;
K1 in IntermediateFields(E,F) by GALOIS_0:def 5; then
K1 is Subfield of E by FIELD_14:4; then
the carrier of K1 c= the carrier of E by EC_PF_1:def 1; then
C5: b in the carrier of E;
thus (f1 * g1 * (f1")).a
= (f1 * (g1 * (f1"))).a1 by RELAT_1:36
.= f1.((g1 * (f1")).a1) by C3,FUNCT_1:13
.= f1.(g1.((f1").(f1.b))) by C2,C3,FUNCT_1:13
.= f1.(g1.b) by C3,C5,FUNCT_1:34
.= a by C2,B1,H2,FIELD_8:def 2;
end; then
f1 * g1 * (f1") is K2-fixing; then
f1 * g1 * (f1") in
the set of all f where f is K2-fixing Automorphism of L2;
hence o in the carrier of H2 by H3,B1,B2,B3,GALOIS_1:def 4;
end; then
H1 |^ f" = H2 by A3,TARSKI:2,GROUP_2:59;
hence Aut(E,K1),Aut(E,K2) are_conjugated_in Aut(E,F) by GROUP_3:102;
end;
now assume Aut(E,K1),Aut(E,K2) are_conjugated_in Aut(E,F); then
consider f being Element of the carrier of Aut(E,F) such that
B1: H2 = H1 |^ f by GROUP_3:102;
reconsider g = f" as Element of the carrier of Aut(E,F);
set h = g|the carrier of K1;
K1 in IntermediateFields(E,F) by GALOIS_0:def 5; then
H1: F is Subfield of K1 & K1 is Subfield of E by FIELD_14:4; then
H2: the carrier of K1 c= the carrier of E by EC_PF_1:def 1;
K2 in IntermediateFields(E,F) by GALOIS_0:def 5; then
H3: K2 is Subfield of E by FIELD_14:4;
dom g = the carrier of E by FUNCT_2:def 1; then
B2: dom h = (the carrier of E) /\ (the carrier of K1) by RELAT_1:61
.= the carrier of K1 by H2,XBOOLE_1:28;
B3: K2 = Fix(E,H1|^g") by B1,G1
.= g.:Fix(E,H1) by Conj2
.= InducedSubfield rng(g,K1) by G1; then
the carrier of K2 = rng(g|the carrier of K1) by FIELD_16:def 3; then
reconsider h as Function of K1,K2 by B2,FUNCT_2:1;
B4: h is onto by B3,FIELD_16:def 3;
now let x,y be Element of K1;
reconsider a = x, b = y as Element of E by H2;
C1: K1 is Subring of E & K2 is Subring of E by H1,H3,FIELD_5:12;
h.x = g.a & h.y = g.b by FUNCT_1:49; then
C2: h.x + h.y = g.a + g.b &
x + y = a + b by C1,FIELD_6:15;
hence h.(x+y) = g.(a+b) by FUNCT_1:49
.= h.x + h.y by C2,VECTSP_1:def 20;
end; then
B5: h is additive;
now let x,y be Element of K1;
reconsider a = x, b = y as Element of E by H2;
C1: K1 is Subring of E & K2 is Subring of E by H1,H3,FIELD_5:12;
h.x = g.a & h.y = g.b by FUNCT_1:49; then
C2: h.x * h.y = g.a * g.b &
x * y = a * b by C1,FIELD_6:16;
hence h.(x*y) = g.(a*b) by FUNCT_1:49
.= h.x * h.y by C2,GROUP_6:def 6;
end; then
B6: h is multiplicative;
C3: 1.E = 1.K1 & 1.E = 1.K2 by H1,H3,EC_PF_1:def 1; then
h.(1_K1) = g.(1_E) by FUNCT_1:49 .= 1_K2 by C3,GROUP_1:def 13; then
B7: h is unity-preserving;
now let x being Element of F;
the carrier of F c= the carrier of K1 by H1,EC_PF_1:def 1; then
reconsider a = x as Element of K1;
reconsider b = a as Element of E by H2;
thus h.x = g.b by FUNCT_1:49 .= x by FIELD_8:def 2;
end; then
h is F-fixing;
hence K1,K2 are_isomorphic_over F by B4,B5,B6,B7,FIELD_8:def 5;
end;
hence thesis by A;
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
by GALOIS_2:35;
theorem T1:
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F
holds K is GaloisExtension of F iff K is F-normal
proof
let F be Field, E be F-finite GaloisExtension of F,
K be IntermediateField of E,F;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
H: E is K-extending by FIELD_4:7;
now assume A: K is F-normal;
K is F-separable by H,FIELD_15:94;
hence K is F-Galois by A;
end;
hence thesis;
end;
theorem T4:
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F
holds K is F-normal iff
for f being Element of the carrier of Aut(E,F) holds f.:K = 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
H: K is Subfield of E by FIELD_14:4;
now assume B: for f being Element of the carrier of Aut(E,F) holds f.:K = K;
now let a be Element of K;
reconsider E1 = E as K-extending FieldExtension of F by H,FIELD_4:7;
B7: the carrier of K c= the carrier of E by H,EC_PF_1:def 1; then
reconsider a1 = a as F-algebraic Element of E1;
Conj a1 = Conj(a1,Aut(E1,F)) by GALOIS_1:def 10; then
reconsider Z = Conj(a1,Aut(E1,F)) as non empty finite Subset of E1;
set p = the Ppoly of E1,Z;
Fix(E,Aut(E,F)) == F by GALOIS_1:def 18; then
B0: p = MinPoly(a1,F) by GALOIS_2:26;
reconsider q = MinPoly(a1,F) as non constant
Element of the carrier of Polynom-Ring F;
B2: q splits_in E1 by GALOIS_2:29;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E1
by FIELD_4:10; then
reconsider q1 = q as Element of the carrier of Polynom-Ring E1;
now let b be Element of E1;
assume B4: b in Roots(E1,q);
B5: Roots q1 = Roots(E,q) by FIELD_7:13;
Z = Roots q1 by B0,RING_5:63; then
b in the set of all f.a where f is Element of the carrier of Aut(E1,F)
by B4,B5,GALOIS_1:def 9; then
consider f being Element of the carrier of Aut(E,F) such that
B3: b = f.a;
reconsider f as F-fixing Automorphism of E;
B6: dom (f|the carrier of K)
= dom f /\ (the carrier of K) by RELAT_1:61
.= (the carrier of E) /\ (the carrier of K) by FUNCT_2:def 1
.= the carrier of K by B7,XBOOLE_1:28;
f.a = (f|the carrier of K).a by FUNCT_1:49; then
f.a in rng(f|the carrier of K) by B6,FUNCT_1:def 3; then
f.a in the carrier of f.:K by FIELD_16:def 3;
hence b in the carrier of K by B,B3;
end;
then Roots(E1,q) c= the carrier of K;
then q splits_in K by B2,FIELD_8:27; then
consider c being non zero Element of K, r being Ppoly of K such that
B5: q = c * r by FIELD_4:def 5;
thus MinPoly(a,F) splits_in K by B5,FIELD_4:def 5,FIELD_10:10;
end;
hence K is F-normal by FIELD_13:54;
end;
hence thesis by T4x;
end;
theorem T2:
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F
holds K is F-normal iff Aut(E,K) is normal Subgroup of Aut(E,F)
proof
let F be Field, E be F-finite GaloisExtension of F;
let K be IntermediateField of E,F;
reconsider G = Aut(E,K) as Subgroup of Aut(E,F) by GALOIS_1:18;
A: now assume AS: K is F-normal;
now let f be Element of the carrier of Aut(E,F);
the carrier of Aut(E,F) c= the carrier of Aut(E) by GROUP_2:def 5;
then reconsider f1 = f as Element of the carrier of Aut(E);
Aut(E,K) = Aut(E,f.:K) by AS,T4x,GALOIS_1:7;
then G = G |^ f1 by T7;
hence G |^ f = G by lemT2;
end;
hence G is normal Subgroup of Aut(E,F) by N3;
end;
now assume AS: G is normal Subgroup of Aut(E,F);
now let f be Element of the carrier of Aut(E,F);
the carrier of Aut(E,F) c= the carrier of Aut(E) by GROUP_2:def 5;
then reconsider f1 = f as Element of the carrier of Aut(E);
reconsider g1 = f1 as Automorphism of E;
reconsider g = f as F-fixing Automorphism of E;
B: f1" = g1" by GALOIS_2:2 .= f" by GALOIS_2:4;
C: Aut(E,f.:K) = G |^ f1" by T7
.= G |^ f" by B,lemT2
.= Aut(E,K) by AS,N3;
reconsider B = Psi E as
a_Bijection of IntermediateFields(E,F),Subgroups Aut(E,F) by BIJ1;
F is Subfield of f.:K by FIELD_4:7; then
E: f.:K in IntermediateFields(E,F) & K in IntermediateFields(E,F)
by GALOIS_0:def 5,FIELD_14:4; then
reconsider fK = f.:K as IntermediateField of E,F by GALOIS_0:def 5;
F: B.K = Aut(E,f.:K) by C,GALOIS_3:def 14
.= Aut(E,fK) by GALOIS_1:7
.= B.fK by GALOIS_3:def 14;
B is bijective by GALOIS_0:def 2;
hence f.:K = K by F,E,FUNCT_2:19;
end;
hence K is F-normal by T4;
end;
hence thesis by A;
end;
definition
let F be Field;
let E be F-finite FieldExtension of F;
let K be IntermediateField of E,F;
assume AS:K is F-normal;
func Restr K -> Homomorphism of Aut(E,F),Aut(K,F) means :defR:
for f being F-fixing Automorphism of E holds it.f = f|(the carrier of K);
existence
proof
defpred P[object,object] means
ex f being F-fixing Automorphism of E st $1 = f & $2 = f|(the carrier of K);
A: now let x be object;
assume x in the carrier of Aut(E,F); then
x is Element of the carrier of Aut(E,F); then
reconsider f = x as F-fixing Automorphism of E;
A1: Aut(K,F) = multMagma(#Auts(K,F),AutComp(K,F)#) by GALOIS_1:def 6;
thus ex y being object st y in the carrier of Aut(K,F) & P[x,y]
proof
take f|(the carrier of K);
f|(the carrier of K) is F-fixing Automorphism of K by AS,T4a; then
f|(the carrier of K) in the set of all f
where f is F-fixing Automorphism of K;
hence f|(the carrier of K) in the carrier of Aut(K,F)
by A1,GALOIS_1:def 4;
thus P[x,f|(the carrier of K)];
end;
end;
consider h being Function of the carrier of Aut(E,F),
the carrier of Aut(K,F) such that
B: for x being object st x in the carrier of Aut(E,F) holds P[x,h.x]
from FUNCT_2:sch 1(A);
now let a,b be Element of the carrier of Aut(E,F);
reconsider g1 = a, g2 = b as F-fixing Automorphism of E;
reconsider hg1 = g1|(the carrier of K), hg2 = g2|(the carrier of K)
as F-fixing Automorphism of K by AS,T4a;
P[a,h.a] & P[b,h.b] by B; then
B2: h.a * h.b = hg1 * hg2 by GALOIS_2:3
.= g1|(the carrier of K) * g2|(the carrier of K);
a * b = g1 * g2 & P[a * b,h.(a * b)] by B,GALOIS_2:3;
hence h.(a * b) = h.a * h.b by B2,AS,lemT5;
end; then
reconsider h as Homomorphism of Aut(E,F),Aut(K,F) by GROUP_6:def 6;
take h;
now let f be F-fixing Automorphism of E;
C: Aut(E,F) = multMagma(#Auts(E,F),AutComp(E,F)#) by GALOIS_1:def 6;
f in the set of all f where f is F-fixing Automorphism of E; then
reconsider g = f as Element of the carrier of Aut(E,F)
by C,GALOIS_1:def 4;
P[g,h.g] by B;
hence h.f = f|(the carrier of K);
end;
hence thesis;
end;
uniqueness
proof
let h1,h2 be Homomorphism of Aut(E,F),Aut(K,F);
assume A: for f being F-fixing Automorphism of E
holds h1.f = f|(the carrier of K);
assume B: for f being F-fixing Automorphism of E
holds h2.f = f|(the carrier of K);
now let o be object;
assume o in the carrier of Aut(E,F); then
o is Element of the carrier of Aut(E,F); then
reconsider f = o as F-fixing Automorphism of E;
h1.f = f|(the carrier of K) by A .= h2.f by B;
hence h1.o = h2.o;
end;
hence thesis;
end;
end;
theorem T3b:
for F being Field
for E being F-finite FieldExtension of F
for K being IntermediateField of E,F st K is F-normal
holds Fix(K,Image(Restr K)) is Subfield of Fix(E,Aut(E,F))
proof
let F be Field, E be F-finite FieldExtension of F;
let K be IntermediateField of E,F;
assume AS: K is F-normal;
Image(Restr K) is Subgroup of Aut(K,F); then
reconsider G = Image(Restr K) as Subgroup of Aut(K);
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
I: K is Subfield of E by FIELD_14:4; then
H: Fix(K,G) is Subfield of E by EC_PF_1:5;
set fG = Fixed_Elements(K,G), fE = Fixed_Elements(E,Aut(E,F));
J: fG = {a where a is Element of K :
for f being Function of K,K st f in G holds f.a = a} &
fE = {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 GALOIS_1:def 16;
now let o be object;
assume o in fG; then
consider a being Element of K such that
A: o = a & for f being Function of K,K st f in G holds f.a = a by J;
the carrier of K c= the carrier of E by I,EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
now let f be Function of E,E;
assume B0: f in Aut(E,F); then
reconsider f1 = f as F-fixing Automorphism of E;
reconsider g = f1|(the carrier of K)
as F-fixing Automorphism of K by AS,T4a;
B2: dom(Restr K) = the carrier of Aut(E,F) by FUNCT_2:def 1;
(Restr K).f1 = g by AS,defR; then
g in rng(Restr K) by B0,B2,FUNCT_1:def 3; then
B1: g in G by GROUP_6:44;
thus f.a1 = g.a by FUNCT_1:49 .= a1 by A,B1;
end;
hence o in fE by A,J;
end; then
fG c= fE; then
the carrier of Fix(K,G) c= fE by GALOIS_1:def 17; then
C: the carrier of Fix(K,G) c= the carrier of Fix(E,Aut(E,F))
by GALOIS_1:def 17; then
C1: [:the carrier of Fix(K,G),the carrier of Fix(K,G):] c=
[:the carrier of Fix(E,Aut(E,F)),the carrier of Fix(E,Aut(E,F)):]
by ZFMISC_1:96;
D: the addF of Fix(K,G)
= (the addF of E) || the carrier of Fix(K,G) by H,EC_PF_1:def 1
.= ((the addF of E) || the carrier of Fix(E,Aut(E,F)))
|| the carrier of Fix(K,G) by C1,FUNCT_1:51
.= (the addF of Fix(E,Aut(E,F))) || the carrier of Fix(K,G)
by EC_PF_1:def 1;
E: the multF of Fix(K,G)
= (the multF of E) || the carrier of Fix(K,G) by H,EC_PF_1:def 1
.= ((the multF of E) || the carrier of Fix(E,Aut(E,F)))
|| the carrier of Fix(K,G) by C1,FUNCT_1:51
.= (the multF of Fix(E,Aut(E,F))) || the carrier of Fix(K,G)
by EC_PF_1:def 1;
F: 1.Fix(K,G) = 1.E by H,EC_PF_1:def 1 .= 1.Fix(E,Aut(E,F)) by EC_PF_1:def 1;
0.Fix(K,G) = 0.E by H,EC_PF_1:def 1 .= 0.Fix(E,Aut(E,F)) by EC_PF_1:def 1;
hence thesis by C,D,E,F,EC_PF_1:def 1;
end;
theorem T3c:
for F being Field
for E being F-finite FieldExtension of F
for K being IntermediateField of E,F
st K is F-normal holds Ker(Restr K) = Aut(E,K)
proof
let F be Field, E be F-finite FieldExtension of F;
let K be IntermediateField of E,F;
assume AS: K is F-normal;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
reconsider E1 = E as FieldExtension of K by FIELD_4:7;
H3: Aut(K,F) = multMagma(#Auts(K,F),AutComp(K,F)#) &
Aut(E,F) = multMagma(#Auts(E,F),AutComp(E,F)#) &
Aut(E1,K) = multMagma(#Auts(E1,K),AutComp(E1,K)#) by GALOIS_1:def 6;
H4: Aut(E,K) = Aut(FieldExt(E,K),K) by GALOIS_1:def 8 .= Aut(E1,K);
set f = Restr K;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
reconsider E1 = E as FieldExtension of K by FIELD_4:7;
C: now let o be object;
assume C1: o in the carrier of Ker f;
the carrier of Ker f =
{a where a is Element of Aut(E,F) : f.a = 1_Aut(K,F)} by GROUP_6:def 9;
then consider a being Element of the carrier of Aut(E,F) such that
C2: o = a & f.a = 1_Aut(K,F) by C1;
reconsider g = a as F-fixing Automorphism of E;
g|K = a|(the carrier of K) by MATRLIN2:def 1
.= f.a by AS,defR
.= 1_Aut(K) by C2,GROUP_2:44
.= id K by GALOIS_1:6; then
g is K-fixing Automorphism of E1 by FIELD_8:35; then
o in the set of all f where f is K-fixing Automorphism of E1 by C2;
hence o in the carrier of Aut(E,K) by H3,H4,GALOIS_1:def 4;
end;
D: now let o be object;
assume o in the carrier of Aut(E,K); then
o in the set of all f where f is K-fixing Automorphism of E1
by H3,H4,GALOIS_1:def 4; then
consider g being K-fixing Automorphism of E1 such that
C4: o = g;
C5: the carrier of Ker f =
{a where a is Element of Aut(E,F) : f.a = 1_Aut(K,F)} by GROUP_6:def 9;
C6: g is F-fixing Automorphism of E by FIELD_8:37; then
g in the set of all f where f is F-fixing Automorphism of E; then
C7: g in Aut(E,F) by H3,GALOIS_1:def 4;
f.g = g|(the carrier of K) by C6,AS,defR
.= g|K by MATRLIN2:def 1
.= id K by FIELD_8:35
.= 1_Aut(K) by GALOIS_1:6
.= 1_Aut(K,F) by GROUP_2:44;
hence o in the carrier of Ker f by C7,C4,C5;
end;
Aut(E,K) is Subgroup of Aut(E,F) by GALOIS_1:18;
hence Ker(Restr K) = Aut(E,K) by C,D,TARSKI:2,GROUP_2:59;
end;
theorem T3:
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F
st K is F-normal holds Image(Restr K) = Aut(K,F)
proof
let F be Field, E be F-finite GaloisExtension of F;
let K be IntermediateField of E,F;
assume AS: K is F-normal;
K in IntermediateFields(E,F) by GALOIS_0:def 5; then
K is Subfield of E by FIELD_14:4; then
reconsider E1 = E as FieldExtension of K by FIELD_4:7;
set f = Restr K;
E1: Image f is Subgroup of Aut(K,F);
Image f in Subgroups Aut(K,F) by GROUP_3:def 1; then
E0: Image f is SubGroup of Aut(K,F) by GALOIS_0:def 10;
reconsider K1 = K as F-finite GaloisExtension of F by AS,T1;
F == Fix(K1,Aut(K1,F)) & F == Fix(E,Aut(E,F)) by GALOIS_1:def 18; then
E3: Fix(K,Aut(K,F)) == Fix(K,Image f) by E1,T3b,GALOIS_1:20;
N: Aut(K,F) is Subgroup of Aut(K1,F) by GROUP_2:54; then
Aut(K,F) in Subgroups Aut(K1,F) by GROUP_3:def 1; then
reconsider G = Aut(K,F) as SubGroup of Aut(K1,F) by N,GALOIS_0:def 10;
reconsider B = Phi K1
as a_Bijection of Subgroups Aut(K1,F),IntermediateFields(K1,F) by BIJ;
E4: B.G = Fix(K1,G) by GALOIS_3:def 15 .= B.(Image f) by E0,E3,GALOIS_3:def 15;
E5: B is bijective by GALOIS_0:def 2;
G in Subgroups Aut(K1,F) & Image f in Subgroups Aut(K1,F)
by GROUP_3:def 1;
hence Aut(K,F) = Image f by E4,E5,FUNCT_2:19;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for K being IntermediateField of E,F
for H being normal Subgroup of Aut(E,F)
st H = Aut(E,K) holds Aut(K,F), Aut(E,F)./.H are_isomorphic
proof
let F be Field, E be F-finite GaloisExtension of F;
let K be IntermediateField of E,F, H be normal Subgroup of Aut(E,F);
assume A: H = Aut(E,K); then
Aut(K,F) = Image(Restr K) & Ker(Restr K) = Aut(E,K) by T2,T3c,T3;
hence thesis by A,GROUP_6:78;
end;
begin :: Some Lattice Properties
theorem lat1:
for F being Field
for E being FieldExtension of F
for K1,K2 being IntermediateField of E,F
holds Aut(E,K1) "\/" Aut(E,K2) is Subgroup of Aut(E,K1 "/\" K2) &
Aut(E,K1 "\/" K2) is Subgroup of Aut(E,K1) /\ Aut(E,K2)
proof
let F be Field, E be FieldExtension of F, K1,K2 be IntermediateField of E,F;
set M = {K1,K2};
K1 in M & K2 in M by TARSKI:def 2; then
K1"/\"K2 is Subfield of K1 & K1"/\"K2 is Subfield of K2 by GALOIS_0:16; then
Aut(E,K1) is Subgroup of Aut(E,K1"/\"K2) &
Aut(E,K2) is Subgroup of Aut(E,K1"/\"K2) by GALOIS_1:19;
hence Aut(E,K1) "\/" Aut(E,K2) is Subgroup of Aut(E,K1 "/\" K2) by GROUP_4:63;
K1 in M & K2 in M by TARSKI:def 2; then
K1 is Subfield of K1"\/"K2 & K2 is Subfield of K1"\/"K2 by GALOIS_0:18; then
Aut(E,K1"\/"K2) is Subgroup of Aut(E,K1) &
Aut(E,K1"\/"K2) is Subgroup of Aut(E,K2) by GALOIS_1:19;
hence thesis by GROUP_2:91;
end;
theorem lat3:
for F being Field
for E being FieldExtension of F
for G1,G2 being Subgroup of Aut(E,F)
holds Fix(E,G1) "\/" Fix(E,G2) is Subfield of Fix(E,G1 /\ G2) &
Fix(E,G1 "\/" G2) is Subfield of Fix(E,G1) "/\" Fix(E,G2)
proof
let F be Field, E be FieldExtension of F, G1,G2 be Subgroup of Aut(E,F);
set M = {Fix(E,G1),Fix(E,G2)};
reconsider G3 = G1, G4 = G2 as Subgroup of Aut(E);
reconsider G = G3 /\ G4 as Subgroup of Aut(E);
Fix(E,G1/\G2) in IntermediateFields(E,F) by GALOIS_0:def 5; then
Fix(E,G1/\G2) is Subfield of E by FIELD_14:4; then
H1: Fix(E,G1/\G2) in SubFields(E) by FIELD_12:45;
H2: G3 /\ G4 is Subgroup of G3 & G3 /\ G4 is Subgroup of G4 by GROUP_2:88;
H3: G1 /\ G2 = G3 /\ G4 by GALOIS_0:8;
now let K be Element of M;
per cases by TARSKI:def 2;
suppose K = Fix(E,G1);
hence K is Subfield of Fix(E,G1/\G2) by H3,H2,GALOIS_1:20;
end;
suppose K = Fix(E,G2);
hence K is Subfield of Fix(E,G1/\G2) by H3,H2,GALOIS_1:20;
end;
end;
hence Fix(E,G1) "\/" Fix(E,G2) is Subfield of Fix(E,G1 /\ G2)
by H1,GALOIS_0:19;
reconsider G = G3 "\/" G4 as Subgroup of Aut(E);
Fix(E,G1"\/"G2) in IntermediateFields(E,F) by GALOIS_0:def 5; then
H1: Fix(E,G1"\/"G2) is Subfield of E by FIELD_14:4;
H2: G3 is Subgroup of G3"\/"G4 & G4 is Subgroup of G3"\/"G4 by GROUP_4:60;
now let K be Element of M;
per cases by TARSKI:def 2;
suppose K = Fix(E,G1);
then Fix(E,G3"\/"G4) is Subfield of K by H2,GALOIS_1:20;
hence Fix(E,G1"\/"G2) is Subfield of K by GALOIS_0:8;
end;
suppose K = Fix(E,G2);
then Fix(E,G3"\/"G4) is Subfield of K by H2,GALOIS_1:20;
hence Fix(E,G1"\/"G2) is Subfield of K by GALOIS_0:8;
end;
end;
hence thesis by H1,GALOIS_0:17;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for K1,K2 being IntermediateField of E,F
holds Aut(E,K1 "/\" K2) = Aut(E,K1) "\/" Aut(E,K2) &
Aut(E,K1 "\/" K2) = Aut(E,K1) /\ Aut(E,K2)
proof
let F be Field, E be F-finite GaloisExtension of F;
let K1,K2 be IntermediateField of E,F;
N: Aut(E,K1) is Subgroup of Aut(E,F) & Aut(E,K2) is Subgroup of Aut(E,F)
by GALOIS_1:18; then
Aut(E,K1) in Subgroups Aut(E,F) & Aut(E,K2) in Subgroups Aut(E,F)
by GROUP_3:def 1; then
reconsider G1 = Aut(E,K1), G2 = Aut(E,K2)
as SubGroup of Aut(E,F) by N,GALOIS_0:def 10;
G1 "\/" G2 in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G = G1 "\/" G2 as SubGroup of Aut(E,F) by GALOIS_0:def 10;
A: Aut(E,K1) "\/" Aut(E,K2) is Subgroup of Aut(E,K1 "/\" K2) by lat1;
B: Aut(E,Fix(E,G)) = G1 "\/" G2 by G2;
C: Fix(E,G1) = K1 & Fix(E,G2) = K2 by G1;
Fix(E,G1 "\/" G2) is Subfield of Fix(E,G1) "/\" Fix(E,G2) by lat3; then
Aut(E,Fix(E,G1) "/\" Fix(E,G2)) is Subgroup of Aut(E,Fix(E,G))
by GALOIS_1:19; then
Aut(E,K1 "/\" K2) is Subgroup of Aut(E,K1) "\/" Aut(E,K2) by C,B,GALOIS_0:8;
hence Aut(E,K1 "/\" K2) = Aut(E,K1) "\/" Aut(E,K2) by A,GROUP_2:55;
G1 /\ G2 in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G = G1 /\ G2 as SubGroup of Aut(E,F) by GALOIS_0:def 10;
A: Aut(E,K1 "\/" K2) is Subgroup of Aut(E,K1) /\ Aut(E,K2) by lat1;
B: Aut(E,Fix(E,G)) = G1 /\ G2 by G2;
C: Fix(E,G1) = K1 & Fix(E,G2) = K2 by G1;
Fix(E,G1) "\/" Fix(E,G2) is Subfield of Fix(E,G1/\G2) by lat3; then
Aut(E,Fix(E,G)) is Subgroup of Aut(E,Fix(E,G1) "\/" Fix(E,G2))
by GALOIS_1:19; then
Aut(E,K1) /\ Aut(E,K2) is Subgroup of Aut(E,K1 "\/" K2) by C,B,GALOIS_0:8;
hence thesis by A,GROUP_2:55;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for G1,G2 being SubGroup of Aut(E,F)
holds Fix(E,G1 /\ G2) = Fix(E,G1) "\/" Fix(E,G2) &
Fix(E,G1 "\/" G2) = Fix(E,G1) "/\" Fix(E,G2)
proof
let F be Field, E be F-finite GaloisExtension of F;
let G1,G2 be SubGroup of Aut(E,F);
set K1 = Fix(E,G1), K2 = Fix(E,G2);
B: Fix(E,Aut(E,K1 "\/" K2)) = K1 "\/" K2 by G1;
C: Aut(E,Fix(E,G1)) = G1 & Aut(E,Fix(E,G2)) = G2 by G2;
D: Fix(E,Aut(E,K1)/\Aut(E,K2)) = Fix(E,G1/\G2) by C,GALOIS_0:8;
Aut(E,K1 "\/" K2) is Subgroup of Aut(E,K1) /\ Aut(E,K2) by lat1;
then Fix(E,G1 /\ G2) == Fix(E,G1) "\/" Fix(E,G2) by lat3,D,B,GALOIS_1:20;
hence Fix(E,G1 /\ G2) = Fix(E,G1) "\/" Fix(E,G2);
B: Fix(E,Aut(E,K1 "/\" K2)) = K1 "/\" K2 by G1;
C: Aut(E,Fix(E,G1)) = G1 & Aut(E,Fix(E,G2)) = G2 by G2;
D: Fix(E,Aut(E,K1)"\/"Aut(E,K2)) = Fix(E,G1"\/"G2) by C,GALOIS_0:8;
Aut(E,K1) "\/" Aut(E,K2) is Subgroup of Aut(E,K1 "/\" K2) by lat1;
then Fix(E,G1 "\/" G2) == Fix(E,G1) "/\" Fix(E,G2) by lat3,D,B,GALOIS_1:20;
hence thesis;
end;
definition
let F be Field;
let E be FieldExtension of F;
let M be non empty Subset of IntermediateFields(E,F);
func Psi.M -> non empty Subset of Subgroups Aut(E,F) equals
{ (Psi E).K where K is Element of IntermediateFields(E,F) : K in M };
coherence
proof
set K = the Element of M;
K in M; then
A: (Psi E).K in {(Psi E).K where
K is Element of IntermediateFields(E,F) : K in M};
now let o be object;
assume o in {(Psi E).K where
K is Element of IntermediateFields(E,F) : K in M}; then
consider K being Element of IntermediateFields(E,F) such that
A: o = (Psi E).K & K in M;
(Psi E).K = Aut(E,K) by GALOIS_3:def 14;
then (Psi E).K is strict Subgroup of Aut(E,F) by GALOIS_1:18;
hence o in Subgroups Aut(E,F) by A,GROUP_3:def 1;
end;
then {(Psi E).K where K is Element of IntermediateFields(E,F) : K in M}
c= Subgroups Aut(E,F);
hence thesis by A;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let M be non empty Subset of Subgroups Aut(E,F);
func Phi.M -> non empty Subset of IntermediateFields(E,F) equals
{ (Phi E).G where G is Element of Subgroups Aut(E,F) : G in M };
coherence
proof
set G1 = the Element of M;
G1 in M; then
A: (Phi E).G1 in {(Phi E).G where
G is Element of Subgroups Aut(E,F) : G in M};
now let o be object;
assume o in {(Phi E).G where
G is Element of Subgroups Aut(E,F) : G in M}; then
consider G being Element of Subgroups Aut(E,F) such that
A: o = (Phi E).G & G in M;
reconsider G1 = G as Subgroup of Aut(E,F);
reconsider G2 = G1 as SubGroup of Aut(E,F) by GALOIS_0:def 10;
(Phi E).G2 = Fix(E,G1) by GALOIS_3:def 15;
hence o in IntermediateFields(E,F) by A,GALOIS_0:def 5;
end;
then {(Phi E).G where G is Element of Subgroups Aut(E,F) : G in M}
c= IntermediateFields(E,F);
hence thesis by A;
end;
end;
theorem lat10:
for F being Field
for E being FieldExtension of F
for M being non empty Subset of IntermediateFields(E,F) holds
Psi.M = { Aut(E,K) where K is Element of IntermediateFields(E,F) : K in M }
proof
let F be Field, E be FieldExtension of F;
let M be non empty Subset of IntermediateFields(E,F);
set S = {Aut(E,K) where K is Element of IntermediateFields(E,F) : K in M};
A: now let o be object;
assume o in S; then
consider K being Element of IntermediateFields(E,F) such that
A1: o = Aut(E,K) & K in M;
(Psi E).K = Aut(E,K) by GALOIS_3:def 14;
hence o in Psi.M by A1;
end;
now let o be object;
assume o in {(Psi E).K where
K is Element of IntermediateFields(E,F) : K in M}; then
consider K being Element of IntermediateFields(E,F) such that
B1: o = (Psi E).K & K in M;
(Psi E).K = Aut(E,K) by GALOIS_3:def 14;
hence o in S by B1;
end;
hence thesis by A,TARSKI:2;
end;
theorem lat11:
for F being Field
for E being FieldExtension of F
for M being non empty Subset of Subgroups Aut(E,F) holds
Phi.M = { Fix(E,G) where G is Element of Subgroups Aut(E,F) : G in M }
proof
let F be Field, E be FieldExtension of F;
let M be non empty Subset of Subgroups Aut(E,F);
set S = {Fix(E,G) where G is Element of Subgroups Aut(E,F) : G in M};
A: now let o be object;
assume o in S; then
consider G being Element of Subgroups Aut(E,F) such that
A1: o = Fix(E,G) & G in M;
reconsider G1 = G as SubGroup of Aut(E,F) by GALOIS_0:def 10;
(Phi E).G1 = Fix(E,G1) by GALOIS_3:def 15;
hence o in Phi.M by A1;
end;
now let o be object;
assume o in {(Phi E).G where
G is Element of Subgroups Aut(E,F) : G in M}; then
consider G being Element of Subgroups Aut(E,F) such that
B1: o = (Phi E).G & G in M;
reconsider G1 = G as SubGroup of Aut(E,F) by GALOIS_0:def 10;
(Phi E).G1 = Fix(E,G1) by GALOIS_3:def 15;
hence o in S by B1;
end;
hence thesis by A,TARSKI:2;
end;
theorem lathh1:
for F being Field
for E being F-finite GaloisExtension of F
for M being non empty Subset of IntermediateFields(E,F) holds Phi.(Psi.M) = M
proof
let F be Field, E be F-finite GaloisExtension of F;
let M be non empty Subset of IntermediateFields(E,F);
H1: Psi.M = {Aut(E,K) where
K is Element of IntermediateFields(E,F) : K in M} by lat10;
H2: Phi.(Psi.M) = {Fix(E,G) where
G is Element of Subgroups Aut(E,F) : G in (Psi.M)} by lat11;
A: now let o be object;
assume B: o in M; then
consider K being strict Field such that
C: K = o & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
reconsider K = o as IntermediateField of E,F by B,C,GALOIS_0:def 5;
Aut(E,K) in Psi.M by B,H1; then
Fix(E,Aut(E,K)) in Phi.(Psi.M) by H2;
hence o in Phi.(Psi.M) by G1;
end;
now let o be object;
assume o in Phi.(Psi.M); then
consider G being Element of Subgroups Aut(E,F) such that
B: o = Fix(E,G) & G in Psi.M by H2;
consider K being Element of IntermediateFields(E,F) such that
C: G = Aut(E,K) & K in M by B,H1;
thus o in M by B,C,G1;
end;
hence thesis by A,TARSKI:2;
end;
theorem lathh2:
for F being Field
for E being F-finite GaloisExtension of F
for M being non empty Subset of Subgroups Aut(E,F) holds Psi.(Phi.M) = M
proof
let F be Field, E be F-finite GaloisExtension of F;
let M be non empty Subset of Subgroups Aut(E,F);
H1: Phi.M = {Fix(E,G) where
G is Element of Subgroups Aut(E,F) : G in M} by lat11;
H2: Psi.(Phi.M) = {Aut(E,K) where
K is Element of IntermediateFields(E,F) : K in Phi.M} by lat10;
A: now let o be object;
assume B: o in M; then
o is Subgroup of Aut(E,F) by GROUP_3:def 1; then
reconsider G = o as SubGroup of Aut(E,F) by B,GALOIS_0:def 10;
Fix(E,G) in Phi.M by B,H1; then
Aut(E,Fix(E,G)) in Psi.(Phi.M) by H2;
hence o in Psi.(Phi.M) by G2;
end;
now let o be object;
assume o in Psi.(Phi.M); then
consider K being Element of IntermediateFields(E,F) such that
B: o = Aut(E,K) & K in Phi.M by H2;
consider G being Element of Subgroups Aut(E,F) such that
C: K = Fix(E,G) & G in M by B,H1;
G is SubGroup of Aut(E,F) by GALOIS_0:def 10;
hence o in M by B,C,G2;
end;
hence thesis by A,TARSKI:2;
end;
theorem lat12:
for F being Field
for E being FieldExtension of F
for M being non empty Subset of IntermediateFields(E,F)
holds Aut(E,\/M) is Subgroup of /\(Psi.M) & \/(Psi.M) is Subgroup of Aut(E,/\M)
proof
let F be Field, E be FieldExtension of F;
let M be non empty Subset of IntermediateFields(E,F);
set G = Aut(E,F);
reconsider K = \/M as IntermediateField of E,F by GALOIS_0:21;
A: Aut(E,K) is Subgroup of Aut(E,F) by GALOIS_1:18;
B: Psi.M = {Aut(E,K) where K is Element of IntermediateFields(E,F) : K in M}
by lat10;
now let H be Element of Psi.M;
H in Psi.M; then
consider K1 being Element of IntermediateFields(E,F) such that
C: H = Aut(E,K1) & K1 in M by B;
K1 is Subfield of \/M by C,GALOIS_0:18;
hence Aut(E,K) is Subgroup of H by C,GALOIS_1:19;
end;
then Aut(E,K) is Subgroup of /\(Psi.M) by A,GALOIS_0:10;
hence Aut(E,\/M) is Subgroup of /\(Psi.M) by GALOIS_1:7;
reconsider K = /\M as IntermediateField of E,F by GALOIS_0:20;
Aut(E,K) is Subgroup of Aut(E,F) by GALOIS_1:18; then
A: Aut(E,K) is Element of Subgroups Aut(E,F) by GROUP_3:def 1;
B: Psi.M = {Aut(E,K) where K is Element of IntermediateFields(E,F) : K in M}
by lat10;
now let H be Element of Psi.M;
H in Psi.M; then
consider K1 being Element of IntermediateFields(E,F) such that
C: H = Aut(E,K1) & K1 in M by B;
K is Subfield of K1 by C,GALOIS_0:16;
hence H is Subgroup of Aut(E,K) by C,GALOIS_1:19;
end;
then \/(Psi.M) is Subgroup of Aut(E,K) by A,GALOIS_0:12;
hence \/(Psi.M) is Subgroup of Aut(E,/\M) by GALOIS_1:7;
end;
theorem lat14:
for F being Field
for E being FieldExtension of F
for M being non empty Subset of Subgroups Aut(E,F)
holds Fix(E,\/M) is Subfield of /\(Phi.M) & \/(Phi.M) is Subfield of Fix(E,/\M)
proof
let F be Field, E be FieldExtension of F;
let M be non empty Subset of Subgroups Aut(E,F);
\/M in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G = \/M as SubGroup of Aut(E,F) by GALOIS_0:def 10;
Fix(E,G) in IntermediateFields(E,F) by GALOIS_0:def 5; then
A: Fix(E,G) is Subfield of E by FIELD_14:4;
B: Phi.M = {Fix(E,G) where G is Element of Subgroups Aut(E,F) : G in M}
by lat11;
now let K1 be Element of Phi.M;
K1 in Phi.M; then
consider G1 being Element of Subgroups Aut(E,F) such that
C: K1 = Fix(E,G1) & G1 in M by B;
D: G1 is Subgroup of Aut(E) & G is Subgroup of Aut(E) by GROUP_2:56;
G1 is Subgroup of G by C,GALOIS_0:11;
hence Fix(E,G) is Subfield of K1 by C,D,GALOIS_1:20;
end;
hence Fix(E,\/M) is Subfield of /\(Phi.M) by A,GALOIS_0:17;
/\M in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G = /\M as SubGroup of Aut(E,F) by GALOIS_0:def 10;
Fix(E,G) in IntermediateFields(E,F) by GALOIS_0:def 5; then
Fix(E,G) is Subfield of E by FIELD_14:4; then
A: Fix(E,G) in SubFields(E) by FIELD_12:45;
B: Phi.M = {Fix(E,G) where G is Element of Subgroups Aut(E,F) : G in M}
by lat11;
now let K1 be Element of Phi.M;
K1 in Phi.M; then
consider G1 being Element of Subgroups Aut(E,F) such that
C: K1 = Fix(E,G1) & G1 in M by B;
D: G1 is Subgroup of Aut(E) & G is Subgroup of Aut(E) by GROUP_2:56;
G is Subgroup of G1 by C,GALOIS_0:9;
hence K1 is Subfield of Fix(E,G) by C,D,GALOIS_1:20;
end;
hence \/(Phi.M) is Subfield of Fix(E,/\M) by A,GALOIS_0:19;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for M being non empty Subset of IntermediateFields(E,F)
holds Aut(E,\/M) = /\(Psi.M) & Aut(E,/\M) = \/(Psi.M)
proof
let F be Field, E be F-finite GaloisExtension of F;
let M be non empty Subset of IntermediateFields(E,F);
set G = Aut(E,F);
reconsider K1 = Fix(E,/\(Psi.M)),
K2 = \/M as IntermediateField of E,F by GALOIS_0:21;
A: Aut(E,\/M) is Subgroup of /\(Psi.M) by lat12;
\/(Phi.(Psi.M)) is Subfield of K1 by lat14; then
\/M is Subfield of K1 by lathh1; then
Aut(E,K1) is Subgroup of Aut(E,K2) by GALOIS_1:19; then
C: Aut(E,K1) is Subgroup of Aut(E,\/M) by GALOIS_1:7;
D: Aut(E,K1) is Subgroup of Aut(E,F) by GALOIS_1:18; then
Aut(E,K1) in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G1 = Aut(E,K1) as SubGroup of Aut(E,F) by D,GALOIS_0:def 10;
/\(Psi.M) in Subgroups G by GROUP_3:def 1; then
reconsider G2 = /\(Psi.M) as SubGroup of G by GALOIS_0:def 10;
Aut(E,K1) = G2 by G2 .= /\(Psi.M);
hence Aut(E,\/M) = /\(Psi.M) by A,C,GROUP_2:55;
reconsider K1 = Fix(E,\/(Psi.M)),
K2 = /\M as IntermediateField of E,F by GALOIS_0:20;
A: \/(Psi.M) is Subgroup of Aut(E,/\M) by lat12;
K1 is Subfield of /\(Phi.(Psi.M)) by lat14; then
K1 is Subfield of /\M by lathh1; then
Aut(E,K2) is Subgroup of Aut(E,K1) by GALOIS_1:19; then
C: Aut(E,/\M) is Subgroup of Aut(E,K1) by GALOIS_1:7;
\/(Psi.M) in Subgroups G by GROUP_3:def 1; then
reconsider G2 = \/(Psi.M) as SubGroup of G by GALOIS_0:def 10;
Aut(E,K1) = G2 by G2 .= \/(Psi.M);
hence Aut(E,/\M) = \/(Psi.M) by A,C,GROUP_2:55;
end;
theorem
for F being Field
for E being F-finite GaloisExtension of F
for M being non empty Subset of Subgroups Aut(E,F)
holds Fix(E,\/M) = /\(Phi.M) & Fix(E,/\M) = \/(Phi.M)
proof
let F be Field, E be F-finite GaloisExtension of F;
let M be non empty Subset of Subgroups Aut(E,F);
reconsider K1 = Fix(E,\/M),
K2 = /\(Phi.M) as IntermediateField of E,F by GALOIS_0:20;
\/(Psi.(Phi.M)) is Subgroup of Aut(E,/\(Phi.M)) by lat12; then
\/M is Subgroup of Aut(E,/\(Phi.M)) by lathh2; then
\/M is Subgroup of Aut(E,K2) by GALOIS_1:7; then
Fix(E,Aut(E,K2)) is Subfield of Fix(E,\/M) by GALOIS_1:20;
then Fix(E,\/M) == /\(Phi.M) by G1,lat14;
hence Fix(E,\/M) = /\(Phi.M);
reconsider K1 = Fix(E,/\M),
K2 = \/(Phi.M) as IntermediateField of E,F by GALOIS_0:21;
B: /\M is Subgroup of Aut(E) by GROUP_2:56;
Aut(E,\/(Phi.M)) is Subgroup of /\(Psi.(Phi.M)) by lat12; then
Aut(E,\/(Phi.M)) is Subgroup of /\M by lathh2; then
Aut(E,K2) is Subgroup of /\M by GALOIS_1:7; then
Fix(E,/\M) is Subfield of Fix(E,Aut(E,K2)) by B,GALOIS_1:20;
then Fix(E,/\M) == \/(Phi.M) by G1,lat14;
hence Fix(E,/\M) = \/(Phi.M);
end;