:: Introduction to {G}alois Theory
:: by Christoph Schwarzweller and Agnieszka Rowi\'nska-Schwarzweller
::
:: Received December 12, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

definition

let X be non empty set ;
let x be Element of X;
:: original: {
redefine func {x} -> Subset of X;
coherence
{x} is Subset of X

proof end;

end;

registration

let F be non quadratic_complete Field;
let a be non square Element of F;

cluster X^2- a -> irreducible ;

coherence
X^2- a is irreducible

proof end;

end;

registration

let F be non quadratic_complete Field;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID Euclidian Polynom-Ring F -homomorphic factorial F -extending F -quadratic gcd-like reduced for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ is F -quadratic

proof end;

end;

registration

let F be Field;

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

coherence
for b₁ being FieldExtension of F st b₁ is F -quadratic holds
b₁ is F -simple

proof end;

end;

registration

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

cluster Roots ((FAdj (F,{a})),(MinPoly (a,F))) -> non empty finite ;

coherence
( not Roots ((FAdj (F,{a})),(MinPoly (a,F))) is empty & Roots ((FAdj (F,{a})),(MinPoly (a,F))) is finite ) by FIELD_16:13;

end;

theorem U0: :: GALOIS_1:1

for z being Element of F_Complex holds
( z is Element of F_Real iff z *' = z )

proof end;

registration

cluster F_Complex -> non 2 -characteristic ;

coherence
not F_Complex is 2 -characteristic

proof end;

end;

definition

:: original: <i>
redefine func <i> -> non zero F_Real -algebraic Element of F_Complex;
coherence
<i> is non zero F_Real -algebraic Element of F_Complex

proof end;

end;

registration

cluster X^2+ (1. F_Real) -> irreducible ;

coherence
X^2+ (1. F_Real) is irreducible

proof end;

end;

theorem lemma: :: GALOIS_1:2

Roots (F_Complex,(X^2+ (1. F_Real))) = {<i>,(- <i>)}

proof end;

theorem lemMinPol: :: GALOIS_1:3

MinPoly (<i>,F_Real) = X^2+ (1. F_Real)

proof end;

theorem lem5: :: GALOIS_1:4

F_Complex is SplittingField of X^2+ (1. F_Real)

proof end;

main1b: deg (F_Complex,F_Real) = 2

proof end;

theorem lem6: :: GALOIS_1:5

F_Complex = FAdj (F_Real,{<i>})

proof end;

registration

cluster F_Complex -> F_Real -quadratic ;

coherence
F_Complex is F_Real -quadratic by main1b;

end;

definition

let F be Field;

func Auts F -> non empty set equals :: GALOIS_1:def 1
{ f where f is Automorphism of F : verum } ;

coherence
{ f where f is Automorphism of F : verum } is non empty set

proof end;

end;

:: deftheorem defines Auts GALOIS_1:def 1 :
for F being Field holds Auts F = { f where f is Automorphism of F : verum } ;

registration

let F be Field;

cluster Auts F -> non empty F -functional ;

coherence
Auts F is F -functional

proof end;

end;

registration

let F be Field;

cluster -> additive unity-preserving isomorphism multiplicative for Element of Auts F;

coherence
for b₁ being Element of Auts F holds
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

end;

definition

let F be Field;

func AutComp F -> BinOp of (Auts F) means :defMult: :: GALOIS_1:def 2
for f, g being Automorphism of F holds it . (f,g) = f * g;

existence
ex b₁ being BinOp of (Auts F) st
for f, g being Automorphism of F holds b₁ . (f,g) = f * g

proof end;

uniqueness
for b₁, b₂ being BinOp of (Auts F) st ( for f, g being Automorphism of F holds b₁ . (f,g) = f * g ) & ( for f, g being Automorphism of F holds b₂ . (f,g) = f * g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defMult defines AutComp GALOIS_1:def 2 :
for F being Field
for b₂ being BinOp of (Auts F) holds
( b₂ = AutComp F iff for f, g being Automorphism of F holds b₂ . (f,g) = f * g );

definition

let F be Field;

func Aut F -> non empty strict multMagma equals :: GALOIS_1:def 3
multMagma(# (Auts F),(AutComp F) #);

coherence
multMagma(# (Auts F),(AutComp F) #) is non empty strict multMagma ;

end;

:: deftheorem defines Aut GALOIS_1:def 3 :
for F being Field holds Aut F = multMagma(# (Auts F),(AutComp F) #);

registration

let F be Field;

cluster Aut F -> non empty strict Group-like associative ;

coherence
( Aut F is Group-like & Aut F is associative )

proof end;

end;

theorem Th1: :: GALOIS_1:6

for F being Field holds 1_ (Aut F) = id F

proof end;

registration

let F be Field;

cluster Aut F -> non empty strict F -functional ;

coherence
Aut F is F -functional ;

cluster the carrier of (Aut F) -> F -functional ;

coherence
the carrier of (Aut F) is F -functional ;

cluster -> F -functional for Element of bool the carrier of (Aut F);

coherence
for b₁ being Subset of (Aut F) holds b₁ is F -functional ;

end;

registration

let F be Field;
let G be Subgroup of Aut F;

cluster the carrier of G -> F -functional ;

coherence
the carrier of G is F -functional

proof end;

end;

registration

let F be Field;

cluster -> additive unity-preserving isomorphism multiplicative for Element of the carrier of (Aut F);

coherence
for b₁ being Element of the carrier of (Aut F) holds
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism ) ;

end;

registration

let F be Field;
let G be non empty Subset of (Aut F);

cluster -> additive unity-preserving isomorphism multiplicative for Element of G;

coherence
for b₁ being Element of G holds
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

end;

registration

let F be Field;
let G be non empty Subgroup of Aut F;

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

coherence
for b₁ being Element of the carrier of G holds
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

end;

definition

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

func Auts (E,F) -> non empty Subset of (Auts E) equals :: GALOIS_1:def 4
{ f where f is F -fixing Automorphism of E : verum } ;

coherence
{ f where f is F -fixing Automorphism of E : verum } is non empty Subset of (Auts E)

proof end;

end;

:: deftheorem defines Auts GALOIS_1:def 4 :
for F being Field
for E being FieldExtension of F holds Auts (E,F) = { f where f is b₁ -fixing Automorphism of E : verum } ;

registration

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

cluster Auts (E,F) -> non empty E -functional ;

coherence
Auts (E,F) is E -functional ;

end;

registration

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

cluster -> additive unity-preserving isomorphism multiplicative F -fixing for Element of Auts (E,F);

coherence
for b₁ being Element of Auts (E,F) holds
( b₁ is F -fixing & b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

end;

definition

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

func AutComp (E,F) -> BinOp of (Auts (E,F)) equals :: GALOIS_1:def 5
(AutComp E) || (Auts (E,F));

coherence
(AutComp E) || (Auts (E,F)) is BinOp of (Auts (E,F))

proof end;

end;

:: deftheorem defines AutComp GALOIS_1:def 5 :
for F being Field
for E being FieldExtension of F holds AutComp (E,F) = (AutComp E) || (Auts (E,F));

definition

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

func Aut (E,F) -> strict multMagma equals :: GALOIS_1:def 6
multMagma(# (Auts (E,F)),(AutComp (E,F)) #);

coherence
multMagma(# (Auts (E,F)),(AutComp (E,F)) #) is strict multMagma ;

end;

:: deftheorem defines Aut GALOIS_1:def 6 :
for F being Field
for E being FieldExtension of F holds Aut (E,F) = multMagma(# (Auts (E,F)),(AutComp (E,F)) #);

registration

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

cluster Aut (E,F) -> non empty strict ;

coherence
not Aut (E,F) is empty ;

end;

registration

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

cluster Aut (E,F) -> strict Group-like associative ;

coherence
( Aut (E,F) is Group-like & Aut (E,F) is associative )

proof end;

end;

definition

let F be Field;
let E be FieldExtension of F;
:: original: Aut
redefine func Aut (E,F) -> strict Subgroup of Aut E;
coherence
Aut (E,F) is strict Subgroup of Aut E by GROUP_2:def 5;

end;

registration

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

cluster Aut (E,F) -> strict E -functional ;

coherence
Aut (E,F) is E -functional ;

cluster the carrier of (Aut (E,F)) -> E -functional ;

coherence
the carrier of (Aut (E,F)) is E -functional ;

cluster -> E -functional for Element of bool the carrier of (Aut (E,F));

coherence
for b₁ being Subset of (Aut (E,F)) holds b₁ is E -functional ;

end;

registration

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

cluster -> additive unity-preserving isomorphism multiplicative F -fixing for Element of the carrier of (Aut (E,F));

coherence
for b₁ being Element of the carrier of (Aut (E,F)) holds
( b₁ is F -fixing & b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism ) ;

end;

registration

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

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

coherence
for b₁ being Element of G holds
( b₁ is F -fixing & b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

end;

registration

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

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

coherence
for b₁ being Element of the carrier of G holds
( b₁ is F -fixing & b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

end;

definition

let E be Field;
let F be Subfield of E;

func Aut (E,F) -> strict Subgroup of Aut E equals :: GALOIS_1:def 7
Aut ((FieldExt (E,F)),F);

coherence
Aut ((FieldExt (E,F)),F) is strict Subgroup of Aut E ;

end;

:: deftheorem defines Aut GALOIS_1:def 7 :
for E being Field
for F being Subfield of E holds Aut (E,F) = Aut ((FieldExt (E,F)),F);

definition

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

func Aut (E,K) -> strict Subgroup of Aut E equals :: GALOIS_1:def 8
Aut ((FieldExt (E,K)),K);

coherence
Aut ((FieldExt (E,K)),K) is strict Subgroup of Aut E ;

end;

:: deftheorem defines Aut GALOIS_1:def 8 :
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds Aut (E,K) = Aut ((FieldExt (E,K)),K);

theorem :: GALOIS_1:7

for F being Field
for E being FieldExtension of F
for K1 being IntermediateField of E,F
for K2 being Subfield of E st K2 = K1 holds
Aut (E,K2) = Aut (E,K1) ;

definition

let F be Field;
let G be Subgroup of Aut F;
let a be Element of F;

func Conjugates (a,G) -> non empty Subset of F equals :: GALOIS_1:def 9
{ (f . a) where f is Element of the carrier of G : verum } ;

coherence
{ (f . a) where f is Element of the carrier of G : verum } is non empty Subset of F

proof end;

end;

:: deftheorem defines Conjugates GALOIS_1:def 9 :
for F being Field
for G being Subgroup of Aut F
for a being Element of F holds Conjugates (a,G) = { (f . a) where f is Element of the carrier of G : verum } ;

definition

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

func Conjugates a -> non empty Subset of E equals :: GALOIS_1:def 10
Conjugates (a,(Aut (E,F)));

coherence
Conjugates (a,(Aut (E,F))) is non empty Subset of E ;

end;

:: deftheorem defines Conjugates GALOIS_1:def 10 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds Conjugates a = Conjugates (a,(Aut (E,F)));

notation

let F be Field;
let G be Subgroup of Aut F;
let a be Element of F;
synonym Conj (a,G) for Conjugates (a,G);

end;

notation

let F be Field;
let E be FieldExtension of F;
let a be Element of E;
synonym Conj a for Conjugates a;

end;

theorem ID2c: :: GALOIS_1:8

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

proof end;

theorem ID2b: :: GALOIS_1:9

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for b being Element of E st b in Roots ((FAdj (F,{a})),(MinPoly (a,F))) holds
ex f being b₁ -fixing Automorphism of (FAdj (F,{a})) st f . a = b

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;

lemBC: for F being Field
for E1, E2 being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F) st E1 == E2 holds
Roots (E1,p) = Roots (E2,p)

proof end;

theorem lemBA: :: GALOIS_1:10

for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut (E,F)
for a being b₁ -algebraic Element of E holds Conj (a,G) c= Roots (E,(MinPoly (a,F)))

proof end;

registration

let F be Field;
let E be FieldExtension of F;
let G be Subgroup of Aut (E,F);
let a be F -algebraic Element of E;

cluster Conjugates (a,G) -> non empty finite ;

coherence
Conj (a,G) is finite

proof end;

end;

registration

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

cluster Conjugates a -> non empty finite ;

coherence
Conj a is finite

proof end;

end;

theorem :: GALOIS_1:11

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

proof end;

theorem ThBij: :: GALOIS_1:12

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E ex f being Function of (Auts ((FAdj (F,{a})),F)),(Roots ((FAdj (F,{a})),(MinPoly (a,F)))) st f is bijective

proof end;

registration

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

cluster Aut ((FAdj (F,{a})),F) -> finite strict ;

coherence
Aut ((FAdj (F,{a})),F) is finite

proof end;

end;

lemZ0: for F being Field
for E being FieldExtension of F
for S being Subset of E holds (id E) .: S = S

proof end;

lemZ1: for F being Field
for E being FieldExtension of F
for S being Subset of E holds id E in { f where f is b₁ -fixing Automorphism of E : f .: S = S }

proof end;

definition

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

func Auts S -> non empty Subset of (Auts (E,F)) equals :: GALOIS_1:def 11
{ f where f is F -fixing Automorphism of E : f .: S = S } ;

coherence
{ f where f is F -fixing Automorphism of E : f .: S = S } is non empty Subset of (Auts (E,F))

proof end;

end;

:: deftheorem defines Auts GALOIS_1:def 11 :
for F being Field
for E being FieldExtension of F
for S being Subset of E holds Auts S = { f where f is b₁ -fixing Automorphism of E : f .: S = S } ;

definition

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

func Auts a -> non empty Subset of (Auts (E,F)) equals :: GALOIS_1:def 12
Auts {a};

coherence
Auts {a} is non empty Subset of (Auts (E,F)) ;

end;

:: deftheorem defines Auts GALOIS_1:def 12 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds Auts a = Auts {a};

theorem lemZ2: :: GALOIS_1:13

for F being Field
for E being FieldExtension of F
for a being Element of E holds Auts a = { f where f is b₁ -fixing Automorphism of E : f . a = a }

proof end;

definition

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

func AutComp S -> BinOp of (Auts S) equals :: GALOIS_1:def 13
(AutComp (E,F)) || (Auts S);

coherence
(AutComp (E,F)) || (Auts S) is BinOp of (Auts S)

proof end;

end;

:: deftheorem defines AutComp GALOIS_1:def 13 :
for F being Field
for E being FieldExtension of F
for S being Subset of E holds AutComp S = (AutComp (E,F)) || (Auts S);

definition

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

func Aut S -> non empty strict multMagma equals :: GALOIS_1:def 14
multMagma(# (Auts S),(AutComp S) #);

coherence
multMagma(# (Auts S),(AutComp S) #) is non empty strict multMagma ;

end;

:: deftheorem defines Aut GALOIS_1:def 14 :
for F being Field
for E being FieldExtension of F
for S being Subset of E holds Aut S = multMagma(# (Auts S),(AutComp S) #);

lemZ3: for F being Field
for E being FieldExtension of F
for S being non empty Subset of E
for h being Automorphism of E st h .: S = S holds
( dom (h | S) = S & rng (h | S) = S & dom ((h ") | S) = S & rng ((h ") | S) = S )

proof end;

registration

let F be Field;
let E be FieldExtension of F;
let S be non empty Subset of E;

cluster Aut S -> non empty strict Group-like associative ;

coherence
( Aut S is Group-like & Aut S is associative )

proof end;

end;

definition

let F be Field;
let E be FieldExtension of F;
let S be non empty Subset of E;
:: original: Aut
redefine func Aut S -> strict Subgroup of Aut (E,F);
coherence
Aut S is strict Subgroup of Aut (E,F) by GROUP_2:def 5;

end;

definition

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

func Aut a -> strict Subgroup of Aut (E,F) equals :: GALOIS_1:def 15
Aut {a};

coherence
Aut {a} is strict Subgroup of Aut (E,F) ;

end;

:: deftheorem defines Aut GALOIS_1:def 15 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds Aut a = Aut {a};

theorem :: GALOIS_1:14

for F being Field
for E being FieldExtension of F
for a being Element of E holds card (Conj a) = Index (Aut a)

proof end;

definition

let F be Field;
let G be Subgroup of Aut F;

func Fixed_Elements (F,G) -> non empty Subset of F equals :: GALOIS_1:def 16
{ a where a is Element of F : for f being Function of F,F st f in G holds
f . a = a } ;

coherence
{ a where a is Element of F : for f being Function of F,F st f in G holds
f . a = a } is non empty Subset of F

proof end;

end;

:: deftheorem defines Fixed_Elements GALOIS_1:def 16 :
for F being Field
for G being Subgroup of Aut F holds Fixed_Elements (F,G) = { a where a is Element of F : for f being Function of F,F st f in G holds
f . a = a } ;

notation

let F be Field;
let G be Subgroup of Aut F;
synonym Fixed_El (F,G) for Fixed_Elements (F,G);

end;

lemH: for F being Field
for f being Automorphism of F
for a being Element of F st a <> 0. F holds
f . (a ") = (f . a) "

proof end;

registration

let F be Field;
let G be Subgroup of Aut F;

cluster Fixed_Elements (F,G) -> non empty inducing_subfield ;

coherence
Fixed_El (F,G) is inducing_subfield

proof end;

end;

definition

let F be Field;
let G be Subgroup of Aut F;

func Fix (F,G) -> strict doubleLoopStr means :df: :: GALOIS_1:def 17
( the carrier of it = Fixed_El (F,G) & the addF of it = the addF of F || (Fixed_El (F,G)) & the multF of it = the multF of F || (Fixed_El (F,G)) & 1. it = 1. F & 0. it = 0. F );

existence
ex b₁ being strict doubleLoopStr st
( the carrier of b₁ = Fixed_El (F,G) & the addF of b₁ = the addF of F || (Fixed_El (F,G)) & the multF of b₁ = the multF of F || (Fixed_El (F,G)) & 1. b₁ = 1. F & 0. b₁ = 0. F )

proof end;

uniqueness
for b₁, b₂ being strict doubleLoopStr st the carrier of b₁ = Fixed_El (F,G) & the addF of b₁ = the addF of F || (Fixed_El (F,G)) & the multF of b₁ = the multF of F || (Fixed_El (F,G)) & 1. b₁ = 1. F & 0. b₁ = 0. F & the carrier of b₂ = Fixed_El (F,G) & the addF of b₂ = the addF of F || (Fixed_El (F,G)) & the multF of b₂ = the multF of F || (Fixed_El (F,G)) & 1. b₂ = 1. F & 0. b₂ = 0. F holds
b₁ = b₂ ;

end;

:: deftheorem df defines Fix GALOIS_1:def 17 :
for F being Field
for G being Subgroup of Aut F
for b₃ being strict doubleLoopStr holds
( b₃ = Fix (F,G) iff ( the carrier of b₃ = Fixed_El (F,G) & the addF of b₃ = the addF of F || (Fixed_El (F,G)) & the multF of b₃ = the multF of F || (Fixed_El (F,G)) & 1. b₃ = 1. F & 0. b₃ = 0. F ) );

lemFix: for F being Field
for G being Subgroup of Aut F holds Fix (F,G) = InducedSubfield (Fixed_El (F,G))

proof end;

registration

let F be Field;
let G be Subgroup of Aut F;

cluster Fix (F,G) -> non degenerated strict ;

coherence
not Fix (F,G) is degenerated

proof end;

end;

registration

let F be Field;
let G be Subgroup of Aut F;

cluster Fix (F,G) -> right_complementable strict Abelian add-associative right_zeroed ;

coherence
( Fix (F,G) is Abelian & Fix (F,G) is add-associative & Fix (F,G) is right_zeroed & Fix (F,G) is right_complementable )

proof end;

end;

registration

let F be Field;
let G be Subgroup of Aut F;

cluster Fix (F,G) -> almost_left_invertible strict well-unital distributive associative commutative ;

coherence
( Fix (F,G) is commutative & Fix (F,G) is associative & Fix (F,G) is well-unital & Fix (F,G) is distributive & Fix (F,G) is almost_left_invertible )

proof end;

end;

definition

let F be Field;
let G be Subgroup of Aut F;
:: original: Fix
redefine func Fix (F,G) -> strict Subfield of F;
coherence
Fix (F,G) is strict Subfield of F

proof end;

end;

G16: for F being Field
for E being FieldExtension of F
for G being Subgroup of Aut (E,F) holds Fix (E,G) is IntermediateField of E,F

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let G be Subgroup of Aut (E,F);
:: original: Fix
redefine func Fix (E,G) -> IntermediateField of E,F;
coherence
Fix (E,G) is IntermediateField of E,F by G16;

end;

theorem G1: :: GALOIS_1:15

for F being Field
for E being FieldExtension of F holds F is Subfield of Fix (E,(Aut (E,F)))

proof end;

theorem :: GALOIS_1:16

for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds K is Subfield of Fix (E,(Aut (E,K))) by G1;

theorem G2: :: GALOIS_1:17

for F being Field
for G being Subgroup of Aut F holds G is Subgroup of Aut (F,(Fix (F,G)))

proof end;

G3: for F being Field
for K being FieldExtension of F
for E being b₂ -extending FieldExtension of F holds Aut (E,K) is Subgroup of Aut (E,F)

proof end;

theorem :: GALOIS_1:18

for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds Aut (E,K) is Subgroup of Aut (E,F) by G3;

theorem :: GALOIS_1:19

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F st K1 is Subfield of K2 holds
Aut (E,K2) is Subgroup of Aut (E,K1)

proof end;

theorem G4: :: GALOIS_1:20

for F being Field
for G1, G2 being Subgroup of Aut F st G1 is Subgroup of G2 holds
Fix (F,G2) is Subfield of Fix (F,G1)

proof end;

theorem :: GALOIS_1:21

for F being Field
for E being FieldExtension of F holds Aut (E,F) = Aut (E,(Fix (E,(Aut (E,F)))))

proof end;

theorem :: GALOIS_1:22

for F being Field
for G being Subgroup of Aut F holds Fix (F,G) = Fix (F,(Aut (F,(Fix (F,G)))))

proof end;

definition

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

attr E is F -Galois means :defGalois: :: GALOIS_1:def 18
Fix (E,(Aut (E,F))) == F;

end;

:: deftheorem defGalois defines -Galois GALOIS_1:def 18 :
for F being Field
for E being FieldExtension of F holds
( E is F -Galois iff Fix (E,(Aut (E,F))) == F );

lemG0: for F being Field
for E being FieldExtension of F holds the carrier of ((1). (Aut (E,F))) = {(id E)}

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;

lemG2: for F being Field holds Fix (F,((1). (Aut F))) == F

proof end;

lemG3: for F being Field
for E being FieldExtension of F st E = F holds
Fix (E,(Aut (E,F))) == F

proof end;

registration

let F be Field;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID Euclidian Polynom-Ring F -homomorphic factorial F -extending gcd-like reduced F -Galois for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ is F -Galois

proof end;

end;

definition

let F be Field;
mode GaloisExtension of F is F -Galois FieldExtension of F;

end;

registration

let F be Field;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID Euclidian Polynom-Ring F -homomorphic factorial F -extending F -finite gcd-like reduced F -Galois for doubleLoopStr ;

existence
ex b₁ being GaloisExtension of F st b₁ is F -finite

proof end;

end;

theorem :: GALOIS_1:23

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

proof end;

theorem :: GALOIS_1:24

for F being Field holds F is GaloisExtension of F

proof end;

definition

func *' -> Function of F_Complex,F_Complex means :di: :: GALOIS_1:def 19
for z being Element of F_Complex holds it . z = z *' ;

existence
ex b₁ being Function of F_Complex,F_Complex st
for z being Element of F_Complex holds b₁ . z = z *'

proof end;

uniqueness
for b₁, b₂ being Function of F_Complex,F_Complex st ( for z being Element of F_Complex holds b₁ . z = z *' ) & ( for z being Element of F_Complex holds b₂ . z = z *' ) holds
b₁ = b₂

proof end;

end;

:: deftheorem di defines *' GALOIS_1:def 19 :
for b₁ being Function of F_Complex,F_Complex holds
( b₁ = *' iff for z being Element of F_Complex holds b₁ . z = z *' );

registration

cluster *' -> isomorphism F_Real -fixing ;

coherence
( *' is F_Real -fixing & *' is isomorphism )

proof end;

end;

definition

:: original: *'
redefine func *' -> Element of the carrier of (Aut (F_Complex,F_Real));
coherence
*' is Element of the carrier of (Aut (F_Complex,F_Real))

proof end;

end;

theorem U1: :: GALOIS_1:25

Auts (F_Complex,F_Real) = {(id F_Complex),*'}

proof end;

lemAT3: for F being Field
for E being FieldExtension of F
for f, g being Function of E,E
for a, b being Element of (Aut (E,F)) st f = a & g = b holds
f * g = a * b

proof end;

lemAT2: for F being Field
for E being FieldExtension of F
for f being Function of E,E
for a being Element of (Aut (E,F))
for m being Nat st f = a holds
f `^ m = a |^ m

proof end;

theorem U2: :: GALOIS_1:26

Aut (F_Complex,F_Real) = gr {*'}

proof end;

registration

cluster Aut (F_Complex,F_Real) -> finite strict cyclic ;

coherence
( Aut (F_Complex,F_Real) is finite & Aut (F_Complex,F_Real) is cyclic ) by U1, U2, GR_CY_1:def 7;

end;

theorem U3: :: GALOIS_1:27

order (Aut (F_Complex,F_Real)) = 2

proof end;

theorem :: GALOIS_1:28

Aut (F_Complex,F_Real), INT.Group 2 are_isomorphic

proof end;

registration

cluster F_Complex -> F_Real -Galois ;

coherence
F_Complex is F_Real -Galois

proof end;

end;

theorem :: GALOIS_1:29

F_Complex is GaloisExtension of F_Real ;

definition

let p be Prime;
let n be non zero Nat;
let F be GaloisField of p |^ n;
:: original: FrobeniusMorphism
redefine func Frob F -> Element of the carrier of (Aut (F,(Z/ p)));
coherence
FrobeniusMorphism F is Element of the carrier of (Aut (F,(Z/ p)))

proof end;

end;

registration

let p be Prime;
let n be non zero Nat;
let F be GaloisField of p |^ n;
let m be Nat;

cluster (Frob F) `^ m -> isomorphism Z/ p -fixing ;

coherence
( (Frob F) `^ m is Z/ p -fixing & (Frob F) `^ m is isomorphism ) ;

end;

theorem AT0: :: GALOIS_1:30

for p being Prime
for n being non zero Nat
for F being GaloisField of p |^ n holds Aut (F,(Z/ p)) = Aut F

proof end;

theorem AT1: :: GALOIS_1:31

for p being Prime
for n being non zero Nat
for F being GaloisField of p |^ n holds Auts (F,(Z/ p)) = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) }

proof end;

theorem AT2: :: GALOIS_1:32

for p being Prime
for n being non zero Nat
for F being GaloisField of p |^ n holds Aut (F,(Z/ p)) = gr {(Frob F)}

proof end;

AT3: for p being Prime
for n being non zero Nat
for F being GaloisField of p |^ n holds card the carrier of (Aut (F,(Z/ p))) = n

proof end;

registration

let p be Prime;
let n be non zero Nat;
let F be GaloisField of p |^ n;

cluster Aut (F,(Z/ p)) -> finite strict cyclic ;

coherence
( Aut (F,(Z/ p)) is finite & Aut (F,(Z/ p)) is cyclic )

proof end;

end;

theorem :: GALOIS_1:33

for p being Prime
for n being non zero Nat
for F being GaloisField of p |^ n holds order (Aut (F,(Z/ p))) = n by AT3;

theorem :: GALOIS_1:34

for p being Prime
for n being non zero Nat
for F being GaloisField of p |^ n holds Aut (F,(Z/ p)), INT.Group n are_isomorphic

proof end;

registration

let p be Prime;
let n be non zero Nat;

cluster -> Z/ p -Galois for GaloisField of p |^ n;

coherence
for b₁ being GaloisField of p |^ n holds b₁ is Z/ p -Galois

proof end;

end;

theorem :: GALOIS_1:35

for p being Prime
for n being non zero Nat
for G being GaloisField of p |^ n holds G is GaloisExtension of Z/ p ;