:: Algebraic Extensions :: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller :: :: Received March 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, VECTSP_2, STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1, NAT_1, MESFUNC1, REALSET1, C0SP1, FUNCT_2, POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, RLVECT_5, CARD_1, HURWITZ, RLVECT_1, RLVECT_2, FINSEQ_1, FUNCT_1, RELAT_1, LATTICES, EC_PF_1, RANKNULL, XBOOLE_0, FINSET_1, NUMBERS, POLYNOM5, GROUP_1, ZFMISC_1, FUNCT_7, AFINSQ_1, MSSUBFAM, GROUP_6, PBOOLE, ALGNUM_1, ARYTM_1, RLVECT_3, MOD_4, RING_2, RING_3, FIELD_4, NEWTON, XXREAL_0, CARD_3, XCMPLX_0, QC_LANG1, FOMODEL1, FIELD_1, RLSUB_1, FIELD_6, GLIB_000, FIELD_7; notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, REALSET1, FUNCT_1, RELSET_1, FUNCT_2, PARTFUN1, FINSEQ_1, MEMBERED, ZFMISC_1, ORDINAL1, NUMBERS, FINSET_1, CARD_1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, INT_1, STRUCT_0, VFUNCT_1, POLYNOM1, POLYNOM3, POLYNOM4, POLYNOM5, GROUP_1, GROUP_4, GROUP_6, MOD_4, VECTSP_4, VECTSP_6, VECTSP_7, BINOM, ALGSTR_0, ALGSTR_1, RLVECT_1, VECTSP_2, VECTSP_9, RANKNULL, MATRLIN, HURWITZ, VECTSP_1, ALGSEQ_1, C0SP1, EC_PF_1, RATFUNC1, RING_2, RING_3, RING_4, ALGNUM_1, FIELD_1, FIELD_4, FIELD_6; constructors XREAL_0, HURWITZ, VECTSP_1, STRUCT_0, C0SP1, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, SUBSET_1, ORDINAL1, NAT_1, ALGSTR_0, NORMSP_1, INT_1, POLYNOM4, XBOOLE_0, RELSET_1, ARYTM_3, QUOFIELD, PARTFUN1, RLVECT_1, NAT_D, FUNCT_7, VFUNCT_1, CARD_1, FINSET_1, POLYNOM1, RATFUNC1, GCD_1, POLYNOM5, REALSET1, MEMBERED, BINOM, POLYDIFF, EC_PF_1, ALGSEQ_1, VECTSP_9, RLVECT_5, RING_2, RINGCAT1, FUNCOP_1, GROUP_4, ALGNUM_1, VECTSP_6, VECTSP_7, GROUP_6, RANKNULL, FIELD_1, FIELD_4, FIELD_5, FIELD_6; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XXREAL_0, XREAL_0, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, NUMBERS, EC_PF_1, POLYNOM4, FUNCT_2, ALGSTR_0, POLYNOM3, SUBSET_1, GROUP_1, MOD_4, RLVECT_1, FINSET_1, FUNCT_1, CARD_1, C0SP1, RATFUNC1, RELAT_1, RINGCAT1, RING_2, RING_4, NAT_1, UPROOTS, REALSET1, PRE_POLY, POLYNOM1, POLYNOM5, FIELD_4, FIELD_6; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: Preliminaries definition let L1,L2 be doubleLoopStr; pred L1 == L2 means :: FIELD_7:def 1 the doubleLoopStr of L1 = the doubleLoopStr of L2; reflexivity; symmetry; end; theorem :: FIELD_7:1 for R,S being Ring holds R == S iff ex f being Function of R,S st f = id R & f is isomorphism; theorem :: FIELD_7:2 for R,S being strict Ring holds R == S iff R = S; definition let F1,F2 be Field; redefine pred F1 == F2 means :: FIELD_7:def 2 F1 is Subfield of F2 & F2 is Subfield of F1; end; theorem :: FIELD_7:3 for F being Field for E being FieldExtension of F for T being Subset of E holds FAdj(F,T) == F iff T is Subset of F; theorem :: FIELD_7:4 for F being Field for E1,E2 being FieldExtension of F st E1 == E2 holds VecSp(E1,F) = VecSp(E2,F); theorem :: FIELD_7:5 for F being Field for E1,E2 being FieldExtension of F st E1 == E2 holds deg(E1,F) = deg(E2,F); registration let F be Field, E be FieldExtension of F; cluster E-homomorphic for FieldExtension of F; cluster E-monomorphic for FieldExtension of F; cluster E-isomorphic for FieldExtension of F; end; definition let R be Ring; let a,b be Element of R; redefine func {a,b} -> Subset of R; end; definition let F be Field; let V be VectSp of F; let a be Element of V; redefine func {a} -> Subset of V; end; definition let F be Field; let V be VectSp of F; let a,b be Element of V; redefine func {a,b} -> Subset of V; end; registration let F be Field; let V be VectSp of F; cluster -> linearly-independent for Basis of V; end; theorem :: FIELD_7:6 for F being Field, V being VectSp of F for X being Subset of V holds X is linearly-independent iff for l1,l2 being Linear_Combination of X st Sum l1 = Sum l2 holds l1 = l2; registration let F be Field; let E be FieldExtension of F; cluster -> non empty for Basis of VecSp(E,F); end; registration let F be Field; let E be FieldExtension of F; cluster deg(E,F) -> non zero; end; registration let F be Field; let E be F-finite FieldExtension of F; cluster -> finite for Basis of VecSp(E,F); end; theorem :: FIELD_7:7 for F being Field for E being FieldExtension of F holds deg(E,F) = 1 iff the carrier of E = the carrier of F; theorem :: FIELD_7:8 for F being Field for E being FieldExtension of F holds deg(E,F) = 1 iff E == F; theorem :: FIELD_7:9 for F being Field for E being FieldExtension of F holds deg(E,F) = 1 iff {1.E} is Basis of VecSp(E,F); registration let F be Field, E be FieldExtension of F; cluster non empty finite linearly-independent for Subset of VecSp(E,F); end; theorem :: FIELD_7:10 for F being Field, E being FieldExtension of F for T1,T2 being Subset of E st T1 c= T2 holds FAdj(F,T1) is Subfield of FAdj(F,T2); definition let F be Field; let p be Polynomial of F; func Coeff p -> Subset of F equals :: FIELD_7:def 3 { p.i where i is Element of NAT : p.i <> 0.F }; end; registration let F be Field; let p be Polynomial of F; cluster Coeff p -> finite; end; theorem :: FIELD_7:11 for F being Field for E being FieldExtension of F for p being Polynomial of E st Coeff p c= the carrier of F holds p is Polynomial of F; theorem :: FIELD_7:12 for F being Field for E being FieldExtension of F for p being non zero Polynomial of E st Coeff p c= the carrier of F holds p is non zero Polynomial of F; theorem :: FIELD_7:13 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 holds Roots(S,p) = Roots(q); registration let R be domRing; let p be non zero Element of the carrier of Polynom-Ring R; cluster Roots p -> finite; end; registration let R be domRing, S be domRingExtension of R; let p be non zero Element of the carrier of Polynom-Ring R; cluster Roots(S,p) -> finite; end; registration let F be Field; let E be FieldExtension of F; cluster F-extending for FieldExtension of E; end; registration let F be Field, E be F-finite FieldExtension of F; cluster F-finite for F-extending FieldExtension of E; end; registration let F be Field; let E be F-finite FieldExtension of F; cluster E-finite for F-extending FieldExtension of E; end; theorem :: FIELD_7:14 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 for a being Element of E, b being Element of U st a = b holds Ext_eval(p,a) = Ext_eval(p,b); theorem :: FIELD_7:15 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 q = p for U being E-extending FieldExtension of F for a being Element of U holds Ext_eval(q,a) = Ext_eval(p,a); definition let R be Ring, S be RingExtension of R; let a be Element of R; func @(a,S) -> Element of S equals :: FIELD_7:def 4 a; end; definition let R be Ring, S be RingExtension of R; let a be Element of S; attr a is R-membered means :: FIELD_7:def 5 a in the carrier of R; end; registration let R be Ring, S be RingExtension of R; cluster R-membered for Element of S; end; definition let R be Ring, S be RingExtension of R; let a be Element of S; assume a is R-membered; func @(R,a) -> Element of R equals :: FIELD_7:def 6 a; end; registration let R be Ring, S be RingExtension of R; let a be R-membered Element of S; reduce @(R,a) to a; end; registration let F be Field, E be FieldExtension of F; cluster non zero F-algebraic for Element of E; end; registration let F be Field, E be FieldExtension of F; let a be Element of F; cluster @(a,E) -> F-algebraic; end; registration let F be Field, E be FieldExtension of F; let K be E-extending FieldExtension of F; let a be F-algebraic Element of E; cluster @(a,K) -> F-algebraic; end; begin :: More on Finite Extensions theorem :: FIELD_7:16 for F being Field, E being FieldExtension of F, K being E-extending FieldExtension of F for l being Linear_Combination of VecSp(K,F) holds l is Linear_Combination of VecSp(K,E); theorem :: FIELD_7:17 for F being Field, E being FieldExtension of F, K being E-extending FieldExtension of F for BE being Subset of VecSp(K,E), BF being Subset of VecSp(K,F) st BF c= BE for l being Linear_Combination of BF holds l is Linear_Combination of BE; theorem :: FIELD_7:18 for F being Field, E being FieldExtension of F, K being E-extending FieldExtension of F for BE being finite Subset of VecSp(K,E), BF being finite Subset of VecSp(K,F) for l1 being Linear_Combination of BF, l2 being Linear_Combination of BE st l1 = l2 & BF c= BE holds Sum l1 = Sum l2; definition let F be Field, E be FieldExtension of F, K be F-extending FieldExtension of E; :: without attribute F-extending Mizar gives an error! let BE be Subset of VecSp(E,F), BK be Subset of VecSp(K,E); func Base(BE,BK) -> Subset of VecSp(K qua FieldExtension of F,F) equals :: FIELD_7:def 7 { a * b where a,b is Element of K : a in BE & b in BK }; end; registration let F be Field, E be FieldExtension of F, K be F-extending FieldExtension of E; let BE be non empty Subset of VecSp(E,F), BK be non empty Subset of VecSp(K,E); cluster Base(BE,BK) -> non empty; end; theorem :: FIELD_7:19 for F being Field, E being FieldExtension of F, K being F-extending FieldExtension of E for BE being linearly-independent Subset of VecSp(E,F), BK being linearly-independent Subset of VecSp(K,E) for a1,a2,b1,b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK holds a1 * b1 = a2 * b2 implies (a1 = a2 & b1 = b2); theorem :: FIELD_7:20 for F being Field, E being FieldExtension of F, K being F-extending FieldExtension of E for BE being non empty linearly-independent Subset of VecSp(E,F), BK being non empty linearly-independent Subset of VecSp(K,E) holds card Base(BE,BK) = card [:BE,BK:]; theorem :: FIELD_7:21 for F being Field, E being FieldExtension of F, K being F-extending FieldExtension of E for BE being non empty finite linearly-independent Subset of VecSp(E,F), BK being non empty finite linearly-independent Subset of VecSp(K,E) holds card Base(BE,BK) = card BE * card BK; registration let F be Field, E be FieldExtension of F, K be F-extending FieldExtension of E; let BE be non empty finite linearly-independent Subset of VecSp(E,F), BK be non empty finite linearly-independent Subset of VecSp(K,E); cluster Base(BE,BK) -> finite; end; definition let F be Field, E be FieldExtension of F, K be F-extending FieldExtension of E; let BE be non empty finite linearly-independent Subset of VecSp(E,F), BK be non empty linearly-independent Subset of VecSp(K,E); let l be Linear_Combination of Base(BE,BK); let b be Element of K; func down(l,b) -> Linear_Combination of BE means :: FIELD_7:def 8 (for a being Element of K st a in BE & b in BK holds it.a = l.(a*b)) & (for a being Element of E st not a in BE or not b in BK holds it.a = 0.F); end; definition let F be Field, E be FieldExtension of F, K be F-extending FieldExtension of E; let BE be non empty finite linearly-independent Subset of VecSp(E,F), BK be non empty finite linearly-independent Subset of VecSp(K,E); let l be Linear_Combination of Base(BE,BK); func down l -> Linear_Combination of BK means :: FIELD_7:def 9 for b being Element of K st b in BK holds it.b = Sum down(l,b); end; definition let F be Field, E be F-finite FieldExtension of F, K be F-extending FieldExtension of E; let BE be Basis of VecSp(E,F), BK be non empty finite linearly-independent Subset of VecSp(K,E); let l1 be Linear_Combination of BK; func lift(l1,BE) -> Linear_Combination of Base(BE,BK) means :: FIELD_7:def 10 for b being Element of K st b in BK ex l2 being Linear_Combination of BE st Sum l2 = l1.b & for a being Element of K st a in BE & a * b in Base(BE,BK) holds it.(a*b) = l2.a; end; theorem :: FIELD_7:22 for F being Field, E being F-finite FieldExtension of F, K being E-finite F-extending FieldExtension of E for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E) for l being Linear_Combination of Base(BE,BK) holds lift(down l,BE) = l; theorem :: FIELD_7:23 for F being Field, E being F-finite FieldExtension of F, K being E-finite F-extending FieldExtension of E for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E) for l being Linear_Combination of BK holds down lift(l,BE) = l; theorem :: FIELD_7:24 for F being Field, E being FieldExtension of F, K being F-extending FieldExtension of E for BE being non empty finite linearly-independent Subset of VecSp(E,F), BK being non empty finite linearly-independent Subset of VecSp(K,E) for l,l1,l2 being Linear_Combination of Base(BE,BK) st l = l1 + l2 for b being Element of K holds down(l,b) = down(l1,b) + down(l2,b); theorem :: FIELD_7:25 for F being Field, E being FieldExtension of F, K being F-extending FieldExtension of E for BE being non empty finite linearly-independent Subset of VecSp(E,F), BK being non empty finite linearly-independent Subset of VecSp(K,E) for l,l1,l2 being Linear_Combination of Base(BE,BK) st l = l1 + l2 holds down l = down l1 + down l2; theorem :: FIELD_7:26 for F being Field, E being F-finite FieldExtension of F, K being E-finite F-extending FieldExtension of E for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E) for l being Linear_Combination of Base(BE,BK) holds Sum l = Sum(down l); theorem :: FIELD_7:27 for F being Field, E being F-finite FieldExtension of F, K being E-finite F-extending FieldExtension of E for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E) for l being Linear_Combination of Base(BE,BK) st Sum(l) = 0.VecSp(K qua FieldExtension of F,F) holds Carrier(l) = {}; theorem :: FIELD_7:28 for F being Field, E being F-finite FieldExtension of F, K being E-finite F-extending FieldExtension of E for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E) holds Lin Base(BE,BK) = the ModuleStr of VecSp(K qua FieldExtension of F,F); theorem :: FIELD_7:29 for F being Field, E being F-finite FieldExtension of F, K being E-finite F-extending FieldExtension of E for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E) holds Base(BE,BK) is Basis of VecSp(K qua FieldExtension of F,F); theorem :: FIELD_7:30 for F being Field, E being F-finite FieldExtension of F, K being E-finite F-extending FieldExtension of E holds deg(K,F) = deg(K,E) * deg(E,F); theorem :: FIELD_7:31 for F being Field, E being FieldExtension of F, K being E-extending FieldExtension of F st K is F-finite holds E is F-finite & deg(E,F) <= deg(K,F) & K is E-finite & deg(K,E) <= deg(K,F); registration let F be Field; let E be F-finite FieldExtension of F; cluster -> F-finite for E-finite F-extending FieldExtension of E; end; begin :: Algebraic Extensions definition let F be Field, E be FieldExtension of F; attr E is F-algebraic means :: FIELD_7:def 11 for a being Element of E holds a is F-algebraic; end; registration let F be Field; cluster F-finite -> F-algebraic for FieldExtension of F; end; registration let F be Field; let E be F-algebraic FieldExtension of F; cluster -> F-algebraic for Element of E; end; theorem :: FIELD_7:32 for F being Field for E being FieldExtension of F holds E is F-algebraic iff for a being Element of E holds FAdj(F,{a}) is F-finite; theorem :: FIELD_7:33 for F being Field, E being FieldExtension of F for a being Element of E holds a is F-algebraic iff ex B being F-finite FieldExtension of F st E is B-extending & a in B; definition let F be Field; let E be FieldExtension of F; let T be Subset of E; attr T is F-algebraic means :: FIELD_7:def 12 for a being Element of E st a in T holds a is F-algebraic; end; registration let F be Field; let E be FieldExtension of F; cluster finite F-algebraic for Subset of E; end; theorem :: FIELD_7:34 for F being Field, E being FieldExtension of F for b being Element of E, T being Subset of E for E1 being FieldExtension of FAdj(F,T), b1 being Element of E1 st E1 = E & b1 = b holds FAdj(F,{b}\/T) = FAdj(FAdj(F,T),{b1}); theorem :: FIELD_7:35 for F being Field, E being FieldExtension of F for b being Element of E, T being Subset of E for E1 being FieldExtension of FAdj(F,{b}), T1 being Subset of E1 st E1 = E & T1 = T holds FAdj(F,{b}\/T) = FAdj(FAdj(F,{b}),T1); registration let F be Field; let E be FieldExtension of F; let T be finite F-algebraic Subset of E; cluster FAdj(F,T) -> F-finite; end; theorem :: FIELD_7:36 for F being Field, E being FieldExtension of F for a being F-algebraic Element of E holds E == FAdj(F,{a}) iff deg MinPoly(a,F) = deg(E,F); theorem :: FIELD_7:37 for F being Field, E being FieldExtension of F holds E is F-finite iff ex T being finite F-algebraic Subset of E st E == FAdj(F,T); registration let F be Field; let E be FieldExtension of F; let p be non zero Element of the carrier of Polynom-Ring F; cluster Roots(E,p) -> F-algebraic; end; theorem :: FIELD_7:38 for F being Field, E being FieldExtension of F for p being non zero Element of the carrier of Polynom-Ring F holds FAdj(F,Roots(E,p)) is F-algebraic; theorem :: FIELD_7:39 for F being Field for E being FieldExtension of F for K being E-extending FieldExtension of F st K is E-algebraic & E is F-algebraic holds K is F-algebraic; theorem :: FIELD_7:40 for F being Field for E being FieldExtension of F for K being E-extending FieldExtension of F st K is F-algebraic holds K is E-algebraic & E is F-algebraic; begin :: The Field of Algebraic Elements registration let F be Field; let E be FieldExtension of F; let a,b be F-algebraic Element of E; cluster FAdj(F,{a,b}) -> F-finite; end; registration let F be Field, E be FieldExtension of F; cluster 0.E -> F-algebraic; cluster 1.E -> F-algebraic; end; registration let F be Field, E be FieldExtension of F; let a,b be F-algebraic Element of E; cluster a + b -> F-algebraic; cluster a - b -> F-algebraic; cluster a * b -> F-algebraic; end; registration let F be Field, E be FieldExtension of F; let a be F-algebraic Element of E; cluster -a -> F-algebraic; end; registration let F be Field, E be FieldExtension of F; let a be non zero F-algebraic Element of E; cluster a" -> F-algebraic; end; definition let F be Field, E be FieldExtension of F; func Alg_El E -> Subset of E equals :: FIELD_7:def 13 the set of all a where a is F-algebraic Element of E; end; definition let F be Field, E be FieldExtension of F; func Field_of_Algebraic_Elements E -> strict doubleLoopStr means :: FIELD_7:def 14 the carrier of it = Alg_El E & the addF of it = (the addF of E)||the carrier of it & the multF of it = (the multF of E)||the carrier of it & the OneF of it = 1.E & the ZeroF of it = 0.E; end; notation let F be Field, E be FieldExtension of F; synonym F_Alg E for Field_of_Algebraic_Elements E; end; registration let F be Field, E be FieldExtension of F; cluster F_Alg E -> non degenerated; end; registration let F be Field, E be FieldExtension of F; cluster F_Alg E -> Abelian add-associative right_zeroed right_complementable; end; registration let F be Field, E be FieldExtension of F; cluster F_Alg E-> commutative associative well-unital distributive almost_left_invertible; end; registration let F be Field, E be FieldExtension of F; cluster F_Alg E -> F-extending; end; registration let F be Field, E be FieldExtension of F; cluster F_Alg E -> F-algebraic; end; theorem :: FIELD_7:41 for F being Field for E being FieldExtension of F holds F_Alg E is FieldExtension of F; theorem :: FIELD_7:42 for F being Field for E being FieldExtension of F holds E is FieldExtension of F_Alg E; theorem :: FIELD_7:43 for F being Field for E being FieldExtension of F for K being FieldExtension of E holds F_Alg K is FieldExtension of F_Alg E; theorem :: FIELD_7:44 for F being Field for E being F-algebraic FieldExtension of F holds F_Alg E == E;