:: Characterization of Finite {G}alois Extensions
:: by Christoph Schwarzweller
::
:: Received December 21, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

definition

let X, Y be non empty set ;
let f be Function of X,Y;
let S be non empty finite Subset of X;
:: original: .:
redefine func f .: S -> non empty finite Subset of Y;
coherence
f .: S is non empty finite Subset of Y

proof end;

end;

theorem :: GALOIS_2:1

for F being Field
for g1, g2 being Element of (Aut F)
for f1, f2 being Automorphism of F st g1 = f1 & g2 = f2 holds
g1 * g2 = f1 * f2 by GALOIS_1:def 2;

theorem :: GALOIS_2:2

for F being Field
for g being Element of (Aut F)
for f being Automorphism of F st g = f holds
g " = f "

proof end;

theorem G3b: :: GALOIS_2:3

for F being Field
for E being FieldExtension of F
for g1, g2 being Element of (Aut (E,F))
for f1, f2 being b₁ -fixing Automorphism of E st g1 = f1 & g2 = f2 holds
g1 * g2 = f1 * f2

proof end;

theorem G3a: :: GALOIS_2:4

for F being Field
for E being FieldExtension of F
for g being Element of (Aut (E,F))
for f being b₁ -fixing Automorphism of E st g = f holds
g " = f "

proof end;

theorem rot: :: GALOIS_2:5

for R being comRing
for S being comRingExtension of R
for p, q being Element of the carrier of (Polynom-Ring R) st q divides p holds
Roots (S,q) c= Roots (S,p)

proof end;

registration

let R be domRing;
let p be non zero Polynomial of R;
let q be non constant Polynomial of R;

cluster p *' q -> non constant ;

coherence
not p *' q is constant

proof end;

end;

registration

let R be domRing;
let p be non zero Element of the carrier of (Polynom-Ring R);
let q be non constant Element of the carrier of (Polynom-Ring R);

cluster p * q -> non constant ;

coherence
not p * q is constant

proof end;

end;

theorem R58: :: GALOIS_2:6

for R being Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S holds Ext_eval ((a | R),b) = a

proof end;

lemsepprodA: for F being Field
for E being FieldExtension of F
for f being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being Polynomial of F
for a being Element of E st q = Product f & ( for i being Element of dom f
for p being Polynomial of F st p = f . i holds
Ext_eval (p,a) <> 0. E ) holds
Ext_eval (q,a) <> 0. E

proof end;

theorem :: GALOIS_2:7

for F being Field
for E being FieldExtension of F
for f being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being Polynomial of F st q = Product f holds
for a being Element of E holds
( Ext_eval (q,a) = 0. E iff ex i being Element of dom f ex p being Polynomial of F st
( p = f . i & Ext_eval (p,a) = 0. E ) ) by FIELD_13:4, lemsepprodA;

theorem sepprodB: :: GALOIS_2:8

for F being Field
for f being FinSequence of (Polynom-Ring F)
for p, q being Element of the carrier of (Polynom-Ring F) st p = Product f & ex i being Nat st
( 1 <= i & i <= len f & f . i = q ) holds
q divides p

proof end;

theorem sepprodC: :: GALOIS_2:9

for F being Field
for f being FinSequence of (Polynom-Ring F)
for p, q1, q2 being Element of the carrier of (Polynom-Ring F) st p = Product f & ex i, j being Nat st
( j <> i & 1 <= i & i <= len f & f . i = q1 & 1 <= j & j <= len f & f . j = q2 ) holds
q1 *' q2 divides p

proof end;

theorem mon: :: GALOIS_2:10

for F being Field
for f being FinSequence of the carrier of (Polynom-Ring F) st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
q is monic ) holds
for p being Polynomial of F st p = Product f holds
p is monic

proof end;

spl1: for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for E being SplittingField of p
for a being Element of E
for q being non constant Element of the carrier of (Polynom-Ring (FAdj (F,{a}))) st q = p holds
E is SplittingField of q

proof end;

theorem splitE: :: GALOIS_2:11

for F being Field
for E being FieldExtension of F
for p being non constant Polynomial of F
for q being non zero Polynomial of F st p *' q splits_in E holds
p splits_in E

proof end;

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

proof end;

lemBF: for F being Field
for E1, E2 being FieldExtension of F
for f being Automorphism of E1 st E1 == E2 holds
f is Automorphism of E2

proof end;

theorem lemBE: :: GALOIS_2:12

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
Aut E1 = Aut E2

proof end;

theorem lemBC: :: GALOIS_2:13

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
Aut (E1,F) = Aut (E2,F)

proof end;

theorem lemBD: :: GALOIS_2:14

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
Fix (E1,(Aut (E1,F))) = Fix (E2,(Aut (E2,F)))

proof end;

theorem :: GALOIS_2:15

for F being Field
for E1 being GaloisExtension of F
for E2 being FieldExtension of F st E2 == E1 holds
E2 is GaloisExtension of F

proof end;

definition

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

attr T is F -separable means :defT: :: GALOIS_2:def 1
for a being Element of E st a in T holds
a is F -separable ;

end;

:: deftheorem defT defines -separable GALOIS_2:def 1 :
for F being Field
for E being FieldExtension of F
for T being Subset of E holds
( T is F -separable iff for a being Element of E st a in T holds
a is F -separable );

registration

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

cluster non empty finite F -separable for Element of bool the carrier of E;

existence
ex b₁ being Subset of E st
( b₁ is finite & b₁ is F -separable & not b₁ is empty )

proof end;

end;

registration

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

cluster F -separable -> F -algebraic F -separable for Element of bool the carrier of E;

coherence
for b₁ being F -separable Subset of E holds b₁ is F -algebraic

proof end;

end;

registration

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

cluster -> F -separable for Element of bool the carrier of E;

coherence
for b₁ being Subset of E holds b₁ is F -separable ;

end;

theorem separ: :: GALOIS_2:16

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being FieldExtension of F st p splits_in E holds
card (Roots (E,p)) = deg p )

proof end;

definition

let F be Field;
let p, q be Element of the carrier of (Polynom-Ring F);

pred p,q have_common_roots_in_some_extension means :: GALOIS_2:def 2
ex E being FieldExtension of F st (Roots (E,p)) /\ (Roots (E,q)) <> {} ;

end;

:: deftheorem defines have_common_roots_in_some_extension GALOIS_2:def 2 :
for F being Field
for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q have_common_roots_in_some_extension iff ex E being FieldExtension of F st (Roots (E,p)) /\ (Roots (E,q)) <> {} );

notation

let F be Field;
let p, q be Element of the carrier of (Polynom-Ring F);
antonym p,q have_nowhere_common_roots for p,q have_common_roots_in_some_extension ;

end;

theorem irrm: :: GALOIS_2:17

for F being Field
for p, q being irreducible monic Element of the carrier of (Polynom-Ring F) st p,q have_common_roots_in_some_extension holds
p = q

proof end;

theorem sepmult: :: GALOIS_2:18

for F being Field
for p, q being non constant Element of the carrier of (Polynom-Ring F) st p is separable & q is separable holds
( p * q is separable iff p,q have_nowhere_common_roots )

proof end;

theorem sepirr: :: GALOIS_2:19

for F being Field
for p, q being irreducible monic Element of the carrier of (Polynom-Ring F) st p is separable & q is separable holds
( p * q is separable iff p <> q )

proof end;

sepprodE1: for F being Field
for E being FieldExtension of F
for f being FinSequence of (Polynom-Ring F)
for p being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of E st p = Product f & ( for i being Nat st 1 <= i & i <= len f holds
for r being non zero Element of the carrier of (Polynom-Ring F) st r = f . i holds
multiplicity (r,a) = 0 ) holds
multiplicity (p,a) = 0

proof end;

sepprodE: for F being Field
for E being FieldExtension of F
for f being FinSequence of (Polynom-Ring F)
for p, r being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of E st p = Product f & ex i being Nat st
( 1 <= i & i <= len f & r = f . i & ( for j being Nat st j <> i & 1 <= j & j <= len f holds
for q being non zero Element of the carrier of (Polynom-Ring F) st q = f . j holds
multiplicity (q,a) = 0 ) ) holds
multiplicity (p,a) = multiplicity (r,a)

proof end;

theorem sepprod: :: GALOIS_2:20

for F being Field
for E being FieldExtension of F
for f being non empty FinSequence of (Polynom-Ring F) st ( for i being Nat st 1 <= i & i <= len f holds
ex q being irreducible monic Element of the carrier of (Polynom-Ring F) st
( f . i = q & q is separable ) ) holds
for p being non constant Element of the carrier of (Polynom-Ring F) st p = Product f holds
( p is separable iff f is one-to-one )

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let T be F -algebraic Subset of E;

func MinPolys T -> Subset of the carrier of (Polynom-Ring F) equals :: GALOIS_2:def 3
{ (MinPoly (a,F)) where a is F -algebraic Element of E : a in T } ;

coherence
{ (MinPoly (a,F)) where a is F -algebraic Element of E : a in T } is Subset of the carrier of (Polynom-Ring F)

proof end;

end;

:: deftheorem defines MinPolys GALOIS_2:def 3 :
for F being Field
for E being FieldExtension of F
for T being b₁ -algebraic Subset of E holds MinPolys T = { (MinPoly (a,F)) where a is b₁ -algebraic Element of E : a in T } ;

registration

let F be Field;
let E be FieldExtension of F;
let T be non empty F -algebraic Subset of E;

cluster MinPolys T -> non empty ;

coherence
not MinPolys T is empty

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let T be finite F -algebraic Subset of E;

cluster MinPolys T -> finite ;

coherence
MinPolys T is finite

proof end;

end;

definition

let F be Field;
let E be FieldExtension of F;
let T be finite F -algebraic Subset of E;

func FinSeq_MinPolys T -> FinSequence of the carrier of (Polynom-Ring F) equals :: GALOIS_2:def 4
canFS (MinPolys T);

coherence
canFS (MinPolys T) is FinSequence of the carrier of (Polynom-Ring F)

proof end;

end;

:: deftheorem defines FinSeq_MinPolys GALOIS_2:def 4 :
for F being Field
for E being FieldExtension of F
for T being finite b₁ -algebraic Subset of E holds FinSeq_MinPolys T = canFS (MinPolys T);

registration

let F be Field;
let E be FieldExtension of F;
let T be non empty finite F -algebraic Subset of E;

cluster FinSeq_MinPolys T -> non empty ;

coherence
not FinSeq_MinPolys T is empty ;

end;

definition

let F be Field;
let E be FieldExtension of F;
let T be finite F -algebraic Subset of E;

func ProductMinPolys T -> Element of the carrier of (Polynom-Ring F) equals :: GALOIS_2:def 5
Product (FinSeq_MinPolys T);

coherence
Product (FinSeq_MinPolys T) is Element of the carrier of (Polynom-Ring F) ;

end;

:: deftheorem defines ProductMinPolys GALOIS_2:def 5 :
for F being Field
for E being FieldExtension of F
for T being finite b₁ -algebraic Subset of E holds ProductMinPolys T = Product (FinSeq_MinPolys T);

registration

let F be Field;
let E be FieldExtension of F;
let T be non empty finite F -algebraic Subset of E;

cluster ProductMinPolys T -> non constant monic ;

coherence
( not ProductMinPolys T is constant & ProductMinPolys T is monic )

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let T be non empty finite F -algebraic Subset of E;

cluster Roots (E,(ProductMinPolys T)) -> non empty ;

coherence
not Roots (E,(ProductMinPolys T)) is empty

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let T be non empty finite F -separable Subset of E;

cluster ProductMinPolys T -> separable ;

coherence
ProductMinPolys T is separable

proof end;

end;

theorem :: GALOIS_2:21

for F being Field
for E being FieldExtension of F
for T being non empty finite b₁ -algebraic Subset of E st E == FAdj (F,T) holds
E == FAdj (F,(Roots (E,(ProductMinPolys T))))

proof end;

theorem :: GALOIS_2:22

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F holds
( E is SplittingField of p iff ( p splits_in E & E == FAdj (F,(Roots (E,p))) ) )

proof end;

G0: for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut E st Fix (E,G) == F holds
for g being Element of G holds g in Auts (E,F)

proof end;

theorem mainG1: :: GALOIS_2:23

for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut E st Fix (E,G) == F holds
G is Subgroup of Aut (E,F)

proof end;

theorem G1: :: GALOIS_2:24

for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut E st Fix (E,G) == F holds
for p being Polynomial of E st ( for g being Element of the carrier of G holds (PolyHom g) . p = p ) holds
p is Polynomial of F

proof end;

theorem G3: :: GALOIS_2:25

for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut E st Fix (E,G) == F holds
for g being Element of the carrier of G
for a being Element of E st Conj (a,G) is finite holds
g .: (Conj (a,G)) = Conj (a,G)

proof end;

theorem GG: :: GALOIS_2:26

for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut E st Fix (E,G) == F holds
for a being b₁ -algebraic Element of E
for Z being non empty finite Subset of E st Z = Conj (a,G) holds
for p being Ppoly of E,Z holds p = MinPoly (a,F)

proof end;

theorem Gv: :: GALOIS_2:27

for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut E st Fix (E,G) == F holds
for a being b₁ -algebraic Element of E st Conj (a,G) is finite holds
( MinPoly (a,F) is separable & MinPoly (a,F) splits_in E & Roots (E,(MinPoly (a,F))) = Conj (a,G) & deg (MinPoly (a,F)) = card (Conj (a,G)) )

proof end;

theorem lem18a: :: GALOIS_2:28

for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut E st Fix (E,G) == F holds
for a being Element of E st Conj (a,G) is finite holds
a is F -algebraic

proof end;

registration

let F be Field;
let E be GaloisExtension of F;
let a be F -algebraic Element of E;

cluster minimal_polynom (a,F) -> separable ;

coherence
MinPoly (a,F) is separable

proof end;

end;

theorem :: GALOIS_2:29

for F being Field
for E being GaloisExtension of F
for a being b₁ -algebraic Element of E holds
( MinPoly (a,F) splits_in E & Roots (E,(MinPoly (a,F))) = Conj a & deg (MinPoly (a,F)) = card (Conj a) )

proof end;

theorem :: GALOIS_2:30

for F being Field
for E being GaloisExtension of F
for a being Element of E holds
( a is F -algebraic iff Conj a is finite )

proof end;

mainA: for F being Field
for E being b₁ -finite GaloisExtension of F holds
( E is F -normal & E is F -separable )

proof end;

mainB: for F being Field
for E being b₁ -finite FieldExtension of F st E is F -normal & E is F -separable holds
ex p being non constant separable Element of (Polynom-Ring F) st E is SplittingField of p

proof end;

theorem :: GALOIS_2:31

for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being SplittingField of p
for a, b being Element of E st a in Roots (E,p) & b in Roots (E,p) holds
ex h being b₁ -fixing Automorphism of E st h . a = b

proof end;

theorem FixAut: :: GALOIS_2:32

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for E being SplittingField of p
for a, b being Element of E st a in Roots (E,p) & b in Roots (E,p) & MinPoly (a,F) = MinPoly (b,F) holds
ex h being b₁ -fixing Automorphism of E st h . a = b

proof end;

Th28: for L being non empty ZeroStr
for a being Element of L holds (a | L) . 0 = a

proof end;

mainC: for F being Field
for E being b₁ -finite FieldExtension of F st ex p being non constant separable Element of (Polynom-Ring F) st E is SplittingField of p holds
E is F -Galois

proof end;

theorem main1: :: GALOIS_2:33

for F being Field
for E being b₁ -finite FieldExtension of F holds
( E is GaloisExtension of F iff ( E is F -normal & E is F -separable ) )

proof end;

theorem main2: :: GALOIS_2:34

for F being Field
for E being b₁ -finite FieldExtension of F holds
( E is GaloisExtension of F iff ex p being non constant separable Element of (Polynom-Ring F) st E is SplittingField of p )

proof end;

registration

let F be Field;

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

coherence
for b₁ being F -finite GaloisExtension of F holds
( b₁ is F -normal & b₁ is F -separable ) by main1;

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

coherence
for b₁ being F -finite FieldExtension of F st b₁ is F -normal & b₁ is F -separable holds
b₁ is F -Galois by main1;

end;

registration

let F be Field;
let p be non constant separable Element of the carrier of (Polynom-Ring F);

cluster -> F -Galois for SplittingField of p;

coherence
for b₁ being SplittingField of p holds b₁ is F -Galois by mainC;

end;

col: for F being Field
for K being b₁ -finite FieldExtension of F
for E being b₂ -extending b₁ -finite FieldExtension of F st E is GaloisExtension of F holds
E is GaloisExtension of K

proof end;

theorem :: GALOIS_2:35

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

proof end;

theorem :: GALOIS_2:36

for F being Field
for E being b₁ -finite FieldExtension of F holds
( E is GaloisExtension of F iff for a being Element of E holds card (Roots (E,(MinPoly (a,F)))) = deg ((FAdj (F,{a})),F) )

proof end;

theorem :: GALOIS_2:37

for F being Field
for E being FieldExtension of F
for T being finite Subset of E holds
( FAdj (F,T) is F -separable iff for a being Element of E st a in T holds
a is F -separable )

proof end;

theorem coll: :: GALOIS_2:38

for F being Field
for E being b₁ -finite FieldExtension of F ex p being non constant Element of the carrier of (Polynom-Ring F) ex K being SplittingField of p st K is E -extending

proof end;

coll1: for F being Field
for E being b₁ -finite FieldExtension of F ex K being b₁ -finite b₁ -normal FieldExtension of F st K is E -extending

proof end;

registration

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

cluster non empty non degenerated non trivial right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible almost_right_invertible Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like F -homomorphic F -monomorphic F -extending E -extending F -normal reduced for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st
( b₁ is F -normal & b₁ is E -extending )

proof end;

end;

theorem colls: :: GALOIS_2:39

for F being Field
for E being b₁ -finite b₁ -separable FieldExtension of F ex p being non constant separable Element of the carrier of (Polynom-Ring F) ex K being SplittingField of p st K is E -extending

proof end;

colls1: for F being Field
for E being b₁ -finite b₁ -separable FieldExtension of F ex K being b₁ -finite GaloisExtension of F st K is E -extending

proof end;

registration

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

cluster non empty non degenerated non trivial right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible almost_right_invertible Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like F -homomorphic F -monomorphic F -extending E -extending F -finite reduced F -Galois for doubleLoopStr ;

existence
ex b₁ being GaloisExtension of F st
( b₁ is F -finite & b₁ is E -extending )

proof end;

end;