GALOIS_3: The Galois Connection between IntermediateFields(E,F) and Subgroups of Aut(E,F)

end;

:: deftheorem defines SubgroupsAut GALOIS_3:def 1 :

registration

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

cluster -> E -functional for SubGroup of Aut (E,F);

proof 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 ;

end;

registration

let F be Field;
let E be FieldExtension of F;
let G be SubGroup of Aut (E,F);

cluster -> unity-preserving additive isomorphism multiplicative F -fixing for Element of the carrier of G;

end;

bb0: for F being Field
for E being FieldExtension of F
for K being b₂ -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 end;

theorem bb1: :: GALOIS_3:1

for F being Field
for E being FieldExtension of F
for K being b₂ -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 end;

bba: for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for a being b₁ -algebraic Element of E
for b being b₁ -algebraic Element of K st b = a holds
the carrier of (FAdj (F,{a})) = the carrier of (FAdj (F,{b}))

proof end;

theorem abc: :: GALOIS_3:2

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

proof end;

lemTH2b: for F being Field
for E being FieldExtension of F
for T being non empty finite b₁ -algebraic Subset of E
for f, g being b₁ -fixing Automorphism of (FAdj (F,T)) st ( for a being Element of E st a in T holds
f . a = g . a ) holds
for p being Polynomial of (card T),F st ex b being bag of card T st Support p = {b} holds
for x being b₃ -evaluating Function of (card T),E holds f . (Ext_eval (p,x)) = g . (Ext_eval (p,x))

proof end;

lemTH2a: for F being Field
for E being FieldExtension of F
for T being non empty finite b₁ -algebraic Subset of E
for f, g being b₁ -fixing Automorphism of (FAdj (F,T)) st ( for a being Element of E st a in T holds
f . a = g . a ) holds
for p being Polynomial of (card T),F
for x being b₃ -evaluating Function of (card T),E holds f . (Ext_eval (p,x)) = g . (Ext_eval (p,x))

proof end;

theorem TH2a: :: GALOIS_3:3

for F being Field
for E being FieldExtension of F
for T being non empty finite b₁ -algebraic Subset of E
for f, g being b₁ -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 end;

theorem :: GALOIS_3:4

for F being Field
for E being FieldExtension of F
for T being non empty finite b₁ -algebraic Subset of E
for f, g being b₁ -fixing Automorphism of (FAdj (F,T)) holds
( f = g iff f | T = g | T )

proof end;

theorem lempr: :: GALOIS_3:5

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

proof end;

lemBB: for F1, F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for f being b₁ -fixing Automorphism of E1 st E1 == E2 & F1 == F2 holds
f is b₂ -fixing Automorphism of E2

proof 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 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 end;

theorem ThH: :: GALOIS_3:6

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 end;

lemB: for F1, F2 being Field
for E1 being FieldExtension of F1
for 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 end;

definition

let X be set ;

func SymmetricGroup X -> strict constituted-Functions multMagma means :Def2: :: GALOIS_3:def 2
( the carrier of it = permutations X & ( for x, y being Element of it holds x * y = x * y ) );

proof end;

proof end;

end;

:: deftheorem Def2 defines SymmetricGroup GALOIS_3:def 2 :

notation

let X be set ;
synonym SymGr X for SymmetricGroup X;

end;

theorem Th5: :: GALOIS_3:7

for X being set
for f being Element of (SymGr X) holds f is Permutation of X

proof end;

registration

let X be set ;

cluster SymmetricGroup X -> non empty strict Group-like associative constituted-Functions ;

proof end;

end;

theorem Th6: :: GALOIS_3:8

for X being set holds 1_ (SymGr X) = id X

proof end;

theorem :: GALOIS_3:9

for X being set
for x being Element of (SymGr X) holds x " = x "

proof end;

registration

let X be finite set ;

cluster SymmetricGroup X -> finite strict constituted-Functions ;

proof end;

end;

lemac1: for G being Group
for X being non empty set ex f being Function of [: the carrier of G,X:],X st
for a being Element of X
for g being Element of G holds f . (g,a) = a

proof end;

lemac2: for G being Group
for X being set
for f being Function of [: the carrier of G,X:],X st ( for a being Element of X
for g being Element of G holds f . (g,a) = a ) holds
for a being Element of X
for g1, g2 being Element of the carrier of G holds f . (g1,(f . (g2,a))) = f . ((g1 * g2),a)

proof end;

definition

let G be Group;
let X be set ;
assume AS: not X is empty ;

mode Action of G,X -> Function of [: the carrier of G,X:],X means :defAC: :: GALOIS_3:def 3
( ( for a being Element of X holds it . ((1_ G),a) = a ) & ( for a being Element of X
for g1, g2 being Element of the carrier of G holds it . (g1,(it . (g2,a))) = it . ((g1 * g2),a) ) );

proof end;

end;

:: deftheorem defAC defines Action GALOIS_3:def 3 :

definition

let G be Group;
let X be set ;
let A be Action of G,X;

attr A is faithful means :: GALOIS_3:def 4
for g1, g2 being Element of G st ( for x being Element of X holds A . (g1,x) = A . (g2,x) ) holds
g1 = g2;

attr A is free means :: GALOIS_3:def 5
for g being Element of G st ex x being Element of X st A . (g,x) = x holds
g = 1_ G;

pred A acts_transitively_on X means :: GALOIS_3:def 6
for a, b being Element of X ex g being Element of G st A . (g,a) = b;

end;

:: deftheorem defines faithful GALOIS_3:def 4 :

:: deftheorem defines free GALOIS_3:def 5 :

:: deftheorem defines acts_transitively_on GALOIS_3:def 6 :

definition

let G be Group;
let X be set ;

pred G acts_on X means :: GALOIS_3:def 7
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 :: GALOIS_3:def 8
ex A being Action of G,X st A acts_transitively_on X;

end;

:: deftheorem defines acts_on GALOIS_3:def 7 :

:: deftheorem defines acts_transitively_on GALOIS_3:def 8 :

definition

let G be Group;
let X be non empty set ;

func trivialAction (G,X) -> Action of G,X means :dtr: :: GALOIS_3:def 9
for a being Element of X
for g being Element of G holds it . (g,a) = a;

proof end;

proof end;

end;

:: deftheorem dtr defines trivialAction GALOIS_3:def 9 :

registration

let G be non trivial Group;
let X be non empty set ;

cluster trivialAction (G,X) -> non faithful ;

proof end;

end;

registration

let G be trivial Group;
let X be non empty set ;

cluster trivialAction (G,X) -> faithful ;

proof end;

end;

definition

let G be Group;

func regularAction G -> Action of G, the carrier of G means :dreg: :: GALOIS_3:def 10
for g1, g2 being Element of G holds it . (g1,g2) = g1 * g2;

proof end;

proof end;

func conjugationAction G -> Action of G, the carrier of G means :: GALOIS_3:def 11
for g1, g2 being Element of G holds it . (g1,g2) = (g1 * g2) * (g1 ");

proof end;

proof end;

end;

:: deftheorem dreg defines regularAction GALOIS_3:def 10 :

:: deftheorem defines conjugationAction GALOIS_3:def 11 :

registration

let G be Group;

cluster regularAction G -> free ;

proof 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: :: GALOIS_3:def 12
for a being Element of X holds it . a = A . (g,a);

proof end;

proof end;

end;

:: deftheorem defApp defines apply GALOIS_3:def 12 :

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: :: GALOIS_3:def 13
for g being Element of G holds it . g = apply (A,g);

proof end;

proof end;

end;

:: deftheorem defHom defines canHom GALOIS_3:def 13 :

theorem app1: :: GALOIS_3:10

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 end;

registration

let G be Group;
let X be non empty set ;
let A be Action of G,X;

cluster canHom A -> multiplicative ;

proof end;

end;

theorem :: GALOIS_3:11

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 :: GALOIS_3:12

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 )

proof end;

theorem TF0: :: GALOIS_3:13

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 end;

theorem TF2: :: GALOIS_3:14

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 end;

theorem TF1: :: GALOIS_3:15

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 end;

registration

let G be Group;
let X be non empty set ;

cluster free -> faithful for Action of G,X;

proof end;

end;

theorem :: GALOIS_3:16

for G being Group ex H being Subgroup of SymmetricGroup the carrier of G st H,G are_isomorphic

proof end;

definition

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

func Psi E -> Function of (LattPOSet (IntermediateFields E)),(LattPOSet (SubgroupsAut E)) means :dA: :: GALOIS_3:def 14
for K being IntermediateField of E,F holds it . K = Aut (E,K);

proof end;

proof end;

func Phi E -> Function of (LattPOSet (SubgroupsAut E)),(LattPOSet (IntermediateFields E)) means :dB: :: GALOIS_3:def 15
for G being SubGroup of Aut (E,F) holds it . G = Fix (E,G);

proof end;

proof end;

end;

:: deftheorem dA defines Psi GALOIS_3:def 14 :

:: deftheorem dB defines Phi GALOIS_3:def 15 :

theorem TH3: :: GALOIS_3:17

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 end;

theorem TH5: :: GALOIS_3:18

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 end;

definition

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

func GalCon E -> Connection of LattPOSet (IntermediateFields E), LattPOSet (SubgroupsAut E) equals :: GALOIS_3:def 16
[(Psi E),(Phi E)];

correctness ;

end;

:: deftheorem defines GalCon GALOIS_3:def 16 :

registration

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

cluster Psi E -> antitone ;

proof end;

cluster Phi E -> antitone ;

proof end;

end;

registration

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

cluster GalCon E -> co-Galois ;

proof end;

end;

definition

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

func ClosedFields E -> Subset of (LattPOSet (IntermediateFields E)) equals :: GALOIS_3:def 17
Closed (Phi E);

correctness ;

func ClosedGroups E -> Subset of (LattPOSet (SubgroupsAut E)) equals :: GALOIS_3:def 18
Closed (Psi E);

correctness ;

end;

:: deftheorem defines ClosedFields GALOIS_3:def 17 :

:: deftheorem defines ClosedGroups GALOIS_3:def 18 :

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 end;

mainA: for S, T being non empty RelStr
for g being Function of S,T
for 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 end;

lemCl: for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is co-Galois holds
( Restr (g,d) is bijective & Restr (d,g) is bijective )

proof 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 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 end;

registration

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

cluster ClosedFields E -> non empty ClosedGroups E -bijective ;

proof end;

cluster ClosedGroups E -> non empty ClosedFields E -bijective ;

proof end;

end;

theorem :: GALOIS_3:19

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 end;

theorem :: GALOIS_3:20

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 end;

theorem ThH1: :: GALOIS_3:21

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 end;

theorem ThH3: :: GALOIS_3:22

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 end;

theorem ThH2: :: GALOIS_3:23

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 end;

theorem ThH4: :: GALOIS_3:24

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 end;

theorem TH7: :: GALOIS_3:25

for F being Field
for E being FieldExtension of F holds
( E is F -Galois iff doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) in ClosedFields E )

proof end;

theorem TH8: :: GALOIS_3:26

for F being Field
for E being b₁ -finite FieldExtension of F holds
( ClosedFields E = IntermediateFields (E,F) iff doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) in ClosedFields E )

proof end;

theorem ClInter: :: GALOIS_3:27

for F being Field
for E being b₁ -finite FieldExtension of F holds
( E is GaloisExtension of F iff ClosedFields E = IntermediateFields (E,F) )

proof end;

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: :: GALOIS_3:def 19
for a being Element of E
for g being Element of the carrier of (Aut (E,F)) holds it . (g,a) = g . a;

proof end;

proof end;

end;

:: deftheorem EF defines Action-Aut GALOIS_3:def 19 :

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 end;

definition

let F be Field;
let E be FieldExtension of F;
let p be 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: :: GALOIS_3:def 20
(Action-Aut (E,F)) | [: the carrier of (Aut (E,F)),(Roots (E,p)):];

coherence by AS, TH1;

end;

:: deftheorem dar defines Action-Roots GALOIS_3:def 20 :

theorem :: GALOIS_3:28

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 end;

theorem :: GALOIS_3:29

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 end;

theorem TT: :: GALOIS_3:30

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 end;

theorem TH2: :: GALOIS_3:31

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
ex f being Homomorphism of (Aut (E,F)),(SymGr (Roots (E,p))) st f is one-to-one

proof end;

theorem TH3: :: GALOIS_3:32

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
ex H being Subgroup of SymGr (Roots (E,p)) st Aut (E,F),H are_isomorphic

proof end;

lemG1: for F being Field
for E being FieldExtension of F st E == F holds
Aut (E,F) = (1). (Aut E)

proof end;

registration

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

cluster Aut (E,F) -> finite ;

proof 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 ;

end;

registration

let F be Field;

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