:: The Fundamental Theorem of {G}alois Theory
:: by Christoph Schwarzweller
::
:: Received January 24, 2026
:: Copyright (c) 2026 Association of Mizar Users

theorem ThN1: :: GALOIS_4:1

for G being Group
for H being Subgroup of G holds
( H is normal iff for g, h being Element of G st h in H holds
h |^ g in H )

proof end;

theorem N3: :: GALOIS_4:2

for G being Group
for H being strict Subgroup of G holds
( H is normal iff for g being Element of G holds H |^ g = H )

proof end;

theorem :: GALOIS_4:3

for G being Group
for H being strict Subgroup of G holds
( H is normal iff ex G1 being Group ex f being Homomorphism of G,G1 st Ker f = H )

proof end;

definition

let G, H be Group;
assume AS: H is Subgroup of G ;

func Index (H,G) -> Cardinal means :di: :: GALOIS_4:def 1
ex H1 being Subgroup of G st
( H1 = H & it = Index H1 );

existence
ex b₁ being Cardinal ex H1 being Subgroup of G st
( H1 = H & b₁ = Index H1 )

proof end;

uniqueness
for b₁, b₂ being Cardinal st ex H1 being Subgroup of G st
( H1 = H & b₁ = Index H1 ) & ex H1 being Subgroup of G st
( H1 = H & b₂ = Index H1 ) holds
b₁ = b₂ ;

end;

:: deftheorem di defines Index GALOIS_4:def 1 :
for G, H being Group st H is Subgroup of G holds
for b₃ being Cardinal holds
( b₃ = Index (H,G) iff ex H1 being Subgroup of G st
( H1 = H & b₃ = Index H1 ) );

definition

let G, H1, H2 be Group;

pred H1,H2 are_conjugated_in G means :: GALOIS_4:def 2
ex H3, H4 being Subgroup of G st
( H3 = H1 & H4 = H2 & H3,H4 are_conjugated );

end;

:: deftheorem defines are_conjugated_in GALOIS_4:def 2 :
for G, H1, H2 being Group holds
( H1,H2 are_conjugated_in G iff ex H3, H4 being Subgroup of G st
( H3 = H1 & H4 = H2 & H3,H4 are_conjugated ) );

lemT2: for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut (E,F)
for f being Element of the carrier of (Aut (E,F))
for f1 being Element of the carrier of (Aut E) st f1 = f holds
G |^ f = G |^ f1

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let h be Homomorphism of E;
let K be IntermediateField of E,F;

func rng (h,K) -> Subset of E equals :: GALOIS_4:def 3
rng (h | the carrier of K);

coherence
rng (h | the carrier of K) is Subset of E

proof end;

end;

:: deftheorem defines rng GALOIS_4:def 3 :
for F being Field
for E being FieldExtension of F
for h being Homomorphism of E
for K being IntermediateField of E,F holds rng (h,K) = rng (h | the carrier of K);

registration

let F be Field;
let E be FieldExtension of F;
let h be Homomorphism of E;
let K be IntermediateField of E,F;

cluster rng (h,K) -> inducing_subfield ;

coherence
rng (h,K) is inducing_subfield

proof end;

end;

definition

let F be Field;
let E be FieldExtension of F;
let K be IntermediateField of E,F;
let h be Homomorphism of E;

func h .: K -> Subfield of E equals :: GALOIS_4:def 4
InducedSubfield (rng (h,K));

coherence
InducedSubfield (rng (h,K)) is Subfield of E ;

end;

:: deftheorem defines .: GALOIS_4:def 4 :
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F
for h being Homomorphism of E holds h .: K = InducedSubfield (rng (h,K));

registration

let F be Field;
let E be FieldExtension of F;
let f be F -fixing Automorphism of E;
let K be IntermediateField of E,F;

cluster f .: K -> F -extending ;

coherence
f .: K is F -extending

proof end;

end;

theorem T4a: :: GALOIS_4:4

for F being Field
for E being b₁ -finite FieldExtension of F
for K being IntermediateField of E,F
for f being b₁ -fixing Automorphism of E st K is F -normal holds
f | the carrier of K is b₁ -fixing Automorphism of K

proof end;

theorem lemT5: :: GALOIS_4:5

for F being Field
for E being b₁ -finite FieldExtension of F
for K being IntermediateField of E,F st K is F -normal holds
for f1, f2 being b₁ -fixing Automorphism of E holds (f1 * f2) | the carrier of K = (f1 | the carrier of K) * (f2 | the carrier of K)

proof end;

lemSubF: for E being Field
for F being Subfield of E st the carrier of F = the carrier of E holds
F == E

proof end;

theorem T4x: :: GALOIS_4:6

for F being Field
for E being b₁ -finite FieldExtension of F
for K being IntermediateField of E,F st K is F -normal holds
for f being Element of the carrier of (Aut (E,F)) holds f .: K = K

proof end;

theorem :: GALOIS_4:7

for F being Field
for E being b₁ -finite FieldExtension of F
for K being IntermediateField of E,F st K is F -normal holds
Fix (K,(Aut (K,F))) is Subfield of Fix (E,(Aut (E,F)))

proof end;

theorem Conj0: :: GALOIS_4:8

for F being Field
for E being b₁ -normal FieldExtension of F
for a being b₁ -algebraic Element of E st E == FAdj (F,{a}) holds
E is SplittingField of MinPoly (a,F)

proof end;

theorem Conj1: :: GALOIS_4:9

for F being Field
for E being b₁ -finite GaloisExtension of F
for K1, K2 being IntermediateField of E,F
for h being Function of K1,K2 st h is F -fixing & h is isomorphism holds
ex f being b₁ -fixing Automorphism of E st f | K1 = h

proof end;

theorem T7: :: GALOIS_4:10

for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F
for f being Element of the carrier of (Aut E) holds
( (Aut (E,(f .: K))) |^ f = Aut (E,K) & (Aut (E,K)) |^ (f ") = Aut (E,(f .: K)) )

proof end;

theorem Conj2: :: GALOIS_4:11

for F being Field
for E being FieldExtension of F
for H being Subgroup of Aut (E,F)
for f being Element of the carrier of (Aut (E,F)) holds f .: (Fix (E,H)) = Fix (E,(H |^ (f ")))

proof end;

theorem :: GALOIS_4:12

for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds (Psi E) . K = Aut (E,K) by GALOIS_3:def 14;

theorem :: GALOIS_4:13

for F being Field
for E being FieldExtension of F
for G being SubGroup of Aut (E,F) holds (Phi E) . G = Fix (E,G) by GALOIS_3:def 15;

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

theorem BIJ1: :: GALOIS_4:14

for F being Field
for E being b₁ -finite GaloisExtension of F holds Psi E is a_Bijection of IntermediateFields (E,F), Subgroups (Aut (E,F))

proof end;

theorem BIJ: :: GALOIS_4:15

for F being Field
for E being b₁ -finite GaloisExtension of F holds Phi E is a_Bijection of Subgroups (Aut (E,F)), IntermediateFields (E,F)

proof end;

theorem :: GALOIS_4:16

for F being Field
for E being b₁ -finite GaloisExtension of F holds
( (Psi E) " = Phi E & (Phi E) " = Psi E )

proof end;

registration

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

cluster IntermediateFields (E,F) -> Subgroups (Aut (E,F)) -bijective ;

coherence
IntermediateFields (E,F) is Subgroups (Aut (E,F)) -bijective

proof end;

cluster Subgroups (Aut (E,F)) -> IntermediateFields (E,F) -bijective ;

coherence
Subgroups (Aut (E,F)) is IntermediateFields (E,F) -bijective

proof end;

end;

theorem G1: :: GALOIS_4:17

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F holds K = Fix (E,(Aut (E,K)))

proof end;

theorem G2: :: GALOIS_4:18

for F being Field
for E being b₁ -finite GaloisExtension of F
for G being SubGroup of Aut (E,F) holds G = Aut (E,(Fix (E,G)))

proof end;

theorem :: GALOIS_4:19

for F being Field
for E being b₁ -finite GaloisExtension of F
for K1, K2 being IntermediateField of E,F holds
( K1 is Subfield of K2 iff Aut (E,K2) is Subgroup of Aut (E,K1) )

proof end;

theorem :: GALOIS_4:20

for F being Field
for E being b₁ -finite GaloisExtension of F
for G1, G2 being SubGroup of Aut (E,F) holds
( G1 is Subgroup of G2 iff Fix (E,G2) is Subfield of Fix (E,G1) )

proof end;

theorem :: GALOIS_4:21

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F holds
( deg (E,K) = order (Aut (E,K)) & deg (K,F) = Index ((Aut (E,K)),(Aut (E,F))) )

proof end;

theorem :: GALOIS_4:22

for F being Field
for E being b₁ -finite GaloisExtension of F
for K1, K2 being IntermediateField of E,F holds
( K1,K2 are_isomorphic_over F iff Aut (E,K1), Aut (E,K2) are_conjugated_in Aut (E,F) )

proof end;

theorem :: GALOIS_4:23

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F holds E is GaloisExtension of K by GALOIS_2:35;

theorem T1: :: GALOIS_4:24

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F holds
( K is GaloisExtension of F iff K is F -normal )

proof end;

theorem T4: :: GALOIS_4:25

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F holds
( K is F -normal iff for f being Element of the carrier of (Aut (E,F)) holds f .: K = K )

proof end;

theorem T2: :: GALOIS_4:26

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F holds
( K is F -normal iff Aut (E,K) is normal Subgroup of Aut (E,F) )

proof end;

definition

let F be Field;
let E be F -finite FieldExtension of F;
let K be IntermediateField of E,F;
assume AS: K is F -normal ;

func Restr K -> Homomorphism of (Aut (E,F)),(Aut (K,F)) means :defR: :: GALOIS_4:def 5
for f being F -fixing Automorphism of E holds it . f = f | the carrier of K;

existence
ex b₁ being Homomorphism of (Aut (E,F)),(Aut (K,F)) st
for f being F -fixing Automorphism of E holds b₁ . f = f | the carrier of K

proof end;

uniqueness
for b₁, b₂ being Homomorphism of (Aut (E,F)),(Aut (K,F)) st ( for f being F -fixing Automorphism of E holds b₁ . f = f | the carrier of K ) & ( for f being F -fixing Automorphism of E holds b₂ . f = f | the carrier of K ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defR defines Restr GALOIS_4:def 5 :
for F being Field
for E being b₁ -finite FieldExtension of F
for K being IntermediateField of E,F st K is F -normal holds
for b₄ being Homomorphism of (Aut (E,F)),(Aut (K,F)) holds
( b₄ = Restr K iff for f being b₁ -fixing Automorphism of E holds b₄ . f = f | the carrier of K );

theorem T3b: :: GALOIS_4:27

for F being Field
for E being b₁ -finite FieldExtension of F
for K being IntermediateField of E,F st K is F -normal holds
Fix (K,(Image (Restr K))) is Subfield of Fix (E,(Aut (E,F)))

proof end;

theorem T3c: :: GALOIS_4:28

for F being Field
for E being b₁ -finite FieldExtension of F
for K being IntermediateField of E,F st K is F -normal holds
Ker (Restr K) = Aut (E,K)

proof end;

theorem T3: :: GALOIS_4:29

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F st K is F -normal holds
Image (Restr K) = Aut (K,F)

proof end;

theorem :: GALOIS_4:30

for F being Field
for E being b₁ -finite GaloisExtension of F
for K being IntermediateField of E,F
for H being normal Subgroup of Aut (E,F) st H = Aut (E,K) holds
Aut (K,F),(Aut (E,F)) ./. H are_isomorphic

proof end;

theorem lat1: :: GALOIS_4:31

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds
( (Aut (E,K1)) "\/" (Aut (E,K2)) is Subgroup of Aut (E,(K1 "/\" K2)) & Aut (E,(K1 "\/" K2)) is Subgroup of (Aut (E,K1)) /\ (Aut (E,K2)) )

proof end;

theorem lat3: :: GALOIS_4:32

for F being Field
for E being FieldExtension of F
for G1, G2 being Subgroup of Aut (E,F) holds
( (Fix (E,G1)) "\/" (Fix (E,G2)) is Subfield of Fix (E,(G1 /\ G2)) & Fix (E,(G1 "\/" G2)) is Subfield of (Fix (E,G1)) "/\" (Fix (E,G2)) )

proof end;

theorem :: GALOIS_4:33

for F being Field
for E being b₁ -finite GaloisExtension of F
for K1, K2 being IntermediateField of E,F holds
( Aut (E,(K1 "/\" K2)) = (Aut (E,K1)) "\/" (Aut (E,K2)) & Aut (E,(K1 "\/" K2)) = (Aut (E,K1)) /\ (Aut (E,K2)) )

proof end;

theorem :: GALOIS_4:34

for F being Field
for E being b₁ -finite GaloisExtension of F
for G1, G2 being SubGroup of Aut (E,F) holds
( Fix (E,(G1 /\ G2)) = (Fix (E,G1)) "\/" (Fix (E,G2)) & Fix (E,(G1 "\/" G2)) = (Fix (E,G1)) "/\" (Fix (E,G2)) )

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let M be non empty Subset of (IntermediateFields (E,F));

func Psi. M -> non empty Subset of (Subgroups (Aut (E,F))) equals :: GALOIS_4:def 6
{ ((Psi E) . K) where K is Element of IntermediateFields (E,F) : K in M } ;

coherence
{ ((Psi E) . K) where K is Element of IntermediateFields (E,F) : K in M } is non empty Subset of (Subgroups (Aut (E,F)))

proof end;

end;

:: deftheorem defines Psi. GALOIS_4:def 6 :
for F being Field
for E being FieldExtension of F
for M being non empty Subset of (IntermediateFields (E,F)) holds Psi. M = { ((Psi E) . K) where K is Element of IntermediateFields (E,F) : K in M } ;

definition

let F be Field;
let E be FieldExtension of F;
let M be non empty Subset of (Subgroups (Aut (E,F)));

func Phi. M -> non empty Subset of (IntermediateFields (E,F)) equals :: GALOIS_4:def 7
{ ((Phi E) . G) where G is Element of Subgroups (Aut (E,F)) : G in M } ;

coherence
{ ((Phi E) . G) where G is Element of Subgroups (Aut (E,F)) : G in M } is non empty Subset of (IntermediateFields (E,F))

proof end;

end;

:: deftheorem defines Phi. GALOIS_4:def 7 :
for F being Field
for E being FieldExtension of F
for M being non empty Subset of (Subgroups (Aut (E,F))) holds Phi. M = { ((Phi E) . G) where G is Element of Subgroups (Aut (E,F)) : G in M } ;

theorem lat10: :: GALOIS_4:35

for F being Field
for E being FieldExtension of F
for M being non empty Subset of (IntermediateFields (E,F)) holds Psi. M = { (Aut (E,K)) where K is Element of IntermediateFields (E,F) : K in M }

proof end;

theorem lat11: :: GALOIS_4:36

for F being Field
for E being FieldExtension of F
for M being non empty Subset of (Subgroups (Aut (E,F))) holds Phi. M = { (Fix (E,G)) where G is Element of Subgroups (Aut (E,F)) : G in M }

proof end;

theorem lathh1: :: GALOIS_4:37

for F being Field
for E being b₁ -finite GaloisExtension of F
for M being non empty Subset of (IntermediateFields (E,F)) holds Phi. (Psi. M) = M

proof end;

theorem lathh2: :: GALOIS_4:38

for F being Field
for E being b₁ -finite GaloisExtension of F
for M being non empty Subset of (Subgroups (Aut (E,F))) holds Psi. (Phi. M) = M

proof end;

theorem lat12: :: GALOIS_4:39

for F being Field
for E being FieldExtension of F
for M being non empty Subset of (IntermediateFields (E,F)) holds
( Aut (E,(\/ M)) is Subgroup of /\ (Psi. M) & \/ (Psi. M) is Subgroup of Aut (E,(/\ M)) )

proof end;

theorem lat14: :: GALOIS_4:40

for F being Field
for E being FieldExtension of F
for M being non empty Subset of (Subgroups (Aut (E,F))) holds
( Fix (E,(\/ M)) is Subfield of /\ (Phi. M) & \/ (Phi. M) is Subfield of Fix (E,(/\ M)) )

proof end;

theorem :: GALOIS_4:41

for F being Field
for E being b₁ -finite GaloisExtension of F
for M being non empty Subset of (IntermediateFields (E,F)) holds
( Aut (E,(\/ M)) = /\ (Psi. M) & Aut (E,(/\ M)) = \/ (Psi. M) )

proof end;

theorem :: GALOIS_4:42

for F being Field
for E being b₁ -finite GaloisExtension of F
for M being non empty Subset of (Subgroups (Aut (E,F))) holds
( Fix (E,(\/ M)) = /\ (Phi. M) & Fix (E,(/\ M)) = \/ (Phi. M) )

proof end;