:: The Lattice of Intermediate Fields and Other Preliminaries 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 A, B be set ;

attr B is A -bijective means :: GALOIS_0:def 1
ex f being Function of A,B st f is bijective ;

end;

:: deftheorem defines -bijective GALOIS_0:def 1 :
for A, B being set holds
( B is A -bijective iff ex f being Function of A,B st f is bijective );

definition

let A, B be non empty set ;
assume AS: B is A -bijective ;

mode a_Bijection of A,B -> Function of A,B means :dX: :: GALOIS_0:def 2
it is bijective ;

existence
ex b₁ being Function of A,B st b₁ is bijective by AS;

end;

:: deftheorem dX defines a_Bijection GALOIS_0:def 2 :
for A, B being non empty set st B is A -bijective holds
for b₃ being Function of A,B holds
( b₃ is a_Bijection of A,B iff b₃ is bijective );

theorem :: GALOIS_0:1

for E being Field
for F1, F2 being Subfield of E st the carrier of F1 c= the carrier of F2 holds
F1 is Subfield of F2

proof end;

registration

let F be finite Field;

cluster SubFields F -> finite ;

coherence
SubFields F is finite

proof end;

end;

definition

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

func FieldExt (E,F) -> FieldExtension of F equals :: GALOIS_0:def 3
E;

coherence
E is FieldExtension of F by FIELD_4:7;

end;

:: deftheorem defines FieldExt GALOIS_0:def 3 :
for E being Field
for F being Subfield of E holds FieldExt (E,F) = E;

definition

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

func deg (E,F) -> Integer equals :: GALOIS_0:def 4
deg ((FieldExt (E,F)),F);

coherence
deg ((FieldExt (E,F)),F) is Integer ;

end;

:: deftheorem defines deg GALOIS_0:def 4 :
for E being Field
for F being Subfield of E holds deg (E,F) = deg ((FieldExt (E,F)),F);

lempr1: for F being Field
for E being FieldExtension of F holds IntermediateFields (E,F) c= SubFields E

proof end;

registration

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

cluster IntermediateFields (E,F) -> finite ;

coherence
IntermediateFields (E,F) is finite

proof end;

end;

definition

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

mode IntermediateField of E,F -> Field means :di: :: GALOIS_0:def 5
it in IntermediateFields (E,F);

existence
ex b₁ being Field st b₁ in IntermediateFields (E,F)

proof end;

end;

:: deftheorem di defines IntermediateField GALOIS_0:def 5 :
for F being Field
for E being FieldExtension of F
for b₃ being Field holds
( b₃ is IntermediateField of E,F iff b₃ in IntermediateFields (E,F) );

registration

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

cluster -> strict F -extending for IntermediateField of E,F;

coherence
for b₁ being IntermediateField of E,F holds
( b₁ is strict & b₁ is F -extending )

proof end;

end;

definition

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

func FieldExt (E,K) -> K -extending FieldExtension of F equals :: GALOIS_0:def 6
E;

coherence
E is K -extending FieldExtension of F

proof end;

end;

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

definition

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

func deg (E,K) -> Integer equals :: GALOIS_0:def 7
deg ((FieldExt (E,K)),K);

coherence
deg ((FieldExt (E,K)),K) is Integer ;

end;

:: deftheorem defines deg GALOIS_0:def 7 :
for F being Field
for E being FieldExtension of F
for K being IntermediateField of E,F holds deg (E,K) = deg ((FieldExt (E,K)),K);

registration

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

cluster FieldExt (E,K) -> K -extending K -finite ;

coherence
FieldExt (E,K) is K -finite by FIELD_7:31;

end;

registration

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

cluster -> F -finite for IntermediateField of E,F;

coherence
for b₁ being IntermediateField of E,F holds b₁ is F -finite

proof end;

end;

definition

let X be set ;

attr X is Group-membered means :dd: :: GALOIS_0:def 8
for x being object st x in X holds
x is Group;

end;

:: deftheorem dd defines Group-membered GALOIS_0:def 8 :
for X being set holds
( X is Group-membered iff for x being object st x in X holds
x is Group );

definition

let G be Group;
let X be set ;

attr X is G -Subgroup-membered means :defG1: :: GALOIS_0:def 9
for x being object st x in X holds
x is Subgroup of G;

end;

:: deftheorem defG1 defines -Subgroup-membered GALOIS_0:def 9 :
for G being Group
for X being set holds
( X is G -Subgroup-membered iff for x being object st x in X holds
x is Subgroup of G );

registration

cluster non empty Group-membered for set ;

existence
ex b₁ being set st
( b₁ is Group-membered & not b₁ is empty )

proof end;

end;

registration

let G be Group;

cluster non empty G -Subgroup-membered for set ;

existence
ex b₁ being set st
( b₁ is G -Subgroup-membered & not b₁ is empty )

proof end;

end;

registration

let G be Group;

cluster G -Subgroup-membered -> Group-membered for set ;

coherence
for b₁ being set st b₁ is G -Subgroup-membered holds
b₁ is Group-membered ;

cluster Subgroups G -> G -Subgroup-membered ;

coherence
Subgroups G is G -Subgroup-membered by GROUP_3:def 1;

cluster -> G -Subgroup-membered for Element of bool (Subgroups G);

coherence
for b₁ being Subset of (Subgroups G) holds b₁ is G -Subgroup-membered by GROUP_3:def 1;

end;

definition

let X be non empty Group-membered set ;
:: original: Element
redefine mode Element of X -> Group;
coherence
for b₁ being Element of X holds b₁ is Group by dd;

end;

definition

let G be Group;
let X be non empty G -Subgroup-membered set ;
:: original: Element
redefine mode Element of X -> Subgroup of G;
coherence
for b₁ being Element of X holds b₁ is Subgroup of G by defG1;

end;

registration

let G be Group;
let H be Subgroup of G;

cluster {H} -> G -Subgroup-membered ;

coherence
{H} is G -Subgroup-membered by TARSKI:def 1;

end;

registration

let G be Group;
let H1, H2 be Subgroup of G;

cluster {H1,H2} -> G -Subgroup-membered ;

coherence
{H1,H2} is G -Subgroup-membered

proof end;

end;

definition

let G be Group;

mode SubGroup of G -> Subgroup of G means :dSG: :: GALOIS_0:def 10
it in Subgroups G;

existence
ex b₁ being Subgroup of G st b₁ in Subgroups G

proof end;

end;

:: deftheorem dSG defines SubGroup GALOIS_0:def 10 :
for G being Group
for b₂ being Subgroup of G holds
( b₂ is SubGroup of G iff b₂ in Subgroups G );

registration

let G be Group;

cluster -> strict for SubGroup of G;

coherence
for b₁ being SubGroup of G holds b₁ is strict

proof end;

end;

registration

let G be Group;

cluster non empty finite strict unital Group-like associative for SubGroup of G;

existence
ex b₁ being SubGroup of G st b₁ is finite

proof end;

end;

registration

let G be finite Group;

cluster -> finite for SubGroup of G;

coherence
for b₁ being SubGroup of G holds b₁ is finite ;

end;

notation

let G be Group;
synonym order G for card G;

end;

definition

let F be Field;
let X be set ;

attr X is F -Subfield-membered means :def1: :: GALOIS_0:def 11
for x being object st x in X holds
x is Subfield of F;

end;

:: deftheorem def1 defines -Subfield-membered GALOIS_0:def 11 :
for F being Field
for X being set holds
( X is F -Subfield-membered iff for x being object st x in X holds
x is Subfield of F );

definition

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

attr X is E -intermediate-membered means :def1i: :: GALOIS_0:def 12
for x being object st x in X holds
x is IntermediateField of E,F;

end;

:: deftheorem def1i defines -intermediate-membered GALOIS_0:def 12 :
for F being Field
for E being FieldExtension of F
for X being set holds
( X is E -intermediate-membered iff for x being object st x in X holds
x is IntermediateField of E,F );

registration

let F be Field;

cluster non empty F -Subfield-membered for set ;

existence
ex b₁ being set st
( b₁ is F -Subfield-membered & not b₁ is empty )

proof end;

end;

registration

let F be Field;

cluster F -Subfield-membered -> Field-membered for set ;

coherence
for b₁ being set st b₁ is F -Subfield-membered holds
b₁ is Field-membered

proof end;

cluster SubFields F -> F -Subfield-membered ;

coherence
SubFields F is F -Subfield-membered

proof end;

cluster -> F -Subfield-membered for Element of bool (SubFields F);

coherence
for b₁ being Subset of (SubFields F) holds b₁ is F -Subfield-membered

proof end;

end;

registration

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

cluster non empty E -intermediate-membered for set ;

existence
ex b₁ being set st
( b₁ is E -intermediate-membered & not b₁ is empty )

proof end;

end;

registration

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

cluster E -intermediate-membered -> E -Subfield-membered for set ;

coherence
for b₁ being set st b₁ is E -intermediate-membered holds
b₁ is E -Subfield-membered

proof end;

cluster IntermediateFields (E,F) -> non empty E -intermediate-membered ;

coherence
( not IntermediateFields (E,F) is empty & IntermediateFields (E,F) is E -intermediate-membered )

proof end;

cluster -> E -intermediate-membered for Element of bool (IntermediateFields (E,F));

coherence
for b₁ being Subset of (IntermediateFields (E,F)) holds b₁ is E -intermediate-membered

proof end;

end;

definition

let F be Field;
let X be non empty F -Subfield-membered set ;
:: original: Element
redefine mode Element of X -> Subfield of F;
coherence
for b₁ being Element of X holds b₁ is Subfield of F by def1;

end;

definition

let F be Field;
let E be FieldExtension of F;
let X be non empty E -intermediate-membered set ;
:: original: Element
redefine mode Element of X -> IntermediateField of E,F;
coherence
for b₁ being Element of X holds b₁ is IntermediateField of E,F by def1i;

end;

registration

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

cluster {F} -> E -Subfield-membered ;

coherence
{F} is E -Subfield-membered by TARSKI:def 1;

end;

registration

let E be Field;
let F1, F2 be Subfield of E;

cluster {F1,F2} -> E -Subfield-membered ;

coherence
{F1,F2} is E -Subfield-membered

proof end;

end;

registration

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

cluster {K} -> E -intermediate-membered ;

coherence
{K} is E -intermediate-membered by TARSKI:def 1;

end;

registration

let F be Field;
let E be FieldExtension of F;
let K1, K2 be IntermediateField of E,F;

cluster {K1,K2} -> E -intermediate-membered ;

coherence
{K1,K2} is E -intermediate-membered

proof end;

end;

definition

let L be Lattice;
:: original: LattRel
redefine func LattRel L -> Relation of the carrier of L;
coherence
LattRel L is Relation of the carrier of L

proof end;

end;

definition

let S, T be non empty RelStr ;
let g be Function of S,T;
let d be Function of T,S;
:: original: [
redefine func [g,d] -> Connection of S,T;
coherence
[g,d] is Connection of S,T

proof end;

end;

definition

let S, T be non empty RelStr ;
let g be Function of S,T;

func Closed g -> non empty Subset of T equals :: GALOIS_0:def 13
{ (g . o) where o is Element of S : verum } ;

coherence
{ (g . o) where o is Element of S : verum } is non empty Subset of T

proof end;

end;

:: deftheorem defines Closed GALOIS_0:def 13 :
for S, T being non empty RelStr
for g being Function of S,T holds Closed g = { (g . o) where o is Element of S : verum } ;

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;

definition

let S, T be non empty RelStr ;
let g be Function of S,T;
let d be Function of T,S;

func Restr (g,d) -> Function of (Closed d),(Closed g) equals :: GALOIS_0:def 14
g | (Closed d);

coherence
g | (Closed d) is Function of (Closed d),(Closed g) by mainA;

func Restr (d,g) -> Function of (Closed g),(Closed d) equals :: GALOIS_0:def 15
d | (Closed g);

coherence
d | (Closed g) is Function of (Closed g),(Closed d) by mainA;

end;

:: deftheorem defines Restr GALOIS_0:def 14 :
for S, T being non empty RelStr
for g being Function of S,T
for d being Function of T,S holds Restr (g,d) = g | (Closed d);

:: deftheorem defines Restr GALOIS_0:def 15 :
for S, T being non empty RelStr
for g being Function of S,T
for d being Function of T,S holds Restr (d,g) = d | (Closed g);

main: 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
( ( for s being Element of S holds
( s in Closed d iff d . (g . s) = s ) ) & ( for t being Element of T holds
( t in Closed g iff g . (d . t) = t ) ) & (g | (Closed d)) " = d | (Closed g) & (d | (Closed g)) " = g | (Closed d) & Restr (g,d) is bijective & Restr (d,g) is bijective )

proof end;

theorem :: GALOIS_0:2

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 a_Bijection of Closed d, Closed g & (Restr (g,d)) " = Restr (d,g) )

proof end;

theorem :: GALOIS_0:3

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 (d,g) is a_Bijection of Closed g, Closed d & (Restr (d,g)) " = Restr (g,d) )

proof end;

theorem :: GALOIS_0:4

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
for s being Element of S holds
( s in Closed d iff d . (g . s) = s ) by main;

theorem :: GALOIS_0:5

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
for t being Element of T holds
( t in Closed g iff g . (d . t) = t ) by main;

theorem hhg: :: GALOIS_0:6

for G1 being Group
for G2 being Subgroup of G1
for H1, H2 being Subset of G1
for H3, H4 being Subset of G2 st H1 = H3 & H2 = H4 holds
H1 * H2 = H3 * H4

proof end;

theorem hhf: :: GALOIS_0:7

for G1 being Group
for G2 being Subgroup of G1
for H1 being Subset of G1
for H2 being Subset of G2 st H1 = H2 holds
gr H1 = gr H2

proof end;

theorem :: GALOIS_0:8

for G1 being Group
for G2, H1, H2 being Subgroup of G1
for H3, H4 being Subgroup of G2 st H1 = H3 & H2 = H4 holds
( H3 "\/" H4 = H1 "\/" H2 & H3 /\ H4 = H1 /\ H2 )

proof end;

registration

let G be Group;

cluster the carrier of (lattice G) -> G -Subgroup-membered ;

coherence
the carrier of (lattice G) is G -Subgroup-membered

proof end;

cluster the carrier of (LattPOSet (lattice G)) -> G -Subgroup-membered ;

coherence
the carrier of (LattPOSet (lattice G)) is G -Subgroup-membered

proof end;

end;

lemmaG0: for G being Group
for M being non empty b₁ -Subgroup-membered set holds meet { the carrier of K where K is Element of M : verum } c= the carrier of G

proof end;

lemmaG1: for G being Group holds
( multMagma(# the carrier of G, the multF of G #) is Subgroup of G & G is Subgroup of multMagma(# the carrier of G, the multF of G #) )

proof end;

lemmaG2: for G being Group
for M being non empty b₁ -Subgroup-membered set holds meet { the carrier of K where K is Element of Subgroups G : for F being Group st F in M holds
F is Subgroup of K } c= the carrier of G

proof end;

definition

let G be Group;
let M be non empty G -Subgroup-membered set ;

func /\ M -> strict Subgroup of G means :defG2: :: GALOIS_0:def 16
the carrier of it = meet { the carrier of H where H is Element of M : verum } ;

existence
ex b₁ being strict Subgroup of G st the carrier of b₁ = meet { the carrier of H where H is Element of M : verum }

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = meet { the carrier of H where H is Element of M : verum } & the carrier of b₂ = meet { the carrier of H where H is Element of M : verum } holds
b₁ = b₂ by GROUP_2:59;

func \/ M -> strict Subgroup of G means :defG3: :: GALOIS_0:def 17
the carrier of it = meet { the carrier of H where H is Element of Subgroups G : for K being Group st K in M holds
K is Subgroup of H } ;

existence
ex b₁ being strict Subgroup of G st the carrier of b₁ = meet { the carrier of H where H is Element of Subgroups G : for K being Group st K in M holds
K is Subgroup of H }

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = meet { the carrier of H where H is Element of Subgroups G : for K being Group st K in M holds
K is Subgroup of H } & the carrier of b₂ = meet { the carrier of H where H is Element of Subgroups G : for K being Group st K in M holds
K is Subgroup of H } holds
b₁ = b₂ by GROUP_2:59;

end;

:: deftheorem defG2 defines /\ GALOIS_0:def 16 :
for G being Group
for M being non empty b₁ -Subgroup-membered set
for b₃ being strict Subgroup of G holds
( b₃ = /\ M iff the carrier of b₃ = meet { the carrier of H where H is Element of M : verum } );

:: deftheorem defG3 defines \/ GALOIS_0:def 17 :
for G being Group
for M being non empty b₁ -Subgroup-membered set
for b₃ being strict Subgroup of G holds
( b₃ = \/ M iff the carrier of b₃ = meet { the carrier of H where H is Element of Subgroups G : for K being Group st K in M holds
K is Subgroup of H } );

theorem lemG8: :: GALOIS_0:9

for G being Group
for M being non empty b₁ -Subgroup-membered set
for H being Element of M holds /\ M is Subgroup of H

proof end;

theorem lemG9: :: GALOIS_0:10

for G being Group
for M being non empty b₁ -Subgroup-membered set
for K being Subgroup of G st ( for H being Element of M holds K is Subgroup of H ) holds
K is Subgroup of /\ M

proof end;

theorem lemG10: :: GALOIS_0:11

for G being Group
for M being non empty b₁ -Subgroup-membered set
for H being Element of M holds H is Subgroup of \/ M

proof end;

theorem lemG11: :: GALOIS_0:12

for G being Group
for M being non empty b₁ -Subgroup-membered set
for K being Element of Subgroups G st ( for F being Element of M holds F is Subgroup of K ) holds
\/ M is Subgroup of K

proof end;

lemGx: for G being Group
for H1, H2 being Subgroup of G holds meet { the carrier of H1, the carrier of H2} = meet { the carrier of H where H is Element of {H1,H2} : verum }

proof end;

theorem :: GALOIS_0:13

for G being Group
for H1, H2 being Subgroup of G holds /\ {H1,H2} = H1 /\ H2

proof end;

theorem :: GALOIS_0:14

for G being Group
for H1, H2 being Subgroup of G holds \/ {H1,H2} = H1 "\/" H2

proof end;

registration

let G be Group;

cluster lattice G -> complete ;

coherence
lattice G is complete

proof end;

end;

theorem :: GALOIS_0:15

for G being Group
for G1, G2 being Element of the carrier of (LattPOSet (lattice G)) holds
( G1 <= G2 iff G1 is Subgroup of G2 )

proof end;

lemma0: for F being Field
for M being non empty b₁ -Subfield-membered set holds meet { the carrier of K where K is Element of M : verum } c= the carrier of F

proof end;

lemma1: for F being Field
for M being non empty b₁ -Subfield-membered set
for S being Subset of F st S = meet { the carrier of K where K is Element of M : verum } holds
S is inducing_subfield

proof end;

lemma2: for E being Field
for M being non empty b₁ -Subfield-membered set holds meet { the carrier of K where K is Element of SubFields E : for F being Field st F in M holds
F is Subfield of K } c= the carrier of E

proof end;

lemma3: for E being Field
for M being non empty b₁ -Subfield-membered set
for S being Subset of E st S = meet { the carrier of K where K is Element of SubFields E : for F being Field st F in M holds
F is Subfield of K } holds
S is inducing_subfield

proof end;

definition

let E be Field;
let M be non empty E -Subfield-membered set ;

func /\ M -> strict Subfield of E means :def2: :: GALOIS_0:def 18
the carrier of it = meet { the carrier of K where K is Element of M : verum } ;

existence
ex b₁ being strict Subfield of E st the carrier of b₁ = meet { the carrier of K where K is Element of M : verum }

proof end;

uniqueness
for b₁, b₂ being strict Subfield of E st the carrier of b₁ = meet { the carrier of K where K is Element of M : verum } & the carrier of b₂ = meet { the carrier of K where K is Element of M : verum } holds
b₁ = b₂ by EC_PF_1:8;

func \/ M -> strict Subfield of E means :def3: :: GALOIS_0:def 19
the carrier of it = meet { the carrier of K where K is Element of SubFields E : for F being Field st F in M holds
F is Subfield of K } ;

existence
ex b₁ being strict Subfield of E st the carrier of b₁ = meet { the carrier of K where K is Element of SubFields E : for F being Field st F in M holds
F is Subfield of K }

proof end;

uniqueness
for b₁, b₂ being strict Subfield of E st the carrier of b₁ = meet { the carrier of K where K is Element of SubFields E : for F being Field st F in M holds
F is Subfield of K } & the carrier of b₂ = meet { the carrier of K where K is Element of SubFields E : for F being Field st F in M holds
F is Subfield of K } holds
b₁ = b₂ by EC_PF_1:8;

end;

:: deftheorem def2 defines /\ GALOIS_0:def 18 :
for E being Field
for M being non empty b₁ -Subfield-membered set
for b₃ being strict Subfield of E holds
( b₃ = /\ M iff the carrier of b₃ = meet { the carrier of K where K is Element of M : verum } );

:: deftheorem def3 defines \/ GALOIS_0:def 19 :
for E being Field
for M being non empty b₁ -Subfield-membered set
for b₃ being strict Subfield of E holds
( b₃ = \/ M iff the carrier of b₃ = meet { the carrier of K where K is Element of SubFields E : for F being Field st F in M holds
F is Subfield of K } );

theorem lem8: :: GALOIS_0:16

for E being Field
for M being non empty b₁ -Subfield-membered set
for F being Element of M holds /\ M is Subfield of F

proof end;

theorem lem9: :: GALOIS_0:17

for E being Field
for M being non empty b₁ -Subfield-membered set
for K being Subfield of E st ( for F being Element of M holds K is Subfield of F ) holds
K is Subfield of /\ M

proof end;

theorem lem10: :: GALOIS_0:18

for E being Field
for M being non empty b₁ -Subfield-membered set
for F being Element of M holds F is Subfield of \/ M

proof end;

theorem lem11: :: GALOIS_0:19

for E being Field
for M being non empty b₁ -Subfield-membered set
for K being Element of SubFields E st ( for F being Element of M holds F is Subfield of K ) holds
\/ M is Subfield of K

proof end;

theorem lem12: :: GALOIS_0:20

for F being Field
for E being FieldExtension of F
for M being non empty Subset of (IntermediateFields (E,F)) holds /\ M is IntermediateField of E,F

proof end;

theorem lem13: :: GALOIS_0:21

for F being Field
for E being FieldExtension of F
for M being non empty Subset of (IntermediateFields (E,F)) holds \/ M is IntermediateField of E,F

proof end;

definition

let F be Field;
let E be FieldExtension of F;
let K1, K2 be IntermediateField of E,F;

func K1 "/\" K2 -> IntermediateField of E,F equals :: GALOIS_0:def 20
/\ {K1,K2};

coherence
/\ {K1,K2} is IntermediateField of E,F

proof end;

commutativity
for b₁, K1, K2 being IntermediateField of E,F st b₁ = /\ {K1,K2} holds
b₁ = /\ {K2,K1} ;

func K1 "\/" K2 -> IntermediateField of E,F equals :: GALOIS_0:def 21
\/ {K1,K2};

coherence
\/ {K1,K2} is IntermediateField of E,F

proof end;

commutativity
for b₁, K1, K2 being IntermediateField of E,F st b₁ = \/ {K1,K2} holds
b₁ = \/ {K2,K1} ;

end;

:: deftheorem defines "/\" GALOIS_0:def 20 :
for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds K1 "/\" K2 = /\ {K1,K2};

:: deftheorem defines "\/" GALOIS_0:def 21 :
for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds K1 "\/" K2 = \/ {K1,K2};

registration

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

reduce K "/\" K to K;

reducibility
K "/\" K = K

proof end;

reduce K "\/" K to K;

reducibility
K "\/" K = K

proof end;

end;

theorem lat1: :: GALOIS_0:22

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds K1 "/\" (K1 "\/" K2) = K1

proof end;

theorem lat2: :: GALOIS_0:23

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds (K1 "/\" K2) "\/" K2 = K2

proof end;

theorem :: GALOIS_0:24

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds K1 "/\" K2 = K2 "/\" K1 ;

theorem :: GALOIS_0:25

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds K1 "\/" K2 = K2 "\/" K1 ;

lemm1: for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds the carrier of (K1 "/\" K2) = the carrier of K1 /\ the carrier of K2

proof end;

theorem lat5: :: GALOIS_0:26

for F being Field
for E being FieldExtension of F
for K1, K2, K3 being IntermediateField of E,F holds (K1 "/\" K2) "/\" K3 = K1 "/\" (K2 "/\" K3)

proof end;

theorem lat6: :: GALOIS_0:27

for F being Field
for E being FieldExtension of F
for K1, K2, K3 being IntermediateField of E,F holds (K1 "\/" K2) "\/" K3 = K1 "\/" (K2 "\/" K3)

proof end;

theorem lem20: :: GALOIS_0:28

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds
( K1 "/\" K2 = K1 iff K1 is Subfield of K2 )

proof end;

theorem :: GALOIS_0:29

for F being Field
for E being FieldExtension of F
for K1, K2 being IntermediateField of E,F holds
( K1 "\/" K2 = K2 iff K1 is Subfield of K2 )

proof end;

definition

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

func SubMeet E -> BinOp of (IntermediateFields (E,F)) means :dM: :: GALOIS_0:def 22
for K1, K2 being IntermediateField of E,F holds it . (K1,K2) = K1 "/\" K2;

existence
ex b₁ being BinOp of (IntermediateFields (E,F)) st
for K1, K2 being IntermediateField of E,F holds b₁ . (K1,K2) = K1 "/\" K2

proof end;

uniqueness
for b₁, b₂ being BinOp of (IntermediateFields (E,F)) st ( for K1, K2 being IntermediateField of E,F holds b₁ . (K1,K2) = K1 "/\" K2 ) & ( for K1, K2 being IntermediateField of E,F holds b₂ . (K1,K2) = K1 "/\" K2 ) holds
b₁ = b₂

proof end;

func SubJoin E -> BinOp of (IntermediateFields (E,F)) means :dJ: :: GALOIS_0:def 23
for K1, K2 being IntermediateField of E,F holds it . (K1,K2) = K1 "\/" K2;

existence
ex b₁ being BinOp of (IntermediateFields (E,F)) st
for K1, K2 being IntermediateField of E,F holds b₁ . (K1,K2) = K1 "\/" K2

proof end;

uniqueness
for b₁, b₂ being BinOp of (IntermediateFields (E,F)) st ( for K1, K2 being IntermediateField of E,F holds b₁ . (K1,K2) = K1 "\/" K2 ) & ( for K1, K2 being IntermediateField of E,F holds b₂ . (K1,K2) = K1 "\/" K2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem dM defines SubMeet GALOIS_0:def 22 :
for F being Field
for E being FieldExtension of F
for b₃ being BinOp of (IntermediateFields (E,F)) holds
( b₃ = SubMeet E iff for K1, K2 being IntermediateField of E,F holds b₃ . (K1,K2) = K1 "/\" K2 );

:: deftheorem dJ defines SubJoin GALOIS_0:def 23 :
for F being Field
for E being FieldExtension of F
for b₃ being BinOp of (IntermediateFields (E,F)) holds
( b₃ = SubJoin E iff for K1, K2 being IntermediateField of E,F holds b₃ . (K1,K2) = K1 "\/" K2 );

definition

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

func IntermediateFields E -> Lattice equals :: GALOIS_0:def 24
LattStr(# (IntermediateFields (E,F)),(SubJoin E),(SubMeet E) #);

coherence
LattStr(# (IntermediateFields (E,F)),(SubJoin E),(SubMeet E) #) is Lattice

proof end;

end;

:: deftheorem defines IntermediateFields GALOIS_0:def 24 :
for F being Field
for E being FieldExtension of F holds IntermediateFields E = LattStr(# (IntermediateFields (E,F)),(SubJoin E),(SubMeet E) #);

registration

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

cluster the carrier of (IntermediateFields E) -> non empty E -intermediate-membered ;

coherence
( not the carrier of (IntermediateFields E) is empty & the carrier of (IntermediateFields E) is E -intermediate-membered ) ;

end;

lemco1: for F being Field
for E being FieldExtension of F ex c being Element of (IntermediateFields E) st
for a being Element of (IntermediateFields E) holds
( c "\/" a = c & a "\/" c = c )

proof end;

lemco2: for F being Field
for E being FieldExtension of F ex c being Element of (IntermediateFields E) st
for a being Element of (IntermediateFields E) holds
( c "/\" a = c & a "/\" c = c )

proof end;

theorem :: GALOIS_0:30

for F being Field
for E being FieldExtension of F holds Top (IntermediateFields E) = doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #)

proof end;

theorem :: GALOIS_0:31

for F being Field
for E being FieldExtension of F holds Bottom (IntermediateFields E) = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #)

proof end;

registration

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

cluster IntermediateFields E -> complete ;

coherence
IntermediateFields E is complete

proof end;

end;

registration

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

cluster the carrier of (LattPOSet (IntermediateFields E)) -> non empty E -intermediate-membered ;

coherence
( not the carrier of (LattPOSet (IntermediateFields E)) is empty & the carrier of (LattPOSet (IntermediateFields E)) is E -intermediate-membered )

proof end;

end;

theorem :: GALOIS_0:32

for F being Field
for E being FieldExtension of F
for K1, K2 being Element of the carrier of (LattPOSet (IntermediateFields E)) holds
( K1 <= K2 iff K1 is Subfield of K2 )

proof end;

definition

let R be Ring;
let X be set ;

attr X is R -functional means :PP: :: GALOIS_0:def 25
for o being object st o in X holds
o is Function of R,R;

end;

:: deftheorem PP defines -functional GALOIS_0:def 25 :
for R being Ring
for X being set holds
( X is R -functional iff for o being object st o in X holds
o is Function of R,R );

definition

let R be Ring;
let L be 1-sorted ;

attr L is R -functional means :PQ: :: GALOIS_0:def 26
the carrier of L is R -functional ;

end;

:: deftheorem PQ defines -functional GALOIS_0:def 26 :
for R being Ring
for L being 1-sorted holds
( L is R -functional iff the carrier of L is R -functional );

registration

let R be Ring;

cluster non empty R -functional for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is R -functional )

proof end;

end;

registration

let R be Ring;
let X be R -functional set ;

cluster -> R -functional for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is R -functional by PP;

end;

definition

let R be Ring;
let X be non empty R -functional set ;
:: original: Element
redefine mode Element of X -> Function of R,R;
coherence
for b₁ being Element of X holds b₁ is Function of R,R by PP;

end;

registration

let R be Ring;

cluster non empty R -functional for 1-sorted ;

existence
ex b₁ being 1-sorted st
( not b₁ is empty & b₁ is R -functional )

proof end;

end;

registration

let R be Ring;
let L be R -functional 1-sorted ;

cluster -> R -functional for Element of bool the carrier of L;

coherence
for b₁ being Subset of L holds b₁ is R -functional by PP, PQ;

end;

registration

let R be Ring;
let L be non empty R -functional 1-sorted ;

cluster the carrier of L -> R -functional ;

coherence
the carrier of L is R -functional by PQ;

end;

registration

let R be Ring;
let S be RingExtension of R;

cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty total quasi_total R -fixing for Element of bool [: the carrier of S, the carrier of S:];

existence
ex b₁ being Function of S,S st b₁ is R -fixing

proof end;

end;

registration

let R be Ring;
let S be RingExtension of R;

cluster id S -> R -fixing ;

coherence
id S is R -fixing

proof end;

end;

registration

let R be Ring;
let S be RingExtension of R;
let f, g be R -fixing Function of S,S;

cluster g * f -> R -fixing for Function of S,S;

coherence
for b₁ being Function of S,S st b₁ = f * g holds
b₁ is R -fixing

proof end;

end;

registration

let R be Ring;
let S be RingExtension of R;
let f be R -fixing Function of S,S;
let n be Nat;

cluster f `^ n -> R -fixing for Function of S,S;

coherence
for b₁ being Function of S,S st b₁ = f `^ n holds
b₁ is R -fixing

proof end;

end;

registration

let R be Ring;
let S be RingExtension of R;
let f be one-to-one R -fixing Function of S,S;

cluster f " -> one-to-one R -fixing for Function of S,S;

coherence
for b₁ being Function of S,S st b₁ = f " holds
( b₁ is R -fixing & b₁ is one-to-one )

proof end;

end;

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;

definition

let R be Ring;
let h be additive Function of R,R;

func PolyHom h -> Function of (Polynom-Ring R),(Polynom-Ring R) means :dp: :: GALOIS_0:def 27
for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (it . f) . i = h . (f . i);

existence
ex b₁ being Function of (Polynom-Ring R),(Polynom-Ring R) st
for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b₁ . f) . i = h . (f . i)

proof end;

uniqueness
for b₁, b₂ being Function of (Polynom-Ring R),(Polynom-Ring R) st ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b₁ . f) . i = h . (f . i) ) & ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b₂ . f) . i = h . (f . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem dp defines PolyHom GALOIS_0:def 27 :
for R being Ring
for h being additive Function of R,R
for b₃ being Function of (Polynom-Ring R),(Polynom-Ring R) holds
( b₃ = PolyHom h iff for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b₃ . f) . i = h . (f . i) );

registration

let R be Ring;
let h be Homomorphism of R;

cluster PolyHom h -> additive unity-preserving multiplicative ;

coherence
( PolyHom h is additive & PolyHom h is multiplicative & PolyHom h is unity-preserving )

proof end;

end;

theorem :: GALOIS_0:33

for R being Ring
for h being Homomorphism of R holds (PolyHom h) . (0_. R) = 0_. R

proof end;

theorem :: GALOIS_0:34

for R being Ring
for h being Homomorphism of R holds (PolyHom h) . (1_. R) = 1_. R

proof end;

theorem :: GALOIS_0:35

for R being Ring
for h being Homomorphism of R
for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p + q) = ((PolyHom h) . p) + ((PolyHom h) . q) by VECTSP_1:def 20;

theorem :: GALOIS_0:36

for R being Ring
for h being Homomorphism of R
for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p * q) = ((PolyHom h) . p) * ((PolyHom h) . q) by GROUP_6:def 6;

theorem :: GALOIS_0:37

for R being Ring
for h being Homomorphism of R
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds (PolyHom h) . (a * p) = (h . a) * ((PolyHom h) . p)

proof end;

theorem :: GALOIS_0:38

for R being Ring
for h being Homomorphism of R
for p being Element of the carrier of (Polynom-Ring R)
for x being Element of R holds h . (eval (p,x)) = eval (((PolyHom h) . p),(h . x))

proof end;

theorem :: GALOIS_0:39

for R being domRing
for h being Homomorphism of R
for p being Element of the carrier of (Polynom-Ring R)
for a, x being Element of R holds h . (eval ((a * p),x)) = (h . a) * (eval (((PolyHom h) . p),(h . x)))

proof end;

theorem :: GALOIS_0:40

for F being Field
for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for a being Element of E
for h being b₁ -fixing Homomorphism of E holds h . (Ext_eval (p,a)) = Ext_eval (p,(h . a))

proof end;

theorem Th32: :: GALOIS_0:41

for R being Ring
for h being Monomorphism of R
for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) = deg p

proof end;

theorem :: GALOIS_0:42

for R being Ring
for h being Monomorphism of R
for p being Element of the carrier of (Polynom-Ring R) holds LM ((PolyHom h) . p) = (PolyHom h) . (LM p)

proof end;

theorem G4a: :: GALOIS_0:43

for F being Field
for h being Homomorphism of F
for a being Element of F holds (PolyHom h) . (X- a) = X- (h . a)

proof end;

theorem :: GALOIS_0:44

for F being Field
for S being non empty finite Subset of F
for p being Ppoly of F,S
for h being Monomorphism of F holds (PolyHom h) . p is Ppoly of F,(h .: S)

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

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;

theorem :: GALOIS_0:45

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
( h | S is Permutation of S & (h ") | S is Permutation of S )

proof end;