:: Splitting Fields
:: by Christoph Schwarzweller
::
:: Received June 30, 2021
:: Copyright (c) 2021 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 3.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/3.0/.
environ
vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, CAT_1, STRUCT_0, SUBSET_1,
SUPINF_2, QC_LANG1, NAT_1, MESFUNC1, REALSET1, C0SP1, FUNCT_4, CARD_3,
POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, CATALG_1, EC_PF_1, HURWITZ,
FINSEQ_1, FINSEQ_3, MOD_4, RANKNULL, FUNCT_1, GLIB_000, RELAT_1, CARD_1,
IDEAL_1, GCD_1, GROUP_6, XBOOLE_0, NUMBERS, MSSUBFAM, POLYNOM5, GROUP_1,
ZFMISC_1, FUNCT_7, GROUP_4, QUOFIELD, FDIFF_1, VECTSP10, YELLOW_8,
RATFUNC1, RING_2, RING_3, FUNCT_2, ALGNUM_1, RING_5, FIELD_4, WELLORD1,
VECTSP_2, RLVECT_5, XXREAL_0, XCMPLX_0, FIELD_6, FOMODEL1, ARYTM_1,
FIELD_1, PARTFUN1, ORDINAL4, FIELD_8;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELSET_1, PARTFUN1, REALSET1,
ORDINAL1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_3, ZFMISC_1, MATRLIN2,
NAT_D, NUMBERS, CARD_1, XCMPLX_0, XXREAL_0, NAT_1, VFUNCT_1, FUNCT_7,
IDEAL_1, ALGSEQ_1, GCD_1, QUOFIELD, STRUCT_0, POLYNOM3, POLYNOM4,
POLYNOM5, GROUP_1, GROUP_4, GROUP_6, MOD_4, VECTSP10, ALGSTR_0, VECTSP_1,
VECTSP_2, VECTSP_9, RANKNULL, RLVECT_1, MATRLIN, HURWITZ, RINGCAT1,
C0SP1, EC_PF_1, RATFUNC1, RING_2, RING_3, RING_4, RING_5, ALGNUM_1,
FIELD_1, FIELD_4, FIELD_6, FIELD_7;
constructors POLYNOM4, RELSET_1, ABIAN, NAT_D, VFUNCT_1, RATFUNC1, GCD_1,
REALSET1, RINGCAT1, RING_3, ALGSEQ_1, VECTSP_9, MATRLIN2, GROUP_4,
ALGNUM_1, RING_5, FIELD_6, FIELD_7;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, FINSET_1,
FUNCT_2, SUBSET_1, RLVECT_1, QUOFIELD, FUNCT_1, CARD_1, RATFUNC1,
RELAT_1, MOD_4, RINGCAT1, FINSEQ_1, RING_2, RING_3, RING_4, RING_5,
VFUNCT_1, REALSET1, POLYNOM3, POLYNOM5, GROUP_6, FIELD_1, FIELD_4,
GRCAT_1, FIELD_6, FIELD_7;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin :: Preliminaries
theorem :: FIELD_8:1
for R being Ring
for p being Polynomial of R
for q being Element of the carrier of Polynom-Ring R
st p = q holds -p = -q;
theorem :: FIELD_8:2
for R being Ring,
p being Polynomial of R
for a being Element of R holds a * p = (a|R) *' p;
theorem :: FIELD_8:3
for R being Ring
for a being Element of R holds LC(a|R) = a;
theorem :: FIELD_8:4
for R being Ring, S being Subring of R
for F being FinSequence of R
for G being FinSequence of S st F = G holds Product F = Product G;
registration
let F be Field;
cluster F-homomorphic F-monomorphic F-isomorphic for Field;
end;
registration
let R be Ring;
cluster -> R-homomorphic R-monomorphic for R-isomorphic Ring;
end;
registration
let R be Ring;
let S be R-homomorphic Ring;
cluster Polynom-Ring S -> (Polynom-Ring R)-homomorphic;
end;
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
cluster Polynom-Ring F2 -> (Polynom-Ring F1)-isomorphic;
end;
begin :: More on Polynomials
theorem :: FIELD_8:5
for R being non degenerated Ring,
S being RingExtension of R
for p being Polynomial of R
for q being Polynomial of S st p = q holds LC p = LC q;
theorem :: FIELD_8:6
for F being Field,
p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
q being Element of the carrier of Polynom-Ring E st p = q
for U being E-extending FieldExtension of F,
a being Element of U
holds Ext_eval(q,a) = Ext_eval(p,a);
theorem :: FIELD_8:7
for R being Ring,
S being RingExtension of R
for p being Element of the carrier of Polynom-Ring R
for q being Element of the carrier of Polynom-Ring S st p = q
for T1 being RingExtension of S,
T2 being RingExtension of R
st T1 = T2 holds Roots(T2,p) = Roots(T1,q);
theorem :: FIELD_8:8
for R being domRing,
F being non empty FinSequence of Polynom-Ring R,
p being Polynomial of R
st p = Product F &
(for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a))
holds deg p = len F;
theorem :: FIELD_8:9
for F being Field,
p being Polynomial of F
for a being non zero Element of F
holds a * p splits_in F iff p splits_in F;
theorem :: FIELD_8:10
for F being Field
for p being non constant monic Polynomial of F
for q being non zero Polynomial of F
st p *' q is Ppoly of F holds p is Ppoly of F;
theorem :: FIELD_8:11
for F being Field
for p being non constant Polynomial of F
for q being non zero Polynomial of F
st p *' q splits_in F holds p splits_in F;
theorem :: FIELD_8:12
for F being Field,
p,q being Polynomial of F
st p splits_in F & q splits_in F holds p *' q splits_in F;
theorem :: FIELD_8:13
for R being Ring,
S being R-homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h).(a|R) = (h.a)|S;
theorem :: FIELD_8:14
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for p,q being Element of the carrier of Polynom-Ring F1
holds p divides q iff (PolyHom h).p divides (PolyHom h).q;
theorem :: FIELD_8:15
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for p being irreducible Element of the carrier of Polynom-Ring F
st Ext_eval(p,a) = 0.E holds MinPoly(a,F) = NormPolynomial p;
theorem :: FIELD_8:16
for F1 being Field,
F2 being F1-monomorphic F1-homomorphic Field
for h being Monomorphism of F1,F2
for p being Element of the carrier of Polynom-Ring F1
holds NormPolynomial((PolyHom h).p) = (PolyHom h).(NormPolynomial p);
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let p be constant Element of the carrier of Polynom-Ring F1;
cluster (PolyHom h).p -> constant for
Element of the carrier of Polynom-Ring F2;
end;
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let p be non constant Element of the carrier of Polynom-Ring F1;
cluster (PolyHom h).p -> non constant for
Element of the carrier of Polynom-Ring F2;
end;
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let p be irreducible Element of the carrier of Polynom-Ring F1;
cluster (PolyHom h).p -> irreducible for
Element of the carrier of Polynom-Ring F2;
end;
theorem :: FIELD_8:17
for F1 being Field,
p being non constant Element of the carrier of Polynom-Ring F1
for F2 being F1-isomorphic Field
for h being Isomorphism of F1,F2
holds p splits_in F1 iff (PolyHom h).p splits_in F2;
theorem :: FIELD_8:18
for F being Field,
p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
U being E-extending FieldExtension of F
holds Roots(E,p) c= Roots(U,p);
theorem :: FIELD_8:19
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being FieldExtension of F
for U being FieldExtension of E holds p splits_in E implies p splits_in U;
begin :: More on Products of Linear Polynomials
theorem :: FIELD_8:20
for F being Field
for G being non empty FinSequence of the carrier of Polynom-Ring F
st for i being Nat st i in dom G
ex a being Element of F st G.i = rpoly(1,a)
holds G is Factorization of (Product G);
theorem :: FIELD_8:21
for F being Field
for G1,G2 being non empty FinSequence of Polynom-Ring F
st (for i being Nat st i in dom G1
ex a being Element of F st G1.i = rpoly(1,a)) &
(for i being Nat st i in dom G2
ex a being Element of F st G2.i = rpoly(1,a)) &
Product G1 = Product G2
for a being Element of F holds
(ex i being Nat st i in dom G1 & G1.i = rpoly(1,a)) iff
(ex i being Nat st i in dom G2 & G2.i = rpoly(1,a));
theorem :: FIELD_8:22
for F being Field,
E being FieldExtension of F
for G1 being non empty FinSequence of Polynom-Ring F
st for i being Nat st i in dom G1
ex a being Element of F st G1.i = rpoly(1,a)
for G2 being non empty FinSequence of Polynom-Ring E
st for i being Nat st i in dom G2
ex a being Element of E st G2.i = rpoly(1,a)
holds Product G1 = Product G2 implies
for a being Element of E holds
(ex i being Nat st i in dom G1 & G1.i = rpoly(1,a)) iff
(ex i being Nat st i in dom G2 & G2.i = rpoly(1,a));
theorem :: FIELD_8:23
for F being Field
for p being Ppoly of F
for a being Element of F holds LC(a * p) = a;
theorem :: FIELD_8:24
for F being Field,
E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E;
theorem :: FIELD_8:25
for F being Field,
E being FieldExtension of F
for a being non zero Element of F,
b being non zero Element of E
for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds a = b & p = q;
theorem :: FIELD_8:26
for F being Field,
E being FieldExtension of F
for G being non empty FinSequence of the carrier of Polynom-Ring E
st for i being Nat st i in dom G ex a being Element of F st G.i = rpoly(1,a)
holds (Product G) is Ppoly of F;
begin
theorem :: FIELD_8:27
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for U being FieldExtension of F
for E being U-extending FieldExtension of F st p splits_in E
holds p splits_in U iff Roots(E,p) c= the carrier of U;
theorem :: FIELD_8:28
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for U being FieldExtension of F
for E being U-extending FieldExtension of F st p splits_in E
holds p splits_in U iff Roots(E,p) c= Roots(U,p);
theorem :: FIELD_8:29
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for U being FieldExtension of F
for E being U-extending FieldExtension of F st p splits_in E
holds p splits_in U iff Roots(E,p) = Roots(U,p);
theorem :: FIELD_8:30
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being FieldExtension of F
st p splits_in E holds p splits_in FAdj(F,Roots(E,p));
definition
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
mode SplittingField of p -> FieldExtension of F means
:: FIELD_8:def 1
p splits_in it &
for E being FieldExtension of F
st p splits_in E & E is Subfield of it holds E == it;
end;
theorem :: FIELD_8:31
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st E is SplittingField of p;
theorem :: FIELD_8:32
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F
st FAdj(F,Roots(E,p)) is SplittingField of p;
theorem :: FIELD_8:33
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being FieldExtension of F st p splits_in E
holds FAdj(F,Roots(E,p)) is SplittingField of p;
theorem :: FIELD_8:34
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being SplittingField of p
holds E == FAdj(F,Roots(E,p));
registration
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster strict for SplittingField of p;
end;
registration
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster -> F-finite for SplittingField of p;
end;
begin :: Fixing and Extending Automorphisms
registration
let R be Ring;
cluster isomorphism for Function of R,R;
end;
definition
let R be Ring;
mode Homomorphism of R is
additive multiplicative unity-preserving Function of R,R;
mode Monomorphism of R is monomorphism Function of R,R;
mode Automorphism of R is isomorphism Function of R,R;
end;
definition
let R,S2 be Ring,
S1 be RingExtension of R;
let h be Function of S1,S2;
attr h is R-fixing means
:: FIELD_8:def 2
for a being Element of R holds h.a = a;
end;
theorem :: FIELD_8:35
for R,S2 being Ring,
S1 being RingExtension of R
for h being Function of S1,S2 holds h is R-fixing iff h|R = id R;
theorem :: FIELD_8:36
for F being Field,
E1 being FieldExtension of F,
E2 being E1-homomorphic FieldExtension of F
for h being Homomorphism of E1,E2
holds h is F-fixing iff
h is linear-transformation of VecSp(E1,F),VecSp(E2,F);
theorem :: FIELD_8:37
for F being Field,
E being FieldExtension of F
for E1 being E-extending FieldExtension of F,
E2 being E-extending FieldExtension of F
for h being Function of E1,E2 holds h is E-fixing implies h is F-fixing;
definition
let R be Ring,
S1,S2 be RingExtension of R;
let h be Function of S1,S2;
attr h is R-homomorphism means
:: FIELD_8:def 3
h is R-fixing additive multiplicative unity-preserving;
attr h is R-monomorphism means
:: FIELD_8:def 4
h is R-fixing monomorphism;
attr h is R-isomorphism means
:: FIELD_8:def 5
h is R-fixing isomorphism;
end;
registration
let R be Ring;
let S be RingExtension of R;
cluster R-fixing for Automorphism of S;
end;
theorem :: FIELD_8:38
for R being Ring,
S being RingExtension of R
for p being Element of the carrier of Polynom-Ring R
for h being R-fixing Monomorphism of S
for a being Element of S holds a in Roots(S,p) iff h.a in Roots(S,p);
theorem :: FIELD_8:39
for R being domRing,
S being domRingExtension of R
for p being non zero Element of the carrier of Polynom-Ring R
for h being R-fixing Monomorphism of S
holds h|Roots(S,p) is Permutation of Roots(S,p);
definition
let R1,R2,S2 be Ring,
S1 be RingExtension of R1;
let h1 be Function of R1,R2, h2 be Function of S1,S2;
attr h2 is h1-extending means
:: FIELD_8:def 6
for a being Element of R1 holds h2.a = h1.a;
end;
theorem :: FIELD_8:40
for R1,R2,S2 being Ring,
S1 being RingExtension of R1
for h1 being Function of R1,R2, h2 being Function of S1,S2
holds h2 is h1-extending iff h2|R1 = h1;
registration
let R be Ring;
let S be RingExtension of R;
cluster R-fixing -> (id R)-extending for Automorphism of S;
cluster (id R)-extending -> R-fixing for Automorphism of S;
end;
theorem :: FIELD_8:41
for F1,F2 being Field,
E1 being FieldExtension of F1, E2 being FieldExtension of F2
for K1 being E1-extending FieldExtension of F1,
K2 being E2-extending FieldExtension of F2
for h1 being Function of F1,F2, h2 being Function of E1,E2,
h3 being Function of K1,K2
st h2 is h1-extending & h3 is h2-extending holds h3 is h1-extending;
definition
let F be Field;
let E1,E2 be FieldExtension of F;
pred E1,E2 are_isomorphic_over F means
:: FIELD_8:def 7
ex i being Function of E1,E2 st i is F-isomorphism;
end;
theorem :: FIELD_8:42
for F being Field,
E being FieldExtension of F holds E,E are_isomorphic_over F;
theorem :: FIELD_8:43
for F being Field,
E1,E2 being FieldExtension of F
st E1,E2 are_isomorphic_over F holds E2,E1 are_isomorphic_over F;
theorem :: FIELD_8:44
for F being Field,
E1,E2,E3 being FieldExtension of F
st E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F
holds E1,E3 are_isomorphic_over F;
theorem :: FIELD_8:45
for F being Field,
E1 being F-finite FieldExtension of F,
E2 being FieldExtension of F
st E1,E2 are_isomorphic_over F holds E2 is F-finite & deg(E1,F) = deg(E2,F);
begin :: Some More Preliminaries
definition
let R be Ring,
S1,S2 be RingExtension of R;
let h be Relation of the carrier of S1,the carrier of S2;
attr h is R-isomorphism means
:: FIELD_8:def 8
ex g being Function of S1,S2 st g = h & g is R-isomorphism;
end;
theorem :: FIELD_8:46
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
holds 0.FAdj(F,{a}) = Ext_eval(0_.F,a) & 1.FAdj(F,{a}) = Ext_eval(1_.F,a);
theorem :: FIELD_8:47
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for x,y being Element of FAdj(F,{a})
for p,q being Polynomial of F st x = Ext_eval(p,a) & y = Ext_eval(q,a)
holds x + y = Ext_eval(p+q,a) & x * y = Ext_eval(p*'q,a);
theorem :: FIELD_8:48
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for x being Element of F holds x = Ext_eval(x|F,a);
theorem :: FIELD_8:49
for F being Field,
E being FieldExtension of F
for a being Element of E
holds hom_Ext_eval(a,F) is Function of (Polynom-Ring F),RAdj(F,{a});
theorem :: FIELD_8:50
for F being Field,
E being FieldExtension of F
for a being Element of E
holds hom_Ext_eval(a,F) is Function of (Polynom-Ring F),FAdj(F,{a});
theorem :: FIELD_8:51
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1, E2 being FieldExtension of F2
for a being F1-algebraic Element of E1, b being F2-algebraic Element of E2
for p being irreducible Element of the carrier of Polynom-Ring F1
st Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2
holds (PolyHom h).MinPoly(a,F1) = MinPoly(b,F2);
theorem :: FIELD_8:52
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1, E2 being FieldExtension of F2
for a being F1-algebraic Element of E1, b being F2-algebraic Element of E2
st Ext_eval((PolyHom h).MinPoly(a,F1),b) = 0.E2
holds (PolyHom h).MinPoly(a,F1) = MinPoly(b,F2);
theorem :: FIELD_8:53
for F1 being Field,
p1 being non constant Element of the carrier of Polynom-Ring F1
for F2 being FieldExtension of F1,
p2 being non constant Element of the carrier of Polynom-Ring F2
for E being SplittingField of p1
st p2 = p1 & E is F2-extending holds E is SplittingField of p2;
begin :: Uniqueness of Splitting Fields
definition
let F be Field,
E be FieldExtension of F;
let a,b be F-algebraic Element of E;
func Phi(a,b) -> Relation of the carrier of FAdj(F,{a}),
the carrier of FAdj(F,{b}) equals
:: FIELD_8:def 9
the set of all [Ext_eval(p,a),Ext_eval(p,b)] where p is Polynomial of F;
end;
registration
let F be Field,
E be FieldExtension of F;
let a,b be F-algebraic Element of E;
cluster Phi(a,b) -> quasi_total;
end;
theorem :: FIELD_8:54
for F being Field,
E being FieldExtension of F
for a,b being F-algebraic Element of E
holds Phi(a,b) is F-isomorphism iff MinPoly(a,F) = MinPoly(b,F);
definition
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let a be Element of E1, b be Element of E2;
let p be irreducible Element of the carrier of Polynom-Ring F1;
assume Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2;
func Psi(a,b,h,p) -> Function of FAdj(F1,{a}),FAdj(F2,{b}) means
:: FIELD_8:def 10
for r being Element of the carrier of Polynom-Ring F1
holds it.Ext_eval(r,a) = Ext_eval((PolyHom h).r,b);
end;
theorem :: FIELD_8:55
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1, E2 being FieldExtension of F2
for a being Element of E1, b being Element of E2
for p being irreducible Element of the carrier of Polynom-Ring F1
st Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2
holds Psi(a,b,h,p) is h-extending isomorphism;
theorem :: FIELD_8:56
for F being Field,
E being FieldExtension of F
for p being irreducible Element of the carrier of Polynom-Ring F
for a,b being Element of E
st a is_a_root_of p,E & b is_a_root_of p,E
holds FAdj(F,{a}),FAdj(F,{b}) are_isomorphic;
theorem :: FIELD_8:57
for F1 being Field,
F2 being F1-homomorphic F1-isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of Polynom-Ring F1
for E1 being SplittingField of p,
E2 being SplittingField of (PolyHom h).p
ex f being Function of E1,E2 st f is h-extending isomorphism;
theorem :: FIELD_8:58
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
for E1,E2 being SplittingField of p holds E1,E2 are_isomorphic_over F;