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