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