:: Renamings and a Condition-free Formalization of {K}ronecker's Construction :: by Christoph Schwarzweller :: :: Received May 19, 2020 :: Copyright (c) 2020-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, WAYBEL20, EC_PF_1, HURWITZ, RLVECT_1, FUNCT_1, RELAT_1, LATTICES, CARD_1, IDEAL_1, GROUP_6, GROUP_2, ZFMISC_1, XBOOLE_0, FINSET_1, NUMBERS, MSSUBFAM, POLYNOM5, GROUP_1, GROEB_2, MOD_4, YELLOW_8, RING_2, RING_3, RING_5, ALGNUM_1, ARYTM_1, FDIFF_1, CARD_2, NEWTON, WELLORD1, XXREAL_0, XCMPLX_0, EQREL_1, ORDINAL2, POLYNOM8, FUNCSDOM, FINSEQ_1, ALGSEQ_1, RATFUNC1, AFINSQ_1, GAUSSINT, ORDINAL1, INT_1, INT_3, BINOP_2, FUNCT_7, QUOFIELD, RING_4, RLSUB_1, RLVECT_5, FIELD_1, FIELD_2, FIELD_3, FIELD_4, FIELD_5, FOMODEL1; notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, RELSET_1, ORDINAL1, INT_2, ARYTM_3, REALSET1, FUNCT_1, FUNCT_2, ZFMISC_1, NUMBERS, FINSET_1, CARD_1, CARD_2, EQREL_1, XCMPLX_0, XXREAL_0, GR_CY_1, INT_3, ENUMSET1, NEWTON, POLYNOM3, POLYNOM4, POLYNOM5, RINGCAT1, STRUCT_0, GROUP_1, RATFUNC1, ALGSEQ_1, GROUP_6, MOD_4, ALGSTR_0, RLVECT_1, MATRLIN, IDEAL_1, VECTSP_2, VECTSP_9, HURWITZ, VECTSP_1, VECTSP_4, C0SP1, EC_PF_1, QUOFIELD, GAUSSINT, RING_1, RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_2, FIELD_3, FIELD_4; constructors ARYTM_3, TSEP_1, VFUNCT_1, RATFUNC1, GCD_1, REALSET1, RINGCAT1, ALGSEQ_1, GR_CY_1, VECTSP_9, ALGNUM_1, RING_5, POLYNOM4, CARD_2, NEWTON, FIELD_2, FIELD_3, FIELD_4; registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM4, VFUNCT_1, FUNCT_2, ALGSTR_0, POLYNOM3, GAUSSINT, SUBSET_1, RLVECT_1, FUNCT_1, CARD_1, CARD_2, FINSET_1, RATFUNC1, INT_3, RELAT_1, MOD_4, RINGCAT1, RING_1, RING_2, RING_3, RING_4, RING_5, NEWTON, REALSET1, POLYNOM5, MATRLIN, VECTSP_9, FIELD_1, FIELD_2, FIELD_3, FIELD_4, NAT_6; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: Preliminaries theorem :: FIELD_5:1 for X,Y being set st Y c= X holds (X \ Y) \/ Y = X; theorem :: FIELD_5:2 for n,m being Nat holds n +` m = n + m & n *` m = n * m; theorem :: FIELD_5:3 for n,m being Nat holds (n c= m iff n <= m) & (n in m iff n < m); theorem :: FIELD_5:4 for n being Nat holds exp(2,n) = 2|^n; theorem :: FIELD_5:5 for n being Nat st n >= 3 holds n + n < 2|^n; theorem :: FIELD_5:6 for n being Nat st n >= 3 holds n +` n in exp(2,n); theorem :: FIELD_5:7 NAT meets bool NAT; theorem :: FIELD_5:8 ::: isn't it just not X in X? for X being set ex o being object st not o in X; theorem :: FIELD_5:9 for X being set ex Y being set st card X c= card Y & X /\ Y = {}; theorem :: FIELD_5:10 for X,Y being set st card X c= card Y ex Z being set st Z c= Y & card Z = card X; theorem :: FIELD_5:11 for X being set ex Y being set st card X = card Y & X /\ Y = {}; theorem :: FIELD_5:12 for E being Field, F being Subfield of E holds F is Subring of E; theorem :: FIELD_5:13 for F being Field, R being Subring of F holds R is Subfield of F iff R is Field; registration let F be Field; let E be FieldExtension of F; cluster E-extending for FieldExtension of F; end; notation let F be Field; let E be FieldExtension of F; antonym E is F-infinite for E is F-finite; end; theorem :: FIELD_5:14 for F being Field, E being FieldExtension of F for K being E-extending FieldExtension of F holds VecSp(E,F) is Subspace of VecSp(K,F); theorem :: FIELD_5:15 for F being Field, E being FieldExtension of F for K being E-extending FieldExtension of F holds K is F-infinite or (E is F-finite & deg(E,F) <= deg(K,F)); theorem :: FIELD_5:16 for F being Field, p being Polynomial of F for q being non zero Polynomial of F holds deg(p mod q) < deg q; begin :: Linear Polynomials definition let R be Ring; let p be Polynomial of R; attr p is linear means :: FIELD_5:def 1 deg p = 1; end; registration let R be non degenerated Ring; cluster linear for Polynomial of R; cluster non linear for Polynomial of R; cluster linear for Element of the carrier of Polynom-Ring R; cluster non linear for Element of the carrier of Polynom-Ring R; end; registration let R be non degenerated Ring; cluster zero -> non linear for Polynomial of R; cluster constant -> non linear for Polynomial of R; end; registration let F be Field; cluster linear -> with_roots for Polynomial of F; end; registration let F be Field; cluster linear -> irreducible for Element of the carrier of Polynom-Ring F; end; registration let F be Field; cluster non linear with_roots -> reducible for Element of the carrier of Polynom-Ring F; end; registration let R be domRing; let p be linear Polynomial of R; let q be non constant Polynomial of R; cluster p *' q -> non linear; end; registration let F be Field; let p be linear Polynomial of F; let q be non constant Polynomial of F; cluster p *' q -> with_roots; end; begin definition let F be Field, p be non constant Element of the carrier of Polynom-Ring F; func canHomP p -> Function of F,Polynom-Ring(p) means :: FIELD_5:def 2 for a being Element of F holds it.a = a|F; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster canHomP p -> additive multiplicative unity-preserving one-to-one; end; registration let F be Field; let p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring p -> F-homomorphic F-monomorphic; end; registration let F be polynomial_disjoint Field; let p be irreducible Element of the carrier of Polynom-Ring F; cluster embField(canHomP p) -> add-associative right_complementable associative distributive almost_left_invertible; end; registration let F be polynomial_disjoint Field; let p be irreducible Element of the carrier of Polynom-Ring F; cluster embField(canHomP p) -> F-extending; end; definition let F be polynomial_disjoint Field; let p be irreducible Element of the carrier of Polynom-Ring F; func KrRootP p -> Element of embField(canHomP p) equals :: FIELD_5:def 3 ((emb_iso (canHomP p))" * (KroneckerIso p)").(KrRoot p); end; theorem :: FIELD_5:17 for F being polynomial_disjoint Field for p being irreducible Element of the carrier of Polynom-Ring F holds Ext_eval(p,KrRootP p) = 0.F; begin :: On Embedding F into F[X]/

and Polynom-Ring(F,p) theorem :: FIELD_5:18 for F being Field for p being linear Element of the carrier of Polynom-Ring F holds (Polynom-Ring p), F are_isomorphic & the carrier of embField(canHomP p) = the carrier of F; theorem :: FIELD_5:19 for F being strict Field for p being linear Element of the carrier of Polynom-Ring F holds embField(canHomP p) = F; theorem :: FIELD_5:20 for F being Field for p being linear Element of the carrier of Polynom-Ring F holds (Polynom-Ring F)/({p}-Ideal), F are_isomorphic & the carrier of embField(emb p) = the carrier of F; theorem :: FIELD_5:21 for F being strict Field for p being linear Element of the carrier of Polynom-Ring F holds embField(emb p) = F; theorem :: FIELD_5:22 for F being polynomial_disjoint Field, p being irreducible Element of the carrier of Polynom-Ring F holds embField(canHomP p) is polynomial_disjoint iff p is linear; theorem :: FIELD_5:23 for F being Field, p being irreducible Element of the carrier of Polynom-Ring F for E being polynomial_disjoint Field st E = embField(emb p) holds F is polynomial_disjoint; registration let n be Prime; let p be irreducible Element of the carrier of Polynom-Ring(Z/n); cluster embField(emb p) -> add-associative right_complementable associative distributive almost_left_invertible; end; registration let p be irreducible Element of the carrier of Polynom-Ring F_Rat; cluster embField(emb p) -> add-associative right_complementable associative distributive almost_left_invertible; end; theorem :: FIELD_5:24 for n being Prime, p being non constant Element of the carrier of Polynom-Ring(Z/n) holds Z/n, (Polynom-Ring Z/n)/({p}-Ideal) are_disjoint; theorem :: FIELD_5:25 for p being non constant Element of the carrier of Polynom-Ring F_Rat holds F_Rat, (Polynom-Ring F_Rat)/({p}-Ideal) are_disjoint; registration let n be Prime; let p be irreducible Element of the carrier of Polynom-Ring(Z/n); cluster embField(emb p) -> polynomial_disjoint; end; registration let p be irreducible Element of the carrier of Polynom-Ring F_Rat; cluster embField(emb p) -> polynomial_disjoint; end; definition let R be Ring; attr R is strong_polynomial_disjoint means :: FIELD_5:def 4 for a being Element of R for S being Ring, p being Element of the carrier of Polynom-Ring S holds a <> p; end; registration cluster INT.Ring -> strong_polynomial_disjoint; cluster F_Rat -> strong_polynomial_disjoint; cluster F_Real -> strong_polynomial_disjoint; end; registration let n be non trivial Nat; cluster Z/n -> strong_polynomial_disjoint; end; registration cluster strong_polynomial_disjoint -> polynomial_disjoint for Ring; end; registration cluster strong_polynomial_disjoint for Field; cluster non strong_polynomial_disjoint for Field; end; theorem :: FIELD_5:26 for F being strong_polynomial_disjoint Field, p being irreducible Element of the carrier of Polynom-Ring F for E being Field st E = embField(emb p) holds E is strong_polynomial_disjoint; begin :: Renamings definition let X be non empty set, Z be set; mode Renaming of X,Z -> Function means :: FIELD_5:def 5 dom it = X & it is one-to-one & (rng it) /\ (X \/ Z) = {}; end; registration let X be non empty set, Z be set; let r be Renaming of X,Z; cluster dom r -> non empty; cluster rng r -> non empty; end; registration let X be non empty set, Z be set; cluster -> X-defined one-to-one for Renaming of X,Z; end; definition let X be non empty set, Z be set; let r be Renaming of X,Z; redefine func r" -> Function of rng r, X; end; theorem :: FIELD_5:27 for X being non empty set, Z being set for r being Renaming of X,Z holds r" is onto; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; func ren_add r -> BinOp of rng r means :: FIELD_5:def 6 for a,b being Element of rng r holds it.(a,b) = r.((r").a + (r").b); end; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; func ren_mult r -> BinOp of (rng r) means :: FIELD_5:def 7 for a,b being Element of (rng r) holds it.(a,b) = r.((r").a * (r").b); end; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; func RenField r -> strict doubleLoopStr means :: FIELD_5:def 8 the carrier of it = rng r & the addF of it = ren_add r & the multF of it = ren_mult r & the OneF of it = r.(1.F) & the ZeroF of it = r.(0.F); end; registration let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; cluster RenField r -> non degenerated; end; registration let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; cluster RenField r -> Abelian add-associative right_zeroed right_complementable; end; registration let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; cluster RenField r -> commutative associative well-unital distributive almost_left_invertible; end; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; redefine func r" -> Function of (RenField r), F; end; theorem :: FIELD_5:28 for F being Field, Z being set for r being Renaming of (the carrier of F), Z holds r" is additive multiplicative unity-preserving one-to-one onto; theorem :: FIELD_5:29 for F being Field, Z being set ex E being Field st E,F are_isomorphic & (the carrier of E) /\ ((the carrier of F) \/ Z) = {}; begin theorem :: FIELD_5:30 :: Kronecker for F being 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; theorem :: FIELD_5:31 for F being Field for f being non constant Element of the carrier of Polynom-Ring F ex E being FieldExtension of F st f splits_in E;