:: Field Extensions and {K}ronecker's Construction
:: by Christoph Schwarzweller
::
:: Received August 29, 2019
:: Copyright (c) 2019-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, XCMPLX_0, VECTSP_2,
STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1, INT_1, ALGSEQ_1, FINSET_1,
MESFUNC1, INT_3, REALSET1, C0SP1, GAUSSINT, NAT_1, WAYBEL20, MOD_4,
POLYNOM1, POLYNOM2, POLYNOM3, POLYNOM8, COMPLFLD, FUNCSDOM, GROEB_2,
EC_PF_1, HURWITZ, FINSEQ_1, RING_4, GROUP_1, FUNCT_2, ARYTM_1, CARD_3,
FUNCT_1, RELAT_1, FUNCOP_1, CARD_1, IDEAL_1, QUOFIELD, FDIFF_1, EQREL_1,
XBOOLE_0, NUMBERS, POLYNOM5, RING_2, RING_3, GROUP_6, FUNCT_4, ZFMISC_1,
XXREAL_0, FUNCT_7, YELLOW_8, ALGNUM_1, MSSUBFAM, RING_5, ORDINAL1,
GROUP_2, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, FIELD_1, FIELD_2,
FIELD_3, FIELD_4, FOMODEL1;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, RELSET_1, REALSET1,
FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, NUMBERS, ZFMISC_1, FUNCT_7,
EQREL_1, ORDINAL1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, INT_1, INT_3,
GAUSSINT, VFUNCT_1, IDEAL_1, COMPLFLD, POLYNOM1, ALGSEQ_1, POLYNOM3,
POLYNOM4, POLYNOM5, FINSET_1, RINGCAT1, GROUP_1, GROUP_6, MOD_4,
RLVECT_1, ALGSTR_0, STRUCT_0, HURWITZ, MATRLIN, VECTSP_6, VECTSP_7,
VECTSP_9, VECTSP_2, VECTSP_1, C0SP1, EC_PF_1, RATFUNC1, QUOFIELD, RING_1,
RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_2, FIELD_3;
constructors REAL_1, FINSOP_1, BINARITH, VECTSP_2, POLYNOM3, ALGSTR_1,
MCART_1, NUMBERS, RING_1, ZFMISC_1, RELAT_1, XREAL_0, HURWITZ, VALUED_0,
STRUCT_0, C0SP1, GCD_1, COMPLFLD, FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0,
XXREAL_0, SUBSET_1, ORDINAL1, NAT_1, ALGSTR_0, POLYNOM4, XBOOLE_0,
RELSET_1, ARYTM_3, FUNCT_7, NAT_D, FINSEQ_1, VFUNCT_1, CARD_1, FINSET_1,
GAUSSINT, RATFUNC1, GROUP_6, REALSET1, UPROOTS, TSEP_1, ALGSTR_2, INT_3,
RINGCAT1, MEMBERED, IDEAL_1, RING_3, EC_PF_1, ALGSEQ_1, RING_2, VECTSP_9,
EQREL_1, RING_4, FUNCOP_1, GROUP_4, ALGNUM_1, MOD_4, RING_5, VECTSP_6,
FIELD_1, FIELD_2, FIELD_3;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
STRUCT_0, VECTSP_1, ALGSTR_1, VFUNCT_1, POLYNOM4, FUNCT_2, ALGSTR_0,
POLYNOM3, SUBSET_1, RLVECT_1, COMPLFLD, FUNCT_1, FINSET_1, INT_3,
RATFUNC1, GAUSSINT, RELAT_1, MOD_4, RING_2, RING_3, RING_4, RING_5,
REALSET1, FIELD_2, FIELD_3;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin :: Preliminaries
reserve K,F,E for Field,
R,S for Ring;
theorem :: FIELD_4:1
K is Subfield of K;
registration
let R be non degenerated Ring;
cluster -> non degenerated for Subring of R;
end;
registration
let R be comRing;
cluster -> commutative for Subring of R;
end;
registration
let R be domRing;
cluster -> domRing-like for Subring of R;
end;
theorem :: FIELD_4:2
for S being Subring of R, F being FinSequence of R, G being FinSequence of S
st F = G holds Sum F = Sum G;
begin :: Ring and Field Extensions
definition
let R,S be Ring;
attr S is R-extending means
:: FIELD_4:def 1
R is Subring of S;
end;
registration
let R be Ring;
cluster R-extending for Ring;
end;
registration
let R be comRing;
cluster R-extending for comRing;
end;
registration
let R be domRing;
cluster R-extending for domRing;
end;
registration
let F be Field;
cluster F-extending for Field;
end;
definition
let R be Ring;
mode RingExtension of R is R-extending Ring;
end;
definition
let R be comRing;
mode comRingExtension of R is R-extending comRing;
end;
definition
let R be domRing;
mode domRingExtension of R is R-extending domRing;
end;
definition
let F be Field;
mode FieldExtension of F is F-extending Field;
end;
theorem :: FIELD_4:3
R is RingExtension of R;
theorem :: FIELD_4:4
for R being comRing holds R is comRingExtension of R;
theorem :: FIELD_4:5
for R being domRing holds R is domRingExtension of R;
theorem :: FIELD_4:6
F is FieldExtension of F;
theorem :: FIELD_4:7
E is FieldExtension of F iff F is Subfield of E;
registration
cluster F_Complex -> (F_Real)-extending;
end;
registration
cluster F_Real -> (F_Rat)-extending;
end;
registration
cluster F_Rat -> (INT.Ring)-extending;
end;
registration
let R be Ring, S be RingExtension of R;
cluster -> R-extending for RingExtension of S;
end;
registration
let R be comRing, S be comRingExtension of R;
cluster -> R-extending for comRingExtension of S;
end;
registration
let R be domRing, S be domRingExtension of R;
cluster -> R-extending for domRingExtension of S;
end;
registration
let F be Field, E be FieldExtension of F;
cluster -> F-extending for FieldExtension of E;
end;
registration
let R be non degenerated Ring;
cluster -> non degenerated for RingExtension of R;
end;
begin :: Extensions of Polynomial Rings
theorem :: FIELD_4:8
for S being RingExtension of R, p being Polynomial of R holds
p is Polynomial of S;
theorem :: FIELD_4:9
for R being Subring of S, p being Polynomial of R holds
p is Polynomial of S;
theorem :: FIELD_4:10
for S being RingExtension of R holds
the carrier of Polynom-Ring R c= the carrier of Polynom-Ring S;
theorem :: FIELD_4:11
S is RingExtension of R implies 0.(Polynom-Ring S) = 0.(Polynom-Ring R);
theorem :: FIELD_4:12
S is RingExtension of R implies 0_.(S) = 0_.(R);
theorem :: FIELD_4:13
S is RingExtension of R implies 1.(Polynom-Ring S) = 1.(Polynom-Ring R);
theorem :: FIELD_4:14
for S being RingExtension of R holds 1_.(S) = 1_.(R);
theorem :: FIELD_4:15
for S being RingExtension of R, p,q being Polynomial of R
for p1,q1 being Polynomial of S st p = p1 & q = q1 holds p + q = p1 + q1;
theorem :: FIELD_4:16
for S being RingExtension of R holds
the addF of Polynom-Ring R
= (the addF of Polynom-Ring S)||the carrier of Polynom-Ring R;
theorem :: FIELD_4:17
for S being RingExtension of R
for p,q being Polynomial of R
for p1,q1 being Polynomial of S st p = p1 & q = q1 holds p *' q = p1 *' q1;
theorem :: FIELD_4:18
S is RingExtension of R implies the multF of Polynom-Ring R
= (the multF of Polynom-Ring S)||the carrier of Polynom-Ring R;
registration
let R be Ring;
let S be RingExtension of R;
cluster Polynom-Ring S -> (Polynom-Ring R)-extending;
end;
theorem :: FIELD_4:19
for R being Ring, S being RingExtension of R
holds Polynom-Ring S is RingExtension of Polynom-Ring R;
theorem :: FIELD_4:20
for S being RingExtension of R,
p being Element of the carrier of Polynom-Ring R,
q being Element of the carrier of Polynom-Ring S st p = q
holds deg p = deg q;
theorem :: FIELD_4:21
for R being non degenerated Ring, S being RingExtension of R,
a being Element of R, b being Element of S st a = b
holds rpoly(1,a) = rpoly(1,b);
begin :: Evaluation of Polynomials in Ring Extensions
theorem :: FIELD_4:22
for a be Element of S holds
S is RingExtension of R implies Ext_eval(0_.(R),a) = 0.S;
theorem :: FIELD_4:23
for R being non degenerated Ring, S being RingExtension of R,
a being Element of S holds Ext_eval(1_.(R),a) = 1.S;
theorem :: FIELD_4:24
for S being RingExtension of R,a being Element of S,
p,q being Polynomial of R holds
Ext_eval(p+q,a) = Ext_eval(p,a) + Ext_eval(q,a);
theorem :: FIELD_4:25
for R being comRing, S being comRingExtension of R, a being Element of S,
p,q being Polynomial of R holds
Ext_eval(p*'q,a) = Ext_eval(p,a) * Ext_eval(q,a);
theorem :: FIELD_4:26
for S being RingExtension of R,
p being Element of the carrier of (Polynom-Ring R),
q being Element of the carrier of Polynom-Ring S,
a being Element of S st p = q holds Ext_eval(p,a) = eval(q,a);
theorem :: FIELD_4:27
for S being RingExtension of R,
p being Element of the carrier of (Polynom-Ring R),
q being Element of the carrier of Polynom-Ring S,
a being Element of R, b being Element of S st q = p & b = a
holds eval(q,b) = eval(p,a);
definition
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
let a be Element of S;
pred a is_a_root_of p,S means
:: FIELD_4:def 2
Ext_eval(p,a) = 0.S;
end;
definition
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
pred p is_with_roots_in S means
:: FIELD_4:def 3
ex a being Element of S st a is_a_root_of p,S;
end;
definition
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
func Roots(S,p) -> Subset of S equals
:: FIELD_4:def 4
{a where a is Element of S : a is_a_root_of p,S};
end;
theorem :: FIELD_4:28
for S being RingExtension of R,
p being Element of the carrier of Polynom-Ring R
holds Roots p c= Roots(S,p);
::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
definition
let R be Ring, S be non degenerated Ring;
let p be Polynomial of R;
pred p splits_in S means
:: FIELD_4:def 5
ex a being non zero Element of S, q being Ppoly of S st p = a * q;
end;
::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
theorem :: FIELD_4:29
for F being Field, p be Polynomial of F st deg p = 1 holds p splits_in F;
begin :: Degree of Extension
definition
let R be Ring, S be RingExtension of R;
func VecSp(S,R) -> strict ModuleStr over R means
:: FIELD_4:def 6
the carrier of it = the carrier of S &
the addF of it = the addF of S &
the ZeroF of it = 0.S &
the lmult of it = (the multF of S)|[:the carrier of R,the carrier of S:];
end;
registration
let R be Ring, S be RingExtension of R;
cluster VecSp(S,R) -> non empty;
end;
registration
let R be Ring, S be RingExtension of R;
cluster VecSp(S,R) ->
Abelian add-associative right_zeroed right_complementable;
end;
registration
let R be Ring, S be RingExtension of R;
cluster VecSp(S,R) ->
scalar-distributive scalar-associative scalar-unital vector-distributive;
end;
theorem :: FIELD_4:30
for S being RingExtension of R holds VecSp(S,R) is VectSp of R;
definition
let F be Field, E be FieldExtension of F;
func deg(E,F) -> Integer equals
:: FIELD_4:def 7
dim VecSp(E,F) if VecSp(E,F) is finite-dimensional
otherwise -1;
end;
registration
let F be Field, E be FieldExtension of F;
cluster deg(E,F) -> dim-like;
end;
definition
let F be Field, E be FieldExtension of F;
attr E is F-finite means
:: FIELD_4:def 8
VecSp(E,F) is finite-dimensional;
end;
registration
let F be Field;
cluster F-finite for FieldExtension of F;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
cluster deg(E,F) -> natural;
end;
begin :: Kronecker's Theorem
registration
let F be Field, p be non constant Element of the carrier of Polynom-Ring F;
cluster the carrier of (Polynom-Ring p) -> F-polynomial-membered;
cluster Polynom-Ring p -> F-polynomial-membered;
end;
definition
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
func KroneckerIso p ->
Function of the carrier of Polynom-Ring p,the carrier of KroneckerField(F,p)
means
:: FIELD_4:def 9
for q being Element of the carrier of Polynom-Ring p
holds it.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q);
end;
registration
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
cluster KroneckerIso p ->
additive multiplicative unity-preserving one-to-one onto;
end;
registration
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
cluster KroneckerField(F,p) -> (Polynom-Ring p)-homomorphic
(Polynom-Ring p)-monomorphic
(Polynom-Ring p)-isomorphic;
cluster Polynom-Ring p -> (KroneckerField(F,p))-homomorphic
(KroneckerField(F,p))-monomorphic
(KroneckerField(F,p))-isomorphic;
cluster Polynom-Ring p -> F-homomorphic F-monomorphic;
end;
theorem :: FIELD_4:31 :: Kronecker
for F being polynomial_disjoint Field
for f being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st f is_with_roots_in E;