:: The Galois Connection between IntermediateFields(E,F) and Subgroups of
:: Aut(E,F)
:: 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,
TOPGEN_1, MESFUNC1, RLSUB_2, CAT_1, PRELAMB, EC_PF_1, HURWITZ, CARD_1,
WELLORD1, RING_2, FUNCT_1, FUNCT_2, RELAT_1, NUMBERS, POLYNOM5, FOMODEL1,
FIELD_14, XCMPLX_0, RLVECT_5, FINSEQ_1, YELLOW_8, FUNCT_7, ARYTM_1,
FIELD_4, QUOFIELD, C0SP1, SIN_COS, XBOOLE_0, XXREAL_0, GLIB_000,
ORDINAL1, POLYNOM2, REALSET1, GROUP_4, POLYNOM1, MCART_1, FIELD_6, NAT_1,
UPROOTS, FIELD_8, GROUP_1, MOD_4, ALGNUM_1, ALGSTR_0, LATTICE3, FINSET_1,
CONLAT_1, WAYBEL_0, WAYBEL_1, NEWTON, GROUP_2, CATALG_1, BINOP_1,
MONOID_0, FIELD_13, FIELD_15, AUTGROUP, PEPIN, GROUP_3, GROUP_6, GROUP_9,
PRE_POLY, FUNCT_4, FUNCOP_1, PARTFUN1, MSSUBFAM, ORDERS_1, ORDERS_2,
CAYLEY, LATTICES, FILTER_1, ZFMISC_1, GALOIS_0, GALOIS_1, GALOIS_2,
GALOIS_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, FINSET_1,
REALSET1, XTUPLE_0, FUNCT_1, FUNCT_2, BINOP_1, ORDINAL1, FUNCOP_1,
NUMBERS, CARD_1, PARTFUN1, FUNCT_4, XCMPLX_0, XXREAL_0, RECDEF_1,
FUNCT_7, ORDERS_1, ORDERS_2, INT_1, FINSEQ_1, PRE_POLY, POLYNOM1,
POLYNOM2, POLYNOM3, UPROOTS, MONOID_0, BINOM, ALGNUM_1, WAYBEL_0,
WAYBEL_1, LATTICE3, CONLAT_1, MOD_4, STRUCT_0, ALGSTR_0, GROUP_1,
GROUP_2, GROUP_3, GROUP_4, GROUP_6, MATRLIN, LATTICES, HURWITZ, C0SP1,
EC_PF_1, VECTSP_1, RATFUNC1, CAYLEY, RING_2, RING_4, RING_5, FIELD_4,
FIELD_6, FIELD_7, FIELD_8, FIELD_11, FIELD_13, FIELD_14, FIELD_15,
GALOIS_0, GALOIS_1, GALOIS_2;
constructors FUNCT_7, NAT_D, POLYNOM2, RECDEF_1, BINOM, RINGCAT1, LATTICE3,
CONLAT_1, REALSET1, ALGNUM_1, GROUP_4, VECTSP_9, RING_5, CAYLEY, BINOP_2,
FIELD_2, FIELD_8, FIELD_11, FIELD_13, FIELD_15, GALOIS_1, GALOIS_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XXREAL_0, XREAL_0,
NAT_1, INT_1, MEMBERED, SUBSET_1, STRUCT_0, VECTSP_1, FINSET_1, FUNCT_2,
VECTSP_2, RLVECT_1, FUNCT_1, PARTFUN1, CARD_1, MOD_4, FINSEQ_1, RELAT_1,
XTUPLE_0, VALUED_0, LATTICE3, MONOID_0, GROUP_2, GR_CY_1, CAYLEY, RING_4,
RINGCAT1, PRE_POLY, POLYNOM1, POLYNOM2, POLYNOM3, FIELD_4, FIELD_6,
FIELD_7, FIELD_10, FIELD_12, FIELD_13, FIELD_15, FIELD_16, GALOIS_0,
GALOIS_1, GALOIS_2, GROUP_24;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions GROUP_1, TARSKI;
equalities XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, FUNCOP_1, FINSEQ_1, BINOM,
REALSET1, GALOIS_0, GALOIS_1;
expansions STRUCT_0, GROUP_1, VECTSP_1, TARSKI, GROUP_6, FUNCT_2, FINSEQ_1,
ORDINAL1, WAYBEL_1, MONOID_0, FIELD_7, FIELD_8, GALOIS_0, GALOIS_1;
theorems GROUP_1, VECTSP_1, FUNCOP_1, FUNCT_2, TARSKI, FUNCT_1, EC_PF_1,
UPROOTS, RING_5, ORDINAL1, XBOOLE_0, FIELD_4, FUNCT_7, ZFMISC_1, NAT_1,
BINOM, FIELD_6, CARD_2, FIELD_8, FINSEQ_1, GROUP_4, FIELD_5, FIELD_14,
GROUP_6, PARTFUN1, POLYNOM2, RELAT_1, XBOOLE_1, FUNCT_4, FIELD_13,
CARD_1, FIELD_7, GROUP_2, INT_1, XXREAL_0, ALGNUM_1, FIELD_12, XCMPLX_1,
POLYNOM1, LATTICE3, CAYLEY, WAYBEL_0, CONLAT_1, XTUPLE_0, GROUP_3, NAT_D,
POLYNOM3, FIELD_11, PRE_POLY, SUBSET_1, PBOOLE, BINOP_1, FIELD_15,
RING_2, ORDERS_2, FIELD_10, GALOIS_0, GALOIS_1, GALOIS_2;
schemes NAT_1, FUNCT_2, BINOP_1;
begin :: Preliminaries
definition
let F be Field;
let E be FieldExtension of F;
func SubgroupsAut E -> Lattice equals
lattice Aut(E,F);
coherence;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster -> E-functional for SubGroup of Aut(E,F);
coherence
proof
let G be SubGroup of Aut(E,F);
reconsider G1 = G as Subgroup of Aut(E,F);
G1 is E-functional;
hence thesis;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
let G be SubGroup of Aut(E,F);
cluster the carrier of G -> E-functional;
coherence;
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;
end;
bb0:
for F being Field
for E being FieldExtension of F
for K being E-extending FieldExtension of F
for a being Element of E
for b being Element of K st b = a
holds the carrier of RAdj(F,{a}) = the carrier of RAdj(F,{b})
proof
let R be Field, S be FieldExtension of R, T be S-extending FieldExtension of R;
let a be Element of S, b be Element of T;
assume AS: b = a;
S is (Polynom-Ring R)-homomorphic FieldExtension of R; then
A: the carrier of RAdj(R,{a}) =
the set of all Ext_eval(p,a) where p is Polynomial of R by FIELD_6:45;
T is (Polynom-Ring R)-homomorphic FieldExtension of R; then
B: the carrier of RAdj(R,{b}) =
the set of all Ext_eval(p,b) where p is Polynomial of R by FIELD_6:45;
C: now let o be object;
assume o in the carrier of RAdj(R,{a}); then
consider p being Polynomial of R such that
D1: o = Ext_eval(p,a) by A;
p is Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
then o = Ext_eval(p,b) by D1,AS,FIELD_7:14;
hence o in the carrier of RAdj(R,{b}) by B;
end;
now let o be object;
assume o in the carrier of RAdj(R,{b}); then
consider p being Polynomial of R such that
D1: o = Ext_eval(p,b) by B;
p is Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
then o = Ext_eval(p,a) by D1,AS,FIELD_7:14;
hence o in the carrier of RAdj(R,{a}) by A;
end;
hence thesis by C,TARSKI:2;
end;
theorem bb1:
for F being Field
for E being FieldExtension of F
for K being E-extending FieldExtension of F
for a being Element of E
for b being Element of K st b = a holds RAdj(F,{a}) = RAdj(F,{b})
proof
let R be Field, S be FieldExtension of R, T be S-extending FieldExtension of R;
let a be Element of S, b be Element of T;
assume AS: b = a;
S is Subring of T by FIELD_4:def 1;
then RAdj(R,{a}) is Subring of T by ALGNUM_1:1;
hence thesis by AS,bb0,FIELD_6:14;
end;
bba:
for F being Field
for E being FieldExtension of F
for K being E-extending FieldExtension of F
for a being F-algebraic Element of E
for b being F-algebraic Element of K st b = a
holds the carrier of FAdj(F,{a}) = the carrier of FAdj(F,{b})
proof
let F be Field;
let E be FieldExtension of F, K being E-extending FieldExtension of F;
let a be F-algebraic Element of E, b be F-algebraic Element of K;
assume AS: b = a;
A: K is (Polynom-Ring F)-homomorphic FieldExtension of F;
E is (Polynom-Ring F)-homomorphic FieldExtension of F; then
FAdj(F,{a}) = RAdj(F,{a}) by FIELD_6:56
.= RAdj(F,{b}) by AS,bb1 .= FAdj(F,{b}) by A,FIELD_6:56;
hence thesis;
end;
theorem abc:
for F being Field
for E being FieldExtension of F
for K being E-extending FieldExtension of F
for a being F-algebraic Element of E
for b being F-algebraic Element of K st b = a holds FAdj(F,{a}) = FAdj(F,{b})
proof
let F be Field;
let E be FieldExtension of F, K be E-extending FieldExtension of F;
let a be F-algebraic Element of E, b be F-algebraic Element of K;
assume AS: b = a;
E is Subfield of K by FIELD_4:7;
then FAdj(F,{a}) is Subfield of K by EC_PF_1:5;
hence thesis by AS,bba,EC_PF_1:8;
end;
lemTH2b:
for F being Field
for E being FieldExtension of F
for T being non empty finite F-algebraic Subset of E
for f,g being F-fixing Automorphism of FAdj(F,T)
st for a being Element of E st a in T holds f.a = g.a
for p being Polynomial of (card T),F
st (ex b being bag of (card T) st Support p = {b})
for x being T-evaluating Function of (card T),E
holds f.Ext_eval(p,x) = g.Ext_eval(p,x)
proof
let F be Field, E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E,
f,g be F-fixing Automorphism of FAdj(F,T);
assume AS1: for a being Element of E st a in T holds f.a = g.a;
let p be Polynomial of (card T),F;
assume AS2: ex b being bag of (card T) st Support p = {b};
let x be T-evaluating Function of (card T),E;
set n = card T, K = FAdj(F,T);
H1: K is Subring of E by FIELD_5:12;
D: now let a be Element of E, u be Nat;
assume D0: a in T;
T is Subset of FAdj(F,T) by FIELD_6:35; then
reconsider a1 = a as Element of K by D0;
defpred P[Nat] means f.(a|^$1) = g.(a|^$1);
f.(a|^0)
= f.(1_E) by BINOM:8
.= f.(1_K) by EC_PF_1:def 1
.= 1_K by GROUP_1:def 13
.= g.(1_K) by GROUP_1:def 13
.= g.(1_E) by EC_PF_1:def 1
.= g.(a|^0) by BINOM:8; then
IA: P[0];
IS: now let k be Nat;
assume P[k]; then
IV: f.(a|^k) = g.(a|^k) & f.a = g.a by D0,AS1;
k is Element of NAT by ORDINAL1:def 12; then
H2: a|^k = a1|^k by H1,FIELD_6:19; then
H3: (a|^k)*a = (a1|^k)*a1 by H1,FIELD_6:16;
f.(a|^(k+1)) = f.((a|^k)*(a|^1)) by BINOM:10
.= f.((a|^k)*a) by BINOM:8
.= g.(a1|^k) * g.a1 by H2,IV,H3,GROUP_6:def 6
.= g.((a|^k)*a) by H3,GROUP_6:def 6
.= g.((a|^k)*(a|^1)) by BINOM:8
.= g.(a|^(k+1)) by BINOM:10;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence f.(a|^u) = g.(a|^u);
end;
E: now let b be bag of n;
assume ex u being Nat st support b = {u}; then
consider u being Nat such that E1: support b = {u};
E2: u in support b by E1,TARSKI:def 1;
n = dom x by FUNCT_2:def 1; then
x.u in rng x by E2,FUNCT_1:def 3; then
reconsider a2 = x.u as Element of T by FIELD_13:def 4;
E2: u in support b by E1,TARSKI:def 1;
n = dom x by FUNCT_2:def 1; then
E3: x.u in rng x by E2,FUNCT_1:def 3;
rng x c= the carrier of E by RELAT_1:def 19; then
reconsider a1 = x.u as Element of E by E3;
reconsider e = b.u as Element of NAT;
E4: a2 in T;
f.eval(b,x) = f.(a1|^e) by E1,POLYNOM2:15
.= g.(a1|^e) by D,E4
.= g.eval(b,x) by E1,POLYNOM2:15;
hence f.eval(b,x) = g.eval(b,x);
end;
F: now let b be bag of n;
defpred P[Nat] means
for b being bag of n
st card(support b) = $1 holds f.eval(b,x) = g.eval(b,x);
G: P[0]
proof
now let b be bag of n;
assume G0: card(support b) = 0;
now let o be object;
assume o in n;
not o in support b by G0;
hence b.o = {} by PRE_POLY:def 7 .= (EmptyBag n).o by PBOOLE:5;
end; then
b = EmptyBag n by PBOOLE:def 10; then
G1: eval(b,x) = 1.E by POLYNOM2:14 .= 1_K by EC_PF_1:def 1;
hence f.eval(b,x) = eval(b,x) by GROUP_1:def 13
.= g.eval(b,x) by G1,GROUP_1:def 13;
end;
hence thesis;
end;
H: now let k be Nat;
assume IV: P[k];
now let b be bag of n;
assume B0: card(support b) = k+1;
set a = the Element of support b;
B3: support b <> {} by B0; then
B1: a in support b & support b c= dom b & dom b c= n by PRE_POLY:37;
then reconsider a as Element of n;
set b1 = b \ a; set b2 = ({a},b.a)-bag;
B2: support b1 = support b \ {a} by RING_5:29;
{a} c= support b by B1,TARSKI:def 1; then
card(support b1)
= card(support b) - card {a} by B2,CARD_2:44
.= (k + 1) - 1 by B0,CARD_2:42; then
B4: f.eval(b1,x) = g.eval(b1,x) by IV;
b.a <> 0 by B3,PRE_POLY:def 7; then
support b2 = {a} & n c= NAT by UPROOTS:8; then
B5: f.eval(b2,x) = g.eval(b2,x) by E;
B7: the carrier of FAdj(F,T) = the carrier of RAdj(F,T) by FIELD_13:40;
reconsider c1 = eval(b1,x) as Element of K by B7,FIELD_13:36;
reconsider c2 = eval(b2,x) as Element of K by B7,FIELD_13:36;
B6: f.(c1 * c2) = g.c1 * g.c2 by B4,B5,GROUP_6:def 6
.= g.(c1 * c2) by GROUP_6:def 6;
thus f.eval(b,x) = f.eval(b1 + b2,x) by RING_5:30
.= f.(eval(b1,x) * eval(b2,x)) by POLYNOM2:16
.= f.(c1 * c2) by H1,FIELD_6:16
.= g.(eval(b1,x) * eval(b2,x)) by B6,H1,FIELD_6:16
.= g.eval(b1 + b2,x) by POLYNOM2:16
.= g.eval(b,x) by RING_5:30;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(G,H);
ex k being Element of NAT st card(support b) = k;
hence f.eval(b,x) = g.eval(b,x) by I;
end;
consider b being bag of n such that A: Support p = {b} by AS2;
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
G: In(p.b,E) = p.b by SUBSET_1:def 8;
F is Subfield of K by FIELD_6:36; then
the carrier of F c= the carrier of K by EC_PF_1:def 1; then
reconsider a1 = p.b as Element of K;
the carrier of FAdj(F,T) = the carrier of RAdj(F,T) by FIELD_13:40; then
reconsider a2 = eval(b,x) as Element of K by FIELD_13:36;
D: g.a1 = In(p.b,E) by G,FIELD_8:def 2;
E: g.a2 = f.a2 by F;
thus g.Ext_eval(p,x) = g.(In(p.b,E) * eval(b,x)) by A,FIELD_11:18
.= g.(a1 * a2) by G,H1,FIELD_6:16
.= g.a1 * g.a2 by GROUP_6:def 6
.= f.a1 * f.a2 by D,E,G,FIELD_8:def 2
.= f.(a1 * a2) by GROUP_6:def 6
.= f.(In(p.b,E) * eval(b,x)) by G,H1,FIELD_6:16
.= f.Ext_eval(p,x) by A,FIELD_11:18;
end;
lemTH2a:
for F being Field
for E being FieldExtension of F
for T being non empty finite F-algebraic Subset of E
for f,g being F-fixing Automorphism of FAdj(F,T)
st for a being Element of E st a in T holds f.a = g.a
for p being Polynomial of (card T),F
for x being T-evaluating Function of (card T),E
holds f.Ext_eval(p,x) = g.Ext_eval(p,x)
proof
let F be Field, E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E,
f,g be F-fixing Automorphism of FAdj(F,T);
assume AS: for a being Element of E st a in T holds f.a = g.a;
let p1 be Polynomial of (card T),F, x be T-evaluating Function of (card T),E;
set n = card T, K = FAdj(F,T);
defpred P[Nat] means
for p being Polynomial of n,F st card(Support p) = $1
holds f.Ext_eval(p,x) = g.Ext_eval(p,x);
A: P[0]
proof
let p be Polynomial of n,F;
assume card(Support p) = 0; then
Support p = {}; then
A1: p = 0_(n,F) by FIELD_11:5;
hence f.Ext_eval(p,x)
= f.(0.E) by FIELD_11:16
.= f.(0.K) by FIELD_6:def 6
.= 0.K by RING_2:6
.= g.(0.K) by RING_2:6
.= g.(0.E) by FIELD_6:def 6
.= g.Ext_eval(p,x) by A1,FIELD_11:16;
end;
B: now let k be Nat;
assume A3: P[k];
A0: F is Subring of E by FIELD_4:def 1;
now let p be Polynomial of n,F;
assume
A4: card Support p = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by POLYNOM2:18;
then sgp <> {} by A4,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp);
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.F by POLYNOM1:def 4;
set m = 0_(n,F)+*(bg,p.bg);
set p9 = p+*(bg,0.F);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: p9 = p+*(bg.-->0.F) by FUNCT_7:def 3;
reconsider p9 as Function of Bags n,F;
for u being object holds u in Support p9 implies u in Support p
proof
let u be object;
assume
A10: u in Support p9;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
now
assume
A11: u = bg;
then u in dom(bg.-->0.F) by TARSKI:def 1;
then p9.u = (bg.-->0.F).bg by A9,A11,FUNCT_4:13;
then p9.u = 0.F by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in dom(bg.-->0.F) by TARSKI:def 1;
then p.u = p9.u by A9,FUNCT_4:11;
then p.u <> 0.F by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support p9 c= Support p;
then reconsider p9 as Polynomial of n,F by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support p9 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.F by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in dom(bg.-->0.F) by TARSKI:def 1;
then p9.u = p.u by A9,FUNCT_4:11;
then u in Support p9 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in dom(bg.-->0.F) by TARSKI:def 1;
then p9.bg = (bg.-->0.F).bg by A9,FUNCT_4:13;
then
A16: p9.bg = 0.F by FUNCOP_1:72;
then
A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object holds u in Support p9 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support p9 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support p9;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in dom(bg.-->0.F) by TARSKI:def 1;
then
A20: p9.u = p.u by A9,FUNCT_4:11;
p9.u <> 0.F by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support p9 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support p9) + 1 by A4,A17,CARD_2:41;
dom 0_(n,F) = Bags n by FUNCT_2:def 1;
then
A22: m = 0_(n,F)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider m as Function of Bags n,F;
A23: for u being object holds u in Support m implies u in {bg}
proof
let u be object;
assume
A24: u in Support m;
then reconsider u as Element of Bags n;
A25: m.u <> 0.F by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in dom(bg.-->p.bg) by TARSKI:def 1;
then m.u = 0_(n,F).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
A27: for u being object holds u in {bg} implies u in Support m
proof
let u be object;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: m.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then
Support m = {bg} by A23,TARSKI:2;
then reconsider m as Polynomial of n,F by POLYNOM1:def 5;
A28: for u being object st u in Bags n holds (p9+m).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: m.bg = p.bg by FUNCOP_1:72;
u in dom(bg.-->0.F) by A29,TARSKI:def 1;
then
A31: p9.u = (bg.-->0.F).bg by A9,A29,FUNCT_4:13;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= 0.F + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg;
hence thesis by A29;
end;
suppose
A32: u <> bg;
then
A33: not u in dom(bg.-->0.F) by TARSKI:def 1;
not u in dom(bg.-->p.bg) by A32,TARSKI:def 1;
then m.u = 0_(n,F).u by A22,FUNCT_4:11;
then
A34: m.u = 0.F by POLYNOM1:22;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= p.u by A9,A33,A34,FUNCT_4:11;
hence thesis;
end;
end;
A35: f.Ext_eval(m,x) = g.Ext_eval(m,x) by AS,A23,A27,TARSKI:2,lemTH2b;
A38: the carrier of FAdj(F,T) = the carrier of RAdj(F,T) by FIELD_13:40
.= the set of all Ext_eval(p,x) where p is Polynomial of (card T),F
by FIELD_13:39;
Ext_eval(m,x) in
the set of all Ext_eval(p,x) where p is Polynomial of (card T),F; then
reconsider a1 = Ext_eval(m,x) as Element of K by A38;
Ext_eval(p9,x) in
the set of all Ext_eval(p,x) where p is Polynomial of (card T),F; then
reconsider a2 = Ext_eval(p9,x) as Element of K by A38;
Ext_eval(p,x) in
the set of all Ext_eval(p,x) where p is Polynomial of (card T),F; then
reconsider a3 = Ext_eval(p,x) as Element of K by A38;
dom(p9 + m) = Bags n by FUNCT_2:def 1;
then
A37: Ext_eval(p,x) = Ext_eval(m+p9,x) by A12,A28,FUNCT_1:2
.= Ext_eval(m,x) + Ext_eval(p9,x) by A0,FIELD_11:19;
K is Subring of E by FIELD_5:12; then
A36: a1 + a2 = a3 by A37,FIELD_6:15;
hence f.Ext_eval(p,x) = f.a1 + f.a2 by VECTSP_1:def 20
.= g.a1 + g.a2 by A3,A21,A35
.= g.Ext_eval(p,x) by A36,VECTSP_1:def 20;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
ex k being Element of NAT st card(Support p1) = k;
hence thesis by I;
end;
theorem TH2a:
for F being Field
for E being FieldExtension of F
for T being non empty finite F-algebraic Subset of E
for f,g being F-fixing Automorphism of FAdj(F,T)
st for a being Element of E st a in T holds f.a = g.a holds f = g
proof
let F be Field, E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E,
f,g be F-fixing Automorphism of FAdj(F,T);
assume AS: for a being Element of E st a in T holds f.a = g.a;
set x = the T-evaluating Function of (card T),E;
A: the carrier of FAdj(F,T) = the carrier of RAdj(F,T) by FIELD_13:40
.= the set of all Ext_eval(p,x) where p is Polynomial of (card T),F
by FIELD_13:39;
now let a be Element of the carrier of FAdj(F,T);
a in the set of all Ext_eval(p,x) where p is Polynomial of (card T),F by A;
then consider p being Polynomial of (card T),F such that
B: a = Ext_eval(p,x);
thus f.a = g.a by B,AS,lemTH2a;
end;
hence thesis;
end;
theorem
for F being Field
for E being FieldExtension of F
for T being non empty finite F-algebraic Subset of E
for f,g being F-fixing Automorphism of FAdj(F,T) holds f = g iff f|T = g|T
proof
let F be Field, E be FieldExtension of F;
let T be non empty finite F-algebraic Subset of E;
let f,g be F-fixing Automorphism of FAdj(F,T);
now assume A: f|T = g|T;
now let a be Element of E;
assume B: a in T;
hence f.a = (g|T).a by A,FUNCT_1:49 .= g.a by B,FUNCT_1:49;
end;
hence f = g by TH2a;
end;
hence thesis;
end;
theorem lempr:
for F being Field
for E being F-finite FieldExtension of F
holds E is F-simple iff IntermediateFields(E,F) is finite
proof
let F be Field, E be F-finite FieldExtension of F;
per cases;
suppose F is infinite;
hence thesis by FIELD_14:76;
end;
suppose F is finite;
hence thesis;
end;
end;
lemBB:
for F1,F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for f being F1-fixing Automorphism of E1
st E1 == E2 & F1 == F2 holds f is F2-fixing Automorphism of E2
proof
let F1,F2 be Field, E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let f be F1-fixing Automorphism of E1;
assume AS: E1 == E2 & F1 == F2; then
reconsider g = f as Function of E2,E2;
A: g is F2-fixing by AS,FIELD_8:def 2;
now let a2,b2 be Element of E2;
reconsider a1 = a2, b1 = b2 as Element of E1 by AS;
a1 + b1 = a2 + b2 by AS;
hence g.(a2+b2) = f.a1 + f.b1 by VECTSP_1:def 20
.= g.a2 + g.b2 by AS;
a1 * b1 = a2 * b2 by AS;
hence g.(a2*b2) = f.a1 * f.b1 by GROUP_6:def 6
.= g.a2 * g.b2 by AS;
end; then
B: g is additive multiplicative;
g.(1_E2) = 1_E1 by AS,GROUP_1:def 13 .= 1_E2 by AS; then
g is unity-preserving;
hence thesis by A,B,AS;
end;
lemBF:
for F1,F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for f being Automorphism of E1
st E1 == E2 & F1 == F2 holds f is Automorphism of E2
proof
let F1,F2 be Field, E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let f be Automorphism of E1;
assume AS: E1 == E2; then
reconsider g = f as Function of E2,E2;
now let a2,b2 be Element of E2;
reconsider a1 = a2, b1 = b2 as Element of E1 by AS;
a1 + b1 = a2 + b2 by AS;
hence g.(a2+b2) = f.a1 + f.b1 by VECTSP_1:def 20
.= g.a2 + g.b2 by AS;
a1 * b1 = a2 * b2 by AS;
hence g.(a2*b2) = f.a1 * f.b1 by GROUP_6:def 6
.= g.a2 * g.b2 by AS;
end; then
B: g is additive multiplicative;
g.(1_E2) = 1_E1 by AS,GROUP_1:def 13 .= 1_E2 by AS; then
g is unity-preserving;
hence thesis by B,AS;
end;
lemBE:
for F1,F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
st E1 == E2 & F1 == F2 holds Aut(E1) = Aut(E2)
proof
let F1,F2 be Field, E1 be FieldExtension of F1, E2 be FieldExtension of F2;
assume A: E1 == E2 & F1 == F2;
B: now let o be object;
assume o in Auts(E1); then
consider f being Automorphism of E1 such that C: o = f;
f is Automorphism of E2 by A,lemBF;
hence o in Auts(E2) by C;
end;
G: now let o be object;
assume o in Auts(E2); then
consider f being Automorphism of E2 such that C: o = f;
f is Automorphism of E1 by A,lemBF;
hence o in Auts(E1) by C;
end;
then C: Auts(E1) = Auts(E2) by B,TARSKI:2;
now let o be object;
assume o in [:Auts(E1),Auts(E1):]; then
consider x,y being object such that
D: x in Auts(E1) & y in Auts(E1) & o = [x,y] by ZFMISC_1:def 2;
consider f1 being Automorphism of E1 such that E: x = f1 by D;
consider g1 being Automorphism of E1 such that F: y = g1 by D;
consider f2 being Automorphism of E2 such that G: x = f2 by C,D;
consider g2 being Automorphism of E2 such that H: y = g2 by C,D;
thus (AutComp E1).o = (AutComp E1).(f1,g1) by D,E,F
.= f2 * g2 by E,F,G,H,GALOIS_1:def 2
.= (AutComp E2).(f2,g2) by GALOIS_1:def 2
.= (AutComp E2).o by D,G,H;
end;
then AutComp E1 = AutComp E2 by C;
hence Aut(E1) = Aut(E2) by G,B,TARSKI:2;
end;
theorem ThH:
for F1,F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
st E1 == E2 & F1 == F2 holds Aut(E1,F1) = Aut(E2,F2)
proof
let F1,F2 be Field, E1 be FieldExtension of F1, E2 be FieldExtension of F2;
assume A: E1 == E2 & F1 == F2;
B: now let o be object;
assume o in Auts(E1,F1); then
consider f being F1-fixing Automorphism of E1 such that C: o = f;
f is F2-fixing Automorphism of E2 by A,lemBB;
hence o in Auts(E2,F2) by C;
end;
C: now let o be object;
assume o in Auts(E2,F2); then
consider f being F2-fixing Automorphism of E2 such that C: o = f;
f is F1-fixing Automorphism of E1 by A,lemBB;
hence o in Auts(E1,F1) by C;
end;
Aut(E1,F1) is Subgroup of Aut(E2) by A,lemBE;
hence Aut(E1,F1) = Aut(E2,F2) by C,B,TARSKI:2,GROUP_2:59;
end;
lemB:
for F1,F2 being Field
for E1 being FieldExtension of F1, E2 being FieldExtension of F2
for p1 being Element of the carrier of Polynom-Ring F1
for p2 being Element of the carrier of Polynom-Ring F2
st E1 == E2 & F1 == F2 & p1 = p2 holds Roots(E1,p1) = Roots(E2,p2)
proof
let F1,F2 be Field;
let E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let p1 be Element of the carrier of Polynom-Ring F1;
let p2 be Element of the carrier of Polynom-Ring F2;
assume AS: E1 == E2 & F1 == F2 & p1 = p2;
A: Roots(E1,p1) = {a where a is Element of E1 : a is_a_root_of p1,E1}
by FIELD_4:def 4;
B: Roots(E2,p2) = {a where a is Element of E2 : a is_a_root_of p2,E2}
by FIELD_4:def 4;
reconsider q1 = p1 as Polynomial of F1;
reconsider q2 = p2 as Polynomial of F2;
C: now let o be object;
assume o in Roots(E1,p1); then
consider a1 being Element of E1 such that
C1: o = a1 & a1 is_a_root_of p1,E1 by A;
reconsider a2 = a1 as Element of E2 by AS;
Ext_eval(q2,a2) = Ext_eval(q1,a1) by AS,FIELD_12:42
.= 0.E1 by C1,FIELD_4:def 2
.= 0.E2 by AS; then
a2 is_a_root_of p2,E2 by FIELD_4:def 2;
hence o in Roots(E2,p2) by C1,B;
end;
now let o be object;
assume o in Roots(E2,p2); then
consider a2 being Element of E2 such that
C1: o = a2 & a2 is_a_root_of p2,E2 by B;
reconsider a1 = a2 as Element of E1 by AS;
Ext_eval(q1,a1) = Ext_eval(q2,a2) by AS,FIELD_12:42
.= 0.E2 by C1,FIELD_4:def 2
.= 0.E1 by AS; then
a1 is_a_root_of p1,E1 by FIELD_4:def 2;
hence o in Roots(E1,p1) by C1,A;
end;
hence thesis by C,TARSKI:2;
end;
begin :: On Symmetric Groups and Group Actions
definition
let X be set;
func SymmetricGroup(X) -> strict constituted-Functions multMagma means :Def2:
the carrier of it = permutations(X) &
for x,y being Element of it holds x * y = (x qua Function) * y;
existence
proof
set c = permutations(X);
defpred P[Element of c,Element of c,set] means $3 = $1 * $2;
A1: for x,y being Element of c ex z being Element of c st P[x,y,z]
proof
let x,y be Element of c;
reconsider f = x, g = y as Permutation of X by CAYLEY:1;
c = the set of all f where f is Permutation of X by CAYLEY:def 1;
then f*g in c;
hence thesis;
end;
consider F being BinOp of c such that
A2: for x,y being Element of c holds P[x,y,F.(x,y)] from BINOP_1:sch 3(A1);
set S = multMagma(#c,F#);
S is constituted-Functions;
then reconsider S as strict constituted-Functions multMagma;
take S;
thus the carrier of S = c;
let x,y be Element of S;
thus thesis by A2;
end;
uniqueness
proof
let A,B be strict constituted-Functions multMagma such that
A3: the carrier of A = permutations(X) and
A4: for x,y being Element of A holds x * y = x qua Function * y and
A5: the carrier of B = permutations(X) and
A6: for x,y being Element of B holds x * y = x qua Function * y;
now
let x,y be Element of A;
reconsider f = x, g = y as Element of B by A3,A5;
thus (the multF of A).(x,y) = x*y
.= x qua Function * y by A4
.= f*g by A6
.= (the multF of B).(x,y);
end;
hence thesis by A3,A5,BINOP_1:2;
end;
end;
notation
let X be set;
synonym SymGr(X) for SymmetricGroup(X);
end;
theorem Th5:
for X being set
for f being Element of SymGr(X) holds f is Permutation of X
proof
let X be set, f be Element of SymGr(X);
the carrier of SymGr(X) = permutations(X) by Def2;
hence thesis by CAYLEY:1;
end;
registration
let X be set;
cluster SymGr(X) -> non empty associative Group-like;
coherence
proof
H: permutations(X)
= the set of all f where f is Permutation of X by CAYLEY:def 1;
the carrier of SymGr(X) = permutations(X) by Def2;
hence SymGr(X) is non empty;
thus SymGr(X) is associative
proof
let x,y,z be Element of SymGr(X);
y*z = (y qua Function*z) by Def2;
hence x*(y*z) = x qua Function*(y qua Function*z) by Def2
.= x qua Function*y qua Function*z by RELAT_1:36
.= (x*y)qua Function*z by Def2
.= (x*y)*z by Def2;
end;
set e = id X;
e in permutations(X) by H;
then reconsider e as Element of SymGr(X) by Def2;
take e;
let h be Element of SymGr(X);
reconsider h1 = h as Permutation of X by Th5;
thus h * e = h1 * e by Def2
.= h by FUNCT_2:17;
thus e * h = e * h1 by Def2
.= h by FUNCT_2:17;
h1" in permutations(X) by H;
then reconsider g = h1" as Element of SymGr(X) by Def2;
take g;
thus h * g = h qua Function * g by Def2
.= e by FUNCT_2:61;
thus g * h = g qua Function * h by Def2
.= e by FUNCT_2:61;
end;
end;
theorem Th6:
for X being set holds 1_SymGr(X) = id X
proof
let X be set;
set e = id X;
permutations(X)
= the set of all f where f is Permutation of X by CAYLEY:def 1;
then e in permutations(X);
then reconsider e as Element of SymGr(X) by Def2;
now
let h be Element of SymGr(X);
reconsider h1 = h as Permutation of X by Th5;
thus h * e = h1 * e by Def2
.= h by FUNCT_2:17;
thus e * h = e * h1 by Def2
.= h by FUNCT_2:17;
end;
hence thesis by GROUP_1:4;
end;
theorem
for X being set, x being Element of SymGr(X) holds x" = x qua Function"
proof
let X be set, x be Element of SymGr(X);
reconsider f = x as Permutation of X by Th5;
permutations(X)
= the set of all f where f is Permutation of X by CAYLEY:def 1;
then f" in permutations(X);
then reconsider g = f" as Element of SymGr(X) by Def2;
A1: 1_SymGr(X) = id X by Th6;
x * g = x qua Function * g by Def2;
then
A2: x*g = id X by FUNCT_2:61;
g * x = g qua Function * x by Def2;
then g*x = id X by FUNCT_2:61;
hence thesis by A2,A1,GROUP_1:def 5;
end;
registration
let X be finite set;
cluster SymGr(X) -> finite;
coherence
proof
the carrier of SymGr(X) = permutations(X) by Def2;
hence thesis;
end;
end;
lemac1:
for G being Group, X being non empty set
ex f being Function of [:the carrier of G,X:],X
st for a being Element of X, g being Element of G holds f.(g,a) = a
proof
let G be Group, X be non empty set;
defpred P[object,object] means ex a,b being object st $1 = [a,b] & $2 = b;
A: for x being object st x in [:the carrier of G,X:]
ex y being object st y in X & P[x,y]
proof
let x be object;
assume x in [:the carrier of G,X:]; then
consider g,a being object such that
A1: g in the carrier of G & a in X & x = [g,a] by ZFMISC_1:def 2;
take a;
thus thesis by A1;
end;
consider f being Function of [:the carrier of G,X:],X such that
B: for x being object st x in [:the carrier of G,X:] holds P[x,f.x]
from FUNCT_2:sch 1(A);
take f;
now let a be Element of X, g be Element of G;
consider c,b being object such that
B1: [g,a] = [c,b] & f.[g,a] = b by B;
thus f.(g,a) = a by B1,XTUPLE_0:1;
end;
hence thesis;
end;
lemac2:
for G being Group, X being set
for f being Function of [:the carrier of G,X:], X
st for a being Element of X, g being Element of G holds f.(g,a) = a
for a being Element of X, g1,g2 being Element of the carrier of G
holds f.(g1,f.(g2,a)) = f.(g1*g2,a)
proof
let G be Group, X be set, f be Function of [:the carrier of G,X:],X;
assume A: for a being Element of X, g being Element of G holds f.(g,a) = a;
now let a be Element of X, g1,g2 be Element of the carrier of G;
thus f.(g1,f.(g2,a)) = f.(g1,a) by A .= a by A .= f.(g1*g2,a) by A;
end;
hence thesis;
end;
definition
let G be Group;
let X be set;
assume AS:X is non empty;
mode Action of G,X -> Function of [:the carrier of G,X:], X means :defAC:
(for a being Element of X holds it.(1_G,a) = a) &
(for a being Element of X, g1,g2 being Element of the carrier of G
holds it.(g1,it.(g2,a)) = it.(g1*g2,a));
existence
proof
consider f being Function of [:the carrier of G,X:], X such that
A: for a being Element of X, g being Element of G holds f.(g,a) = a
by AS,lemac1;
take f;
thus thesis by A,lemac2;
end;
end;
definition
let G be Group;
let X be set;
let A be Action of G,X;
attr A is faithful means
for g1,g2 being Element of G holds
(for x being Element of X holds A.(g1,x) = A.(g2,x)) implies g1 = g2;
attr A is free means
for g being Element of G holds
(ex x being Element of X st A.(g,x) = x) implies g = 1_G;
pred A acts_transitively_on X means
for a,b being Element of X ex g being Element of G st A.(g,a) = b;
end;
definition
let G be Group;
let X be set;
pred G acts_on X means
ex f being Function of [:the carrier of G,X:], X st f is Action of G,X;
:: ex A being Action of G,X;
pred G acts_transitively_on X means
ex A being Action of G,X st A acts_transitively_on X;
end;
definition
let G be Group;
let X be non empty set;
func trivialAction(G,X) -> Action of G,X means :dtr:
for a being Element of X, g being Element of G holds it.(g,a) = a;
existence
proof
consider f being Function of [:the carrier of G,X:], X such that
A: for a being Element of X, g being Element of G holds f.(g,a) = a by lemac1;
B: for a being Element of X holds f.(1_G,a) = a by A;
for a being Element of X, g1,g2 being Element of the carrier of G
holds f.(g1,f.(g2,a)) = f.(g1*g2,a) by A,lemac2;
then reconsider f as Action of G,X by B,defAC;
take f;
thus thesis by A;
end;
uniqueness
proof
let f1,f2 be Action of G,X such that
A1: for a being Element of X, g being Element of G holds f1.(g,a) = a and
A2: for a being Element of X, g being Element of G holds f2.(g,a) = a;
for x being object st x in [:the carrier of G,X:] holds f1.x = f2.x
proof
let x be object;
assume x in [:the carrier of G,X:]; then
consider g,a being object such that
A3: g in the carrier of G & a in X & x = [g,a] by ZFMISC_1:def 2;
reconsider a as Element of X by A3;
reconsider g as Element of G by A3;
thus f1.x = f1.(g,a) by A3 .= a by A1 .= f2.(g,a) by A2 .= f2.x by A3;
end;
hence thesis;
end;
end;
registration
let G be non trivial Group;
let X be non empty set;
cluster trivialAction(G,X) -> non faithful;
coherence
proof
set A = trivialAction(G,X);
now assume A: for g1,g2 being Element of G holds g1 = g2;
now let o be object;
assume o in the carrier of G;
then o = 1_G by A;
hence o in {1_G} by TARSKI:def 1;
end; then
the carrier of G c= {1_G};
hence contradiction;
end; then
consider g1,g2 being Element of G such that A: g1 <> g2;
now assume B: A is faithful;
now let x being Element of X;
thus A.(g1,x) = x by dtr .= A.(g2,x) by dtr;
end;
hence contradiction by A,B;
end;
hence thesis;
end;
end;
registration
let G be trivial Group;
let X be non empty set;
cluster trivialAction(G,X) -> faithful;
coherence
proof
set A = trivialAction(G,X);
now let g1,g2 be Element of G;
assume for x being Element of X holds A.(g1,x) = A.(g2,x);
G is trivial iff the carrier of G = { 1_G } by TARSKI:def 1;
hence g1 = g2;
end;
hence thesis;
end;
end;
definition
let G be Group;
func regularAction G -> Action of G,the carrier of G means :dreg:
for g1,g2 being Element of G holds it.(g1,g2) = g1 * g2;
existence
proof
set X = the carrier of G;
defpred P[object,object] means
ex a,b being Element of G st $1 = [a,b] & $2 = a*b;
A: for x being object st x in [:X,X:]
ex y being object st y in X & P[x,y]
proof
let x be object;
assume x in [:X,X:]; then
consider a,g being object such that
A1: a in X & g in X & x = [a,g] by ZFMISC_1:def 2;
reconsider a,g as Element of G by A1;
take a * g;
thus thesis by A1;
end;
consider f being Function of [:X,X:],X such that
B: for x being object st x in [:X,X:] holds P[x,f.x]
from FUNCT_2:sch 1(A);
C: now let a be Element of X;
consider c,b being Element of G such that
C1: [1_G,a] = [c,b] & f.[1_G,a] = c * b by B;
thus f.(1_G,a) = (1_G) * a by C1 .= a by GROUP_1:def 4;
end;
now let a be Element of X, g1,g2 be Element of X;
consider c,b being Element of G such that
C1: [g2,a] = [c,b] & f.[g2,a] = c * b by B;
consider c,b being Element of G such that
C3: [g1,g2*a] = [c,b] & f.[g1,g2*a] = c * b by B;
C4: g1 * (g2 * a) = f.(g1,f.(g2,a)) by C1,C3;
consider c,b being Element of G such that
C5: [g1*g2,a] = [c,b] & f.[g1*g2,a] = c * b by B;
f.(g1*g2,a) = (g1 * g2) * a by C5;
hence f.(g1,f.(g2,a)) = f.(g1*g2,a) by C4,GROUP_1:def 3;
end; then
reconsider f as Action of G,X by C,defAC;
take f;
now let a be Element of X, g be Element of G;
consider c,b being Element of G such that
B1: [a,g] = [c,b] & f.[a,g] = c * b by B;
thus f.(a,g) = a * g by B1;
end;
hence thesis;
end;
uniqueness
proof
set X = the carrier of G;
let f1,f2 be Action of G,X such that
A1: for g,h being Element of G holds f1.(g,h) = g * h and
A2: for g,h being Element of G holds f2.(g,h) = g * h;
for x being object st x in [:X,X:] holds f1.x = f2.x
proof
let x be object;
assume x in [:X,X:]; then
consider g,a being object such that
A3: g in the carrier of G & a in the carrier of G & x = [g,a]
by ZFMISC_1:def 2;
reconsider a,g as Element of G by A3;
thus f1.x = f1.(g,a) by A3 .= g * a by A1 .= f2.(g,a) by A2 .= f2.x by A3;
end;
hence thesis;
end;
func conjugationAction G -> Action of G,the carrier of G means
for g1,g2 being Element of G holds it.(g1,g2) = g1 * g2 * g1";
existence
proof
set X = the carrier of G;
defpred P[object,object] means
ex a,b being Element of G st $1 = [a,b] & $2 = a*b*a";
A: for x being object st x in [:the carrier of G,X:]
ex y being object st y in X & P[x,y]
proof
let x be object;
assume x in [:X,X:]; then
consider g,a being object such that
A1: g in X & a in X & x = [g,a] by ZFMISC_1:def 2;
reconsider a,g as Element of G by A1;
take g * a * g";
thus thesis by A1;
end;
consider f being Function of [:X,the carrier of G:],X such that
B: for x being object st x in [:X,the carrier of G:] holds P[x,f.x]
from FUNCT_2:sch 1(A);
C: now let a be Element of X;
consider c,b being Element of G such that
C1: [1_G,a] = [c,b] & f.[1_G,a] = c * b * c" by B;
a = b & 1_G = c by C1,XTUPLE_0:1;
hence f.(1_G,a) = a * (1_G)" by C1,GROUP_1:def 4
.= a * (1_G) by GROUP_1:8
.= a by GROUP_1:def 4;
end;
now let a be Element of X, g,h be Element of the carrier of G;
consider c,b being Element of G such that
C1: [h,a] = [c,b] & f.[h,a] = c * b * c" by B;
C2: a = b & h = c by C1,XTUPLE_0:1;
consider c,b being Element of G such that
C3: [g,h*a*h"] = [c,b] & f.[g,h*a*h"] = c * b * c" by B;
h * a * h" = b & g = c by C3,XTUPLE_0:1; then
C4: f.(g,f.(h,a))
= g * (h * (a * h")) * g" by C1,C2,C3,GROUP_1:def 3
.= g * ((h * (a * h")) * g") by GROUP_1:def 3
.= g * (h * ((a * h") * g")) by GROUP_1:def 3
.= (g * h) * ((a * h") * g") by GROUP_1:def 3
.= (g * h) * (a * (h" * g")) by GROUP_1:def 3
.= (g * h) * a * (h" * g") by GROUP_1:def 3;
consider c,b being Element of G such that
C5: [g*h,a] = [c,b] & f.[g*h,a] = c * b * c" by B;
thus f.(g*h,a) = (g * h) * a * (g * h)" by C5,XTUPLE_0:1
.= f.(g,f.(h,a)) by C4,GROUP_1:17;
end; then
reconsider f as Action of G,X by C,defAC;
take f;
now let a be Element of X, g be Element of G;
consider c,b being Element of G such that
B1: [g,a] = [c,b] & f.[g,a] = c * b * c" by B;
thus f.(g,a) = g * a * g" by B1,XTUPLE_0:1;
end;
hence thesis;
end;
uniqueness
proof
set X = the carrier of G;
let f1,f2 be Action of G,X such that
A1: for g,h being Element of G holds f1.(g,h) = g * h * g" and
A2: for g,h being Element of G holds f2.(g,h) = g * h * g";
for x being object st x in [:X,X:] holds f1.x = f2.x
proof
let x be object;
assume x in [:X,X:]; then
consider g,a being object such that
A3: g in X & a in X & x = [g,a] by ZFMISC_1:def 2;
reconsider a,g as Element of G by A3;
thus f1.x = f1.(g,a) by A3 .= g * a * g" by A1
.= f2.(g,a) by A2 .= f2.x by A3;
end;
hence thesis;
end;
end;
registration
let G be Group;
cluster regularAction G -> free;
coherence
proof
set A = regularAction G;
now let g be Element of G;
assume ex x being Element of G st A.(g,x) = x; then
consider x being Element of G such that
B: A.(g,x) = x;
g * x = x by B,dreg;
hence g = 1_G by GROUP_1:7;
end;
hence thesis;
end;
end;
definition
let G be Group;
let X be non empty set;
let A be Action of G,X;
let g be Element of G;
func apply(A,g) -> Permutation of X means :defApp:
for a being Element of X holds it.a = A.(g,a);
existence
proof
defpred P[object,object] means
ex a being Element of X st $1 = a & $2 = A.(g,a);
A: for x being object st x in X
ex y being object st y in X & P[x,y]
proof
let x be object;
assume x in X; then
reconsider a = x as Element of X;
take A.(g,a);
thus thesis;
end;
consider f being Function of X,X such that
B: for x being object st x in X holds P[x,f.x] from FUNCT_2:sch 1(A);
defpred Q[object,object] means
ex a being Element of X st $1 = a & $2 = A.(g",a);
C: for x being object st x in X
ex y being object st y in X & Q[x,y]
proof
let x be object;
assume x in X; then
reconsider a = x as Element of X;
take A.(g",a);
thus thesis;
end;
consider h being Function of X,X such that
D: for x being object st x in X holds Q[x,h.x] from FUNCT_2:sch 1(C);
now let x be object;
assume x in X; then
reconsider a = x as Element of X;
consider b being Element of X such that
H1: b = a & h.a = A.(g",b) by D;
consider c being Element of X such that
H2: c = A.(g",a) & f.(A.(g",a)) = A.(g,c) by B;
thus (f * h).x = f.(A.(g",a)) by H1,FUNCT_2:15
.= A.(g*g",a) by H2,defAC
.= A.(1_G,a) by GROUP_1:def 5
.= (id X).x by defAC;
end; then
f * h = id X; then
E: f is onto by FUNCT_2:23;
now let x be object;
assume x in X; then
reconsider a = x as Element of X;
consider b being Element of X such that
H1: b = a & f.a = A.(g,b) by B;
consider c being Element of X such that
H2: c = A.(g,a) & h.(A.(g,a)) = A.(g",c) by D;
thus (h * f).x = h.(A.(g,a)) by H1,FUNCT_2:15
.= A.(g"*g,a) by H2,defAC
.= A.(1_G,a) by GROUP_1:def 5
.= (id X).x by defAC;
end; then
h * f = id X; then
f is one-to-one by FUNCT_2:23; then
reconsider f as Permutation of X by E;
take f;
now let a be Element of X;
consider b being Element of X such that H: b = a & f.a = A.(g,b) by B;
thus f.a = A.(g,a) by H;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Permutation of X such that
A1: for a being Element of X holds f1.a = A.(g,a) and
A2: for a being Element of X holds f2.a = A.(g,a);
for x being object st x in X holds f1.x = f2.x
proof
let x be object;
assume x in X; then
reconsider a = x as Element of X;
thus f1.x = A.(g,a) by A1 .= f2.x by A2;
end;
hence thesis;
end;
end;
definition
let G be Group;
let X be non empty set;
let A be Action of G,X;
func canHom A -> Function of G,SymGr(X) means :defHom:
for g being Element of G holds it.g = apply(A,g);
existence
proof
defpred P[object,object] means
ex g being Element of G st $1 = g & $2 = apply(A,g);
A: for x being object st x in the carrier of G
ex y being object st y in the carrier of SymGr(X) & P[x,y]
proof
let x be object;
assume x in the carrier of G; then
reconsider g = x as Element of G;
take apply(A,g);
the carrier of SymGr(X) = permutations(X) by Def2
.= the set of all f where f is Permutation of X by CAYLEY:def 1;
hence thesis;
end;
consider f being Function of the carrier of G,the carrier of SymGr(X)
such that
B: for x being object st x in the carrier of G holds P[x,f.x]
from FUNCT_2:sch 1(A);
take f;
now let g be Element of G;
P[g,f.g] by B;
hence f.g = apply(A,g);
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of G,SymGr(X) such that
A1: for g being Element of G holds f1.g = apply(A,g) and
A2: for g being Element of G holds f2.g = apply(A,g);
for x being object st x in the carrier of G holds f1.x = f2.x
proof
let x be object;
assume x in the carrier of G; then
reconsider g = x as Element of G;
thus f1.x = apply(A,g) by A1 .= f2.x by A2;
end;
hence thesis;
end;
end;
theorem app1:
for G being Group
for X being non empty set
for A being Action of G,X
for g1,g2 being Element of G holds apply(A,g1*g2) = apply(A,g1) * apply(A,g2)
proof
let G be Group, X be non empty set, A be Action of G,X;
let g1,g2 be Element of G;
set f = apply(A,g1*g2), f1 = apply(A,g1), f2 = apply(A,g2);
now let o be object;
assume o in X; then
reconsider a = o as Element of X;
thus f.o = A.(g1*g2,a) by defApp
.= A.(g1,A.(g2,a)) by defAC
.= A.(g1,f2.a) by defApp
.= f1.(f2.a) by defApp
.= (f1 * f2).o by FUNCT_2:15;
end;
hence thesis;
end;
registration
let G be Group;
let X be non empty set;
let A be Action of G,X;
cluster canHom A -> multiplicative;
coherence
proof
set f = canHom A, H = SymGr(X);
now let g1,g2 be Element of G;
A: the carrier of H = permutations(X) by Def2
.= the set of all f where f is Permutation of X by CAYLEY:def 1;
apply(A,g1) in the set of all f where f is Permutation of X &
apply(A,g2) in the set of all f where f is Permutation of X; then
reconsider a = apply(A,g1), b = apply(A,g2) as Element of H by A;
f.g1 = a & f.g2 = b by defHom;
hence f.g1 * f.g2 = apply(A,g1) * apply(A,g2) by Def2
.= apply(A,g1*g2) by app1
.= f.(g1 * g2) by defHom;
end;
hence thesis;
end;
end;
theorem
for G being Group
for X being non empty set
for A being Action of G,X holds canHom A is Homomorphism of G,SymGr(X);
theorem
for G being Group
for X being non empty set holds
G acts_on X iff ex h being Function of G,SymGr(X) st h is multiplicative
:: iff ex h being Homomorphism of G,SymGr(X);
proof
let G be Group, X be non empty set;
A: now assume G acts_on X; then
consider A being Function of [:the carrier of G,X:],X such that
A1: A is Action of G,X;
reconsider A as Action of G,X by A1;
thus ex h being Function of G,SymGr(X) st h is multiplicative
proof
take canHom A;
thus thesis;
end;
end;
now assume ex h being Function of G,SymGr(X) st h is multiplicative; then
consider h being Function of G,SymGr(X) such that
B1: h is multiplicative;
reconsider h as Homomorphism of G,SymGr(X) by B1;
defpred P[object,object] means
ex g being Element of G, a being Element of X,
p being Permutation of X st h.g = p & $1 = [g,a] & $2 = p.a;
A: for x being object st x in [:the carrier of G,X:]
ex y being object st y in X & P[x,y]
proof
let x be object;
assume x in [:the carrier of G,X:]; then
consider g,a being object such that
A1: g in the carrier of G & a in X & x = [g,a] by ZFMISC_1:def 2;
reconsider a as Element of X by A1;
reconsider g as Element of G by A1;
H: the carrier of SymGr(X) = permutations(X) by Def2
.= the set of all f where f is Permutation of X by CAYLEY:def 1;
h.g in the carrier of SymGr(X); then
consider p being Permutation of X such that A2: p = h.g by H;
take p.a;
thus thesis by A1,A2;
end;
consider f being Function of [:the carrier of G,X:],X such that
B: for x being object st x in [:the carrier of G,X:] holds P[x,f.x]
from FUNCT_2:sch 1(A);
C: now let a be Element of X;
consider b being Element of G, c being Element of X,
p being Permutation of X such that
C1: p = h.b & [1_G,a] = [b,c] & f.[1_G,a] = p.c by B;
C2: a = c & b = 1_G by C1,XTUPLE_0:1;
h.(1_G) = 1_SymGr(X) by GROUP_6:31 .= id X by Th6;
hence f.(1_G,a) = a by C1,C2;
end;
now let a be Element of X, g1,g2 be Element of G;
consider b1 being Element of G, c1 being Element of X,
p1 being Permutation of X such that
C1: p1 = h.b1 & [g2,a] = [b1,c1] & f.[g2,a] = p1.c1 by B;
H1: a = c1 & b1 = g2 by C1,XTUPLE_0:1;
consider b2 being Element of G, c2 being Element of X,
p2 being Permutation of X such that
C3: p2 = h.b2 & [g1,p1.a] = [b2,c2] & f.[g1,p1.a] = p2.c2 by B;
C4: f.(g1,f.(g2,a)) = p2.(p1.a) by H1,C1,C3,XTUPLE_0:1;
consider b3 being Element of G, c3 being Element of X,
p3 being Permutation of X such that
C5: p3 = h.b3 & [g1*g2,a] = [b3,c3] & f.[g1*g2,a] = p3.c3 by B;
H3: p1 = h.g2 & p2 = h.g1 by C1,C3,XTUPLE_0:1;
C6: a = c3 & b3 = g1*g2 by C5,XTUPLE_0:1; then
p3 = h.g1 * h.g2 by C5,GROUP_6:def 6 .= p2 * p1 by H3,Def2;
hence f.(g1,f.(g2,a)) = f.(g1*g2,a) by C4,C5,C6,FUNCT_2:15;
end; then
f is Action of G,X by C,defAC;
hence G acts_on X;
end;
hence thesis by A;
end;
theorem TF0:
for G being Group
for X being non empty set
for A being Action of G,X holds
Ker(canHom A) = (1).G iff
for g being Element of G
st for x being Element of X holds A.(g,x) = x holds g = 1_G
proof
let G be Group, X be non empty set, A be Action of G,X;
B: now assume C: Ker(canHom A) = (1).G;
now let g be Element of G;
assume D: for x being Element of X holds A.(g,x) = x;
E: now let o be object;
assume o in X; then
reconsider x = o as Element of X;
thus apply(A,g).o = A.(g,x) by defApp .= (id X).o by D;
end;
(canHom A).g = apply(A,g) by defHom
.= id X by E
.= 1_SymGr(X) by Th6;
then g in Ker(canHom A) by GROUP_6:41;
then g in { 1_G } by C,GROUP_2:def 7;
hence g = 1_G by TARSKI:def 1;
end;
hence for g being Element of G
st for x being Element of X holds A.(g,x) = x holds g = 1_G;
end;
now assume C: for g being Element of G
st for x being Element of X holds A.(g,x) = x holds g = 1_G;
D: now let o be object;
assume o in the carrier of (1).G;
then o in {1_G} by GROUP_2:def 7;
then o = 1_G by TARSKI:def 1;
then o in Ker(canHom A) by GROUP_2:46;
hence o in the carrier of Ker(canHom A);
end;
now let o be object;
assume E: o in the carrier of Ker(canHom A);
the carrier of Ker(canHom A) =
{a where a is Element of G : (canHom A).a = 1_SymGr(X)}
by GROUP_6:def 9; then
consider g being Element of G such that
F: o = g & (canHom A).g = 1_SymGr(X) by E;
now let x be Element of X;
thus A.(g,x) = apply(A,g).x by defApp
.= ((canHom A).g).x by defHom
.= (id X).x by F,Th6
.= x;
end;
then g = 1_G by C;
then g in {1_G} by TARSKI:def 1;
hence o in the carrier of (1).G by F,GROUP_2:def 7;
end;
hence Ker(canHom A) = (1).G by D,TARSKI:2,GROUP_2:59;
end;
hence thesis by B;
end;
theorem TF2:
for G being Group
for X being non empty set
for A being Action of G,X
holds A is faithful iff canHom A is one-to-one
proof
let G be Group, X be non empty set, A be Action of G,X;
set f = canHom A;
B: now assume C: A is faithful;
now let x1,x2 be object;
assume D: x1 in the carrier of G & x2 in the carrier of G &
f.x1 = f.x2; then
reconsider g1 = x1, g2 = x2 as Element of G;
E: apply(A,g1) = (canHom A).g2 by D,defHom .= apply(A,g2) by defHom;
now let x be Element of X;
thus A.(g1,x) = apply(A,g2).x by E,defApp
.= A.(g2,x) by defApp;
end;
hence x1 = x2 by C;
end;
hence canHom A is one-to-one;
end;
now assume C: canHom A is one-to-one;
now let g1,g2 being Element of G;
assume D: for x being Element of X holds A.(g1,x) = A.(g2,x);
now let o be object;
assume o in X; then
reconsider x = o as Element of X;
thus apply(A,g1).o = A.(g1,x) by defApp
.= A.(g2,x) by D
.= apply(A,g2).o by defApp;
end;
then apply(A,g1) = apply(A,g2);
then (canHom A).g1 = apply(A,g2) by defHom
.= (canHom A).g2 by defHom;
hence g1 = g2 by C;
end;
hence A is faithful;
end;
hence thesis by B;
end;
theorem TF1:
for G being Group
for X being non empty set
for A being Action of G,X holds
A is faithful iff
for g being Element of G
st for x being Element of X holds A.(g,x) = x holds g = 1_G
proof
let G be Group, X be non empty set, A be Action of G,X;
B: now assume A is faithful;
then canHom A is one-to-one by TF2;
then Ker(canHom A) = (1).G by GROUP_6:56;
hence for g being Element of G st for x being Element of X
holds A.(g,x) = x holds g = 1_G by TF0;
end;
now assume for g being Element of G st for x being Element of X
holds A.(g,x) = x holds g = 1_G;
then Ker(canHom A) = (1).G by TF0;
then canHom A is one-to-one by GROUP_6:56;
hence A is faithful by TF2;
end;
hence thesis by B;
end;
registration
let G be Group;
let X be non empty set;
cluster free -> faithful for Action of G,X;
coherence
proof
let A be Action of G,X;
assume AS: A is free;
set x = the Element of X;
now let g be Element of G;
assume for x being Element of X holds A.(g,x) = x;
then A.(g,x) = x;
hence g = 1_G by AS;
end;
hence thesis by TF1;
end;
end;
theorem
for G being Group
ex H being Subgroup of SymmetricGroup(the carrier of G)
st H,G are_isomorphic
proof
let G be Group;
set A = regularAction G;
A: canHom A is one-to-one by TF2;
reconsider H = Image(canHom A) as Subgroup of SymGr(the carrier of G);
take H;
thus thesis by A,GROUP_6:68;
end;
begin :: The Galois Connection between Intermediate Fields and Subgroups
definition
let F be Field;
let E be FieldExtension of F;
func Psi E -> Function of LattPOSet(IntermediateFields E),
LattPOSet(SubgroupsAut E) means :dA:
for K being IntermediateField of E,F holds it.K = Aut(E,K);
existence
proof
set L1 = LattPOSet(IntermediateFields E), L2 = LattPOSet(SubgroupsAut E);
set L3 = IntermediateFields E, L4 = SubgroupsAut E;
M: L3 = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
L1 = RelStr(#the carrier of L3,LattRel L3#) by LATTICE3:def 2;
N: 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;
defpred P[object,object] means
ex K being IntermediateField of E,F st $1 = K & $2 = Aut(E,K);
A: now let x be object;
assume C: x in the carrier of L1; then
consider K being strict Field such that
B: x = K & F is Subfield of K & K is Subfield of E by M,FIELD_14:def 1;
reconsider K as IntermediateField of E,F by B,C,M,GALOIS_0:def 5;
Aut(E,K) is Subgroup of Aut(E,F) by GALOIS_1:18; then
Aut(E,K) in Subgroups Aut(E,F) by GROUP_3:def 1;
hence ex y being object st y in the carrier of L2 & P[x,y] by B,N;
end;
consider f being Function of the carrier of L1, the carrier of L2
such that
B: for x being object st x in the carrier of L1 holds P[x,f.x]
from FUNCT_2:sch 1(A);
take f;
now let K be IntermediateField of E,F;
P[K,f.K] by B,M,GALOIS_0:def 5;
hence f.K = Aut(E,K);
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of LattPOSet(IntermediateFields E),
LattPOSet(SubgroupsAut E);
assume A: for K being IntermediateField of E,F holds f1.K = Aut(E,K);
assume B: for K being IntermediateField of E,F holds f2.K = Aut(E,K);
set P = LattPOSet(IntermediateFields E), L = IntermediateFields E;
M: L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
P = RelStr(#the carrier of L,LattRel L#) by LATTICE3:def 2;
now let o be object;
assume D: o in the carrier of LattPOSet(IntermediateFields E); then
consider K being strict Field such that
E: o = K & F is Subfield of K & K is Subfield of E by M,FIELD_14:def 1;
reconsider K as IntermediateField of E,F by M,D,E,GALOIS_0:def 5;
thus f1.o = Aut(E,K) by E,A .= f2.o by E,B;
end;
hence f1 = f2;
end;
func Phi E -> Function of LattPOSet(SubgroupsAut E),
LattPOSet(IntermediateFields E) means :dB:
for G being SubGroup of Aut(E,F) holds it.G = Fix(E,G);
existence
proof
defpred P[object,object] means
ex G being strict Subgroup of Aut(E) st $1 = G & $2 = Fix(E,G);
set L1 = LattPOSet(IntermediateFields E), L2 = LattPOSet(SubgroupsAut E);
set L3 = IntermediateFields E, L4 = SubgroupsAut E;
M: L3 = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
L1 = RelStr(#the carrier of L3,LattRel L3#) by LATTICE3:def 2;
N: 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;
A: now let x be object;
assume x in the carrier of L2; then
reconsider G = x as strict Subgroup of Aut(E,F) by N,GROUP_3:def 1;
reconsider G1 = G as Subgroup of Aut(E,F);
Fix(E,G1) is IntermediateField of E,F;
hence ex y being object st y in the carrier of L1 & P[x,y]
by M,GALOIS_0:def 5;
end;
consider f being Function of the carrier of L2,the carrier of L1
such that
B: for x being object st x in the carrier of L2 holds P[x,f.x]
from FUNCT_2:sch 1(A);
take f;
now let G be SubGroup of Aut(E,F);
P[G,f.G] by N,B,GALOIS_0:def 10;
hence f.G = Fix(E,G);
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of LattPOSet(SubgroupsAut E),
LattPOSet(IntermediateFields E);
assume A: for G being SubGroup of Aut(E,F) holds f1.G = Fix(E,G);
assume B: for G being SubGroup of Aut(E,F) holds f2.G = Fix(E,G);
set L2 = LattPOSet(SubgroupsAut E), L4 = SubgroupsAut E;
N: 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;
now let o be object;
assume C: o in the carrier of LattPOSet(SubgroupsAut E); then
o is Subgroup of Aut(E,F) by N,GROUP_3:def 1; then
reconsider G = o as SubGroup of Aut(E,F) by N,C,GALOIS_0:def 10;
thus f1.o = Fix(E,G) by A .= f2.o by B;
end;
hence f1 = f2;
end;
end;
theorem TH3:
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F
holds (Phi E).((Psi E).K) = Fix(E,Aut(E,K))
proof
let F be Field, E be FieldExtension of F, K be IntermediateField of E,F;
A: Aut(E,K) is Subgroup of Aut(E,F) by GALOIS_1:18; then
Aut(E,K) in Subgroups Aut(E,F) by GROUP_3:def 1; then
reconsider G = Aut(E,K) as SubGroup of Aut(E,F) by A,GALOIS_0:def 10;
thus (Phi E).((Psi E).K) = (Phi E).G by dA .= Fix(E,Aut(E,K)) by dB;
end;
theorem TH5:
for F being Field
for E being FieldExtension of F
for G being SubGroup of Aut(E,F) holds (Psi E).((Phi E).G) = Aut(E,Fix(E,G))
proof
let F be Field, E be FieldExtension of F, G be SubGroup of Aut(E,F);
reconsider K = Fix(E,G) as IntermediateField of E,F;
thus (Psi E).((Phi E).G) = (Psi E).K by dB .= Aut(E,Fix(E,G)) by dA;
end;
definition
let F be Field;
let E be FieldExtension of F;
func GalCon E -> Connection of LattPOSet(IntermediateFields E),
LattPOSet(SubgroupsAut E) equals
[Psi E, Phi E];
correctness;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster Psi E -> antitone;
coherence
proof
set L = IntermediateFields E;
set L1 = LattPOSet(IntermediateFields E), L2 = LattPOSet(SubgroupsAut E);
now let x,y be Element of L1;
assume A: x <= y;
let a,b be Element of L2;
assume B: a = (Psi E).x & b = (Psi E).y;
reconsider a1 = a, b1 = b as Element of the carrier of L2;
reconsider x1 = x, y1 = y as Element of the carrier of L1;
reconsider K1 = x1, K2 = y1 as IntermediateField of E,F;
I: a1 = Aut(E,K1) & b1 = Aut(E,K2) by B,dA;
K1 is Subfield of K2 by A,GALOIS_0:32; then
Aut(E,K2) is Subgroup of Aut(E,K1) by GALOIS_1:19;
hence a >= b by I,GALOIS_0:15;
end;
hence thesis by WAYBEL_0:def 5;
end;
cluster Phi E -> antitone;
coherence
proof
set L = SubgroupsAut E, G = Aut(E,F);
set L1 = LattPOSet(SubgroupsAut E), L2 = LattPOSet(IntermediateFields E);
now let x,y be Element of L1;
assume A: x <= y;
let a,b be Element of L2;
assume B: a = (Phi E).x & b = (Phi E).y;
reconsider a1 = a, b1 = b as Element of the carrier of L2;
reconsider x1 = x, y1 = y as Element of the carrier of L1;
M: L = LattStr(# Subgroups G, SubJoin G, SubMeet G #) &
L1 = RelStr(#the carrier of L,LattRel L#)
by LATTICE3:def 2,GROUP_4:def 12; then
reconsider G1 = x1, G2 = y1 as Subgroup of Aut(E,F) by GROUP_3:def 1;
reconsider G1s = G1, G2s = G2 as SubGroup of Aut(E,F) by M,GALOIS_0:def 10;
I1: Fix(E,G1s) = Fix(E,G1);
Fix(E,G2s) = Fix(E,G2); then
I: a1 = Fix(E,G1) & b1 = Fix(E,G2) by I1,B,dB;
G1 is Subgroup of G2 by A,GALOIS_0:15; then
Fix(E,G2) is Subfield of Fix(E,G1) by GALOIS_1:20;
hence a >= b by I,GALOIS_0:32;
end;
hence thesis by WAYBEL_0:def 5;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster GalCon E -> co-Galois;
coherence
proof
set P = LattPOSet(IntermediateFields E), R = LattPOSet(SubgroupsAut E),
f = Psi E, g = Phi E;
now let p1,p2 be Element of P, r1,r2 be Element of R;
reconsider q1 = p1 as Element of the carrier of P;
set L = IntermediateFields E;
M: L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
P = RelStr(#the carrier of L,LattRel L#) by LATTICE3:def 2; then
consider K1 being strict Field such that
H: p1 = K1 & F is Subfield of K1 & K1 is Subfield of E by FIELD_14:def 1;
reconsider K1 = p1 as IntermediateField of E,F by M,H,GALOIS_0:def 5;
reconsider H = Aut(E,K1) as Subgroup of Aut(E,F) by GALOIS_1:18;
Fix(E,H) is IntermediateField of E,F; then
reconsider q3 = Fix(E,Aut(E,K1)) as Element of the carrier of P
by M,GALOIS_0:def 5;
K1 is Subfield of Fix(E,Aut(E,K1)) by GALOIS_1:16; then
q1 <= q3 by GALOIS_0:32;
hence p1 <= g.(f.p1) by TH3;
reconsider q1 = r1 as Element of the carrier of R;
set L = SubgroupsAut E, G = Aut(E,F);
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; then
r1 is Subgroup of G by GROUP_3:def 1; then
reconsider G2 = r1 as SubGroup of G by M,GALOIS_0:def 10;
reconsider G1 = G2 as Subgroup of G;
reconsider K = Fix(E,G1) as IntermediateField of E,F;
D: Aut(E,K) is Subgroup of Aut(E,F) by GALOIS_1:18;
reconsider q3 = Aut(E,Fix(E,G1)) as Element of the carrier of R
by D,M,GROUP_3:def 1;
reconsider G3 = G1 as Subgroup of Aut(E);
G3 is Subgroup of Aut(E,Fix(E,G3)) by GALOIS_1:17; then
q1 <= q3 by GALOIS_0:15;
hence r1 <= f.(g.r1) by TH5;
end;
hence thesis by CONLAT_1:def 7;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
func ClosedFields E -> Subset of LattPOSet(IntermediateFields E) equals
Closed(Phi E);
correctness;
func ClosedGroups E -> Subset of LattPOSet(SubgroupsAut E) equals
Closed(Psi E);
correctness;
end;
CLFG:
for F being Field
for E being FieldExtension of F
holds ClosedFields E c= IntermediateFields(E,F) &
ClosedGroups E c= Subgroups Aut(E,F)
proof
let F be Field, E be FieldExtension of F;
LattPOSet(IntermediateFields E)
= RelStr(#the carrier of (IntermediateFields E),
LattRel (IntermediateFields E)#) by LATTICE3:def 2;
hence ClosedFields E c= IntermediateFields(E,F);
H: SubgroupsAut E = LattStr (# Subgroups Aut(E,F), SubJoin Aut(E,F),
SubMeet Aut(E,F) #) by GROUP_4:def 12;
LattPOSet(SubgroupsAut E)
= RelStr(#the carrier of (SubgroupsAut E),LattRel (SubgroupsAut E)#)
by LATTICE3:def 2;
hence thesis by H;
end;
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;
now 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
rng d1 c= Closed d; 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;
lemClFd:
for F being Field
for E being FieldExtension of F
ex f being Function of (ClosedFields E),(ClosedGroups E)
st f = (Psi E)|(ClosedFields E) & f is bijective
proof
let F be Field, E be FieldExtension of F;
GalCon E is co-Galois;
then Restr(Psi E,Phi E) is bijective by lemCl;
hence thesis;
end;
lemClGr:
for F being Field
for E being FieldExtension of F
ex f being Function of (ClosedGroups E),(ClosedFields E)
st f = (Phi E)|(ClosedGroups E) & f is bijective
proof
let F be Field, E be FieldExtension of F;
GalCon E is co-Galois;
then Restr(Phi E,Psi E) is bijective by lemCl;
hence thesis;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster ClosedFields E -> non empty (ClosedGroups E)-bijective;
coherence
proof
ex f being Function of (ClosedGroups E),(ClosedFields E)
st f = (Phi E)|(ClosedGroups E) & f is bijective by lemClGr;
hence thesis;
end;
cluster ClosedGroups E -> non empty (ClosedFields E)-bijective;
coherence
proof
ex f being Function of (ClosedFields E),(ClosedGroups E)
st f = (Psi E)|(ClosedFields E) & f is bijective by lemClFd;
hence thesis;
end;
end;
theorem
for F being Field
for E being FieldExtension of F holds
(Psi E)|(ClosedFields E) is a_Bijection of (ClosedFields E),(ClosedGroups E) &
((Psi E)|(ClosedFields E))" = (Phi E)|(ClosedGroups E)
proof
let F be Field, E be FieldExtension of F;
ex f being Function of (ClosedFields E),(ClosedGroups E)
st f = (Psi E)|(ClosedFields E) & f is bijective by lemClFd;
hence (Psi E)|(ClosedFields E) is
a_Bijection of (ClosedFields E),(ClosedGroups E) by GALOIS_0:def 2;
GalCon E is co-Galois; then
(Restr(Psi E,Phi E))" = Restr(Phi E,Psi E) by GALOIS_0:2;
hence thesis;
end;
theorem
for F being Field
for E being FieldExtension of F holds
(Phi E)|(ClosedGroups E) is a_Bijection of (ClosedGroups E),(ClosedFields E) &
((Phi E)|(ClosedGroups E))" = (Psi E)|(ClosedFields E)
proof
let F be Field, E be FieldExtension of F;
ex f being Function of (ClosedGroups E),(ClosedFields E)
st f = (Phi E)|(ClosedGroups E) & f is bijective by lemClGr;
hence (Phi E)|(ClosedGroups E) is
a_Bijection of (ClosedGroups E),(ClosedFields E) by GALOIS_0:def 2;
GalCon E is co-Galois; then
(Restr(Phi E,Psi E))" = Restr(Psi E,Phi E) by GALOIS_0:3;
hence thesis;
end;
theorem ThH1:
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F
holds K in ClosedFields E iff (Phi E).((Psi E).K) = K
proof
let F be Field, E be FieldExtension of F, K be IntermediateField of E,F;
set L = IntermediateFields E;
L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
LattPOSet L = RelStr(#the carrier of L,LattRel L#)
by LATTICE3:def 2; then
reconsider K1 = K as Element of LattPOSet(IntermediateFields E)
by GALOIS_0:def 5;
GalCon E is co-Galois; then
K1 in ClosedFields E iff (Phi E).((Psi E).K1) = K1 by GALOIS_0:4;
hence thesis;
end;
theorem ThH3:
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F
holds K in ClosedFields E iff Fix(E,Aut(E,K)) = K
proof
let F be Field, E be FieldExtension of F, K be IntermediateField of E,F;
A: now assume K in ClosedFields E;
then (Phi E).((Psi E).K) = K by ThH1;
hence Fix(E,Aut(E,K)) = K by TH3;
end;
now assume Fix(E,Aut(E,K)) = K;
then (Phi E).((Psi E).K) = K by TH3;
hence K in ClosedFields E by ThH1;
end;
hence thesis by A;
end;
theorem ThH2:
for F being Field
for E being FieldExtension of F
for G being SubGroup of Aut(E,F)
holds G in ClosedGroups E iff (Psi E).((Phi E).G) = G
proof
let F be Field, E be FieldExtension of F, G be SubGroup of Aut(E,F);
set L = SubgroupsAut E;
L = LattStr(#Subgroups Aut(E,F),SubJoin Aut(E,F),SubMeet Aut(E,F)#) &
LattPOSet L = RelStr(#the carrier of L,LattRel L#)
by GROUP_4:def 12,LATTICE3:def 2; then
reconsider G1 = G as Element of LattPOSet L by GALOIS_0:def 10;
GalCon E is co-Galois; then
G1 in ClosedGroups E iff (Psi E).((Phi E).G1) = G1 by GALOIS_0:5;
hence thesis;
end;
theorem ThH4:
for F being Field
for E being FieldExtension of F
for G being SubGroup of Aut(E,F)
holds G in ClosedGroups E iff Aut(E,Fix(E,G)) = G
proof
let F be Field, E be FieldExtension of F, G be SubGroup of Aut(E,F);
A: now assume G in ClosedGroups E;
then (Psi E).((Phi E).G) = G by ThH2;
hence Aut(E,Fix(E,G)) = G by TH5;
end;
now assume Aut(E,Fix(E,G)) = G;
then (Psi E).((Phi E).G) = G by TH5;
hence G in ClosedGroups E by ThH2;
end;
hence thesis by A;
end;
theorem TH7:
for F being Field
for E being FieldExtension of F
holds E is F-Galois iff the doubleLoopStr of F in ClosedFields E
proof
let F be Field, E be FieldExtension of F;
set L = the doubleLoopStr of F;
I0: L == F;
L is Subfield of F & F is Subfield of E by I0,FIELD_4:7; then
I2: L is Subfield of E by EC_PF_1:5; then
I3: L in IntermediateFields(E,F) by I0,FIELD_14:4;
reconsider L as IntermediateField of E,F by I3,GALOIS_0:def 5;
reconsider E1 = E as FieldExtension of L by I2,FIELD_4:7;
H: Aut(E,F) = Aut(E,L) by I0,ThH;
A: now assume the doubleLoopStr of F in ClosedFields E; then
(Phi E).((Psi E).L) = L by ThH1; then
Fix(E,Aut(E,F)) == F by H,TH3;
hence E is F-Galois;
end;
now assume E is F-Galois;
then Fix(E,Aut(E,F)) == F;
then (Phi E).((Psi E).L) = L by H,TH3;
hence the doubleLoopStr of F in ClosedFields E by ThH1;
end;
hence thesis by A;
end;
theorem TH8:
for F being Field
for E being F-finite FieldExtension of F
holds ClosedFields E = IntermediateFields(E,F) iff
the doubleLoopStr of F in ClosedFields E
proof
let F be Field, E be F-finite FieldExtension of F;
set L = the doubleLoopStr of F;
I0: L == F;
L is Subfield of F & F is Subfield of E by I0,FIELD_4:7; then
A: L is Subfield of E by EC_PF_1:5;
now assume the doubleLoopStr of F in ClosedFields E;
then reconsider E1 = E as F-finite GaloisExtension of F by TH7;
B: now let o be object;
set L = IntermediateFields E;
M: L = LattStr(#IntermediateFields(E,F),SubJoin E,SubMeet E#) &
LattPOSet L = RelStr(#the carrier of L,LattRel L#) by LATTICE3:def 2;
assume o in ClosedFields E;
hence o in IntermediateFields(E,F) by M;
end;
now let o be object;
assume B: o in IntermediateFields(E,F); 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 as IntermediateField of E1,F by B,C,GALOIS_0:def 5;
reconsider E2 = E1 as GaloisExtension of K by GALOIS_2:35;
D: Fix(E2,Aut(E2,K)) == K by GALOIS_1:def 18;
Aut(E1,K) = Aut(E2,K);
hence o in ClosedFields E by C,D,ThH3;
end;
hence ClosedFields E = IntermediateFields(E,F) by B,TARSKI:2;
end;
hence thesis by A,I0,FIELD_14:4;
end;
theorem ClInter:
for F being Field
for E being F-finite FieldExtension of F
holds E is GaloisExtension of F iff ClosedFields E = IntermediateFields(E,F)
proof
let F be Field, E be F-finite FieldExtension of F;
A: now assume E is F-Galois;
then the doubleLoopStr of F in ClosedFields E by TH7;
hence ClosedFields E = IntermediateFields(E,F) by TH8;
end;
now assume ClosedFields E = IntermediateFields(E,F);
then the doubleLoopStr of F in ClosedFields E by TH8;
hence E is GaloisExtension of F by TH7;
end;
hence thesis by A;
end;
begin :: The Order of Aut(E,F)
definition
let F be Field;
let E be FieldExtension of F;
func Action-Aut(E,F) -> Action of Aut(E,F),the carrier of E means :EF:
for a being Element of E
for g being Element of the carrier of Aut(E,F) holds it.(g,a) = g.a;
existence
proof
set X = the carrier of E, G = Aut(E,F);
defpred P[object,object] means
ex a being Element of X,
g being Element of the carrier of G st $1 = [g,a] & $2 = g.a;
A: for x being object st x in [:the carrier of G,X:]
ex y being object st y in X & P[x,y]
proof
let x be object;
assume x in [:the carrier of G,X:]; then
consider g,a being object such that
A1: g in the carrier of G & a in X & x = [g,a] by ZFMISC_1:def 2;
reconsider a as Element of X by A1;
reconsider g as Element of the carrier of G by A1;
take g.a;
thus thesis by A1;
end;
consider f being Function of [:the carrier of G,X:],X such that
B: for x being object st x in [:the carrier of G,X:] holds P[x,f.x]
from FUNCT_2:sch 1(A);
C: now let a be Element of X;
C1: 1_G = 1_Aut(E) by GROUP_2:44 .= id E by GALOIS_1:6;
consider a1 being Element of X,
g1 being Element of the carrier of G such that
C2: [1_G,a] = [g1,a1] & f.[1_G,a] = g1.a1 by B;
a1 = a & g1 = 1_G by C2,XTUPLE_0:1;
hence f.(1_G,a) = a by C1,C2;
end;
now let a be Element of X, g,h be Element of the carrier of G;
reconsider gh = g*h as Element of the carrier of G;
consider g1 being F-fixing Automorphism of E such that C1: g1 = g;
consider h1 being F-fixing Automorphism of E such that C2: h1 = h;
g1 in Auts(E,F) & h1 in Auts(E,F); then
H: [g1,h1] in [:Auts(E,F),Auts(E,F):] by ZFMISC_1:def 2;
C3: g * h = (AutComp E).(g1,h1) by C1,C2,H,FUNCT_1:49
.= g1 * h1 by GALOIS_1:def 2;
consider aa being Element of X,
gg being Element of the carrier of G such that
C4: [g*h,a] = [gg,aa] & f.[g*h,a] = gg.aa by B;
C5: aa = a & gg = g*h by C4,XTUPLE_0:1;
consider aa being Element of X,
gg being Element of the carrier of G such that
C6: [h,a] = [gg,aa] & f.[h,a] = gg.aa by B;
C7: aa = a & gg = h by C6,XTUPLE_0:1;
consider aa being Element of X,
gg being Element of the carrier of G such that
C8: [g,h.a] = [gg,aa] & f.[g,h.a] = gg.aa by B;
aa = h.a & gg = g by C8,XTUPLE_0:1;
hence f.(g,f.(h,a)) = f.(g*h,a) by C1,C2,C3,C4,C5,C6,C7,C8,FUNCT_2:15;
end; then
reconsider f as Action of Aut(E,F),the carrier of E by C,defAC;
take f;
now let a be Element of E, g be Element of the carrier of Aut(E,F);
consider a1 being Element of X,
g1 being Element of the carrier of G such that
H: [g,a] = [g1,a1] & f.[g,a] = g1.a1 by B;
a1 = a & g1 = g by H,XTUPLE_0:1;
hence f.(g,a) = g.a by H;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Action of Aut(E,F),the carrier of E such that
A1: for a being Element of E
for g being Element of the carrier of Aut(E,F) holds f1.(g,a) = g.a and
A2: for a being Element of E
for g being Element of the carrier of Aut(E,F) holds f2.(g,a) = g.a;
now let x be object;
assume x in [:the carrier of Aut(E,F),the carrier of E:]; then
consider g,a being object such that
A3: g in the carrier of Aut(E,F) & a in the carrier of E & x = [g,a]
by ZFMISC_1:def 2;
reconsider a as Element of the carrier of E by A3;
reconsider g as Element of the carrier of Aut(E,F) by A3;
thus f1.x = f1.(g,a) by A3 .= g.a by A1
.= f2.(g,a) by A2 .= f2.x by A3;
end;
hence thesis;
end;
end;
TH1:
for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of Polynom-Ring F
st Roots(E,p) <> {} holds
Action-Aut(E,F)|[:the carrier of Aut(E,F),Roots(E,p):]
is Action of Aut(E,F),Roots(E,p)
proof
let F be Field, E be FieldExtension of F;
let p be non zero Element of the carrier of Polynom-Ring F;
assume AS: Roots(E,p) <> {};
set A = Action-Aut(E,F), G = Aut(E,F), X = Roots(E,p);
set f = Action-Aut(E,F)|[:the carrier of G,X:];
[:the carrier of G,X:] c= [:the carrier of G,the carrier of E:]
by ZFMISC_1:96; then
[:the carrier of G,X:] c= dom A by FUNCT_2:def 1; then
H0: dom A /\ [:the carrier of G,X:] = [:the carrier of G,X:]
by XBOOLE_1:28; then
H1: dom f = [:the carrier of G,X:] by RELAT_1:61;
rng f c= X
proof let o be object;
assume o in rng f; then
consider x being object such that
H2: x in [:the carrier of G,X:] & f.x = o by H1,FUNCT_1:def 3;
consider g,a being object such that
H3: g in the carrier of G & a in X & x = [g,a] by H2,ZFMISC_1:def 2;
reconsider a as Element of E by H3;
reconsider g as Element of the carrier of G by H3;
[g,a] in dom f by H0,H2,H3,RELAT_1:61; then
f.(g,a) = A.(g,a) by FUNCT_1:47 .= g.a by EF;
hence o in X by H3,H2,FIELD_8:38;
end; then
reconsider f as Function of [:the carrier of G,X:],X by H1,FUNCT_2:2;
B: now let a be Element of X;
X c= the carrier of E; then
reconsider a1 = a as Element of E by AS;
[1_G,a] in [:the carrier of G,X:] by AS,ZFMISC_1:def 2;
hence f.(1_G,a) = A.(1_G,a1) by H1,FUNCT_1:47 .= a by defAC;
end;
now let a be Element of X, g1,g2 be Element of the carrier of G;
X c= the carrier of E; then
reconsider a1 = a as Element of E by AS;
[g2,a] in [:the carrier of G,X:] by AS,ZFMISC_1:def 2; then
B1: f.(g2,a) = A.(g2,a1) by H1,FUNCT_1:47; then
H2: f.(g2,a) = g2.a1 by EF;
a in Roots(E,p) by AS; then
g2.a in Roots(E,p) by FIELD_8:38; then
[g1,g2.a] in [:the carrier of G,X:] by ZFMISC_1:def 2; then
B2: f.(g1,g2.a) = A.(g1,A.(g2,a1)) by B1,H1,H2,FUNCT_1:47
.= A.(g1*g2,a1) by defAC;
[g1*g2,a] in [:the carrier of G,X:] by AS,ZFMISC_1:def 2;
hence f.(g1,f.(g2,a)) = f.(g1*g2,a) by H1,H2,B2,FUNCT_1:47;
end;
hence thesis by AS,B,defAC;
end;
definition
let F being Field;
let E being FieldExtension of F;
let p being non zero Element of the carrier of Polynom-Ring F;
assume AS:Roots(E,p) <> {};
func Action-Roots(E,p) -> Action of Aut(E,F),Roots(E,p) equals :dar:
Action-Aut(E,F)|[:the carrier of Aut(E,F),Roots(E,p):];
coherence by AS,TH1;
end;
theorem
for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of Polynom-Ring F
st Roots(E,p) <> {} holds Aut(E,F) acts_on Roots(E,p)
proof
let F be Field, E be FieldExtension of F;
let p be non zero Element of the carrier of Polynom-Ring F;
assume Roots(E,p) <> {}; then
Action-Aut(E,F)|[:the carrier of Aut(E,F),Roots(E,p):]
is Action of Aut(E,F),Roots(E,p) by TH1;
hence thesis;
end;
theorem
for F being Field
for p being irreducible Element of the carrier of Polynom-Ring F
for E being SplittingField of p
holds Aut(E,F) acts_transitively_on Roots(E,p)
proof
let F be Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
let E be SplittingField of p;
set G = Aut(E,F), X = Roots(E,p);
reconsider A = Action-Aut(E,F)|[:the carrier of G,X:] as Action of G,X by TH1;
now let a,b be Element of X;
reconsider a1 = a, b1 = b as Element of E;
consider h being F-fixing Automorphism of E such that
A: h.a1 = b1 by GALOIS_2:31;
h in the set of all f where f is F-fixing Automorphism of E; then
reconsider g = h as Element of the carrier of G;
take g;
[:the carrier of G,X:] c= [:the carrier of G,the carrier of E:]
by ZFMISC_1:96; then
[:the carrier of G,X:] c= dom Action-Aut(E,F) by FUNCT_2:def 1; then
dom Action-Aut(E,F) /\ [:the carrier of G,X:] = [:the carrier of G,X:]
by XBOOLE_1:28; then
B: dom A = [:the carrier of G,X:] by RELAT_1:61;
[g,a] in [:the carrier of G,X:];
hence A.(g,a) = Action-Aut(E,F).(g,a) by B,FUNCT_1:47 .= b by EF,A;
end;
then A acts_transitively_on X;
hence thesis;
end;
theorem TT:
for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of Polynom-Ring F
st Roots(E,p) <> {} & E == FAdj(F,Roots(E,p))
holds Action-Roots(E,p) is faithful
proof
let F be Field, E be FieldExtension of F;
let p be non zero Element of the carrier of Polynom-Ring F;
assume AS: Roots(E,p) <> {} & E == FAdj(F,Roots(E,p)); then
reconsider T = Roots(E,p) as non empty finite F-algebraic Subset of E;
reconsider A = Action-Roots(E,p) as Action of Aut(E,F),T;
set G = Aut(E,F), f = canHom A;
reconsider B = Action-Aut(E,F)|[:the carrier of G,T:] as Action of G,T by TH1;
[:the carrier of G,T:] c= [:the carrier of G,the carrier of E:]
by ZFMISC_1:96; then
[:the carrier of G,T:] c= dom Action-Aut(E,F) by FUNCT_2:def 1; then
dom Action-Aut(E,F) /\ [:the carrier of G,T:] = [:the carrier of G,T:]
by XBOOLE_1:28; then
dom B = [:the carrier of G,T:] by RELAT_1:61; then
H0: dom A = [:the carrier of G,T:] by dar;
H1: 1_G = 1_Aut(E) by GROUP_2:44 .= id E by GALOIS_1:6; then
H2: f.(id E) = 1_SymGr(T) by GROUP_6:31;
the carrier of Ker f = {a where a is Element of G : f.a = 1_SymGr(T)}
by GROUP_6:def 9; then
id E in the carrier of (Ker f) by H1,H2; then
H2: {id E} c= the carrier of (Ker f) by TARSKI:def 1;
now let o be object;
assume H3: o in the carrier of Ker f;
the carrier of Ker f c= the carrier of G by GROUP_2:def 5; then
reconsider g1 = o as Element of the carrier of G by H3;
reconsider g = g1 as F-fixing Automorphism of E;
H4: g is F-fixing Automorphism of FAdj(F,T) &
id E is F-fixing Automorphism of FAdj(F,T) by AS,lemBB;
now let a be Element of E;
assume K: a in T; then
reconsider a1 = a as Element of T;
H5: g1 in Ker f & [g,a] in dom A by K,H3,H0,ZFMISC_1:def 2;
H6: apply(A,g1) = f.g1 by defHom
.= 1_SymGr(T) by H5,GROUP_6:41 .= id T by Th6;
thus (id E).a = (id T).a1
.= Action-Roots(E,p).(g,a) by H6,defApp
.= (Action-Aut(E,F)|[:the carrier of G,T:]).(g,a) by dar
.= Action-Aut(E,F).(g,a) by H5,FUNCT_1:49
.= g.a by EF;
end;
then g = id E by H4,TH2a;
hence o in {id E} by TARSKI:def 1;
end;
then the carrier of Ker f c= {id E};
then Ker f = (1).G by H1,H2,XBOOLE_0:def 10,GROUP_2:def 7;
then canHom A is one-to-one by GROUP_6:56;
hence thesis by TF2;
end;
theorem TH2:
for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of Polynom-Ring F
st Roots(E,p) <> {} & E == FAdj(F,Roots(E,p))
ex f being Homomorphism of Aut(E,F),SymGr(Roots(E,p)) st f is one-to-one
proof
let F be Field, E be FieldExtension of F;
let p be non zero Element of the carrier of Polynom-Ring F;
assume AS: Roots(E,p) <> {} & E == FAdj(F,Roots(E,p)); then
reconsider Z = Roots(E,p) as non empty Subset of E;
reconsider A = Action-Roots(E,p) as Action of Aut(E,F),Z;
canHom A is one-to-one by AS,TT,TF2;
hence thesis;
end;
theorem TH3:
for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of Polynom-Ring F
st Roots(E,p) <> {} & E == FAdj(F,Roots(E,p))
ex H being Subgroup of SymGr(Roots(E,p)) st Aut(E,F),H are_isomorphic
proof
let F be Field, E be FieldExtension of F;
let p be non zero Element of the carrier of Polynom-Ring F;
assume AS: Roots(E,p) <> {} & E == FAdj(F,Roots(E,p)); then
reconsider X = Roots(E,p) as non empty Subset of E;
set G = Aut(E,F);
consider f being Homomorphism of Aut(E,F),SymGr(Roots(E,p)) such that
A: f is one-to-one by AS,TH2;
reconsider H = Image f as Subgroup of SymGr(Roots(E,p));
take H;
thus thesis by A,GROUP_6:68;
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;
G: the carrier of (1).Aut(E,F) = {id E}
proof
id E = 1_(Aut E) by GALOIS_1:6;
then the carrier of (1).(Aut E) = {id E} by GROUP_2:def 7;
hence thesis by GROUP_2:63;
end;
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 G,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;
hence o in the carrier of (1).Aut(E) by G,GROUP_2:63;
end;
hence thesis by A,TARSKI:2,GROUP_2:59;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
cluster Aut(E,F) -> finite;
coherence
proof
consider T being finite F-algebraic Subset of E such that
A: E == FAdj(F,T) by FIELD_7:37;
per cases;
suppose T is empty; then
T c= the carrier of F; then
FAdj(F,T) == F by FIELD_7:3; then
E == F by A; then
Aut(E,F) = (1).Aut(E) by lemG1;
hence Aut(E,F) is finite;
end;
suppose T is non empty; then
reconsider T as non empty finite F-algebraic Subset of E;
set p = ProductMinPolys T;
Roots(E,p) <> {} & E == FAdj(F,Roots(E,p)) by A,GALOIS_2:21; then
consider H being Subgroup of SymGr(Roots(E,p)) such that
B: Aut(E,F),H are_isomorphic by TH3;
thus Aut(E,F) is finite by B,GROUP_6:74;
end;
end;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
let K be IntermediateField of E,F;
cluster Aut(E,K) -> finite;
coherence;
end;
registration
let F be Field;
cluster -> F-simple for F-finite F-separable FieldExtension of F;
coherence
proof
let K be F-finite F-separable FieldExtension of F;
set E = the F-finite K-extending GaloisExtension of F;
A: IntermediateFields(K,F) c= IntermediateFields(E,F) by FIELD_14:5;
B: ClosedFields E = IntermediateFields(E,F) by ClInter;
C: ClosedGroups E c= Subgroups Aut(E,F) by CLFG;
consider f being Function of (ClosedGroups E),(ClosedFields E) such that
D: f = (Phi E)|(ClosedGroups E) & f is bijective by lemClGr;
Subgroups Aut(E,F) is finite by GROUP_3:15; then
rng f is finite by C; then
IntermediateFields(E,F) is finite by B,D,FUNCT_2:def 3;
hence K is F-simple by A,lempr;
end;
end;
theorem mainH1:
for F being Field
for E being F-finite FieldExtension of F
holds E is GaloisExtension of F iff deg(E,F) = order Aut(E,F)
proof
let F be Field, E be F-finite FieldExtension of F;
A: now let F be Field, E be F-finite FieldExtension of F;
assume E is GaloisExtension of F; then
reconsider E1 = E as F-finite GaloisExtension of F;
consider a being Element of E1 such that
A1: E1 == FAdj(F,{a}) by FIELD_14:def 7;
set p = MinPoly(a,F);
consider f being
Function of Auts(FAdj(F,{a}),F),Roots(FAdj(F,{a}),p) such that
A2: f is bijective by GALOIS_1:12;
dom f = Auts(FAdj(F,{a}),F) & rng f = Roots(FAdj(F,{a}),p)
by A2,FUNCT_2:def 1, FUNCT_2:def 3; then
A3: card Auts(FAdj(F,{a}),F) = card Roots(FAdj(F,{a}),p) by A2,CARD_1:70;
A4: Auts(E1,F) = Auts(FAdj(F,{a}),F)
proof
Aut(E1,F) = Aut(FAdj(F,{a}),F) by A1,GALOIS_2:13;
hence thesis;
end;
thus order Aut(E,F) = card Roots(E,p) by A4,A3,A1,lemB
.= card(Conj a) by A1,GALOIS_1:11
.= deg p by GALOIS_2:29
.= deg(E,F) by A1,FIELD_7:36;
end;
Aut(E,F) in Subgroups Aut(E) by GROUP_3:def 1; then
reconsider G = Aut(E,F) as SubGroup of Aut(E) by GALOIS_0:def 10;
reconsider G1 = Aut(E,F) as Subgroup of Aut(E,F) by GROUP_2:54;
reconsider K = Fix(E,G1) as IntermediateField of E,F;
K = Fix(E,Aut(E,Fix(E,G))) by GALOIS_1:22
.= Fix(E,Aut(E,K)); then
C: FieldExt(E,K) is GaloisExtension of K by GALOIS_1:def 18;
I: Aut(E,F) = Aut(E,Fix(E,G)) by GALOIS_1:21
.= Aut(FieldExt(E,K),K);
D: deg(E,F) = deg(E,K) * deg(K,F) by FIELD_7:30
.= deg(K,F) * (order Aut(E,F)) by I,C,A;
now assume deg(E,F) = order Aut(E,F);
then deg(E,F) * (deg(E,F))" = (deg(K,F) * deg(E,F)) * (deg(E,F))" by D
.= deg(K,F) * (deg(E,F) / deg(E,F))
.= deg(K,F) * 1 by XCMPLX_1:60;
then deg(E,F) / deg(E,F) = deg(K,F);
then FieldExt(E,K) is F-Galois by FIELD_7:8,XCMPLX_1:60;
hence E is GaloisExtension of F;
end;
hence thesis by A;
end;
theorem mainH2:
for F being Field
for E being F-finite FieldExtension of F
holds order Aut(E,F) divides deg(E,F)
proof
let F be Field, E be F-finite FieldExtension of F;
A: for F being Field, E being F-finite FieldExtension of F holds
E is GaloisExtension of F iff deg(E,F) = order Aut(E,F)
by mainH1;
Aut(E,F) in Subgroups Aut(E) by GROUP_3:def 1; then
reconsider G = Aut(E,F) as SubGroup of Aut(E) by GALOIS_0:def 10;
reconsider G1 = Aut(E,F) as Subgroup of Aut(E,F) by GROUP_2:54;
reconsider K = Fix(E,G1) as IntermediateField of E,F;
K = Fix(E,Aut(E,Fix(E,G))) by GALOIS_1:22
.= Fix(E,Aut(E,K)); then
C: FieldExt(E,K) is GaloisExtension of K by GALOIS_1:def 18;
I: Aut(E,F) = Aut(E,Fix(E,G)) by GALOIS_1:21
.= Aut(FieldExt(E,K),K);
deg(E,F) = deg(E,K) * deg(K,F) by FIELD_7:30
.= deg(K,F) * (order Aut(E,F)) by I,C,A;
hence order Aut(E,F) divides deg(E,F) by INT_1:def 3;
end;
theorem mainG:
for E being Field
for G being finite SubGroup of Aut(E)
holds G = Aut(E,Fix(E,G)) &
order Aut(E,Fix(E,G)) = deg(FieldExt(E,Fix(E,G)),Fix(E,G))
proof
let E1 be Field, G be finite SubGroup of Aut(E1);
set F = Fix(E1,G);
reconsider E = E1 as FieldExtension of F by FIELD_4:7;
A: now let a be Element of E;
reconsider G0 = G as finite Subgroup of Aut(E,F) by GALOIS_2:23;
set Z = Conj(a,G0);
defpred P[object,object] means
ex f being Element of the carrier of G0 st $1 = f & $2 = f.a;
O0: now let x be object;
assume x in the carrier of G0; then
reconsider f = x as Element of the carrier of G0;
thus ex y being object st y in Z & P[x,y]
proof
take f.a;
thus f.a in Z;
thus thesis;
end;
end;
consider f being Function of G0,Z such that
O1: for o being object st o in the carrier of G0 holds P[o,f.o]
from FUNCT_2:sch 1(O0);
O2: dom f = the carrier of G0 by FUNCT_2:def 1;
reconsider R = rng f as finite set;
now let o be object;
assume o in Z; then
consider g being Element of the carrier of G such that O3: o = g.a;
consider g1 being Element of the carrier of G0 such that
O4: g = g1 & f.g = g1.a by O1;
thus o in rng f by O2,O3,O4,FUNCT_1:3;
end; then
O4: Z c= rng f; then
reconsider Z as finite Subset of E;
reconsider G1 = the carrier of G0 as finite set;
O5: card Z <= card R by O4,NAT_1:43;
N: card R <= card(dom f) by CARD_2:47;
reconsider a1 = a as F-algebraic Element of E by O4,GALOIS_2:28;
Conj(a1,G0) = Conj(a,G0); then
MinPoly(a1,F) is separable by GALOIS_2:27;
hence a is F-separable by FIELD_15:def 5;
deg(FAdj(F,{a1}),F) = deg MinPoly(a1,F) by FIELD_6:67
.= card Z by GALOIS_2:27;
hence deg(FAdj(F,{a}),F) <= card G by N,O2,O5,XXREAL_0:2;
end;
ex a being Element of E
st for b being Element of E holds deg(FAdj(F,{b}),F) <= deg(FAdj(F,{a}),F)
proof
defpred P[Nat] means ex b being Element of E st $1 = deg(FAdj(F,{b}),F);
D1: for k being Nat st P[k] holds k <= card G by A;
D2: ex k being Nat st P[k]
proof
set b = the Element of E;
reconsider b as F-separable Element of E by A;
set n = deg(FAdj(F,{b}),F); n is natural; then
reconsider n as Element of NAT;
take n;
thus thesis;
end;
consider k being Nat such that
D3: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(D1,D2);
consider n being Nat such that
D4: ex b being Element of E st n = deg(FAdj(F,{b}),F) &
for n1 being Nat st P[n1] holds n1 <= n by D3;
consider a being Element of E such that
D5: n = deg(FAdj(F,{a}),F) &
for n1 being Nat st P[n1] holds n1 <= n by D4;
take a;
now let b be Element of E;
reconsider b1 = b as F-separable Element of E by A;
set n1 = deg(FAdj(F,{b1}),F); n1 is natural; then
reconsider n1 as Element of NAT;
consider b2 being Element of E such that
D6: b2 = b1 & n1 = deg(FAdj(F,{b2}),F);
thus deg(FAdj(F,{b}),F) <= deg(FAdj(F,{a}),F) by D6,D5;
end;
hence thesis;
end; then
consider a being Element of E such that
B: for b being Element of E holds deg(FAdj(F,{b}),F) <= deg(FAdj(F,{a}),F);
reconsider a as F-separable Element of E by A;
C: E == FAdj(F,{a})
proof
now assume C0: not(E == FAdj(F,{a}));
ex b being Element of E st not b in the carrier of FAdj(F,{a})
proof
now assume for b being Element of E
holds b in the carrier of FAdj(F,{a}); then
C1: the carrier of E c= the carrier of FAdj(F,{a});
the carrier of FAdj(F,{a}) c= the carrier of E by EC_PF_1:def 1; then
C2: the carrier of E = the carrier of FAdj(F,{a})
by C1,XBOOLE_0:def 10;
the addF of FAdj(F,{a})=(the addF of E)||the carrier of FAdj(F,{a}) &
the multF of FAdj(F,{a})=(the multF of E)||the carrier of FAdj(F,{a})
& 1.FAdj(F,{a}) = 1.E & 0.FAdj(F,{a}) = 0.E by EC_PF_1:def 1;
hence contradiction by C0,C2;
end;
hence thesis;
end; then
consider b being Element of E such that
C1: not b in the carrier of FAdj(F,{a});
reconsider b as F-separable Element of E by A;
C6: deg(FAdj(F,{a}),F) <= deg(FAdj(F,{a,b}),F) by FIELD_7:31;
now assume D0: deg(FAdj(F,{a,b}),F) = deg(FAdj(F,{a}),F);
reconsider K = FAdj(F,{a,b}) as F-finite FieldExtension of F;
F is Subfield of FAdj(F,{a}) &
FAdj(F,{a}) is Subfield of K by FIELD_4:7; then
FAdj(F,{a}) in IntermediateFields(K,F) by FIELD_14:4; then
reconsider K1 = FAdj(F,{a}) as IntermediateField of K,F
by GALOIS_0:def 5;
deg(K,F) = deg(K,K1) * deg(K1,F) by FIELD_7:30; then
deg(K,F) * (deg(K,F))"
= deg(K,K1) * (deg(K1,F) / deg(K,F))
.= deg(K,K1) * 1 by D0,XCMPLX_1:60; then
deg(K,F) / deg(K,F) = deg(K,K1); then
C8: FAdj(F,{a,b}) == FAdj(F,{a}) by FIELD_7:8,XCMPLX_1:60;
b in {a,b} & {a,b} is Subset of FAdj(F,{a,b})
by TARSKI:def 2,FIELD_6:35;
hence contradiction by C1,C8;
end; then
C2: deg(FAdj(F,{a,b}),F) > deg(FAdj(F,{a}),F) by C6,XXREAL_0:1;
now let c be Element of FAdj(F,{a,b});
reconsider c1 = c as F-algebraic Element of FAdj(F,{a,b});
the carrier of FAdj(F,{a,b}) c= the carrier of E by EC_PF_1:def 1;
then reconsider c2 = c as Element of E;
reconsider c2 as F-separable Element of E by A;
E is FAdj(F,{a,b})-extending by FIELD_4:7; then
MinPoly(c2,F) = MinPoly(c1,F) by FIELD_10:10;
hence c is F-separable by FIELD_15:def 5;
end; then
FAdj(F,{a,b}) is F-separable by FIELD_15:def 6; then
consider c being Element of FAdj(F,{a,b}) such that
C3: FAdj(F,{c}) == FAdj(F,{a,b}) by FIELD_14:def 7;
the carrier of FAdj(F,{a,b}) c= the carrier of E by EC_PF_1:def 1;
then reconsider c1 = c as Element of E;
reconsider c1 as F-separable Element of E by A;
reconsider c as F-algebraic Element of FAdj(F,{a,b});
E is FAdj(F,{a,b})-extending by FIELD_4:7; then
FAdj(F,{c1}) = FAdj(F,{c}) by abc;
hence contradiction by C3,C2,B;
end;
hence thesis;
end; then
reconsider E as F-simple FieldExtension of F by FIELD_14:def 7;
reconsider a as F-separable Element of E;
deg(E,F) = deg(FAdj(F,{a}),F) by C,FIELD_7:5; then
D: deg(E,F) <= card G by A;
VecSp(E,F) = VecSp(FAdj(F,{a}),F) by C,FIELD_7:4; then
VecSp(E,F) is finite-dimensional by FIELD_4:def 8; then
reconsider E as F-finite F-simple FieldExtension of F by FIELD_4:def 8;
E: G is Subgroup of Aut(E,F) by GALOIS_2:23; then
F: card G <= card Aut(E,F) by GROUP_2:72;
G: card Aut(E,F) <= deg(E,F) by NAT_D:7,mainH2; then
card G <= deg(E,F) by F,XXREAL_0:2; then
I: card G = deg(E,F) by D,XXREAL_0:1;
hence G = Aut(E1,Fix(E1,G)) by E,G,F,XXREAL_0:1,GROUP_2:73;
thus card Aut(E1,Fix(E1,G)) = deg(FieldExt(E1,Fix(E1,G)),Fix(E1,G))
by I,G,F,XXREAL_0:1;
end;
theorem
for E being Field
for G being finite SubGroup of Aut(E)
holds E is Fix(E,G)-finite GaloisExtension of Fix(E,G)
proof
let E be Field, G be finite SubGroup of Aut(E);
set F = Fix(E,G), K = FieldExt(E,Fix(E,G));
A: G = Aut(E,Fix(E,G)) by mainG;
card Aut(E,F) = deg(FieldExt(E,F),F) by mainG; then
B: VecSp(FieldExt(E,F),F) is finite-dimensional by A,FIELD_4:def 7;
Fix(E,G) = Fix(E,Aut(E,Fix(E,G))) by mainG .= Fix(K,Aut(K,F));
hence thesis by B,GALOIS_1:def 18,FIELD_4:def 8;
end;
theorem
for F being Field
for E being F-finite FieldExtension of F
holds ClosedGroups E = Subgroups Aut(E,F)
proof
let F be Field, E be F-finite FieldExtension of F;
A: now let o be object;
assume o in ClosedGroups E; then
consider G being Element of LattPOSet(SubgroupsAut E) such that
A1: o = G;
A2: SubgroupsAut E = LattStr (# Subgroups Aut(E,F), SubJoin Aut(E,F),
SubMeet Aut(E,F) #) by GROUP_4:def 12;
LattPOSet(SubgroupsAut E) =
RelStr(#the carrier of (SubgroupsAut E),LattRel (SubgroupsAut E)#)
by LATTICE3:def 2;
hence o in Subgroups Aut(E,F) by A1,A2;
end;
now let o be object;
assume A: o in Subgroups Aut(E,F); then
o is Subgroup of Aut(E,F) by GROUP_3:def 1; then
reconsider G = o as SubGroup of Aut(E,F) by A,GALOIS_0:def 10;
B: G is Subgroup of Aut(E) by GROUP_2:56; then
G in Subgroups Aut(E) by GROUP_3:def 1; then
reconsider G1 = G as SubGroup of Aut(E) by B,GALOIS_0:def 10;
Aut(E,Fix(E,G)) = Aut(E,Fix(E,G1)) .= G by mainG;
hence o in ClosedGroups E by ThH4;
end;
hence thesis by A,TARSKI:2;
end;