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