:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies ARYTM_3, VECTSP_1, TARSKI, STRUCT_0, SUBSET_1, SUPINF_2, RING_3,
MESFUNC1, RLSUB_2, PBOOLE, FUNCSDOM, EC_PF_1, HURWITZ, CARD_1, RING_2,
FUNCT_1, INT_1, FUNCT_2, RELAT_1, NUMBERS, POLYNOM5, FOMODEL1, FIELD_14,
XCMPLX_0, FIELD_9, FINSEQ_1, FIELD_12, EQREL_1, ARYTM_1, FIELD_4,
QUOFIELD, C0SP1, XBOOLE_0, XXREAL_0, GLIB_000, FIELD_1, POLYNOM2,
ALGSEQ_1, REALSET1, GROUP_4, NAT_1, VECTSP_2, FIELD_8, GROUP_1, ALGNUM_1,
ALGSTR_0, LATTICES, LATTICE3, FINSET_1, CONLAT_1, REWRITE1, POLYNOM3,
WAYBEL_0, POLYNOM1, MOD_4, GROUP_2, RATFUNC1, FIELD_16, MSSUBFAM, PEPIN,
GROUP_3, WAYBEL_1, ORDERS_2, SETFAM_1, BINOP_1, RING_5, FILTER_1,
MCART_1, GROUP_6, ZFMISC_1, GALOIS_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FINSET_1,
REALSET1, XTUPLE_0, FUNCT_1, ORDINAL1, FUNCT_2, BINOP_1, SETFAM_1,
NUMBERS, CARD_1, PARTFUN1, NAT_D, XCMPLX_0, XXREAL_0, NAT_1, INT_1,
ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5, WAYBEL_0, WAYBEL_1, ORDERS_2,
LATTICES, LATTICE3, FILTER_1, CONLAT_1, STRUCT_0, ALGSTR_0, VECTSP_1,
VECTSP_2, C0SP1, EC_PF_1, RATFUNC1, GROUP_1, GROUP_2, GROUP_3, GROUP_4,
GROUP_6, QUOFIELD, RING_2, RING_4, RING_5, HURWITZ, ALGNUM_1, FIELD_1,
FIELD_4, FIELD_7, FIELD_8, FIELD_9, FIELD_12, FIELD_14, FIELD_16;
constructors REALSET1, ALGNUM_1, RINGCAT1, RATFUNC1, ALGSEQ_1, LATTICE3,
CONLAT_1, GROUP_4, POLYNOM4, NAT_D, RING_5, FIELD_8, FIELD_9, FIELD_14,
FIELD_16;
registrations XBOOLE_0, XXREAL_0, XREAL_0, NAT_1, INT_1, SUBSET_1, RELSET_1,
RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, CARD_1, FINSET_1, XTUPLE_0,
LATTICES, LATTICE3, STRUCT_0, VECTSP_1, VECTSP_2, MOD_4, GROUP_2,
GROUP_3, GROUP_4, RING_3, RING_4, RING_5, RINGCAT1, POLYNOM3, POLYNOM4,
POLYNOM5, EC_PF_1, FIELD_1, FIELD_8, FIELD_12, FIELD_14, FIELD_16,
GROUP_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities REALSET1, BINOP_1, STRUCT_0, FIELD_9;
expansions TARSKI, FUNCT_2, STRUCT_0, VECTSP_1, FIELD_7, FIELD_8, FIELD_16;
theorems GROUP_1, VECTSP_1, C0SP1, FUNCT_2, TARSKI, FUNCT_1, EC_PF_1, NAT_1,
RATFUNC1, POLYNOM5, RING_4, RING_5, HURWITZ, XREAL_1, XBOOLE_0, FIELD_4,
POLYNOM3, ZFMISC_1, XXREAL_0, FIELD_6, ALGSEQ_1, CARD_2, FIELD_7,
FIELD_8, GROUP_4, FIELD_5, FIELD_14, NIVEN, FIELD_12, RING_2, GROUP_6,
LATTICES, FIELD_1, RELAT_1, XBOOLE_1, FIELD_13, GROUP_2, FIELD_16,
LATTICE3, CARD_1, WAYBEL_0, CONLAT_1, ORDERS_2, GROUP_3, SETFAM_1,
FILTER_1, INT_1, POLYNOM4, VECTSP_8;
schemes NAT_1, FUNCT_2, BINOP_1, ALGSEQ_1;
begin :: Preliminaries
definition
let A,B be set;
attr B is A-bijective means
ex f being Function of A,B st f is bijective;
end;
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:
it is bijective;
existence by AS;
end;
theorem
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
let E be Field, F1,F2 be Subfield of E;
H3: the addF of F2 = (the addF of E) || the carrier of F2 &
the multF of F2 = (the multF of E) || the carrier of F2
by EC_PF_1:def 1;
assume AS: the carrier of F1 c= the carrier of F2; then
B: (the addF of F2) || the carrier of F1
= (the addF of E) || the carrier of F1 by H3,ZFMISC_1:96,RELAT_1:74
.= the addF of F1 by EC_PF_1:def 1;
C: (the multF of F2) || the carrier of F1
= (the multF of E) || the carrier of F1 by H3,AS,ZFMISC_1:96,RELAT_1:74
.= the multF of F1 by EC_PF_1:def 1;
D: 1.F1 = 1.E by EC_PF_1:def 1 .= 1.F2 by EC_PF_1:def 1;
0.F1 = 0.E by EC_PF_1:def 1 .= 0.F2 by EC_PF_1:def 1;
hence F1 is Subfield of F2 by AS,B,C,D,EC_PF_1:def 1;
end;
registration
let F be finite Field;
cluster SubFields F -> finite;
coherence
proof
set M = bool(the carrier of F);
defpred P[object,object] means
ex K being strict Subfield of F st $1 = K & $2 = the carrier of K;
A: for x being object st x in SubFields F
ex y being object st y in M & P[x,y]
proof
let x be object;
assume x in SubFields F; then
consider K being strict Field such that
A1: x = K & K is Subfield of F by FIELD_12:def 13;
take y = the carrier of K;
y c= the carrier of F by A1,EC_PF_1:def 1;
hence y in M & P[x,y] by A1;
end;
consider f being Function of SubFields F, M such that
B: for o being object st o in SubFields F holds P[o,f.o]
from FUNCT_2:sch 1(A);
now let x1,x2 being object;
assume C0: x1 in SubFields F & x2 in SubFields F & f.x1 = f.x2;
consider E1 being strict Subfield of F such that
C3: E1 = x1 & f.x1 = the carrier of E1 by C0,B;
consider E2 being strict Subfield of F such that
C4: E2 = x2 & f.x2 = the carrier of E2 by C0,B;
thus x1 = x2 by C0,C3,C4,EC_PF_1:8;
end; then
C: f is one-to-one by FUNCT_2:19;
rng f c= M by RELAT_1:def 19; then
dom f is finite by C,CARD_1:59;
hence thesis by FUNCT_2:def 1;
end;
end;
definition
let E be Field;
let F be Subfield of E;
func FieldExt(E,F) -> FieldExtension of F equals
E;
coherence by FIELD_4:7;
end;
definition
let E be Field;
let F be Subfield of E;
func deg(E,F) -> Integer equals
deg(FieldExt(E,F),F);
coherence;
end;
lempr1:
for F being Field
for E being FieldExtension of F
holds IntermediateFields(E,F) c= SubFields E
proof
let F be Field, E be FieldExtension of F;
now let o be object;
assume o in IntermediateFields(E,F); then
consider K being strict Field such that
A: K = o & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
thus o in SubFields E by A,FIELD_12:def 13;
end;
hence thesis;
end;
registration
let F be finite Field;
let E be F-finite FieldExtension of F;
cluster IntermediateFields(E,F) -> finite;
coherence
proof
IntermediateFields(E,F) c= SubFields E by lempr1;
hence IntermediateFields(E,F) is finite;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
mode IntermediateField of E,F -> Field means :di:
it in IntermediateFields(E,F);
existence
proof
set F1 = the doubleLoopStr of F;
H: F1 == F; then
reconsider F1 as strict FieldExtension of F by FIELD_4:7;
take F1;
A: F is Subfield of F1 by FIELD_4:7;
E is FieldExtension of F1 by H,FIELD_12:37; then
F1 is Subfield of E by FIELD_4:7;
hence thesis by A,FIELD_14:4;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster -> strict F-extending for IntermediateField of E,F;
coherence
proof
let K be IntermediateField of E,F;
K in IntermediateFields(E,F) by di; then
consider K1 being strict Field such that
A: K = K1 & F is Subfield of K1 & K1 is Subfield of E
by FIELD_14:def 1;
thus K is strict by A;
thus K is F-extending by A,FIELD_4:7;
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
E;
coherence
proof
K in IntermediateFields(E,F) by di; then
consider K1 being strict Field such that
A: K = K1 & F is Subfield of K1 & K1 is Subfield of E by FIELD_14:def 1;
thus thesis by A,FIELD_4:7;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
let K be IntermediateField of E,F;
func deg(E,K) -> Integer equals
deg(FieldExt(E,K),K);
coherence;
end;
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-finite;
coherence 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
proof
let K be IntermediateField of E,F;
FieldExt(E,K) = E;
hence thesis by FIELD_7:31;
end;
end;
begin :: Sets of Groups
definition
let X be set;
attr X is Group-membered means :dd:
for x being object st x in X holds x is Group;
end;
definition
let G be Group;
let X be set;
attr X is G-Subgroup-membered means :defG1:
for x being object st x in X holds x is Subgroup of G;
end;
registration
cluster Group-membered non empty for set;
existence
proof
set G = the Group;
take X = { G };
thus thesis by TARSKI:def 1;
end;
end;
registration
let G be Group;
cluster G-Subgroup-membered non empty for set;
existence
proof
H: G is Subgroup of G by GROUP_2:54;
take X = {G};
thus thesis by H,TARSKI:def 1;
end;
end;
registration
let G be Group;
cluster G-Subgroup-membered -> Group-membered for set;
coherence;
cluster Subgroups(G) -> G-Subgroup-membered;
coherence by GROUP_3:def 1;
cluster -> G-Subgroup-membered for Subset of Subgroups(G);
coherence by GROUP_3:def 1;
end;
definition
let X be non empty Group-membered set;
redefine mode Element of X -> Group; :: redefines Element (SUBSET_1, definition)
coherence by dd;
end;
definition
let G be Group;
let X be non empty G-Subgroup-membered set;
redefine mode Element of X -> Subgroup of G; :: redefines Element (SUBSET_1, definition)
coherence by defG1;
end;
registration
let G be Group;
let H be Subgroup of G;
cluster {H} -> G-Subgroup-membered;
coherence by TARSKI:def 1;
end;
registration
let G be Group;
let H1,H2 be Subgroup of G;
cluster {H1,H2} -> G-Subgroup-membered;
coherence
proof
let o be object;
assume o in {H1,H2}; then
per cases by TARSKI:def 2;
suppose o = H1;
hence o is Subgroup of G;
end;
suppose o = H2;
hence o is Subgroup of G;
end;
end;
end;
definition
let G be Group;
mode SubGroup of G -> Subgroup of G means :dSG:
it in Subgroups(G);
existence
proof
take (1).G;
thus thesis by GROUP_3:def 1;
end;
end;
registration ::: MOVE
let G be Group;
cluster -> strict for SubGroup of G;
coherence
proof
let H be SubGroup of G;
H in Subgroups(G) by dSG;
hence H is strict by GROUP_3:def 1;
end;
end;
registration
let G be Group;
cluster finite for SubGroup of G;
existence
proof
(1).G in Subgroups(G) by GROUP_3:def 1; then
reconsider H = (1).G as SubGroup of G by dSG;
take H;
thus thesis;
end;
end;
registration
let G be finite Group;
cluster -> finite for SubGroup of G;
coherence;
end;
notation
let G be Group;
synonym order G for card G;
end;
begin :: Sets of Subfields and Intermediate Fields
definition
let F be Field;
let X be set;
attr X is F-Subfield-membered means :def1:
for x being object st x in X holds x is Subfield of F;
end;
definition
let F be Field;
let E be FieldExtension of F;
let X be set;
attr X is E-intermediate-membered means :def1i:
for x being object st x in X holds x is IntermediateField of E,F;
end;
registration
let F be Field;
cluster F-Subfield-membered non empty for set;
existence
proof
H: F is Subfield of F by FIELD_4:1;
take X = {F};
thus thesis by H,TARSKI:def 1;
end;
end;
registration
let F be Field;
cluster F-Subfield-membered -> Field-membered for set;
coherence
proof
let X be set;
assume X is F-Subfield-membered;
then for o being object st o in X holds o is Field;
hence thesis by FIELD_12:def 12;
end;
cluster SubFields(F) -> F-Subfield-membered;
coherence
proof
let x be object;
assume x in SubFields(F); then
ex K being strict Field st K = x & K is Subfield of F by FIELD_12:def 13;
hence x is Subfield of F;
end;
cluster -> F-Subfield-membered for Subset of SubFields(F);
coherence
proof
let X be Subset of SubFields(F);
let x be object;
assume x in X; then
ex K being strict Field st K = x & K is Subfield of F by FIELD_12:def 13;
hence x is Subfield of F;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster E-intermediate-membered non empty for set;
existence
proof
set K = the IntermediateField of E,F;
take X = {K};
thus thesis by TARSKI:def 1;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster E-intermediate-membered -> E-Subfield-membered for set;
coherence
proof
let X be set;
assume A: X is E-intermediate-membered;
let x be object;
assume x in X;
then x is IntermediateField of E,F by A;
then x in IntermediateFields(E,F) by di;
then ex K being strict Field st K = x &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
hence x is Subfield of E;
end;
cluster IntermediateFields(E,F) -> non empty E-intermediate-membered;
coherence
proof
now let x be object;
assume A: x in IntermediateFields(E,F);
then ex K being strict Field st K = x &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
hence x is IntermediateField of E,F by A,di;
end;
hence thesis;
end;
cluster -> E-intermediate-membered for Subset of IntermediateFields(E,F);
coherence
proof
let X be Subset of IntermediateFields(E,F);
let x be object;
assume A: x in X;
then ex K being strict Field st K = x &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
hence x is IntermediateField of E,F by A,di;
end;
end;
definition
let F be Field;
let X be non empty F-Subfield-membered set;
redefine mode Element of X -> Subfield of F; :: redefines Element (SUBSET_1, definition)
coherence by def1;
end;
definition
let F be Field;
let E be FieldExtension of F;
let X be non empty E-intermediate-membered set;
redefine mode Element of X -> IntermediateField of E,F; :: redefines Element (SUBSET_1, definition)
coherence by def1i;
end;
registration
let E be Field;
let F be Subfield of E;
cluster {F} -> E-Subfield-membered;
coherence by TARSKI:def 1;
end;
registration
let E be Field;
let F1,F2 be Subfield of E;
cluster {F1,F2} -> E-Subfield-membered;
coherence
proof
let o be object;
assume o in {F1,F2}; then
per cases by TARSKI:def 2;
suppose o = F1;
hence o is Subfield of E;
end;
suppose o = F2;
hence o is Subfield of E;
end;
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 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
proof
let o be object;
assume o in {K1,K2}; then
per cases by TARSKI:def 2;
suppose o = K1;
hence o is IntermediateField of E,F;
end;
suppose o = K2;
hence o is IntermediateField of E,F;
end;
end;
end;
definition ::: MOVE
let L be Lattice;
redefine func LattRel L -> Relation of the carrier of L; :: redefines LattRel (FILTER_1, definition)
coherence
proof
A1: LattRel L = { [p,q] where p is Element of L, q is Element of L: p [= q }
by FILTER_1:def 8;
now let o be object;
assume o in LattRel L;
then ex p,q being Element of L st o = [p,q] & p [= q by A1;
hence o in [:the carrier of L,the carrier of L:] by ZFMISC_1:87;
end;
then LattRel L c= [:the carrier of L,the carrier of L:];
hence LattRel L is Relation of the carrier of L;
end;
end;
begin :: On Galois Connections
definition
let S,T be non empty RelStr;
let g be Function of S,T, d be Function of T,S;
redefine func [g,d] -> Connection of S,T; :: redefines [ (TARSKI, definition)
coherence
proof
set C = [g,d];
thus C is Connection of S,T;
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
the set of all g.o where o is Element of S;
coherence
proof
set M = the set of all g.o where o is Element of S;
set s = the Element of S;
A: g.s in M;
now let o be object;
assume o in M; then
consider x being Element of S such that A: o = g.x;
thus o in the carrier of T by A;
end;
then M c= the carrier of T;
hence thesis by A;
end;
end;
mainA:
for S,T being non empty RelStr
for g being Function of S,T, 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
let S,T be non empty RelStr, g be Function of S,T, d be Function of T,S;
reconsider g1 = g|(Closed d) as Function of (Closed d),the carrier of T
by FUNCT_2:32;
D: dom g1 = Closed d by FUNCT_2:def 1;
now let o be object;
assume o in rng g1; then
consider x being object such that
D1: x in dom g1 & g1.x = o by FUNCT_1:def 3;
reconsider x as Element of S by D,D1;
g.x = g1.x by D1,FUNCT_1:49;
hence o in Closed g by D1;
end; then
rng g1 c= Closed g; then
reconsider g1 as Function of (Closed d),(Closed g) by D,FUNCT_2:2;
g1 = g|(Closed d);
hence g|(Closed d) is Function of (Closed d),(Closed g);
reconsider d1 = d|(Closed g) as Function of (Closed g),the carrier of S
by FUNCT_2:32;
E: dom d1 = Closed g by FUNCT_2:def 1;
now let o be object;
assume o in rng d1; then
consider x being object such that
E1: x in dom d1 & d1.x = o by FUNCT_1:def 3;
reconsider x as Element of T by E,E1;
d.x = d1.x by E1,FUNCT_1:49;
hence o in Closed d by E1;
end; then
rng d1 c= Closed d; then
reconsider d1 as Function of (Closed g),(Closed d) by E,FUNCT_2:2;
d1 = d|(Closed g);
hence d|(Closed g) is Function of (Closed g),(Closed d);
end;
definition
let S,T be non empty RelStr;
let g be Function of S,T, d be Function of T,S;
func Restr(g,d) -> Function of Closed d, Closed g equals
g|(Closed d);
coherence by mainA;
func Restr(d,g) -> Function of Closed g, Closed d equals
d|(Closed g);
coherence by mainA;
end;
main:
for S,T being non empty Poset
for g being Function of S,T, 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
let S,T be non empty Poset, g be Function of S,T, d be Function of T,S;
assume [g,d] is co-Galois; then
consider f1 being Function of S,T,
f2 being Function of T,S such that
A: [f1,f2] = [g,d] & f1 is antitone & f2 is antitone &
for p1,p2 being Element of S, r1,r2 being Element of T
holds p1 <= f2.(f1.p1) & r1 <= f1.(f2.r1) by CONLAT_1:def 7;
B: f1 = [g,d]`1 by A .= g;
C: f2 = [g,d]`2 by A .= d;
reconsider g1 = g|(Closed d) as Function of (Closed d),(Closed g)
by mainA;
reconsider d1 = d|(Closed g) as Function of (Closed g),(Closed d)
by mainA;
K: now let s be Element of S;
now assume s in Closed d; then
consider t being Element of T such that F1: s = d.t;
F2: s <= d.(g.s) by A,B,C;
d.(g.(d.t)) <= d.t by A,B,C,WAYBEL_0:def 5;
hence d.(g.s) = s by F1,F2,ORDERS_2:2;
end;
hence s in Closed d iff d.(g.s) = s;
end;
hence for s being Element of S holds s in Closed d iff d.(g.s) = s;
E: now let t be Element of T;
now assume t in Closed g; then
consider s being Element of S such that F1: t = g.s;
F2: t <= g.(d.t) by A,B,C;
g.(d.(g.s)) <= g.s by A,B,C,WAYBEL_0:def 5;
hence g.(d.t) = t by F1,F2,ORDERS_2:2;
end;
hence t in Closed g iff g.(d.t) = t;
end;
hence for t being Element of T holds t in Closed g iff g.(d.t) = t;
now let o be object;
assume E1: o in Closed g; then
reconsider t = o as Element of T;
E2: d1.t = d.t by E1,FUNCT_1:49;
dom d1 = Closed g by FUNCT_2:def 1; then
E3: d1.t in rng d1 & rng d1 c= Closed d by E1,FUNCT_1:3,RELAT_1:def 19;
thus (g1 * d1).o = g1.(d1.t) by E1,FUNCT_2:15
.= g.(d.t) by E2,E3,FUNCT_1:49
.= t by E1,E
.= (id (Closed g)).o by E1,FUNCT_1:18;
end; then
G1: g1 * d1 = id(Closed g); then
B1: d1 is one-to-one & g1 is onto by FUNCT_2:23;
now let o be object;
assume E1: o in Closed d; then
reconsider s = o as Element of S;
E2: g1.s = g.s by E1,FUNCT_1:49;
dom g1 = Closed d by FUNCT_2:def 1; then
E3: g1.s in rng g1 & rng g1 c= Closed g by E1,FUNCT_1:3,RELAT_1:def 19;
thus (d1 * g1).o
= d1.(g1.s) by E1,FUNCT_2:15
.= d.(g.s) by E2,E3,FUNCT_1:49
.= s by E1,K
.= (id (Closed d)).o by E1,FUNCT_1:18;
end; then
G3: d1 * g1 = id(Closed d); then
g1 is one-to-one & d1 is onto by FUNCT_2:23;
hence (g|(Closed d))" = d|(Closed g) & (d|(Closed g))" = g|(Closed d)
by G1,B1,G3,FUNCT_2:30;
thus thesis by G3,G1,FUNCT_2:23;
end;
theorem
for S,T being non empty Poset
for g being Function of S,T, 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
let S,T be non empty Poset, g be Function of S,T, d be Function of T,S;
assume A: [g,d] is co-Galois;
then B: Restr(g,d) is bijective by main;
then Closed g is (Closed d)-bijective;
hence Restr(g,d) is a_Bijection of Closed d, Closed g by B,dX;
thus thesis by A,main;
end;
theorem
for S,T being non empty Poset
for g being Function of S,T, 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
let S,T be non empty Poset, g be Function of S,T, d be Function of T,S;
assume A: [g,d] is co-Galois;
then B: Restr(d,g) is bijective by main;
then Closed d is (Closed g)-bijective;
hence Restr(d,g) is a_Bijection of Closed g, Closed d by B,dX;
thus thesis by A,main;
end;
theorem
for S,T being non empty Poset
for g being Function of S,T, d being Function of T,S
st [g,d] is co-Galois
for s being Element of S holds s in Closed d iff d.(g.s) = s by main;
theorem
for S,T being non empty Poset
for g being Function of S,T, d being Function of T,S
st [g,d] is co-Galois
for t being Element of T holds t in Closed g iff g.(d.t) = t by main;
begin :: On the Lattice of Subgroups
theorem hhg:
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
let G1 be Group, G2 be Subgroup of G1,
H1,H2 be Subset of G1, H3,H4 be Subset of G2;
assume AS: H1 = H3 & H2 = H4;
A: H1 * H2 = {g * h where g,h is Element of G1 : g in H1 & h in H2}
by GROUP_2:def 2;
B: H3 * H4 = {g * h where g,h is Element of G2 : g in H3 & h in H4}
by GROUP_2:def 2;
C: now let o be object;
assume o in H3 * H4; then
consider h3,h4 being Element of G2 such that
C1: o = h3 * h4 & h3 in H3 & h4 in H4 by B;
reconsider h1 = h3, h2 = h4 as Element of G1 by AS,C1;
C2: h1*h2 in {g*h where g,h is Element of G1 : g in H1 & h in H2} by AS,C1;
thus o in H1 * H2 by C1,C2,A,GROUP_2:43;
end;
now let o be object;
assume o in H1 * H2; then
consider h1,h2 being Element of G1 such that
C1: o = h1 * h2 & h1 in H1 & h2 in H2 by A;
reconsider h3 = h1, h4 = h2 as Element of G2 by AS,C1;
C2: h3*h4 in {g*h where g,h is Element of G2 : g in H3 & h in H4} by AS,C1;
thus o in H3 * H4 by C1,C2,B,GROUP_2:43;
end;
hence thesis by C,TARSKI:2;
end;
theorem hhf:
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
let G1 be Group, G2 be Subgroup of G1, H1 be Subset of G1, H2 be Subset of G2;
assume AS: H1 = H2;
A: H1 c= the carrier of gr H1 &
for H being strict Subgroup of G1
st H1 c= the carrier of H holds gr H1 is Subgroup of H by GROUP_4:def 4;
B: H2 c= the carrier of gr H2 &
for H being strict Subgroup of G2
st H2 c= the carrier of H holds gr H2 is Subgroup of H by GROUP_4:def 4;
gr H2 is Subgroup of G1 by GROUP_2:56; then
C: gr H1 is Subgroup of gr H2 by AS,B,GROUP_4:def 4; then
gr H2 is Subgroup of gr H1 by AS,A,GROUP_4:def 4;
hence thesis by C,GROUP_2:55;
end;
theorem
for G1 being Group
for G2 being Subgroup of G1
for 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
let G1 be Group, G2 be Subgroup of G1,
H1,H2 be Subgroup of G1, H3,H4 be Subgroup of G2;
assume AS: H1 = H3 & H2 = H4;
reconsider X = H3 "\/" H4 as Subgroup of G1 by GROUP_2:56;
A: carr H1 = the carrier of H1 by GROUP_2:def 9 .= carr H3 by AS,GROUP_2:def 9;
B: carr H2 = the carrier of H2 by GROUP_2:def 9 .= carr H4 by AS,GROUP_2:def 9;
then C: (carr H1) * (carr H2) = (carr H3) * (carr H4) by A,hhg;
thus H3 "\/" H4
= gr(H3 * H4) by GROUP_4:50
.= gr(carr H3 * carr H4) by GROUP_4:def 8
.= gr(H1 * H2) by C,hhf,GROUP_4:def 8
.= H1 "\/" H2 by GROUP_4:50;
D: the carrier of H1 /\ H2
= carr (H1) /\ carr(H2) by GROUP_2:def 10
.= the carrier of H3 /\ H4 by A,B,GROUP_2:def 10;
H3 /\ H4 is Subgroup of G1 by GROUP_2:56;
hence H3 /\ H4 = H1 /\ H2 by D,GROUP_2:59;
end;
registration
let G be Group;
cluster the carrier of lattice G -> G-Subgroup-membered;
coherence
proof
lattice G = LattStr(#Subgroups G,SubJoin G,SubMeet G#) by GROUP_4:def 12;
hence thesis;
end;
cluster the carrier of LattPOSet(lattice G) -> G-Subgroup-membered;
coherence
proof
set L = lattice G;
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
hence thesis;
end;
end;
lemmaG0:
for G be Group, M be non empty G-Subgroup-membered set
holds meet(the set of all the carrier of K where K is Element of M)
c= the carrier of G
proof
let G be Group, M be non empty G-Subgroup-membered set;
set K = the Element of M;
J: the carrier of K in
the set of all the carrier of K where K is Element of M;
I: the carrier of K c= the carrier of G by GROUP_2:def 5;
now let x be object;
assume x in meet(the set of all the carrier of K where K is Element of M);
then x in K by J,SETFAM_1:def 1;
hence x in the carrier of G by I;
end;
hence thesis;
end;
lemmaG1:
for G be Group holds
the multMagma of G is Subgroup of G & G is Subgroup of the multMagma of G
proof
let G be Group;
set L = the multMagma of G;
the multF of L = (the multF of G)||(the carrier of L);
hence L is Subgroup of G by GROUP_2:def 5;
the multF of G = (the multF of L)||(the carrier of G);
hence thesis by GROUP_2:def 5;
end;
lemmaG2:
for G be Group, M be non empty G-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
let G be Group, M be non empty G-Subgroup-membered set;
set L = the multMagma of G;
L is Subgroup of G by lemmaG1; then
K: L in Subgroups G by GROUP_3:def 1;
now let F be Group;
assume F in M; then
reconsider F1 = F as Element of M;
F1 is Subgroup of G & G is Subgroup of L by lemmaG1;
hence F is Subgroup of L by GROUP_2:56;
end; then
the carrier of G in
{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} by K;
hence thesis by SETFAM_1:def 1;
end;
definition
let G be Group;
let M be non empty G-Subgroup-membered set;
func /\M -> strict Subgroup of G means :defG2:
the carrier of it =
meet (the set of all the carrier of H where H is Element of M);
existence
proof
set S = the set of all the carrier of H where H is Element of M;
reconsider A = meet S as Subset of G by lemmaG0;
set L = the Element of M;
H: the carrier of L in S;
now let Y be set;
assume Y in S; then
consider H being Element of M such that
H1: Y = the carrier of H;
1_G = 1_H by GROUP_2:44;
hence 1_G in Y by H1;
end; then
A: 1_G in A by H,SETFAM_1:def 1;
B: now let g1,g2 be Element of G;
assume B1: g1 in A & g2 in A;
now let Y be set;
assume B2: Y in S; then
consider H being Element of M such that
B3: Y = the carrier of H;
reconsider h1 = g1, h2 = g2 as Element of H by B1,B2,B3,SETFAM_1:def 1;
h1 * h2 = g1 * g2 by GROUP_2:43;
hence g1 * g2 in Y by B3;
end;
hence g1 * g2 in A by H,SETFAM_1:def 1;
end;
now let g be Element of G;
assume B1: g in A;
now let Y be set;
assume B2: Y in S; then
consider H being Element of M such that
B3: Y = the carrier of H;
reconsider h = g as Element of H by B1,B2,B3,SETFAM_1:def 1;
h" = g" by GROUP_2:48;
hence g" in Y by B3;
end;
hence g" in A by H,SETFAM_1:def 1;
end;
hence thesis by A,B,GROUP_2:52;
end;
uniqueness by GROUP_2:59;
func \/M -> strict Subgroup of G means :defG3:
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
proof
set S = {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};
reconsider A = meet S as Subset of G by lemmaG2;
set L = the multMagma of G;
L is Subgroup of G by lemmaG1; then
K: L in Subgroups G by GROUP_3:def 1;
now let F be Group;
assume F in M; then
reconsider F1 = F as Element of M;
F1 is Subgroup of G & G is Subgroup of L by lemmaG1;
hence F is Subgroup of L by GROUP_2:56;
end; then
H: the carrier of G in
{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} by K;
now let Y be set;
assume Y in S; then
consider H being Element of Subgroups(G) such that
H1: Y = the carrier of H &
for K being Group st K in M holds K is Subgroup of H;
1_G = 1_H by GROUP_2:44;
hence 1_G in Y by H1;
end; then
A: 1_G in A by H,SETFAM_1:def 1;
B: now let g1,g2 be Element of G;
assume B1: g1 in A & g2 in A;
now let Y be set;
assume B2: Y in S; then
consider H being Element of Subgroups(G) such that
B3: Y = the carrier of H &
for K being Group st K in M holds K is Subgroup of H;
reconsider h1 = g1, h2 = g2 as Element of H by B1,B2,B3,SETFAM_1:def 1;
h1 * h2 = g1 * g2 by GROUP_2:43;
hence g1 * g2 in Y by B3;
end;
hence g1 * g2 in A by H,SETFAM_1:def 1;
end;
now let g be Element of G;
assume B1: g in A;
now let Y be set;
assume B2: Y in S; then
consider H being Element of Subgroups(G) such that
B3: Y = the carrier of H &
for K being Group st K in M holds K is Subgroup of H;
reconsider h = g as Element of H by B1,B2,B3,SETFAM_1:def 1;
h" = g" by GROUP_2:48;
hence g" in Y by B3;
end;
hence g" in A by H,SETFAM_1:def 1;
end;
hence thesis by A,B,GROUP_2:52;
end;
uniqueness by GROUP_2:59;
end;
theorem lemG8:
for G being Group
for M being non empty G-Subgroup-membered set
for H being Element of M holds /\M is Subgroup of H
proof
let G be Group, M be non empty G-Subgroup-membered set, H be Element of M;
set K = the Element of M;
now let o be object;
assume o in the carrier of /\M; then
B: o in meet(the set of all the carrier of K where K is Element of M)
by defG2;
the carrier of H in
the set of all the carrier of K where K is Element of M;
hence o in the carrier of H by B,SETFAM_1:def 1;
end; then
the carrier of /\M c= the carrier of H;
hence thesis by GROUP_2:57;
end;
theorem lemG9:
for G being Group
for M being non empty G-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
let E be Group, M be non empty E-Subgroup-membered set, K be Subgroup of E;
assume A: for F being Element of M holds K is Subgroup of F;
set L = the Element of M;
H: the carrier of L in
the set of all the carrier of K where K is Element of M;
now let o be object;
assume B: o in the carrier of K;
now let Y be set;
assume Y in the set of all the carrier of K where K is Element of M;
then consider F being Element of M such that
C: Y = the carrier of F;
K is Subgroup of F by A; then
the carrier of K c= the carrier of F by GROUP_2:def 5;
hence o in Y by B,C;
end; then
o in meet(the set of all the carrier of K where K is Element of M)
by H,SETFAM_1:def 1;
hence o in the carrier of /\M by defG2;
end; then
the carrier of K c= the carrier of /\M;
hence thesis by GROUP_2:57;
end;
theorem lemG10:
for G being Group
for M being non empty G-Subgroup-membered set
for H being Element of M holds H is Subgroup of \/M
proof
let G be Group, M be non empty G-Subgroup-membered set, F be Element of M;
set S = {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};
set L = the multMagma of G;
L is Subgroup of G by lemmaG1; then
K: L in Subgroups G by GROUP_3:def 1;
now let F be Group;
assume F in M; then
reconsider F1 = F as Element of M;
F1 is Subgroup of G & G is Subgroup of L by lemmaG1;
hence F is Subgroup of L by GROUP_2:56;
end; then
H: the carrier of G in
{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} by K;
now let o be object;
assume A: o in the carrier of F;
now let Y be set;
assume Y in {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}; then
consider K being Element of Subgroups(G) such that
A1: Y = the carrier of K &
for F being Group st F in M holds F is Subgroup of K;
F is Subgroup of K by A1; then
the carrier of F c= the carrier of K by GROUP_2:def 5;
hence o in Y by A,A1;
end;
then o in meet S by H,SETFAM_1:def 1;
hence o in the carrier of \/M by defG3;
end; then
the carrier of F c= the carrier of \/M;
hence thesis by GROUP_2:57;
end;
theorem lemG11:
for G being Group
for M being non empty G-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
let G be Group, M be non empty G-Subgroup-membered set,
K be Element of Subgroups(G);
assume AS: for F being Element of M holds F is Subgroup of K;
set S = {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};
now let o be object;
assume o in the carrier of \/M; then
B: o in meet S by defG3;
for F being Group st F in M holds F is Subgroup of K by AS; then
the carrier of K in {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};
hence o in the carrier of K by B,SETFAM_1:def 1;
end; then
the carrier of \/M c= the carrier of K;
hence thesis by GROUP_2:57;
end;
lemGx:
for G be Group for H1,H2 be Subgroup of G holds
meet{the carrier of H1,the carrier of H2} =
meet(the set of all the carrier of H where H is Element of {H1,H2})
proof
let G be Group, H1,H2 be Subgroup of G;
H1 in {H1,H2} by TARSKI:def 2; then
H: the carrier of H1 in the set of all the carrier of H
where H is Element of {H1,H2};
A: now let o be object;
assume o in meet{the carrier of H1,the carrier of H2}; then
B: o in (the carrier of H1) /\ (the carrier of H2) by SETFAM_1:11;
now let Y be set;
assume Y in the set of all the carrier of H
where H is Element of {H1,H2}; then
consider H being Element of {H1,H2} such that
C: Y = the carrier of H;
per cases by TARSKI:def 2;
suppose H = H1;
hence o in Y by B,C,XBOOLE_0:def 4;
end;
suppose H = H2;
hence o in Y by B,C,XBOOLE_0:def 4;
end;
end;
hence o in meet(the set of all the carrier of H
where H is Element of {H1,H2}) by H,SETFAM_1:def 1;
end;
now let o be object;
assume B: o in meet(the set of all the carrier of H
where H is Element of {H1,H2}); then
C: o in the carrier of H1 by H,SETFAM_1:def 1;
H2 in {H1,H2} by TARSKI:def 2; then
the carrier of H2 in the set of all the carrier of H
where H is Element of {H1,H2}; then
o in the carrier of H2 by B,SETFAM_1:def 1; then
o in (the carrier of H1) /\ (the carrier of H2) by C,XBOOLE_0:def 4;
hence o in meet{the carrier of H1,the carrier of H2} by SETFAM_1:11;
end;
hence thesis by A,TARSKI:2;
end;
theorem
for G being Group
for H1,H2 being Subgroup of G holds /\{H1,H2} = H1 /\ H2
proof
let G be Group, H1,H2 be Subgroup of G;
the carrier of H1 /\ H2
= carr(H1) /\ carr(H2) by GROUP_2:def 10
.= (the carrier of H1) /\ carr(H2) by GROUP_2:def 9
.= (the carrier of H1) /\ (the carrier of H2) by GROUP_2:def 9
.= meet{the carrier of H1,the carrier of H2} by SETFAM_1:11
.= meet(the set of all the carrier of H where H is Element of {H1,H2})
by lemGx
.= the carrier of /\{H1,H2} by defG2;
hence thesis by GROUP_2:59;
end;
theorem
for G being Group
for H1,H2 being Subgroup of G holds \/{H1,H2} = H1 "\/" H2
proof
let G be Group, H1,H2 be Subgroup of G;
A: H1 "\/" H2 in Subgroups(G) by GROUP_3:def 1;
now let F be Element of {H1,H2};
per cases by TARSKI:def 2;
suppose F = H1;
hence F is Subgroup of H1 "\/" H2 by GROUP_4:60;
end;
suppose F = H2;
hence F is Subgroup of H1 "\/" H2 by GROUP_4:60;
end;
end; then
B: \/{H1,H2} is Subgroup of H1 "\/" H2 by A,lemG11;
C: H1 "\/" H2 = gr(carr H1 \/ carr H2) by GROUP_4:def 9;
now let o be object;
assume o in carr(H1) \/ carr(H2); then
per cases by XBOOLE_0:def 3;
suppose o in carr(H1); then
D: o in the carrier of H1 by GROUP_2:def 9;
H1 in {H1,H2} by TARSKI:def 2; then
H1 is Subgroup of \/{H1,H2} by lemG10; then
the carrier of H1 c= the carrier of \/{H1,H2} by GROUP_2:def 5;
hence o in the carrier of \/{H1,H2} by D;
end;
suppose o in carr(H2); then
D: o in the carrier of H2 by GROUP_2:def 9;
H2 in {H1,H2} by TARSKI:def 2; then
H2 is Subgroup of \/{H1,H2} by lemG10; then
the carrier of H2 c= the carrier of \/{H1,H2} by GROUP_2:def 5;
hence o in the carrier of \/{H1,H2} by D;
end;
end; then
carr(H1) \/ carr(H2) c= the carrier of \/{H1,H2}; then
H1 "\/" H2 is Subgroup of \/{H1,H2} by C,GROUP_4:def 4;
hence thesis by B,GROUP_2:55;
end;
registration
let G be Group;
cluster lattice G -> complete;
coherence
proof
set L = lattice G;
B: L = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by GROUP_4:def 12;
I: now let a,b be Element of L, K1,K2 be SubGroup of G;
assume K1 = a & K2 = b;
hence K1 /\ K2 = (SubMeet G).(a,b) by GROUP_4:def 11
.= a "/\" b by B,LATTICES:def 2;
end;
now let Y be Subset of L;
per cases;
suppose A1: Y = {};
thus ex a being Element of L st a is_less_than Y &
for b being Element of L st b is_less_than Y holds b [= a
proof
take Top L;
for a being Element of L st a in Y holds Top L [= a by A1;
hence Top L is_less_than Y by LATTICE3:def 16;
let b be Element of L;
assume b is_less_than Y;
thus thesis by LATTICES:19;
end;
end;
suppose Y <> {}; then
reconsider M = Y as non empty Subset of Subgroups(G) by B;
/\M in Subgroups(G) by GROUP_3:def 1; then
reconsider K1 = /\M as SubGroup of G by dSG;
reconsider a = K1 as Element of L by B,GROUP_3:def 1;
thus ex a being Element of L st a is_less_than Y &
for b being Element of L st b is_less_than Y holds b [= a
proof
take a;
now let q be Element of L;
assume q in Y; then
reconsider K2 = q as Element of M;
reconsider K2 as SubGroup of G by dSG,B;
/\M is Subgroup of K2 by lemG8;
then K1 /\ K2 = K1 by GROUP_2:89;
then a "/\" q = a by I;
hence a [= q by LATTICES:4;
end;
hence a is_less_than Y by LATTICE3:def 16;
thus for b being Element of L st b is_less_than Y holds b [= a
proof
let b be Element of L;
b is strict Subgroup of G by B,GROUP_3:def 1; then
reconsider Kb = b as SubGroup of G by B,dSG;
assume A2: b is_less_than Y;
now let F be Element of M;
A3: F in M & M c= Subgroups(G); then
reconsider F1 = F as SubGroup of G by dSG;
reconsider c = F1 as Element of L by A3;
b "/\" c = b by A2,LATTICE3:def 16,LATTICES:4; then
Kb /\ F1 = Kb by I;
hence Kb is Subgroup of F by GROUP_2:89;
end; then
Kb is Subgroup of K1 by lemG9; then
Kb /\ K1 = Kb by GROUP_2:89; then
b "/\" a = b by I;
hence b [= a by LATTICES:4;
end;
end;
end;
end;
hence thesis by VECTSP_8:def 6;
end;
end;
theorem
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
let G be Group;
let a,b be Element of the carrier of LattPOSet(lattice G);
set L = lattice G;
H: LattRel L = { [p,q] where p is Element of L, q is Element of L: p [= q } &
LattPOSet L = RelStr(#the carrier of L, LattRel L#) &
L = LattStr (# Subgroups G, SubJoin G, SubMeet G #)
by LATTICE3:def 2,FILTER_1:def 8,GROUP_4:def 12;
reconsider p = a, q = b as Element of L by H;
reconsider K1 = p, K2 = q as SubGroup of G by H,dSG;
J: now let a,b be Element of L, K1,K2 be SubGroup of G;
assume K1 = a & K2 = b;
hence K1 /\ K2 = (SubMeet G).(a,b) by GROUP_4:def 11
.= a "/\" b by H,LATTICES:def 2;
end;
A: now assume a <= b; then
[p,q] in LattRel L by H,ORDERS_2:def 5; then
p "/\" q = p by LATTICES:4,FILTER_1:31; then
K1 /\ K2 = K1 by J;
hence K1 is Subgroup of K2 by GROUP_2:89;
end;
now assume K1 is Subgroup of K2;
then K1 /\ K2 = K1 by GROUP_2:89;
then p "/\" q = p by J; then
[p,q] in LattRel L by FILTER_1:31,LATTICES:4;
hence a <= b by H,ORDERS_2:def 5;
end;
hence thesis by A;
end;
begin :: The Lattice of Intermediate Fields
lemma0:
for F be Field, M be non empty F-Subfield-membered set
holds meet(the set of all the carrier of K where K is Element of M)
c= the carrier of F
proof
let F be Field, M be non empty F-Subfield-membered set;
set K = the Element of M;
J: the carrier of K in
the set of all the carrier of K where K is Element of M;
I: the carrier of K c= the carrier of F by EC_PF_1:def 1;
now let x be object;
assume x in meet(the set of all the carrier of K where K is Element of M);
then x in K by J,SETFAM_1:def 1;
hence x in the carrier of F by I;
end;
hence thesis;
end;
lemma1:
for F be Field, M be non empty F-Subfield-membered set, S be Subset of F
st S = meet(the set of all the carrier of K where K is Element of M)
holds S is inducing_subfield
proof
let F be Field, M be non empty F-Subfield-membered set, S be Subset of F;
set K = the Element of M;
H: the carrier of K in
the set of all the carrier of K where K is Element of M;
assume AS: S = meet(the set of all the carrier of K where K is Element of M);
A: now let Y be set;
assume Y in the set of all the carrier of K where K is Element of M; then
consider K being Element of M such that
A1: Y = the carrier of K;
0.K = 0.F by EC_PF_1:def 1;
hence 0.F in Y by A1;
end;
B: now let Y be set;
assume Y in the set of all the carrier of K where K is Element of M; then
consider K being Element of M such that
B1: Y = the carrier of K;
1.K = 1.F by EC_PF_1:def 1;
hence 1.F in Y by B1;
end;
C: now let a,b be Element of F;
assume C0: a in S & b in S;
now let Y be set;
assume C1: Y in the set of all the carrier of K where K is Element of M;
then consider K being Element of M such that
C2: Y = the carrier of K;
reconsider a1 = a, b1 = b as Element of K by C0,C1,C2,AS,SETFAM_1:def 1;
K is Subring of F by FIELD_5:12;
then a1 + b1 = a + b by FIELD_6:15;
hence a + b in Y by C2;
end;
hence a + b in S by H,AS,SETFAM_1:def 1;
now let Y be set;
assume C1: Y in the set of all the carrier of K where K is Element of M;
then consider K being Element of M such that
C2: Y = the carrier of K;
reconsider a1 = a, b1 = b as Element of K by C0,C1,C2,AS,SETFAM_1:def 1;
K is Subring of F by FIELD_5:12;
then a1 * b1 = a * b by FIELD_6:16;
hence a * b in Y by C2;
end;
hence a * b in S by H,AS,SETFAM_1:def 1;
now let Y be set;
assume C1: Y in the set of all the carrier of K where K is Element of M;
then consider K being Element of M such that
C2: Y = the carrier of K;
reconsider a1 = a as Element of K by C0,C1,C2,AS,SETFAM_1:def 1;
K is Subring of F by FIELD_5:12;
then -a1 = -a by FIELD_6:17;
hence -a in Y by C2;
end;
hence -a in S by H,AS,SETFAM_1:def 1;
end;
now let a be non zero Element of F;
assume D0: a in S;
now let Y be set;
assume D1: Y in the set of all the carrier of K where K is Element of M;
then consider K being Element of M such that
D2: Y = the carrier of K;
reconsider a1 = a as Element of K by D0,D1,D2,AS,SETFAM_1:def 1;
a1" = a" by FIELD_6:18;
hence a" in Y by D2;
end;
hence a" in S by H,AS,SETFAM_1:def 1;
end;
hence thesis by A,B,C,H,AS,SETFAM_1:def 1;
end;
lemma2:
for E be Field, M be non empty E-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
let E be Field, M be non empty E-Subfield-membered set;
set L = the doubleLoopStr of E;
L == E; then
K: L in SubFields E by FIELD_12:45;
now let F be Field;
assume F in M; then
reconsider F1 = F as Element of M;
L == E; then
F1 is Subfield of E & E is Subfield of L;
hence F is Subfield of L by EC_PF_1:5;
end; then
the carrier of L in
{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} by K;
hence thesis by SETFAM_1:def 1;
end;
lemma3:
for E be Field, M be non empty E-Subfield-membered set
for S be 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
let E be Field, M be non empty E-Subfield-membered set, S be Subset of E;
set L = the doubleLoopStr of E;
L == E; then
K: L in SubFields E by FIELD_12:45;
now let F be Field;
assume F in M; then
reconsider F1 = F as Element of M;
L == E; then
F1 is Subfield of E & E is Subfield of L;
hence F is Subfield of L by EC_PF_1:5;
end; then
H: the carrier of L in
{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} by K;
assume AS: 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};
A: now let Y be set;
assume Y in {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}; then
consider K being Element of SubFields(E) such that
A1: Y = the carrier of K &
for F being Field st F in M holds F is Subfield of K;
0.K = 0.E by EC_PF_1:def 1;
hence 0.E in Y by A1;
end;
B: now let Y be set;
assume Y in {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}; then
consider K being Element of SubFields(E) such that
B1: Y = the carrier of K &
for F being Field st F in M holds F is Subfield of K;
1.K = 1.E by EC_PF_1:def 1;
hence 1.E in Y by B1;
end;
C: now let a,b be Element of E;
assume C0: a in S & b in S;
now let Y be set;
assume C1: Y in {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};
then consider K being Element of SubFields(E) such that
C2: Y = the carrier of K &
for F being Field st F in M holds F is Subfield of K;
reconsider a1 = a, b1 = b as Element of K by C0,C1,C2,AS,SETFAM_1:def 1;
K is Subring of E by FIELD_5:12;
then a1 + b1 = a + b by FIELD_6:15;
hence a + b in Y by C2;
end;
hence a + b in S by H,AS,SETFAM_1:def 1;
now let Y be set;
assume C1: Y in {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};
then consider K being Element of SubFields(E) such that
C2: Y = the carrier of K &
for F being Field st F in M holds F is Subfield of K;
reconsider a1 = a, b1 = b as Element of K by C0,C1,C2,AS,SETFAM_1:def 1;
K is Subring of E by FIELD_5:12;
then a1 * b1 = a * b by FIELD_6:16;
hence a * b in Y by C2;
end;
hence a * b in S by H,AS,SETFAM_1:def 1;
now let Y be set;
assume C1: Y in {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};
then consider K being Element of SubFields(E) such that
C2: Y = the carrier of K &
for F being Field st F in M holds F is Subfield of K;
reconsider a1 = a as Element of K by C0,C1,C2,AS,SETFAM_1:def 1;
K is Subring of E by FIELD_5:12;
then -a1 = -a by FIELD_6:17;
hence -a in Y by C2;
end;
hence -a in S by H,AS,SETFAM_1:def 1;
end;
now let a being non zero Element of E;
assume D0: a in S;
now let Y be set;
assume C1: Y in {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};
then consider K being Element of SubFields(E) such that
C2: Y = the carrier of K &
for F being Field st F in M holds F is Subfield of K;
reconsider a1 = a as Element of K by D0,C1,C2,AS,SETFAM_1:def 1;
a1" = a" by FIELD_6:18;
hence a" in Y by C2;
end;
hence a" in S by H,AS,SETFAM_1:def 1;
end;
hence thesis by A,B,C,H,AS,SETFAM_1:def 1;
end;
definition
let E be Field;
let M be non empty E-Subfield-membered set;
func /\M -> strict Subfield of E means :def2:
the carrier of it =
meet (the set of all the carrier of K where K is Element of M);
existence
proof
reconsider S = meet(the set of all the carrier of K where K is Element of M)
as inducing_subfield Subset of E by lemma0,lemma1;
reconsider K = InducedSubfield S as strict Subfield of E;
take K;
thus thesis by FIELD_16:def 3;
end;
uniqueness by EC_PF_1:8;
func \/M -> strict Subfield of E means :def3:
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
proof
reconsider 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}
as inducing_subfield Subset of E by lemma2,lemma3;
reconsider K = InducedSubfield S as strict Subfield of E;
take K;
thus thesis by FIELD_16:def 3;
end;
uniqueness by EC_PF_1:8;
end;
theorem lem8:
for E being Field
for M being non empty E-Subfield-membered set
for F being Element of M holds /\M is Subfield of F
proof
let F be Field, M be non empty F-Subfield-membered set, F be Element of M;
set K = the Element of M;
now let o be object;
assume o in the carrier of /\M; then
B: o in meet(the set of all the carrier of K where K is Element of M)
by def2;
the carrier of F in
the set of all the carrier of K where K is Element of M;
hence o in the carrier of F by B,SETFAM_1:def 1;
end; then
the carrier of /\M c= the carrier of F;
hence thesis by EC_PF_1:6;
end;
theorem lem9:
for E being Field
for M being non empty E-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
let E be Field, M be non empty E-Subfield-membered set, K be Subfield of E;
assume A: for F being Element of M holds K is Subfield of F;
set L = the Element of M;
H: the carrier of L in
the set of all the carrier of K where K is Element of M;
now let o be object;
assume B: o in the carrier of K;
now let Y be set;
assume Y in the set of all the carrier of K where K is Element of M;
then consider F being Element of M such that
C: Y = the carrier of F;
K is Subfield of F by A; then
the carrier of K c= the carrier of F by EC_PF_1:def 1;
hence o in Y by B,C;
end; then
o in meet(the set of all the carrier of K where K is Element of M)
by H,SETFAM_1:def 1;
hence o in the carrier of /\M by def2;
end; then
the carrier of K c= the carrier of /\M;
hence thesis by EC_PF_1:6;
end;
theorem lem10:
for E being Field
for M being non empty E-Subfield-membered set
for F being Element of M holds F is Subfield of \/M
proof
let E be Field, M be non empty E-Subfield-membered set, F be Element of M;
set S = {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};
set L = the doubleLoopStr of E;
L == E; then
K: L in SubFields E by FIELD_12:45;
now let F be Field;
assume F in M; then
reconsider F1 = F as Element of M;
L == E; then
F1 is Subfield of E & E is Subfield of L;
hence F is Subfield of L by EC_PF_1:5;
end; then
H: the carrier of L in
{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} by K;
now let o be object;
assume A: o in the carrier of F;
now let Y be set;
assume Y in {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}; then
consider K being Element of SubFields(E) such that
A1: Y = the carrier of K &
for F being Field st F in M holds F is Subfield of K;
F is Subfield of K by A1; then
the carrier of F c= the carrier of K by EC_PF_1:def 1;
hence o in Y by A,A1;
end;
then o in meet S by H,SETFAM_1:def 1;
hence o in the carrier of \/M by def3;
end; then
the carrier of F c= the carrier of \/M;
hence thesis by EC_PF_1:6;
end;
theorem lem11:
for E being Field
for M being non empty E-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
let E be Field, M be non empty E-Subfield-membered set,
K be Element of SubFields(E);
assume AS: for F being Element of M holds F is Subfield of K;
set S = {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};
now let o be object;
assume o in the carrier of \/M; then
B: o in meet S by def3;
for F being Field st F in M holds F is Subfield of K by AS; then
the carrier of K in {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};
hence o in the carrier of K by B,SETFAM_1:def 1;
end; then
the carrier of \/M c= the carrier of K;
hence thesis by EC_PF_1:6;
end;
theorem lem12:
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
let F be Field, E be FieldExtension of F,
M be non empty Subset of IntermediateFields(E,F);
A: F is Subfield of E by FIELD_4:7;
J: now let x be Element of M;
M c= IntermediateFields(E,F); then
x in IntermediateFields(E,F); then
consider K being strict Field such that
P: K = x & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
thus F is Subfield of x by P;
end;
set L = the Element of M;
H: the carrier of L in
the set of all the carrier of K where K is Element of M;
now let o be object;
assume B: o in the carrier of F;
now let Y be set;
assume Y in the set of all the carrier of K where K is Element of M;
then consider K being Element of M such that
C: Y = the carrier of K;
F is Subfield of K by J; then
the carrier of F c= the carrier of K by EC_PF_1:def 1;
hence o in Y by B,C;
end; then
o in meet(the set of all the carrier of K where K is Element of M)
by H,SETFAM_1:def 1;
hence o in the carrier of /\M by def2;
end; then
the carrier of F c= the carrier of /\M;
then F is Subfield of /\M by A,EC_PF_1:6;
hence thesis by FIELD_14:4,di;
end;
theorem lem13:
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
let F be Field, E be FieldExtension of F,
M be non empty Subset of IntermediateFields(E,F);
J: now let x be Element of M;
M c= IntermediateFields(E,F); then
x in IntermediateFields(E,F); then
consider K being strict Field such that
P: K = x & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
thus F is Subfield of x by P;
end;
set K = the Element of M;
F is Subfield of K & K is Subfield of \/M by J,lem10;
then F is Subfield of \/M by EC_PF_1:5;
hence thesis by FIELD_14:4,di;
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
/\{K1,K2};
coherence
proof
now let o be object;
assume o in {K1,K2}; then
per cases by TARSKI:def 2;
suppose o = K1;
hence o in IntermediateFields(E,F) by di;
end;
suppose o = K2;
hence o in IntermediateFields(E,F) by di;
end;
end; then
{K1,K2} c= IntermediateFields(E,F);
hence thesis by lem12;
end;
commutativity;
func K1 "\/" K2 -> IntermediateField of E,F equals
\/{K1,K2};
coherence
proof
now let o be object;
assume o in {K1,K2}; then
per cases by TARSKI:def 2;
suppose o = K1;
hence o in IntermediateFields(E,F) by di;
end;
suppose o = K2;
hence o in IntermediateFields(E,F) by di;
end;
end; then
{K1,K2} c= IntermediateFields(E,F);
hence thesis by lem13;
end;
commutativity;
end;
registration
let F be Field;
let E be FieldExtension of F;
let K be IntermediateField of E,F;
reduce K "/\" K to K;
reducibility
proof
K in IntermediateFields(E,F) by di; then
H: ex L being strict Field st K = L &
F is Subfield of L & L is Subfield of E by FIELD_14:def 1;
now let o be object;
assume o in the carrier of K "/\" K; then
I: o in meet(the set of all the carrier of L
where L is Element of {K,K}) by def2;
K in {K,K} by TARSKI:def 2; then
the carrier of K in
the set of all the carrier of L where L is Element of {K,K};
hence o in the carrier of K by I,SETFAM_1:def 1;
end; then
A: the carrier of K "/\" K c= the carrier of K;
K in {K,K} by TARSKI:def 2; then
B: the carrier of K in the set of all the carrier of L
where L is Element of {K,K};
now let o be object;
assume C: o in the carrier of K;
now let Y be set;
assume Y in the set of all the carrier of L where L is Element of {K,K};
then consider L being Element of {K,K} such that
D: Y = the carrier of L;
thus o in Y by C,D,TARSKI:def 2;
end; then
o in meet(the set of all the carrier of L
where L is Element of {K,K}) by B,SETFAM_1:def 1;
hence o in the carrier of K "/\" K by def2;
end; then
the carrier of K c= the carrier of K "/\" K;
hence thesis by H,A,XBOOLE_0:def 10,EC_PF_1:8;
end;
reduce K "\/" K to K;
reducibility
proof
K in IntermediateFields(E,F) by di; then
H: ex L being strict Field st K = L &
F is Subfield of L & L is Subfield of E by FIELD_14:def 1; then
L: K in SubFields(E) by FIELD_12:45;
set S = {the carrier of L where L is Element of SubFields(E) :
for F being Field st F in {K,K} holds F is Subfield of L};
now let F be Field;
assume F in {K,K};
then F = K by TARSKI:def 2;
hence F is Subfield of K by FIELD_4:1;
end; then
B: the carrier of K in S by L;
now let o be object;
assume o in the carrier of K "\/" K; then
o in meet S by def3;
hence o in the carrier of K by B,SETFAM_1:def 1;
end; then
A: the carrier of K "\/" K c= the carrier of K;
now let o be object;
assume C: o in the carrier of K;
now let Y be set;
assume Y in S;
then consider L being Element of SubFields(E) such that
D: Y = the carrier of L &
for F being Field st F in {K,K} holds F is Subfield of L;
K in {K,K} by TARSKI:def 2; then
K is Subfield of L by D; then
the carrier of K c= the carrier of L by EC_PF_1:def 1;
hence o in Y by C,D;
end; then
o in meet S by B,SETFAM_1:def 1;
hence o in the carrier of K "\/" K by def3;
end; then
the carrier of K c= the carrier of K "\/" K;
hence thesis by H,A,XBOOLE_0:def 10,EC_PF_1:8;
end;
end;
theorem lat1:
for F being Field
for E being FieldExtension of F
for K1,K2 being IntermediateField of E,F holds K1 "/\" (K1 "\/" K2) = K1
proof
let F be Field, E be FieldExtension of F, K1,K2 be IntermediateField of E,F;
K1 in IntermediateFields(E,F) by di; then
H1: ex L being strict Field st K1 = L &
F is Subfield of L & L is Subfield of E by FIELD_14:def 1;
now let o be object;
assume o in the carrier of K1 "/\" (K1 "\/" K2); then
I: o in meet(the set of all the carrier of L
where L is Element of {K1,K1"\/"K2}) by def2;
K1 in {K1,K1"\/"K2} by TARSKI:def 2; then
the carrier of K1 in
the set of all the carrier of L where L is Element of {K1,K1"\/"K2};
hence o in the carrier of K1 by I,SETFAM_1:def 1;
end; then
A: the carrier of K1 "/\" (K1 "\/" K2) c= the carrier of K1;
K1 in {K1,K1"\/"K2} by TARSKI:def 2; then
B: the carrier of K1 in the set of all the carrier of L
where L is Element of {K1,K1"\/"K2};
now let o be object;
assume C: o in the carrier of K1;
now let Y be set;
assume Y in the set of all the carrier of L
where L is Element of {K1,K1"\/"K2};
then consider L being Element of {K1,K1"\/"K2} such that
D: Y = the carrier of L;
K1 is Subfield of L
proof
per cases by TARSKI:def 2;
suppose L = K1;
hence thesis by FIELD_4:1;
end;
suppose E: L = K1 "\/" K2;
K1 in {K1,K2} by TARSKI:def 2;
hence thesis by E,lem10;
end;
end; then
the carrier of K1 c= the carrier of L by EC_PF_1:def 1;
hence o in Y by C,D;
end; then
o in meet the set of all the carrier of L
where L is Element of {K1,K1"\/"K2} by B,SETFAM_1:def 1;
hence o in the carrier of K1 "/\" (K1 "\/" K2) by def2;
end; then
the carrier of K1 c= the carrier of K1 "/\" (K1 "\/" K2);
hence thesis by H1,A,XBOOLE_0:def 10,EC_PF_1:8;
end;
theorem lat2:
for F being Field
for E being FieldExtension of F
for K1,K2 being IntermediateField of E,F holds (K1 "/\" K2) "\/" K2 = K2
proof
let F be Field, E be FieldExtension of F, K1,K2 be IntermediateField of E,F;
K2 in IntermediateFields(E,F) by di; then
H1: ex L being strict Field st K2 = L &
F is Subfield of L & L is Subfield of E by FIELD_14:def 1; then
H2: K2 in SubFields(E) by FIELD_12:45;
set M = {K1"/\"K2,K2};
now let F be Field;
assume F in M; then
per cases by TARSKI:def 2;
suppose F = K2;
hence F is Subfield of K2 by FIELD_4:1;
end;
suppose H6: F = K1 "/\" K2;
K2 in {K1,K2} by TARSKI:def 2;
hence F is Subfield of K2 by H6,lem8;
end;
end; then
B: the carrier of K2 in {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} by H2;
now let o be object;
assume o in the carrier of (K1 "/\" K2) "\/" K2; then
o in 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} by def3;
hence o in the carrier of K2 by B,SETFAM_1:def 1;
end; then
A: the carrier of (K1 "/\" K2) "\/" K2 c= the carrier of K2;
now let o be object;
assume C: o in the carrier of K2;
now let Y be set;
assume Y in {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};
then consider L being Element of SubFields(E) such that
D: Y = the carrier of L &
for F being Field st F in M holds F is Subfield of L;
K2 in M by TARSKI:def 2; then
K2 is Subfield of L by D; then
the carrier of K2 c= the carrier of L by EC_PF_1:def 1;
hence o in Y by C,D;
end; then
o in 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}
by B,SETFAM_1:def 1;
hence o in the carrier of (K1 "/\" K2) "\/" K2 by def3;
end; then
the carrier of K2 c= the carrier of (K1 "/\" K2) "\/" K2;
hence thesis by H1,A,XBOOLE_0:def 10,EC_PF_1:8;
end;
theorem
for F being Field
for E being FieldExtension of F
for K1,K2 being IntermediateField of E,F holds K1 "/\" K2 = K2 "/\" K1;
theorem
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
let F be Field, E be FieldExtension of F, K1,K2 be IntermediateField of E,F;
K1 in {K1,K2} by TARSKI:def 2; then
H1: the carrier of K1 in
the set of all the carrier of L where L is Element of {K1,K2};
K2 in {K1,K2} by TARSKI:def 2; then
H2: the carrier of K2 in
the set of all the carrier of L where L is Element of {K1,K2};
A: now let o be object;
assume o in the carrier of K1 "/\" K2; then
o in meet(the set of all the carrier of L
where L is Element of {K1,K2}) by def2; then
o in the carrier of K1 & o in the carrier of K2 by H1,H2,SETFAM_1:def 1;
hence o in (the carrier of K1) /\ the carrier of K2 by XBOOLE_0:def 4;
end;
now let o be object;
assume B: o in (the carrier of K1) /\ the carrier of K2;
now let Y be set;
assume Y in the set of all the carrier of L
where L is Element of {K1,K2}; then
consider L being Element of {K1,K2} such that
C: Y = the carrier of L;
per cases by TARSKI:def 2;
suppose L = K1;
hence o in Y by B,C,XBOOLE_0:def 4;
end;
suppose L = K2;
hence o in Y by B,C,XBOOLE_0:def 4;
end;
end; then
o in meet(the set of all the carrier of L
where L is Element of {K1,K2}) by H1,SETFAM_1:def 1;
hence o in the carrier of K1 "/\" K2 by def2;
end;
hence thesis by A,TARSKI:2;
end;
theorem lat5:
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
let F be Field, E be FieldExtension of F, K1,K2,K3 be IntermediateField of E,F;
the carrier of K1 "/\" (K2 "/\" K3)
= (the carrier of K1) /\ the carrier of (K2 "/\" K3) by lemm1
.= (the carrier of K1) /\ ((the carrier of K2) /\ the carrier of K3) by lemm1
.= ((the carrier of K1) /\ (the carrier of K2)) /\ the carrier of K3
by XBOOLE_1:16
.= (the carrier of K1 "/\" K2) /\ the carrier of K3 by lemm1
.= the carrier of (K1 "/\" K2) "/\" K3 by lemm1;
hence thesis by EC_PF_1:8;
end;
theorem lat6:
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
let F be Field, E be FieldExtension of F, K1,K2,K3 be IntermediateField of E,F;
set L = the doubleLoopStr of E;
Y: L == E; then
K: L in SubFields E by FIELD_12:45;
now let G be Field;
assume G in {K1,K2"\/"K3}; then
per cases by TARSKI:def 2;
suppose M1: G = K1;
K1 in IntermediateFields(E,F) by di; then
K1 is Subfield of E by FIELD_14:4;
hence G is Subfield of L by M1,Y,EC_PF_1:5;
end;
suppose G = K2"\/"K3;
hence G is Subfield of L by Y,EC_PF_1:5;
end;
end; then
H: the carrier of L in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2"\/"K3} holds F is Subfield of K} by K;
now let o be object;
assume o in the carrier of (K1 "\/" K2) "\/" K3; then
I: o in meet
{the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1"\/"K2,K3} holds F is Subfield of K} by def3;
now let Y be set;
assume Y in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2"\/"K3} holds F is Subfield of K};
then consider K being Element of SubFields(E) such that
D: Y = the carrier of K &
for F being Field st F in {K1,K2"\/"K3} holds F is Subfield of K;
K1 in {K1,K2"\/"K3} & K2"\/"K3 in {K1,K2"\/"K3} by TARSKI:def 2; then
E: K1 is Subfield of K & K2 "\/" K3 is Subfield of K by D;
K2 in {K2,K3} & K3 in {K2,K3} by TARSKI:def 2; then
F: K2 is Subfield of K2 "\/" K3 & K3 is Subfield of K2 "\/" K3 by lem10;
K2 is Subfield of K by E,F,EC_PF_1:5; then
G: for F being Element of {K1,K2} holds F is Subfield of K
by E,TARSKI:def 2;
now let F be Field;
assume F in {K1"\/"K2,K3}; then
per cases by TARSKI:def 2;
suppose F = K3;
hence F is Subfield of K by E,F,EC_PF_1:5;
end;
suppose F = K1"\/"K2;
hence F is Subfield of K by G,lem11;
end;
end; then
Y in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1"\/"K2,K3} holds F is Subfield of K} by D;
hence o in Y by I,SETFAM_1:def 1;
end; then
o in meet
{the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2"\/"K3} holds F is Subfield of K}
by H,SETFAM_1:def 1;
hence o in the carrier of K1 "\/" (K2 "\/" K3) by def3;
end; then
A: the carrier of (K1 "\/" K2) "\/" K3 c= the carrier of K1 "\/" (K2 "\/" K3);
now let G be Field;
assume G in {K1"\/"K2,K3}; then
per cases by TARSKI:def 2;
suppose M1: G = K3;
K3 in IntermediateFields(E,F) by di; then
K3 is Subfield of E by FIELD_14:4;
hence G is Subfield of L by M1,Y,EC_PF_1:5;
end;
suppose G = K1"\/"K2;
hence G is Subfield of L by Y,EC_PF_1:5;
end;
end; then
H: the carrier of L in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1"\/"K2,K3} holds F is Subfield of K} by K;
now let o be object;
assume o in the carrier of K1 "\/" (K2 "\/" K3); then
I: o in meet
{the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2"\/"K3} holds F is Subfield of K} by def3;
now let Y be set;
assume Y in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1"\/"K2,K3} holds F is Subfield of K};
then consider K being Element of SubFields(E) such that
D: Y = the carrier of K &
for F being Field st F in {K1"\/"K2,K3} holds F is Subfield of K;
K3 in {K1"\/"K2,K3} & K1"\/"K2 in {K1"\/"K2,K3} by TARSKI:def 2; then
E: K3 is Subfield of K & K1"\/"K2 is Subfield of K by D;
K1 in {K1,K2} & K2 in {K1,K2} by TARSKI:def 2; then
F: K1 is Subfield of K1 "\/" K2 & K2 is Subfield of K1 "\/" K2 by lem10;
K2 is Subfield of K by E,F,EC_PF_1:5; then
G: for F being Element of {K2,K3} holds F is Subfield of K
by E,TARSKI:def 2;
now let F be Field;
assume F in {K1,K2"\/"K3}; then
per cases by TARSKI:def 2;
suppose F = K1;
hence F is Subfield of K by E,F,EC_PF_1:5;
end;
suppose F = K2"\/"K3;
hence F is Subfield of K by G,lem11;
end;
end; then
Y in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2"\/"K3} holds F is Subfield of K} by D;
hence o in Y by I,SETFAM_1:def 1;
end; then
o in meet
{the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1"\/"K2,K3} holds F is Subfield of K}
by H,SETFAM_1:def 1;
hence o in the carrier of (K1 "\/" K2) "\/" K3 by def3;
end; then
the carrier of K1 "\/" (K2 "\/" K3) c= the carrier of (K1 "\/" K2) "\/" K3;
hence thesis by A,XBOOLE_0:def 10,EC_PF_1:8;
end;
theorem lem20:
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
let F be Field, E be FieldExtension of F, K1,K2 be IntermediateField of E,F;
K1 in IntermediateFields(E,F) & K2 in IntermediateFields(E,F) by di; then
H: K1 is Subfield of E & K2 is Subfield of E by FIELD_14:4;
A: now assume A1: K1 "/\" K2 = K1;
now let o be object;
assume o in the carrier of K1; then
A2: o in meet the set of all the carrier of K
where K is Element of {K1,K2} by A1,def2;
K2 in {K1,K2} by TARSKI:def 2; then
the carrier of K2 in the set of all the carrier of K
where K is Element of {K1,K2};
hence o in the carrier of K2 by A2,SETFAM_1:def 1;
end; then
the carrier of K1 c= the carrier of K2;
hence K1 is Subfield of K2 by H,EC_PF_1:6;
end;
now assume B: K1 is Subfield of K2;
now let F be Element of {K1,K2};
per cases by TARSKI:def 2;
suppose F = K2;
hence K1 is Subfield of F by B;
end;
suppose F = K1;
hence K1 is Subfield of F by FIELD_4:1;
end;
end; then
C: K1 is Subfield of K1 "/\" K2 by H,lem9;
K1 in {K1,K2} by TARSKI:def 2; then
K1 "/\" K2 is Subfield of K1 by lem8;
hence K1 "/\" K2 = K1 by C,EC_PF_1:4;
end;
hence thesis by A;
end;
theorem
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
let F be Field, E be FieldExtension of F, K1,K2 be IntermediateField of E,F;
set L = the doubleLoopStr of E;
Y: L == E; then
K: L in SubFields E by FIELD_12:45;
now let G be Field;
assume G in {K1,K2}; then
per cases by TARSKI:def 2;
suppose M1: G = K1;
K1 in IntermediateFields(E,F) by di; then
K1 is Subfield of E by FIELD_14:4;
hence G is Subfield of L by M1,Y,EC_PF_1:5;
end;
suppose M1: G = K2;
K2 in IntermediateFields(E,F) by di; then
K2 is Subfield of E by FIELD_14:4;
hence G is Subfield of L by M1,Y,EC_PF_1:5;
end;
end; then
J: the carrier of L in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2} holds F is Subfield of K} by K;
K1 in IntermediateFields(E,F) & K2 in IntermediateFields(E,F) by di; then
H: K1 is Subfield of E & K2 is Subfield of E by FIELD_14:4; then
I: K1 in SubFields(E) & K2 in SubFields(E) by FIELD_12:45;
A: now assume A1: K1 "\/" K2 = K2;
now let o be object;
assume A2: o in the carrier of K1;
A3: the carrier of K1 "\/" K2 =
meet {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2} holds F is Subfield of K} by def3;
now let Y be set;
assume Y in {the carrier of K where K is Element of SubFields(E) :
for F being Field st F in {K1,K2} holds F is Subfield of K}; then
consider K being Element of SubFields(E) such that
A4: Y = the carrier of K &
for F being Field st F in {K1,K2} holds F is Subfield of K;
K1 in {K1,K2} by TARSKI:def 2; then
K1 is Subfield of K by A4; then
the carrier of K1 c= the carrier of K by EC_PF_1:def 1;
hence o in Y by A2,A4;
end;
hence o in the carrier of K2 by J,A1,A3,SETFAM_1:def 1;
end; then
the carrier of K1 c= the carrier of K2;
hence K1 is Subfield of K2 by H,EC_PF_1:6;
end;
now assume B: K1 is Subfield of K2;
now let F be Element of {K1,K2};
per cases by TARSKI:def 2;
suppose F = K1;
hence F is Subfield of K2 by B;
end;
suppose F = K2;
hence F is Subfield of K2 by FIELD_4:1;
end;
end; then
C: K1 "\/" K2 is Subfield of K2 by I,lem11;
K2 in {K1,K2} by TARSKI:def 2; then
K2 is Subfield of K1 "\/" K2 by lem10;
hence K1 "\/" K2 = K2 by C,EC_PF_1:4;
end;
hence thesis by A;
end;
definition
let F be Field;
let E be FieldExtension of F;
func SubMeet E -> BinOp of IntermediateFields(E,F) means :dM:
for K1,K2 being IntermediateField of E,F holds it.(K1,K2) = K1 "/\" K2;
existence
proof
set M = IntermediateFields(E,F);
defpred P[object,object,object] means
ex K1,K2 being IntermediateField of E,F st $1 = K1 & $2 = K2 & $3 = K1 "/\" K2;
A: now let x,y be Element of M;
reconsider K1 = x, K2 = y as IntermediateField of E,F;
thus ex z being Element of M st P[x,y,z]
proof
reconsider z = K1 "/\" K2 as Element of M by di;
take z;
take K1,K2;
thus thesis;
end;
end;
consider f being Function of [:M,M:],M such that
B: for x,y being Element of M holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A);
reconsider f as BinOp of M;
take f;
now let K1,K2 be IntermediateField of E,F;
reconsider x = K1, y = K2 as Element of M by di;
P[x,y,f.(x,y)] by B;
hence f.(K1,K2) = K1 "/\" K2;
end;
hence thesis;
end;
uniqueness
proof
set M = IntermediateFields(E,F);
let g1,g2 be BinOp of M such that
A1: for K1,K2 being IntermediateField of E,F holds g1.(K1,K2) = K1 "/\" K2 and
A2: for K1,K2 being IntermediateField of E,F holds g2.(K1,K2) = K1 "/\" K2;
now let z be object;
assume z in [:M,M:];
then consider x,y being object such that
A3: x in M & y in M & z = [x,y] by ZFMISC_1:def 2;
reconsider x,y as Element of M by A3;
reconsider K1 = x, K2 = y as IntermediateField of E,F;
thus g1.z = g1.(x,y) by A3
.= K1 "/\" K2 by A1 .= g2.(x,y) by A2 .= g2.z by A3;
end;
hence thesis;
end;
func SubJoin E -> BinOp of IntermediateFields(E,F) means :dJ:
for K1,K2 being IntermediateField of E,F holds it.(K1,K2) = K1 "\/" K2;
existence
proof
set M = IntermediateFields(E,F);
defpred P[object,object,object] means
ex K1,K2 being IntermediateField of E,F st $1 = K1 & $2 = K2 & $3 = K1 "\/" K2;
A: now let x,y be Element of M;
reconsider K1 = x, K2 = y as IntermediateField of E,F;
thus ex z being Element of M st P[x,y,z]
proof
reconsider z = K1 "\/" K2 as Element of M by di;
take z;
take K1,K2;
thus thesis;
end;
end;
consider f being Function of [:M,M:],M such that
B: for x,y being Element of M holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A);
reconsider f as BinOp of M;
take f;
now let K1,K2 be IntermediateField of E,F;
reconsider x = K1, y = K2 as Element of M by di;
P[x,y,f.(x,y)] by B;
hence f.(K1,K2) = K1 "\/" K2;
end;
hence thesis;
end;
uniqueness
proof
set M = IntermediateFields(E,F);
let g1,g2 be BinOp of M such that
A1: for K1,K2 being IntermediateField of E,F holds g1.(K1,K2) = K1 "\/" K2 and
A2: for K1,K2 being IntermediateField of E,F holds g2.(K1,K2) = K1 "\/" K2;
now let z be object;
assume z in [:M,M:];
then consider x,y being object such that
A3: x in M & y in M & z = [x,y] by ZFMISC_1:def 2;
reconsider x,y as Element of M by A3;
reconsider K1 = x, K2 = y as IntermediateField of E,F;
thus g1.z = g1.(x,y) by A3
.= K1 "\/" K2 by A1 .= g2.(x,y) by A2 .= g2.z by A3;
end;
hence thesis;
end;
end;
definition
let F be Field;
let E be FieldExtension of F;
func IntermediateFields E -> Lattice equals
LattStr (# IntermediateFields(E,F), SubJoin E, SubMeet E #);
coherence
proof
set L = LattStr (# IntermediateFields(E,F), SubJoin E, SubMeet E #);
H: now let a,b be Element of L, K1,K2 be IntermediateField of E,F;
assume H1: K1 = a & K2 = b;
thus a"\/"b = (SubJoin E).(a,b) by LATTICES:def 1 .= K1"\/"K2 by H1,dJ;
thus a"/\"b = (SubMeet E).(a,b) by LATTICES:def 2 .= K1"/\"K2 by H1,dM;
end;
now let a,b be Element of L;
ex K being strict Field st K = a &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K1 = a as IntermediateField of E,F by di;
ex K being strict Field st K = b &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K2 = b as IntermediateField of E,F by di;
a "\/" b = K1 "\/" K2 by H;
hence a "/\" (a "\/" b) = K1 "/\" (K1 "\/" K2) by H .= a by lat1;
end; then
A: L is join-absorbing by LATTICES:def 9;
now let a,b be Element of L;
ex K being strict Field st K = a &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K1 = a as IntermediateField of E,F by di;
ex K being strict Field st K = b &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K2 = b as IntermediateField of E,F by di;
a "/\" b = K1 "/\" K2 by H;
hence (a "/\" b) "\/" b = (K1 "/\" K2) "\/" K2 by H .= b by lat2;
end; then
B: L is meet-absorbing by LATTICES:def 8;
now let a,b be Element of L;
ex K being strict Field st K = a &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K1 = a as IntermediateField of E,F by di;
ex K being strict Field st K = b &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K2 = b as IntermediateField of E,F by di;
thus a "\/" b = K1 "\/" K2 by H .= b "\/" a by H;
end; then
C: L is join-commutative by LATTICES:def 4;
now let a,b be Element of L;
ex K being strict Field st K = a &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K1 = a as IntermediateField of E,F by di;
ex K being strict Field st K = b &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K2 = b as IntermediateField of E,F by di;
thus a "/\" b = K1 "/\" K2 by H .= b "/\" a by H;
end; then
D: L is meet-commutative by LATTICES:def 6;
now let a,b,c be Element of L;
ex K being strict Field st K = a &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K1 = a as IntermediateField of E,F by di;
ex K being strict Field st K = b &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K2 = b as IntermediateField of E,F by di;
ex K being strict Field st K = c &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K3 = c as IntermediateField of E,F by di;
D1: b "\/" c = K2 "\/" K3 & a "\/" b = K1 "\/" K2 by H;
thus a "\/" (b "\/" c)
= K1 "\/" (K2 "\/" K3) by H,D1
.= (K1 "\/" K2) "\/" K3 by lat6
.= (a "\/" b) "\/" c by H,D1;
end; then
E: L is join-associative by LATTICES:def 5;
now let a,b,c be Element of L;
ex K being strict Field st K = a &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K1 = a as IntermediateField of E,F by di;
ex K being strict Field st K = b &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K2 = b as IntermediateField of E,F by di;
ex K being strict Field st K = c &
F is Subfield of K & K is Subfield of E by FIELD_14:def 1; then
reconsider K3 = c as IntermediateField of E,F by di;
D1: b "/\" c = K2 "/\" K3 & a "/\" b = K1 "/\" K2 by H;
thus a "/\" (b "/\" c)
= K1 "/\" (K2 "/\" K3) by H,D1
.= (K1 "/\" K2) "/\" K3 by lat5
.= (a "/\" b) "/\" c by H,D1;
end; then
L is meet-associative by LATTICES:def 7;
hence thesis by A,B,C,D,E;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster the carrier of IntermediateFields E
-> non empty E-intermediate-membered;
coherence;
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
let F be Field, E be FieldExtension of F;
set L = IntermediateFields E;
H: the doubleLoopStr of E == E;
F is Subfield of E by FIELD_4:7; then
F is Subfield of the doubleLoopStr of E by H,EC_PF_1:5; then
the doubleLoopStr of E in IntermediateFields(E,F) by H,FIELD_14:4; then
reconsider Ed = the doubleLoopStr of E as IntermediateField of E,F by di;
reconsider c = Ed as Element of L by di;
I: now let a,b be Element of L, K1,K2 be IntermediateField of E,F;
assume K1 = a & K2 = b;
hence K1"\/"K2 = (SubJoin E).(a,b) by dJ .= a"\/"b by LATTICES:def 1;
end;
take c;
J: now let K be IntermediateField of E,F;
Ed in {Ed,K} by TARSKI:def 2; then
Ed is Subfield of Ed "\/" K by lem10; then
J1: the carrier of Ed c= the carrier of Ed "\/" K by EC_PF_1:def 1;
the carrier of Ed "\/" K c= the carrier of Ed by EC_PF_1:def 1;
hence Ed "\/" K = Ed by H,J1,XBOOLE_0:def 10,EC_PF_1:8;
end;
now let a be Element of L;
consider K being strict Field such that
K: K = a & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
reconsider K = a as IntermediateField of E,F by K,di;
thus c"\/"a = Ed "\/" K by I .= c by J;
hence a"\/"c = c;
end;
hence thesis;
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
let F be Field, E be FieldExtension of F;
set L = IntermediateFields E;
H: the doubleLoopStr of F == F;
F is Subfield of E by FIELD_4:7; then
K: the doubleLoopStr of F is Subfield of E by H,EC_PF_1:5; then
the doubleLoopStr of F in IntermediateFields(E,F) by H,FIELD_14:4; then
reconsider Fd = the doubleLoopStr of F as IntermediateField of E,F by di;
reconsider c = Fd as Element of L by di;
I: now let a,b be Element of L, K1,K2 be IntermediateField of E,F;
assume K1 = a & K2 = b;
hence K1"/\"K2 = (SubMeet E).(a,b) by dM .= a"/\"b by LATTICES:def 2;
end;
take c;
J: now let K be IntermediateField of E,F;
Fd in {Fd,K} by TARSKI:def 2; then
Fd "/\" K is Subfield of Fd by lem8; then
J1: the carrier of Fd "/\" K c= the carrier of Fd by EC_PF_1:def 1;
now let G be Element of {Fd,K};
per cases by TARSKI:def 2;
suppose G = Fd;
hence Fd is Subfield of G by FIELD_4:1;
end;
suppose J2: G = K;
K in IntermediateFields(E,F) by di; then
F is Subfield of G & G is Subfield of E by J2,FIELD_14:4;
hence Fd is Subfield of G by H,EC_PF_1:5;
end;
end; then
Fd is Subfield of Fd "/\" K by K,lem9; then
the carrier of Fd c= the carrier of Fd "/\" K by EC_PF_1:def 1;
hence Fd "/\" K = Fd by K,J1,XBOOLE_0:def 10,EC_PF_1:8;
end;
now let a be Element of L;
consider K being strict Field such that
K: K = a & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
reconsider K = a as IntermediateField of E,F by K,di;
thus c"/\"a = Fd "/\" K by I .= c by J;
hence a"/\"c = c;
end;
hence thesis;
end;
theorem
for F being Field
for E being FieldExtension of F
holds Top(IntermediateFields E) = the doubleLoopStr of E
proof
let F be Field, E be FieldExtension of F;
set L = IntermediateFields E;
ex c being Element of L st
for a being Element of L holds c"\/"a = c & a"\/"c = c
by lemco1; then
reconsider L as upper-bounded Lattice by LATTICES:def 14;
H: the doubleLoopStr of E == E;
F is Subfield of E by FIELD_4:7; then
F is Subfield of the doubleLoopStr of E by H,EC_PF_1:5; then
the doubleLoopStr of E in IntermediateFields(E,F) by H,FIELD_14:4; then
reconsider Ed = the doubleLoopStr of E as IntermediateField of E,F by di;
reconsider c = Ed as Element of L by di;
I: now let a,b be Element of L, K1,K2 be IntermediateField of E,F;
assume K1 = a & K2 = b;
hence K1 "\/" K2 = (SubJoin E).(a,b) by dJ .= a "\/" b by LATTICES:def 1;
end;
J: now let K be IntermediateField of E,F;
Ed in {Ed,K} by TARSKI:def 2; then
Ed is Subfield of Ed "\/" K by lem10; then
J1: the carrier of Ed c= the carrier of Ed "\/" K by EC_PF_1:def 1;
the carrier of Ed "\/" K c= the carrier of Ed by EC_PF_1:def 1;
hence Ed "\/" K = Ed by H,J1,XBOOLE_0:def 10,EC_PF_1:8;
end;
now let a be Element of L;
consider K being strict Field such that
K: K = a & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
reconsider K = a as IntermediateField of E,F by K,di;
thus c"\/"a = Ed "\/" K by I .= c by J;
hence a"\/"c = c;
end;
hence thesis by LATTICES:def 17;
end;
theorem
for F being Field
for E being FieldExtension of F
holds Bottom(IntermediateFields E) = the doubleLoopStr of F
proof
let F be Field, E be FieldExtension of F;
set L = IntermediateFields E;
ex c being Element of L st
for a being Element of L holds c"/\"a = c & a"/\"c = c
by lemco2; then
reconsider L as lower-bounded Lattice by LATTICES:def 13;
H: the doubleLoopStr of F == F;
F is Subfield of E by FIELD_4:7; then
K: the doubleLoopStr of F is Subfield of E by H,EC_PF_1:5; then
the doubleLoopStr of F in IntermediateFields(E,F) by H,FIELD_14:4; then
reconsider Fd = the doubleLoopStr of F as IntermediateField of E,F by di;
reconsider c = Fd as Element of L by di;
I: now let a,b be Element of L, K1,K2 be IntermediateField of E,F;
assume K1 = a & K2 = b;
hence K1 "/\" K2 = (SubMeet E).(a,b) by dM .= a "/\" b by LATTICES:def 2;
end;
J: now let K be IntermediateField of E,F;
Fd in {Fd,K} by TARSKI:def 2; then
Fd "/\" K is Subfield of Fd by lem8; then
J1: the carrier of Fd "/\" K c= the carrier of Fd by EC_PF_1:def 1;
now let G be Element of {Fd,K};
per cases by TARSKI:def 2;
suppose G = Fd;
hence Fd is Subfield of G by FIELD_4:1;
end;
suppose J2: G = K;
K in IntermediateFields(E,F) by di; then
F is Subfield of G & G is Subfield of E by J2,FIELD_14:4;
hence Fd is Subfield of G by H,EC_PF_1:5;
end;
end; then
Fd is Subfield of Fd "/\" K by K,lem9; then
the carrier of Fd c= the carrier of Fd "/\" K by EC_PF_1:def 1;
hence Fd "/\" K = Fd by K,J1,XBOOLE_0:def 10,EC_PF_1:8;
end;
now let a be Element of L;
consider K being strict Field such that
K: K = a & F is Subfield of K & K is Subfield of E by FIELD_14:def 1;
reconsider K = a as IntermediateField of E,F by K,di;
thus c"/\"a = Fd "/\" K by I .= c by J;
hence a"/\"c = c;
end;
hence thesis by LATTICES:def 16;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster IntermediateFields E -> complete;
coherence
proof
set L = IntermediateFields E;
ex c being Element of L st
for a being Element of L holds c"\/"a = c & a"\/"c = c
by lemco1; then
reconsider L as upper-bounded Lattice by LATTICES:def 14;
I: now let a,b be Element of L, K1,K2 be IntermediateField of E,F;
assume K1 = a & K2 = b;
hence K1"/\"K2 = (SubMeet E).(a,b) by dM .= a"/\"b by LATTICES:def 2;
end;
now let Y be Subset of L;
per cases;
suppose A1: Y = {};
thus ex a being Element of L st a is_less_than Y &
for b being Element of L st b is_less_than Y holds b [= a
proof
take Top L;
for a being Element of L st a in Y holds Top L [= a by A1;
hence Top L is_less_than Y by LATTICE3:def 16;
let b be Element of L;
assume b is_less_than Y;
thus thesis by LATTICES:19;
end;
end;
suppose Y <> {}; then
reconsider M = Y as non empty Subset of IntermediateFields(E,F);
reconsider K1 = /\M as IntermediateField of E,F by lem12;
reconsider a = K1 as Element of L by di;
thus ex a being Element of L st a is_less_than Y &
for b being Element of L st b is_less_than Y holds b [= a
proof
take a;
now let q be Element of L;
assume q in Y; then
reconsider K2 = q as Element of M;
reconsider K2 as IntermediateField of E,F;
/\M is Subfield of K2 by lem8;
then K1 "/\" K2 = K1 by lem20;
then a "/\" q = a by I;
hence a [= q by LATTICES:4;
end;
hence a is_less_than Y by LATTICE3:def 16;
thus for b being Element of L st b is_less_than Y holds b [= a
proof
let b be Element of L;
consider Kb being strict Field such that
A1: Kb = b &
F is Subfield of Kb & Kb is Subfield of E by FIELD_14:def 1;
reconsider Kb = b as IntermediateField of E,F by A1,di;
assume A2: b is_less_than Y;
now let G be Element of M;
A3: M c= IntermediateFields(E,F);
reconsider G1 = G as IntermediateField of E,F;
reconsider c = G1 as Element of L by A3;
b "/\" c = b by A2,LATTICE3:def 16,LATTICES:4; then
Kb "/\" G1 = Kb by I;
hence Kb is Subfield of G by lem20;
end; then
Kb is Subfield of K1 by A1,lem9; then
Kb "/\" K1 = Kb by lem20; then
b "/\" a = b by I;
hence b [= a by LATTICES:4;
end;
end;
end;
end;
hence thesis by VECTSP_8:def 6;
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
proof
set L = IntermediateFields E;
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
hence thesis;
end;
end;
theorem
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
let F be Field, E be FieldExtension of F;
let a,b be Element of the carrier of LattPOSet(IntermediateFields E);
set L = IntermediateFields E;
H: LattRel L = { [p,q] where p is Element of L, q is Element of L: p [= q } &
LattPOSet L = RelStr(#the carrier of L, LattRel L#)
by LATTICE3:def 2,FILTER_1:def 8;
reconsider p = a, q = b as Element of L by H;
reconsider K1 = p, K2 = q as IntermediateField of E,F;
J: now let a,b be Element of L, K1,K2 be IntermediateField of E,F;
assume K1 = a & K2 = b;
hence K1 "/\" K2 = (SubMeet E).(a,b) by dM .= a "/\" b by LATTICES:def 2;
end;
A: now assume a <= b; then
[p,q] in LattRel L by H,ORDERS_2:def 5; then
p "/\" q = p by LATTICES:4,FILTER_1:31; then
K1 "/\" K2 = K1 by J;
hence K1 is Subfield of K2 by lem20;
end;
now assume K1 is Subfield of K2;
then K1 "/\" K2 = K1 by lem20;
then p "/\" q = p by J; then
[p,q] in LattRel L by FILTER_1:31,LATTICES:4;
hence a <= b by H,ORDERS_2:def 5;
end;
hence thesis by A;
end;
begin :: Sets of Functions of Rings
definition
let R be Ring;
let X be set;
attr X is R-functional means :PP:
for o being object st o in X holds o is Function of R,R;
end;
definition
let R be Ring;
let L be 1-sorted;
attr L is R-functional means :PQ:
the carrier of L is R-functional;
end;
registration
let R be Ring;
cluster non empty R-functional for set;
existence
proof
take {id R};
thus thesis by TARSKI:def 1;
end;
end;
registration
let R be Ring;
let X be R-functional set;
cluster -> R-functional for Subset of X;
coherence by PP;
end;
definition
let R be Ring;
let X be non empty R-functional set;
redefine mode Element of X -> Function of R,R; :: redefines Element (SUBSET_1, definition)
coherence by PP;
end;
registration
let R be Ring;
cluster non empty R-functional for 1-sorted;
existence
proof
take L = 1-sorted(#{id R}#);
for o being object st o in the carrier of L holds o is Function of R,R
by TARSKI:def 1;
hence thesis by PP;
end;
end;
registration
let R be Ring;
let L be R-functional 1-sorted;
cluster -> R-functional for Subset of L;
coherence 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 by PQ;
end;
registration
let R be Ring;
let S be RingExtension of R;
cluster R-fixing for Function of S,S;
existence
proof
take id S;
now
let a be Element of R;
R is Subring of S by FIELD_4:def 1; then
the carrier of R c= the carrier of S by C0SP1:def 3; then
reconsider a1 = a as Element of S;
thus (id S).a = a1 .= a;
end;
hence thesis;
end;
end;
registration
let R be Ring;
let S be RingExtension of R;
cluster id S -> R-fixing;
coherence
proof
now
let a be Element of R;
R is Subring of S by FIELD_4:def 1; then
the carrier of R c= the carrier of S by C0SP1:def 3; then
reconsider a1 = a as Element of S;
thus (id S).a = a1 .= a;
end;
hence thesis;
end;
end;
registration
let R be Ring;
let S be RingExtension of R;
let f,g be R-fixing Function of S,S;
cluster f * g -> R-fixing for Function of S,S;
coherence
proof
now
let a be Element of R;
R is Subring of S by FIELD_4:def 1; then
the carrier of R c= the carrier of S by C0SP1:def 3; then
reconsider a1 = a as Element of S;
thus (f*g).a = f.(g.a1) by FUNCT_2:15
.= f.a by FIELD_8:def 2 .= a by FIELD_8:def 2;
end;
hence thesis;
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
proof
defpred P[Nat] means f`^($1) is R-fixing;
f`^0 = id S by FIELD_16:1; then
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
f`^(k+1) = f`^k * f by FIELD_16:2;
hence P[k+1] by IV;
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
end;
registration
let R be Ring;
let S be RingExtension of R;
let f be R-fixing one-to-one Function of S,S;
cluster f" -> R-fixing one-to-one for Function of S,S;
coherence
proof
H: dom f = the carrier of S by FUNCT_2:def 1;
now let a be Element of R;
R is Subring of S by FIELD_4:def 1; then
the carrier of R c= the carrier of S by C0SP1:def 3; then
reconsider a1 = a as Element of S;
f.a = a by FIELD_8:def 2;
hence (f").a = a1 by H,FUNCT_1:34 .= a;
end;
hence thesis;
end;
end;
begin :: On Homomorphisms from R[X] to R[X]
definition
let X,Y be non empty set;
let f be Function of X,Y;
let S be non empty finite Subset of X;
redefine func f.:S -> non empty finite Subset of Y; :: redefines .: (FUNCT_1, redefinition) → .: (RELAT_1, definition)
coherence
proof
now let o be object;
assume o in f.:S; then
consider x being object such that
A: x in dom f & x in S & o = f.x by FUNCT_1:def 6;
o in rng f & rng f c= Y by A,FUNCT_1:3,RELAT_1:def 19;
hence o in Y;
end; then
reconsider M = f.:S as Subset of Y by TARSKI:def 3;
set x = the Element of S;
f.x in Y & dom f = X by FUNCT_2:def 1;
then f.x in M by FUNCT_1:def 6;
hence thesis;
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:
for f being Element of the carrier of Polynom-Ring R
for i being Nat holds (it.f).i = h.(f.i);
existence
proof
A1: for f being Polynomial of R ex g being Polynomial of R
st for i being Nat holds g.i = h.(f.i)
proof
let f be Polynomial of R;
deffunc F(Nat) = h.(f.$1);
consider q being AlgSequence of R such that
A2: len q <= len f & for k being Nat st k < len f holds q.k = F(k)
from ALGSEQ_1:sch 1;
take q;
now let i be Nat;
per cases;
suppose i < len f;
hence q.i = h.(f.i) by A2;
end;
suppose A3: i >= len f; then
f.i = 0.R by ALGSEQ_1:8;
hence h.(f.i) = q.i by A3,A2,ALGSEQ_1:8,XXREAL_0:2;
end;
end;
hence thesis;
end;
defpred P[object,object] means
ex f being (Polynomial of R), g being Polynomial of R
st $1 = f & $2 = g & for i being Nat holds g.i = h.(f.i);
A4: for x being object st x in the carrier of Polynom-Ring R
ex y being object st y in the carrier of Polynom-Ring R & P[x,y]
proof
let x be object;
assume x in the carrier of Polynom-Ring R; then
reconsider y = x as Polynomial of R by POLYNOM3:def 10;
consider z being Polynomial of R such that
A5: for i being Nat holds z.i = h.(y.i) by A1;
take z;
thus thesis by A5,POLYNOM3:def 10;
end;
consider F being Function of
the carrier of Polynom-Ring R, the carrier of Polynom-Ring R such that
A6: for x being object st x in the carrier of Polynom-Ring R holds P[x,F.x]
from FUNCT_2:sch 1(A4);
take F;
now let f be (Polynomial of R), g be Polynomial of R;
assume
A7: g = F.f;
let i be Nat;
f in the carrier of Polynom-Ring R by POLYNOM3:def 10; then
P[f,F.f] by A6;
hence g.i = h.(f.i) by A7;
end;
hence thesis;
end;
uniqueness
proof
let F,G be Function of Polynom-Ring R, Polynom-Ring R;
assume that
A8: for f being Element of the carrier of Polynom-Ring R
for i being Nat holds (F.f).i = h.(f.i) and
A9: for f being Element of the carrier of Polynom-Ring R
for i being Nat holds (G.f).i = h.(f.i);
now let o be object;
assume o in the carrier of Polynom-Ring R;
then reconsider p = o as Element of the carrier of Polynom-Ring R;
now let u be object;
assume u in NAT;
then reconsider m = u as Nat;
(F.p).m = h.(p.m) by A8 .= (G.p).m by A9;
hence (F.p).u = (G.p).u;
end;
then F.p = G.p;
hence F.o = G.o;
end;
hence F = G;
end;
end;
registration
let R be Ring;
let h be Homomorphism of R;
cluster PolyHom h -> additive multiplicative unity-preserving;
coherence
proof
id R is RingHomomorphism; then
reconsider S = R as R-homomorphic Ring by RING_2:def 4;
reconsider h1 = h as Homomorphism of R,S;
A: now let a,b be Element of the carrier of Polynom-Ring R;
now let i be Nat;
thus ((PolyHom h1).a).i
= h1.(a.i) by FIELD_1:def 2
.= ((PolyHom h).a).i by dp;
end;
hence (PolyHom h1).a = (PolyHom h).a;
end;
now let a,b be Element of the carrier of Polynom-Ring R;
B: (PolyHom h1).a = (PolyHom h).a & (PolyHom h1).b = (PolyHom h).b by A;
thus (PolyHom h).(a+b)
= (PolyHom h1).(a+b) by A
.= (PolyHom h).a + (PolyHom h).b by B,VECTSP_1:def 20;
end;
hence PolyHom h is additive;
now let a,b be Element of the carrier of Polynom-Ring R;
B: (PolyHom h1).a = (PolyHom h).a & (PolyHom h1).b = (PolyHom h).b by A;
thus (PolyHom h).(a*b)
= (PolyHom h1).(a*b) by A
.= (PolyHom h).a * (PolyHom h).b by B,GROUP_6:def 6;
end;
hence PolyHom h is multiplicative by GROUP_6:def 6;
(PolyHom h).(1_(Polynom-Ring R))
= (PolyHom h1).(1_(Polynom-Ring R)) by A
.= 1_(Polynom-Ring R) by GROUP_1:def 13;
hence PolyHom h is unity-preserving by GROUP_1:def 13;
end;
end;
theorem
for R being Ring
for h being Homomorphism of R holds (PolyHom h).(0_.R) = 0_.R
proof
let R be Ring, h be Homomorphism of R;
0_.R = 0.(Polynom-Ring R) by POLYNOM3:def 10;
hence thesis;
end;
theorem
for R being Ring
for h being Homomorphism of R holds (PolyHom h).(1_.R) = 1_.R
proof
let R be Ring,h be Homomorphism of R;
thus (PolyHom h).(1_.R) = (PolyHom h).(1_(Polynom-Ring R)) by POLYNOM3:def 10
.= 1_(Polynom-Ring R) by GROUP_1:def 13 .= 1_.R by POLYNOM3:def 10;
end;
theorem
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
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
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
let R be Ring; let h be Homomorphism of R;
let p be Element of the carrier of (Polynom-Ring R), b be Element of R;
reconsider q = b * p as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
reconsider f = (PolyHom h).q as Element of the carrier of Polynom-Ring R;
now let i be Element of NAT;
f.i = h.(q.i) by dp
.= h.(b * (p.i)) by POLYNOM5:def 4
.= h.b * h.(p.i) by GROUP_6:def 6
.= h.b * ((PolyHom h).p).i by dp
.= (h.b * (PolyHom h).p).i by POLYNOM5:def 4;
hence f.i = (h.b * (PolyHom h).p).i;
end;
hence thesis by FUNCT_2:63;
end;
theorem
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
let R be Ring; let h be Homomorphism of R;
let p be Element of the carrier of (Polynom-Ring R), x be Element of R;
id R is RingHomomorphism; then
reconsider S = R as R-homomorphic Ring by RING_2:def 4;
reconsider h1 = h as Homomorphism of R,S;
A: now let a,b be Element of the carrier of Polynom-Ring R;
now let i be Nat;
thus ((PolyHom h1).a).i
= h1.(a.i) by FIELD_1:def 2
.= ((PolyHom h).a).i by dp;
end;
hence (PolyHom h1).a = (PolyHom h).a;
end;
thus h.eval(p,x)
= eval((PolyHom h1).p, h1.x) by FIELD_1:27
.= eval((PolyHom h).p, h.x) by A;
end;
theorem
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
let R be domRing; let h be Homomorphism of R;
let p be Element of the carrier of (Polynom-Ring R), a,x be Element of R;
id R is RingHomomorphism; then
reconsider S = R as R-homomorphic domRing by RING_2:def 4;
reconsider h1 = h as Homomorphism of R,S;
A: now let a,b be Element of the carrier of Polynom-Ring R;
now let i be Nat;
thus ((PolyHom h1).a).i
= h1.(a.i) by FIELD_1:def 2
.= ((PolyHom h).a).i by dp;
end;
hence (PolyHom h1).a = (PolyHom h).a;
end;
thus h.eval(a*p,x)
= h1.a * eval((PolyHom h1).p,h1.x) by FIELD_1:28
.= h.a * eval((PolyHom h).p,h.x) by A;
end;
theorem
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, h being F-fixing Homomorphism of E
holds h.(Ext_eval(p,a)) = Ext_eval(p,h.a)
proof
let F be Field, E be FieldExtension of F,
p be Element of the carrier of Polynom-Ring F;
let a be Element of E, h be F-fixing Homomorphism of E;
E is Subfield of E by FIELD_4:1; then
reconsider E1 = E as FieldExtension of E by FIELD_4:7;
reconsider h1 = h as Homomorphism of E,E1;
h1.(Ext_eval(p,a)) = Ext_eval(p,h1.a) by FIELD_13:42;
hence thesis;
end;
theorem Th32:
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
let R be Ring, h be Monomorphism of R;
let p be Element of the carrier of (Polynom-Ring R);
reconsider f = (PolyHom h).p as
Element of the carrier of Polynom-Ring R;
A1: now let i be Nat;
assume i >= len p; then
p.i = 0.R by ALGSEQ_1:8;
hence f.i = h.(0.R) by dp .= 0.R;
end;
now let m be Nat;
assume
A2: m is_at_least_length_of f;
now assume A0: len p > m; then
A3: len p - 1 >= (m - 1) + 1 by INT_1:7,XREAL_1:9;
reconsider lp = len p - 1 as Element of NAT by A0,INT_1:3;
A4: lp + 1 = len p;
h.(0.R) = f.lp by A3,A2,ALGSEQ_1:def 2
.= h.(p.lp) by dp; then
p.lp = 0.R by FUNCT_2:19;
hence contradiction by A4,ALGSEQ_1:10;
end;
hence len p <= m;
end; then
len f = len p by A1,ALGSEQ_1:def 3,def 2;
hence deg p = (len f)-1 by HURWITZ:def 2 .= deg (PolyHom h).p by HURWITZ:def 2;
end;
theorem
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
let R be Ring, h be Monomorphism of R;
let p be Element of the carrier of Polynom-Ring R;
reconsider f = (PolyHom h).p as Polynomial of R;
reconsider LMp = LM p as
Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
A1: len f - 1 = deg f by HURWITZ:def 2
.= deg p by Th32 .= len p - 1 by HURWITZ:def 2;
now let i be Element of NAT;
per cases;
suppose A2: i = len p -'1; then
(LM f).i = f.(len p -'1) by A1,POLYNOM4:def 1
.= h.(p.(len p -'1)) by dp
.= h.((LM p).i) by A2,POLYNOM4:def 1
.= ((PolyHom h).(LMp)).i by dp;
hence (LM f).i = ((PolyHom h).(LMp)).i;
end;
suppose A3: i <> len p -'1; then
(LM f).i = h.(0.R) by A1,POLYNOM4:def 1
.= h.((LM p).i) by A3,POLYNOM4:def 1
.= ((PolyHom h).(LMp)).i by dp;
hence (LM f).i = ((PolyHom h).(LMp)).i;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem G4a:
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
let F be Field, h be Homomorphism of F; let a be Element of F;
id F is RingHomomorphism; then
reconsider S = F as F-homomorphic Field by RING_2:def 4;
reconsider h1 = h as Homomorphism of F,S;
now let i be Nat;
thus ((PolyHom h1).(X-a)).i
= h1.((X-a).i) by FIELD_1:def 2
.= ((PolyHom h).(X-a)).i by dp;
end; then
(PolyHom h1).(X-a) = (PolyHom h).(X-a);
hence thesis by FIELD_13:25;
end;
theorem
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
let R be Field, S be non empty finite Subset of R;
let p be Ppoly of R,S, h be Monomorphism of R;
defpred P[Nat] means
for S being non empty finite Subset of R
for p being Ppoly of R,S st deg p = $1
holds (PolyHom h).p is Ppoly of R,(h.:S);
IA: P[1]
proof
now let S be non empty finite Subset of R, p be Ppoly of R,S;
assume deg p = 1; then
card S = 1 by RING_5:60; then
consider a being object such that A1: S = {a} by CARD_2:42;
a in S by A1,TARSKI:def 1; then
reconsider a as Element of R;
p = X-a by A1,FIELD_14:20; then
A2: (PolyHom h).p = X-(h.a) by G4a;
dom h = the carrier of R by FUNCT_2:def 1; then
{h.a} = Im(h,a) by FUNCT_1:59 .= h.:{a} by RELAT_1:def 16;
hence (PolyHom h).p is Ppoly of R,(h.:S) by A1,A2,RING_5:57;
end;
hence thesis;
end;
IS: now let k be Nat;
assume k >= 1;
assume IV: P[k];
now let S be non empty finite Subset of R, p be Ppoly of R,S;
assume A0: deg p = k+1;
set a = the Element of S;
A1: card S = k + 1 by A0,RING_5:60;
reconsider a as Element of R;
reconsider S1 = S \ {a} as finite Subset of R;
now let o be object;
assume o in {a}; then
o = a by TARSKI:def 1;
hence o in S;
end; then
{a} c= S; then
A4: S = S1 \/ {a} by XBOOLE_1:45;
a in {a} by TARSKI:def 1; then
A8: not a in S1 by XBOOLE_0:def 5; then
A5: card S = card S1 + 1 by A4,CARD_2:41;
per cases;
suppose S1 is empty;
then deg p = 1 by A5,RING_5:60;
hence (PolyHom h).p is Ppoly of R,(h.:S) by IA;
end;
suppose S1 is non empty; then
reconsider S1 as non empty finite Subset of R;
Roots p = S by RING_5:63; then
a is_a_root_of p by POLYNOM5:def 10; then
consider p1 being Polynomial of R such that
A7: p = rpoly(1,a) *' p1 by HURWITZ:33;
reconsider p2 = p1 as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
per cases;
suppose p1 is constant; then
deg p1 <= 0 by RATFUNC1:def 2; then
consider b being Element of R such that
B1: p2 = b|R by RING_4:20,RING_4:def 4;
1.R = LC p by RATFUNC1:def 7
.= LC rpoly(1,a) * LC p1 by A7,NIVEN:46
.= (1.(R)) * LC(b|R) by B1,RATFUNC1:def 7
.= b by RING_5:6;
then p1 = 1_.(R) by B1,RING_4:14;
then deg p = 1 by A7,HURWITZ:27;
hence (PolyHom h).p is Ppoly of R,(h.:S) by IA;
end;
suppose p1 is non constant; then
reconsider p1 as non constant Polynomial of R;
reconsider p1 as Ppoly of R,S1 by A7,FIELD_14:33;
reconsider p2 = p1 as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
deg p1 = k by A5,A1,RING_5:60; then
reconsider q1 = (PolyHom h).p1 as Ppoly of R,(h.:S1) by IV;
(PolyHom h).rpoly(1,a) = (PolyHom h).(X-a) .= X-(h.a) by G4a; then
reconsider qa = (PolyHom h).rpoly(1,a) as Ppoly of R,{h.a}
by RING_5:57;
H0: dom h = the carrier of R by FUNCT_2:def 1; then
H: {h.a} = Im(h,a) by FUNCT_1:59 .= h.:{a} by RELAT_1:def 16;
A9: now assume H1: (h.:S1) /\ {h.a} <> {};
set x = the Element of (h.:S1) /\ {h.a};
H2: x in (h.:S1) & x in {h.a} by H1,XBOOLE_0:def 4;
h.a in h.:S1 by H2,TARSKI:def 1; then
consider b being object such that
H3: b in dom h & b in S1 & h.a = h.b by FUNCT_1:def 6;
reconsider b as Element of R by H3;
thus contradiction by A8,H0,H3,FUNCT_1:def 4;
end;
(PolyHom h).p
= (PolyHom h).((X-a) * p2) by A7,POLYNOM3:def 10
.= ((PolyHom h).(X-a)) * ((PolyHom h).p2) by GROUP_6:def 6
.= qa *' q1 by POLYNOM3:def 10; then
(PolyHom h).p is Ppoly of R,((h.:S1) \/ {h.a}) by A9,FIELD_14:28;
hence (PolyHom h).p is Ppoly of R,(h.:S) by A4,H,RELAT_1:120;
end;
end;
end;
hence P[k+1];
end;
I: for k being Nat st k >= 1 holds P[k] from NAT_1:sch 8(IA,IS);
reconsider n = deg p as Element of NAT;
n + 1 > 0 + 1 by RATFUNC1:def 2,XREAL_1:6;
then n >= 1 by NAT_1:13;
hence thesis by I;
end;
lemZ0:
for F being Field, E being FieldExtension of F, S being Subset of E
holds (id E).:S = S
proof
let F be Field, E be FieldExtension of F, S be Subset of E;
A: now let o be object;
assume B: o in S; then
reconsider a = o as Element of E;
(id E).a = a & dom(id E) = the carrier of E;
hence o in (id E).:S by B,FUNCT_1:def 6;
end;
now let o be object;
assume o in (id E).:S; then
consider x being object such that
C: x in dom(id E) & x in S & o = (id E).x by FUNCT_1:def 6;
reconsider a = x as Element of E by C;
(id E).a = a;
hence o in S by C;
end;
hence thesis by A,TARSKI:2;
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
let F be Field, E be FieldExtension of F, S be non empty Subset of E;
let h be Automorphism of E;
assume AS: h.:S = S;
U: now let h be Automorphism of E;
assume A: h.:S = S;
dom h = the carrier of E by FUNCT_2:def 1;
hence dom(h|S) = S by RELAT_1:62;
B: now let o be object;
assume o in S; then
consider x being object such that
A1: x in dom h & x in S & o = h.x by A,FUNCT_1:def 6;
thus o in rng(h|S) by A1,FUNCT_1:50;
end;
now let o be object;
assume o in rng(h|S); then
consider x being object such that
A2: x in dom(h|S) & o = (h|S).x by FUNCT_1:def 3;
A3: o = h.x by A2,FUNCT_1:47;
x in dom h & x in S by A2,RELAT_1:57;
hence o in S by A,A3,FUNCT_1:def 6;
end;
hence rng(h|S) = S by B,TARSKI:2;
end;
hence dom(h|S) = S & rng(h|S) = S by AS;
dom(h") = the carrier of E by FUNCT_2:def 1;
hence dom(h"|S) = S by RELAT_1:62;
B: rng h = the carrier of E & h is one-to-one by FUNCT_2:def 3;
h".:S = (h"*h).:S by AS,RELAT_1:126
.= (id E).:S by B,FUNCT_2:29
.= S by lemZ0;
hence thesis by U;
end;
theorem
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
let F be Field, E be FieldExtension of F, S be non empty Subset of E;
let h be Automorphism of E;
assume AS: h.:S = S; then
dom(h|S) = S & rng(h|S) = S by lemZ3; then
reconsider g = h|S as Function of S,S by FUNCT_2:2;
rng g = S by AS,lemZ3;
then g is bijective by FUNCT_1:52,FUNCT_2:def 3;
hence h|S is Permutation of S;
dom(h"|S) = S & rng(h"|S) = S by AS,lemZ3; then
reconsider g = h"|S as Function of S,S by FUNCT_2:2;
rng g = S by AS,lemZ3;
then g is bijective by FUNCT_1:52,FUNCT_2:def 3;
hence h"|S is Permutation of S;
end;