:: On the Intersection of Fields $F$ with $F[X]$
:: 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 VECTSP_1, ALGSTR_0, STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1,
CARD_1, MESFUNC1, POLYNOM1, FUNCSDOM, HURWITZ, RLVECT_1, FINSEQ_1,
FUNCT_1, RELAT_1, XBOOLE_0, NUMBERS, AFINSQ_1, ARYTM_1, IDEAL_1, RAT_1,
ARYTM_3, GROUP_2, XXREAL_0, QUOFIELD, ZFMISC_1, PARTFUN1, TARSKI,
EQREL_1, BINOP_2, INT_3, MOD_4, MCART_1, RING_3, WELLORD1, GROUP_1,
NAT_1, INT_1, FDIFF_1, ORDINAL1, FUNCT_2, MSSUBFAM, FUNCT_7, XCMPLX_0,
FINSET_1, ALGSEQ_1, POLYNOM3, REAL_1, LATTICES, PREFER_1, CLASSES1,
GAUSSINT, WAYBEL20, ARYTM_2, FIELD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, CLASSES1,
RELSET_1, FUNCT_1, FUNCT_2, NUMBERS, PARTFUN1, XTUPLE_0, RAT_1, XCMPLX_0,
XXREAL_0, XREAL_0, ARYTM_2, ARYTM_3, BINOP_1, STRUCT_0, NAT_1, INT_1,
GR_CY_1, INT_3, GAUSSINT, POLYNOM3, POLYNOM5, ALGSEQ_1, GROUP_1, GROUP_6,
ALGSTR_0, IDEAL_1, EQREL_1, RLVECT_1, HURWITZ, VECTSP_1, RINGCAT1, MOD_4,
RING_1, RING_3, RING_4;
constructors HURWITZ, XBOOLE_0, RELSET_1, ARYTM_3, ABIAN, QUOFIELD, PARTFUN1,
RLVECT_1, FUNCT_7, FINSET_1, GAUSSINT, ALGSEQ_1, RATFUNC1, GROUP_6,
RAT_1, BINOP_2, CLASSES1, REALSET1, ALGSTR_2, INT_3, RINGCAT1, MEMBERED,
MOD_4, GR_CY_1, NAT_D, IDEAL_1, EQREL_1, ARYTM_2, RLVECT_5, RING_1,
RING_3, RING_4, GROUP_4, CARD_2, POLYNOM1, ORDINAL2, INT_1, POLYNOM5;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, CARD_2, NAT_1, INT_1,
MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, FUNCT_2, XREAL_0, ALGSTR_0,
RING_1, RLVECT_1, PARTFUN1, RATFUNC1, XTUPLE_0, FINSET_1, GAUSSINT,
POLYNOM4, INT_3, CARD_1, RING_2, RING_3, RING_4, RING_5, POLYNOM1,
POLYNOM3, RINGCAT1, SUBSET_1, POLYNOM5;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin
theorem :: FIELD_3:1
for n being Nat, x being object st n = {x} holds x = 0;
theorem :: FIELD_3:2
for n being Nat, x,y being object st n = {x,y} & x <> y
holds (x = 0 & y = 1) or (x = 1 & y = 0);
theorem :: FIELD_3:3
for n being Nat st 1 < n holds 0.(Z/n) = 0;
theorem :: FIELD_3:4
1.(Z/2) + 1.(Z/2) = 0.(Z/2);
theorem :: FIELD_3:5
for R being Ring, n being non zero Nat holds power(R).(0.R,n) = 0.R;
registration
cluster Z/3 -> non degenerated almost_left_invertible;
end;
registration
cluster finite for Field;
cluster infinite for Field;
end;
definition
let L be non empty doubleLoopStr;
attr L is almost_trivial means
:: FIELD_3:def 1
for a being Element of L holds a = 1.L or a = 0.L;
end;
registration
cluster degenerated -> almost_trivial for Ring;
cluster non almost_trivial for Field;
end;
theorem :: FIELD_3:6
for R being Ring holds
R is almost_trivial iff (R is degenerated or R,Z/2 are_isomorphic);
definition
let R be Ring;
let a be Element of R;
attr a is trivial means
:: FIELD_3:def 2
a = 1.R or a = 0.R;
end;
registration
let R be non almost_trivial Ring;
cluster non trivial for Element of R;
end;
definition
let R be Ring;
attr R is polynomial_disjoint means
:: FIELD_3:def 3
[#]R /\ [#]Polynom-Ring R = {};
end;
begin :: Some Negative Results
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
func carr(x,o) -> non empty set equals
:: FIELD_3:def 4
([#]R \ {x}) \/ {o};
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
let a,b be Element of carr(x,o);
func addR(a,b) -> Element of carr(x,o) equals
:: FIELD_3:def 5
(the addF of R).(x,x) if a = o & b = o & (the addF of R).(x,x) <> x,
(the addF of R).(a,x) if a <> o & b = o & (the addF of R).(a,x) <> x,
(the addF of R).(x,b) if a = o & b <> o & (the addF of R).(x,b) <> x,
(the addF of R).(a,b) if a <> o & b <> o & (the addF of R).(a,b) <> x
otherwise o;
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
func addR(x,o) -> BinOp of carr(x,o) means
:: FIELD_3:def 6
for a,b being Element of carr(x,o) holds it.(a,b) = addR(a,b);
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
let a,b be Element of carr(x,o);
func multR(a,b) -> Element of carr(x,o) equals
:: FIELD_3:def 7
(the multF of R).(x,x) if a = o & b = o & (the multF of R).(x,x) <> x,
(the multF of R).(a,x) if a <> o & b = o & (the multF of R).(a,x) <> x,
(the multF of R).(x,b) if a = o & b <> o & (the multF of R).(x,b) <> x,
(the multF of R).(a,b) if a <> o & b <> o & (the multF of R).(a,b) <> x
otherwise o;
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
func multR(x,o) -> BinOp of carr(x,o) means
:: FIELD_3:def 8
for a,b being Element of carr(x,o) holds it.(a,b) = multR(a,b);
end;
definition
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
func ExField(x,o) -> strict doubleLoopStr means
:: FIELD_3:def 9
the carrier of it = carr(x,o) &
the addF of it = addR(x,o) &
the multF of it = multR(x,o) &
the OneF of it = 1.F &
the ZeroF of it = 0.F;
end;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster ExField(x,o) -> non degenerated;
end;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster ExField(x,o) -> Abelian;
end;
reserve o for object;
reserve F for non almost_trivial Field;
reserve x,a for Element of F;
theorem :: FIELD_3:7
for x being non trivial Element of F, o being object st
not o in [#]F holds ExField(x,o) is right_zeroed right_complementable;
theorem :: FIELD_3:8
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is add-associative;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster ExField(x,o) -> commutative;
end;
theorem :: FIELD_3:9
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is well-unital;
theorem :: FIELD_3:10
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is associative;
theorem :: FIELD_3:11
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is distributive;
theorem :: FIELD_3:12
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is almost_left_invertible;
theorem :: FIELD_3:13
for x being non trivial Element of F, P being Ring
st P = ExField(x,<%0.F,1.F%>) holds <%0.F,1.F%> in [#]P /\ [#]Polynom-Ring P;
theorem :: FIELD_3:14
ex K being Field st [#]K /\ [#]Polynom-Ring K <> {};
reserve n for non zero Nat;
theorem :: FIELD_3:15
ex K being Field, p being Polynomial of K
st deg p = n & p in [#]K /\ [#]Polynom-Ring K;
theorem :: FIELD_3:16
ex K being Field, x being object st not x in rng(canHom K) &
x in [#]K /\ [#]Polynom-Ring K;
registration
cluster non polynomial_disjoint for Field;
end;
definition
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
func isoR(x,o) -> Function of F,ExField(x,o) means
:: FIELD_3:def 10
it.x = o &
for a being Element of F st a <> x holds it.a = a;
end;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster isoR(x,o) -> onto;
end;
theorem :: FIELD_3:17
for x being non trivial Element of F, o being object st not o in [#]F
holds isoR(x,o) is one-to-one;
theorem :: FIELD_3:18
for x being non trivial Element of F, u being object st not u in [#]F
holds isoR(x,u) is additive multiplicative unity-preserving;
theorem :: FIELD_3:19
for F being non almost_trivial Field
ex K being non polynomial_disjoint Field st K,F are_isomorphic;
theorem :: FIELD_3:20
for F being non almost_trivial Field holds
ex K being non polynomial_disjoint Field, p being Polynomial of K
st K,F are_isomorphic & deg p = n & p in [#]K /\ [#]Polynom-Ring K;
begin :: An Intuitive "Solution"
definition
let R be Ring;
attr R is flat means
:: FIELD_3:def 11
for a,b being Element of R holds the_rank_of a = the_rank_of b;
end;
registration
cluster flat for Ring;
end;
theorem :: FIELD_3:21
for R being flat Ring, p being Polynomial of R holds not p in [#]R;
registration
cluster -> polynomial_disjoint for flat Ring;
end;
theorem :: FIELD_3:22
for R being non degenerated Ring st 0 in the carrier of R
holds R is non flat;
registration
cluster INT.Ring -> non flat;
cluster F_Rat -> non flat;
cluster F_Real -> non flat;
end;
registration
let n be non trivial Nat;
cluster Z/n -> non flat;
end;
begin :: Some Positive Results
theorem :: FIELD_3:23
for R being Ring, p being Polynomial of R for n being Nat holds p <> n;
registration
let n be non trivial Nat;
cluster Z/n -> polynomial_disjoint;
end;
registration
cluster polynomial_disjoint for finite Field;
end;
theorem :: FIELD_3:24
for R being Ring, p being Polynomial of R for i being Integer holds p <> i;
registration
cluster INT.Ring -> polynomial_disjoint;
end;
theorem :: FIELD_3:25
for R being Ring, p being Polynomial of R for r being Rational holds p <> r;
registration
cluster F_Rat -> polynomial_disjoint;
end;
theorem :: FIELD_3:26
for R being Ring, p being Polynomial of R for r being Real holds p <> r;
registration
cluster F_Real -> polynomial_disjoint;
end;
registration
cluster polynomial_disjoint for infinite Field;
end;
registration
let R be polynomial_disjoint Ring;
cluster Polynom-Ring R -> polynomial_disjoint;
end;
registration
let F be Field, p be Element of [#]Polynom-Ring F;
cluster (Polynom-Ring F)/({p}-Ideal) -> polynomial_disjoint;
end;
registration
let F be polynomial_disjoint Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring p -> polynomial_disjoint;
end;