:: Quadratic Extensions
:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller
::
:: Received November 30, 2021
:: Copyright (c) 2021-2026 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, STRUCT_0, SUBSET_1, NAT_1,
SUPINF_2, BINOP_2, MESFUNC1, C0SP1, FUNCT_4, CARD_3, POLYNOM1, POLYNOM2,
POLYNOM3, FUNCSDOM, ALGSEQ_1, EC_PF_1, HURWITZ, FINSEQ_1, RLVECT_3,
CARD_1, VECTSP_2, FUNCT_1, RELAT_1, RLVECT_5, FOMODEL1, XBOOLE_0,
NUMBERS, POLYNOM5, GROUP_1, FUNCT_7, ZFMISC_1, AFINSQ_1, REALALG2,
REALSET1, LATTICE5, FDIFF_1, ALGNUM_1, ARYTM_1, FIELD_4, FIELD_2,
FIELD_3, O_RING_1, YELLOW_8, PYTHTRIP, RATFUNC1, NEWTON, XXREAL_0,
REALALG1, GAUSSINT, COMPLFLD, RING_5, GLIB_000, SQUARE_1, QC_LANG1,
CAT_1, XCMPLX_0, INT_1, INT_3, FIELD_5, RING_3, FUNCT_2, MSSUBFAM,
RLVECT_2, RLSUB_1, MOD_4, FIELD_6, FIELD_7, FIELD_8, FIELD_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, RELSET_1,
REALSET1, FUNCT_1, ORDINAL1, FUNCT_2, MEMBERED, FUNCOP_1, NUMBERS,
CARD_1, FINSEQ_1, ENUMSET1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, NAT_D,
SQUARE_1, INT_1, FUNCT_7, STRUCT_0, POLYNOM4, ALGSEQ_1, POLYNOM3,
POLYNOM1, POLYNOM5, GROUP_1, GROUP_4, GROUP_6, MOD_4, VECTSP_4, VECTSP_6,
VECTSP_7, VECTSP_9, BINOM, O_RING_1, GCD_1, ALGSTR_0, ALGSTR_1, QUOFIELD,
INT_3, GR_CY_1, RLVECT_1, VECTSP_2, MATRLIN, HURWITZ, VECTSP_1, C0SP1,
EC_PF_1, RATFUNC1, RINGCAT1, REALALG1, GAUSSINT, COMPLFLD, RING_2,
RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_2, FIELD_3, FIELD_4,
FIELD_5, FIELD_6, FIELD_7, FIELD_8;
constructors BINOP_1, REAL_1, FINSOP_1, BINARITH, VECTSP_2, POLYNOM3, C0SP1,
ALGSTR_1, BHSP_1, MCART_1, NUMBERS, ZFMISC_1, RELAT_1, XREAL_0, FUNCOP_1,
HURWITZ, VALUED_0, VECTSP_1, STRUCT_0, FUNCT_4, ARYTM_1, ARYTM_0,
XCMPLX_0, XXREAL_0, SUBSET_1, FINSEQ_4, ORDINAL1, NAT_1, ALGSTR_0,
NORMSP_1, FUNCT_2, FUNCT_1, POLYNOM4, XBOOLE_0, RELSET_1, ARYTM_3, ABIAN,
QUOFIELD, PARTFUN1, RLVECT_1, FUNCT_7, NAT_D, FINSEQ_1, VFUNCT_1, CARD_1,
FINSET_1, GAUSSINT, RATFUNC1, GCD_1, GROUP_6, FUNCT_5, REALSET1,
O_RING_1, ALGSTR_2, INT_3, BINOM, RINGCAT1, MEMBERED, RING_2, RING_3,
EC_PF_1, ALGSEQ_1, VECTSP_9, POLYNOM1, RING_4, GROUP_4, ALGNUM_1,
ENUMSET1, GROUP_1, BINOP_2, GR_CY_1, RING_5, SQUARE_1, REALALG2,
COMPLFLD, INT_1, POLYNOM5, FIELD_1, FIELD_2, FIELD_3, FIELD_4, FIELD_5,
FIELD_6, FIELD_7, FIELD_8;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, SUBSET_1, STRUCT_0, VECTSP_1, ALGSTR_1,
EC_PF_1, FINSET_1, FUNCT_2, ALGSTR_0, GROUP_1, RLVECT_1, QUOFIELD,
FUNCT_1, PARTFUN1, VFUNCT_1, CARD_1, REALSET1, RATFUNC1, GAUSSINT, MOD_4,
COMPLFLD, RELAT_1, RINGCAT1, FINSEQ_1, POLYNOM1, POLYNOM3, POLYNOM5,
RING_2, RING_3, RING_4, RING_5, REALALG1, REALALG2, FIELD_2, FIELD_4,
FIELD_5, FIELD_6, FIELD_7;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions XXREAL_0, GROUP_1, RLVECT_1, TARSKI, FUNCT_1, FUNCT_2, ALGSEQ_1,
REALSET1, GROUP_6;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, POLYNOM3, FIELD_6,
POLYNOM5, FUNCOP_1, VECTSP_1, QUOFIELD, FUNCT_2;
expansions STRUCT_0, GROUP_1, ALGSTR_0, ALGSTR_1, RLVECT_1, VECTSP_1, TARSKI,
GROUP_6, QUOFIELD, ALGSEQ_1, POLYNOM5, REALSET1, FUNCT_1, FUNCT_2,
FIELD_8;
theorems GROUP_1, VECTSP_1, VECTSP_2, RLVECT_1, C0SP1, SUBSET_1, INT_3,
FUNCT_2, TARSKI, FUNCT_1, RELAT_1, EC_PF_1, POLYNOM4, RING_3, RATFUNC1,
POLYNOM5, UPROOTS, RING_4, RING_5, NAT_2, HURWITZ, XREAL_1, INT_1, BINOM,
XBOOLE_0, FUNCT_7, FIELD_2, FIELD_4, ALGSEQ_1, FUNCOP_1, POLYNOM3, NAT_1,
CARD_1, ZFMISC_1, XXREAL_0, FINSEQ_1, ALGNUM_1, STRUCT_0, ORDINAL1,
NAT_D, XREAL_0, REALALG1, REALALG2, FIELD_3, FIELD_6, FINSEQ_3, ENUMSET1,
FIELD_5, O_RING_1, FIELD_7, FIELD_8, CARD_2, SQUARE_1, VECTSP_4,
VECTSP_6, VECTSP_7, GCD_1, VECTSP_9;
schemes INT_1, FUNCT_2;
begin :: Preliminaries
theorem lemmonus:
for a,b being Nat st a <= b holds a -' 1 <= b -' 1
proof
let a,b be Nat;
assume AS: a <= b;
per cases;
suppose a = 0;
then a - 1 = -1;
hence thesis by XREAL_0:def 2;
end;
suppose a > 0;
then a -'1 = a - 1 & b -' 1 = b - 1 by AS,XREAL_0:def 2;
hence thesis by AS,XREAL_1:9;
end;
end;
registration
let i be Integer;
cluster i^2 -> integer;
coherence
proof
i * i = i^2 by SQUARE_1:def 1;
hence thesis;
end;
end;
definition
let R be Ring, S be RingExtension of R;
let a be R-membered Element of S;
func @a -> Element of R equals
a;
coherence by FIELD_7:def 5;
end;
registration
let R be Ring, S be RingExtension of R;
let a be R-membered Element of S;
cluster -a -> R-membered;
coherence
proof
H1: R is Subring of S by FIELD_4:def 1;
reconsider aR = a as Element of R by FIELD_7:def 5;
-a = - aR by H1,FIELD_6:17;
hence thesis by FIELD_7:def 5;
end;
end;
registration
let R be Ring, S be RingExtension of R;
let a,b be R-membered Element of S;
cluster a + b -> R-membered;
coherence
proof
H1: R is Subring of S by FIELD_4:def 1;
reconsider aR = a, bR = b as Element of R by FIELD_7:def 5;
[aR,bR] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2; then
a + b = ((the addF of S) || the carrier of R).(a,b) by FUNCT_1:49
.= aR + bR by H1,C0SP1:def 3;
hence a + b is R-membered by FIELD_7:def 5;
end;
cluster a * b -> R-membered;
coherence
proof
H1: R is Subring of S by FIELD_4:def 1;
reconsider aR = a, bR = b as Element of R by FIELD_7:def 5;
[aR,bR] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2; then
a * b = ((the multF of S) || the carrier of R).(a,b) by FUNCT_1:49
.= aR * bR by H1,C0SP1:def 3;
hence a * b is R-membered by FIELD_7:def 5;
end;
end;
registration
let R be Ring, S be RingExtension of R;
cluster 0.S -> R-membered;
coherence
proof
R is Subring of S by FIELD_4:def 1;
then 0.S = 0.R by C0SP1:def 3;
hence thesis by FIELD_7:def 5;
end;
end;
registration
let R be non degenerated Ring, S be RingExtension of R;
cluster 1.S -> non zero R-membered;
coherence
proof
thus 1.S is non zero;
R is Subring of S by FIELD_4:def 1;
then 1.S = 1.R by C0SP1:def 3;
hence thesis by FIELD_7:def 5;
end;
end;
registration
let R be non degenerated Ring, S be RingExtension of R;
cluster non zero R-membered for Element of S;
existence
proof
take 1.S;
thus thesis;
end;
end;
registration
let F be Field, E be FieldExtension of F;
let a be non zero F-membered Element of E;
cluster a" -> F-membered;
coherence
proof
reconsider aF = a as Element of F by FIELD_7:def 5;
F is Subfield of E by FIELD_4:7;
then a" = aF" by FIELD_6:18;
hence a" is F-membered by FIELD_7:def 5;
end;
end;
registration
let R be Ring;
let a,b,c be Element of R;
cluster <*a,b,c*> -> (the carrier of R)-valued;
coherence
proof
set f = <*a,b,c*>;
len f = 3 & f.1 = a & f.2 = b & f.3 = c by FINSEQ_1:45; then
A2: dom f = Seg 3 by FINSEQ_1:def 3
.= Seg 2 \/ {2+1} by FINSEQ_1:9
.= {1,2} \/ {3} by FINSEQ_1:2;
now let o be object;
assume o in rng f; then
consider y being object such that
B: y in dom f & f.y = o by FUNCT_1:def 3;
per cases by B,A2,XBOOLE_0:def 3;
suppose y in {1,2}; then
per cases by TARSKI:def 2;
suppose y = 1;
hence o in the carrier of R by B;
end;
suppose y = 2;
hence o in the carrier of R by B;
end;
end;
suppose y in {3};
then y = 3 by TARSKI:def 1;
hence o in the carrier of R by B;
end;
end;
then rng f c= the carrier of R;
hence thesis by RELAT_1:def 19;
end;
end;
registration
cluster non 2-characteristic strict for Field;
existence
proof
take F_Rat;
Char F_Rat = 0 by RING_3:def 6;
hence thesis;
end;
end;
registration
let R be Ring;
reduce (0.R)^2 to 0.R;
reducibility
proof
thus (0.R)^2 = 0.R * 0.R by O_RING_1:def 1 .= 0.R;
end;
reduce (1.R)^2 to 1.R;
reducibility
proof
thus (1.R)^2 = 1.R * 1.R by O_RING_1:def 1 .= 1.R;
end;
reduce (-(1.R))^2 to 1.R;
reducibility
proof
thus (-(1.R))^2 = (-1.R) * (-1.R) by O_RING_1:def 1
.= 1.R * 1.R by VECTSP_1:10 .= 1.R;
end;
end;
theorem ch0:
for R being comRing,
a,b being Element of R holds (a * b)^2 = a^2 * b^2
proof
let R be comRing, a,b be Element of R;
thus (a * b)^2 = (a * b) * (a * b) by O_RING_1:def 1
.= a * (b * (a * b)) by GROUP_1:def 3
.= a * (b * (b * a)) by GROUP_1:def 12
.= a * ((b * b) * a) by GROUP_1:def 3
.= a * (a * (b * b)) by GROUP_1:def 12
.= (a * a) * (b * b) by GROUP_1:def 3
.= (a * a) * (b^2) by O_RING_1:def 1
.= (a^2) * (b^2) by O_RING_1:def 1;
end;
theorem ch0a:
for F being Field,
a being Element of F, b being non zero Element of F
for i being Integer
st i '*' a <> 0.F & i '*' b <> 0.F holds (i '*' a) * ((i '*' b)") = a * b"
proof
let F be Field, a be Element of F, b be non zero Element of F;
let i be Integer;
assume AS: i '*' a <> 0.F & i '*' b <> 0.F;
H: b <> 0.F;
((a * b") * ((i '*' a)")) * (i '*' b)
= (((i '*' a)") * (a * b")) * (i '*' b) by GROUP_1:def 12
.= ((i '*' a)") * ((a * b") * (i '*' b)) by GROUP_1:def 3
.= ((i '*' a)") * ((i '*' b) * (a * b")) by GROUP_1:def 12
.= ((i '*' a)") * (i '*' (b * (a * b"))) by REALALG2:5
.= ((i '*' a)") * (i '*' (b * (b" * a))) by GROUP_1:def 12
.= ((i '*' a)") * (i '*' ((b * b") * a)) by GROUP_1:def 3
.= ((i '*' a)") * (i '*' ((b" * b) * a)) by GROUP_1:def 12
.= ((i '*' a)") * (i '*' (1.F * a)) by H,VECTSP_1:def 10
.= 1.F by AS,VECTSP_1:def 10;
then (a * b") * ((i '*' a)") = (i '*' b)" by AS,VECTSP_1:def 10;
hence (i '*' a) * ((i '*' b)")
= (i '*' a) * ((i '*' a)" * (a * b")) by GROUP_1:def 12
.= ((i '*' a) * (i '*' a)") * (a * b") by GROUP_1:def 3
.= ((i '*' a)" * (i '*' a)) * (a * b") by GROUP_1:def 12
.= 1.F * (a * b") by AS,VECTSP_1:def 10
.= a * b";
end;
theorem ch1:
for R being comRing
for a being Element of R,
i being Integer holds (i '*' a)^2 = i^2 '*' a^2
proof
let R be comRing, a be Element of R, i be Integer;
thus (i '*' a)^2 = (i '*' a) * (i '*' a) by O_RING_1:def 1
.= i '*' (a * (i '*' a)) by REALALG2:5
.= i '*' ((i '*' a) * a) by GROUP_1:def 12
.= i '*' (i '*' (a * a)) by REALALG2:5
.= (i * i) '*' (a * a) by RING_3:65
.= (i^2) '*' (a * a) by SQUARE_1:def 1
.= (i^2) '*' a^2 by O_RING_1:def 1;
end;
theorem ch2:
for R being non 2-characteristic domRing
for a being Element of R holds 2 '*' a = 0.R iff a = 0.R
proof
let R be non 2-characteristic domRing;
let a be Element of R;
Char R <> 2 by RING_3:def 6; then
H: 2 '*' 1.R <> 0.R by REALALG2:24;
A: now assume 2 '*' a = 0.R;
then 0.R = 2 '*' (1.R * a) .= (2 '*' 1.R) * a by REALALG2:5;
hence a = 0.R by H,VECTSP_2:def 1;
end;
now assume B: a = 0.R;
(1 + 1) '*' a = 1 '*' a + 1 '*' a by RING_3:62
.= 1 '*' a + a by RING_3:60 .= a + a by RING_3:60;
hence 2 '*' a = 0.R by B;
end;
hence thesis by A;
end;
theorem ch4:
for R being non 2-characteristic domRing
for a being Element of R holds 4 '*' a = 0.R iff a = 0.R
proof
let F be non 2-characteristic domRing; let a be Element of F;
Char F <> 2 by RING_3:def 6; then
I: 2 '*' 1.F <> 0.F by REALALG2:24;
H: now assume 4 '*' a = 0.F;
then 0.F = (2 * 2) '*' a
.= 2 '*' (2 '*' (1.F * a)) by RING_3:65
.= 2 '*' ((2 '*' 1.F) * a) by REALALG2:5
.= 2 '*' (a * (2 '*' 1.F)) by GROUP_1:def 12
.= (2 '*' a) * (2 '*' 1.F) by REALALG2:5;
then 2 '*' a = 0.F by I,VECTSP_2:def 1;
hence a = 0.F by ch2;
end;
now assume a = 0.F;
then B: 2 '*' a = 0.F by ch2;
(2 + 2) '*' a = 2 '*' a + 2 '*' a by RING_3:62;
hence 4 '*' a = 0.F by B;
end;
hence thesis by H;
end;
theorem Z3:
for R being Ring,
S being RingExtension of R
for a being Element of R, b being Element of S st b = a
for i being Integer holds i '*' a = i '*' b
proof
let R be Ring, S be RingExtension of R;
let a be Element of R, b be Element of S;
assume AS: b = a;
let i be Integer;
K: R is Subring of S by FIELD_4:def 1;
defpred P[Integer] means
for k being Integer st k = $1 holds k'*'a = k'*'b;
now let k be Integer;
assume A1: k = 0;
hence k'*'a = 0.R by RING_3:59
.= 0.S by K,C0SP1:def 3 .= k'*'b by A1,RING_3:59;
end; then
A2: P[0];
A6: 1 '*' a = b by AS,RING_3:60 .= 1 '*' b by RING_3:60; then
A7: -(1 '*' a) = -(1 '*' b) by K,FIELD_6:17;
A3: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume P[u]; then
A4: u'*'a = u'*'b;
now let k be Integer;
assume A5: k = u-1;
hence k'*'a
= u'*'a - 1'*'a by RING_3:64
.= u'*'b - 1'*'b by A4,A7,K,FIELD_6:15
.= k'*'b by A5,RING_3:64;
end;
hence P[u-1];
now let k be Integer;
assume A5:k = u+1;
hence k'*'a
= u'*'a + 1'*'a by RING_3:62
.= u'*'b + 1'*'b by A4,A6,K,FIELD_6:15
.= k'*'b by A5,RING_3:62;
end;
hence P[u+1];
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
theorem lemquadr:
for R being domRing,
S being domRingExtension of R
for a being Element of R,
b being Element of S st b^2 = a^2 holds b = a or b = -a
proof
let R be domRing,S be domRingExtension of R;
let a be Element of R, b be Element of S;
assume AS: b^2 = a^2;
A: R is Subring of S by FIELD_4:def 1; then
the carrier of R c= the carrier of S by C0SP1:def 3; then
reconsider a1 = a as Element of S;
a1^2 = a1 * a1 by O_RING_1:def 1
.= a * a by A,FIELD_6:16
.= b^2 by AS,O_RING_1:def 1; then
b = a1 or b = -a1 by REALALG2:10;
hence thesis by A,FIELD_6:17;
end;
theorem ext1:
for F being Field,
E being FieldExtension of F
for a being Element of E holds FAdj(F,{a,-a}) = FAdj(F,{a})
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
Y: FAdj(F,{a}) is Subfield of FAdj(F,{a,-a}) by FIELD_7:10,ZFMISC_1:7;
now let o be object;
assume A: o in the carrier of FAdj(F,{a,-a});
the carrier of FAdj(F,{a,-a}) = carrierFA({a,-a}) by FIELD_6:def 6
.= {x where x is Element of E :
for U being Subfield of E st F is Subfield of U &
{a,-a} is Subset of U holds x in U};
then consider oe being Element of E such that
C: oe = o &
for U being Subfield of E st F is Subfield of U &
{a,-a} is Subset of U holds oe in U by A;
D: now let U be Subfield of E;
assume D: F is Subfield of U & {a} is Subset of U;
E: a in {a} by TARSKI:def 1; then
reconsider au = a as Element of U by D;
U is Subring of E by FIELD_5:12; then
F: -au = -a by FIELD_6:17;
now let u be object;
assume u in {a,-a};
then per cases by TARSKI:def 2;
suppose u = a;
hence u in the carrier of U by E,D;
end;
suppose u = -a;
hence u in the carrier of U by F;
end;
end;
then {a,-a} is Subset of U by TARSKI:def 3;
hence oe in U by C,D;
end;
the carrier of FAdj(F,{a}) = carrierFA({a}) by FIELD_6:def 6
.= {x where x is Element of E :
for U being Subfield of E st F is Subfield of U &
{a} is Subset of U holds x in U};
hence o in the carrier of FAdj(F,{a}) by C,D;
end; then
the carrier of FAdj(F,{a,-a}) c= the carrier of FAdj(F,{a}); then
FAdj(F,{a,-a}) is Subfield of FAdj(F,{a}) by EC_PF_1:6;
hence thesis by Y,EC_PF_1:4;
end;
theorem
for F being Field,
E being FieldExtension of F
for a being Element of E holds FAdj(F,{a}) = FAdj(F,{-a})
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
thus FAdj(F,{a}) = FAdj(F,{--a,-a}) by ext1 .= FAdj(F,{-a}) by ext1;
end;
registration
cluster non algebraic-closed for polynomial_disjoint Field;
existence
proof
take F_Real;
thus thesis;
end;
end;
registration
let F be non algebraic-closed Field;
cluster irreducible non linear for Element of the carrier of Polynom-Ring F;
existence
proof
now assume A: for p being Element of the carrier of Polynom-Ring F
st p is irreducible holds p is linear;
for p being monic Element of the carrier of Polynom-Ring F
holds p is irreducible iff deg p = 1
proof
let p being monic Element of the carrier of Polynom-Ring F;
now assume p is irreducible;
then p is linear by A;
hence deg p = 1 by FIELD_5:def 1;
end;
hence thesis by RING_4:44;
end;
hence contradiction by RING_4:46;
end;
hence thesis;
end;
end;
registration
let F be Field;
cluster irreducible non linear -> non with_roots for
Element of the carrier of Polynom-Ring F;
coherence;
cluster irreducible with_roots -> linear for
Element of the carrier of Polynom-Ring F;
coherence;
end;
registration
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
cluster KrRootP p -> F-algebraic;
coherence
proof
Ext_eval(p,KrRootP p) = 0.F by FIELD_5:17
.= 0.embField(canHomP p) by FIELD_2:def 7;
hence KrRootP p is F-algebraic by FIELD_6:43;
end;
end;
registration
let F be non algebraic-closed polynomial_disjoint Field;
let p be irreducible non linear Element of the carrier of Polynom-Ring F;
cluster KrRootP p -> non zero non F-membered;
coherence
proof
now assume KrRootP p in the carrier of F; then
reconsider o = KrRootP p as Element of F;
eval(p,o) = Ext_eval(p,KrRootP p) by FIELD_6:10
.= 0.F by FIELD_5:17; then
o is_a_root_of p; then
p is with_roots;
hence contradiction;
end;
hence thesis by FIELD_7:def 5;
end;
end;
begin :: More on Polynomials
leng:
for R being Ring,
p,q being Polynomial of R holds len(p*'q) <= len p + len q -' 1
proof
let R be Ring; let p,q be Polynomial of R;
len p + len q -' 1 is_at_least_length_of p*'q
proof
let i be Nat;
i in NAT by ORDINAL1:def 12;
then consider r be FinSequence of the carrier of R such that
A2: len r = i+1 and
A3: (p*'q).i = Sum r and
A4: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i
+1-'k) by POLYNOM3:def 9;
assume i >= len p + len q -' 1;
then i >= len p + len q - 1 by XREAL_0:def 2;
then i+1 >= len p + len q by XREAL_1:20;
then
A5: -len p >= -(i+1 - len q) by XREAL_1:24,XREAL_1:19;
now
let k be Element of NAT;
assume
A6: k in dom r;
then
A7: r.k = p.(k-'1) * q.(i+1-'k) by A4;
k in Seg len r by A6,FINSEQ_1:def 3;
then
A8: k <= i+1 by A2,FINSEQ_1:1;
per cases;
suppose
k-'1 < len p;
then k-1 < len p by XREAL_0:def 2;
then -(k-1) > -len p by XREAL_1:24;
then 1-k > len q - (i+1) by A5,XXREAL_0:2;
then i+1+(1-k) > len q by XREAL_1:19;
then i+1-k+1 > len q;
then i+1-'k+1 > len q by A8,XREAL_1:48,XREAL_0:def 2;
then q.(i+1-'k) = 0.R by NAT_1:13,ALGSEQ_1:8;
hence r.k = 0.R by A7;
end;
suppose
k-'1 >= len p;
then p.(k-'1) = 0.R by ALGSEQ_1:8;
hence r.k = 0.R by A7;
end;
end;
hence (p*'q).i = 0.R by A3,POLYNOM3:1;
end;
hence thesis by ALGSEQ_1:def 3;
end;
theorem
for R being non degenerated Ring,
p being non zero Polynomial of R
for q being Polynomial of R holds deg(p*'q) <= deg p + deg q
proof
let R be non degenerated Ring;
let p be non zero Polynomial of R; let q be Polynomial of R;
deg p = len p - 1 & deg q = len q - 1 &
deg(p*'q) = len(p*'q) - 1 by HURWITZ:def 2;
then C: deg(p*'q) + 1 <= (deg p + 1) + (deg q + 1) -' 1 by leng;
reconsider degp = deg p as Element of NAT;
D: deg p + 1 >= 0 + 1 by XREAL_1:6;
deg q + 1 >= 0
proof
per cases;
suppose q = 0_.(R);
then deg q = -1 by HURWITZ:20;
hence thesis;
end;
suppose q <> 0_.(R);
then reconsider q1 = q as non zero Polynomial of R by UPROOTS:def 5;
reconsider degq = deg q1 as Element of NAT;
degq >= 0;
hence thesis;
end;
end;
then (deg p + 1) + (deg q + 1) >= 1 + 0 by D,XREAL_1:7;
then (deg p + 1) + (deg q + 1) - 1 >= 1 - 1 by XREAL_1:9;
then deg(p*'q) + 1 <= (deg p + 1) + deg q by C,XREAL_0:def 2;
then deg(p*'q) + 1 - 1 <= (deg p + 1) + deg q - 1 by XREAL_1:9;
hence thesis;
end;
registration
let L be well-unital non degenerated doubleLoopStr;
let k be non zero Element of NAT;
let a be Element of L;
cluster rpoly(k,a) -> monic;
coherence
proof
set p = rpoly(k,a);
k = deg p by HURWITZ:27 .= len(p) - 1 by HURWITZ:def 2;
then k + 1 = len p;
then len(p) -' 1 = k by NAT_D:34;
then p.(len(p) -' 1) = 1_L by HURWITZ:25;
then LC p = 1_L by RATFUNC1:def 6;
hence p is monic by RATFUNC1:def 7;
end;
end;
registration
let R be non degenerated Ring;
let a be non zero Element of R,
b be Element of R;
cluster <%b,a%> -> linear;
coherence
proof
len <%b,a%> = 2 by POLYNOM5:40;
then deg <%b,a%> = 2 - 1 by HURWITZ:def 2;
hence thesis by FIELD_5:def 1;
end;
end;
registration
let R be non degenerated Ring;
let b be Element of R;
cluster <%b,1.R%> -> monic linear;
coherence
proof
A: 2-'1 = 2-1 by XREAL_0:def 2;
len <%b,1.R%> = 2 by POLYNOM5:40;
then <%b,1.R%>.(len <%b,1.R%>-'1) = 1.R by A,POLYNOM5:38;
then LC <%b,1.R%> = 1.R by RATFUNC1:def 6;
hence thesis by RATFUNC1:def 7;
end;
end;
theorem qua20:
for R being Ring
for a,b,x being Element of R holds x * <%b,a%> = <%x*b,x*a%>
proof
let R be Ring; let a,b,x be Element of R;
set p = <%x*b,x*a%>;
H: len <%b,a%> <= 2 & len p <= 2 by POLYNOM5:39;
now let i be Element of NAT;
i <= 1 implies i = 0 or ... or i = 1; then
per cases;
suppose B: i = 0;
then <%b,a%>.i = b by POLYNOM5:38;
hence (x*<%b,a%>).i = x * b by POLYNOM5:def 4 .= p.i by B,POLYNOM5:38;
end;
suppose B: i = 1;
then <%b,a%>.i = a by POLYNOM5:38;
hence (x*<%b,a%>).i = x * a by POLYNOM5:def 4 .= p.i by B,POLYNOM5:38;
end;
suppose i > 1;
then i + 1 > 1 + 1 by XREAL_1:6;
then C: i >= 2 by NAT_1:13;
then <%b,a%>.i = 0.R by H,XXREAL_0:2,ALGSEQ_1:8;
hence (x*<%b,a%>).i = x * 0.R by POLYNOM5:def 4
.= p.i by C,H,XXREAL_0:2,ALGSEQ_1:8;
end;
end;
hence thesis;
end;
theorem deg2:
for R being Ring,
p being Polynomial of R st deg p < 2
for a being Element of R ex y,z being Element of R st p = <%y,z%>
proof
let R be Ring, p be Polynomial of R;
assume A: deg p < 2;
let a be Element of R;
take y = p.0, z = p.1;
set q = <%y,z%>;
now let i be Element of NAT;
per cases;
suppose i = 0;
hence p.i = q.i by POLYNOM5:38;
end;
suppose i = 1;
hence p.i = q.i by POLYNOM5:38;
end;
suppose i <> 0 & i <> 1; then
B: i is non trivial by NAT_2:def 1; then
i >= 2 by NAT_2:29; then
i > deg p by A,XXREAL_0:2; then
i > len p - 1 by HURWITZ:def 2; then
i >= len p - 1 + 1 by INT_1:7;
hence p.i = 0.R by ALGSEQ_1:8 .= q.i by B,NAT_2:29,POLYNOM5:38;
end;
end;
hence thesis;
end;
theorem
for R being comRing,
p being Polynomial of R st deg p < 2
for a being Element of R ex y,z being Element of R st eval(p,a) = y + a * z
proof
let R be comRing; let p be Polynomial of R;
assume A: deg p < 2;
let a be Element of R;
consider y,z being Element of R such that B: p = <%y,z%> by A,deg2;
take y,z;
thus eval(p,a) = y + z * a by B,POLYNOM5:44 .= y + a * z by GROUP_1:def 12;
end;
theorem deg2evale:
for F being Field,
E being FieldExtension of F
for p being Polynomial of F st deg p < 2
for a being Element of E
ex y,z being F-membered Element of E st Ext_eval(p,a) = y + a * z
proof
let F be Field, E be FieldExtension of F; let p be Polynomial of F;
assume A: deg p < 2;
let a be Element of E;
reconsider q = p as Polynomial of E by FIELD_4:8;
B: p is Element of the carrier of Polynom-Ring F &
q is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10; then
C: deg q = deg p by FIELD_4:20;
consider yF,zF being Element of F such that D: p = <%yF,zF%> by A,deg2;
consider y,z being Element of E such that E: q = <%y,z%> by A,C,deg2;
y = q.0 by E,POLYNOM5:38 .= yF by D,POLYNOM5:38; then
G1: y is F-membered by FIELD_7:def 5;
z = q.1 by E,POLYNOM5:38 .= zF by D,POLYNOM5:38; then
G2: z is F-membered by FIELD_7:def 5;
Ext_eval(p,a) = eval(q,a) by B,FIELD_4:26
.= y + z * a by E,POLYNOM5:44
.= y + a * z by GROUP_1:def 12;
hence thesis by G1,G2;
end;
definition
let R be Ring;
let a be Element of R;
func X-a -> Element of the carrier of Polynom-Ring R equals
rpoly(1,a);
coherence by POLYNOM3:def 10;
func X+a -> Element of the carrier of Polynom-Ring R equals
rpoly(1,-a);
coherence by POLYNOM3:def 10;
end;
registration
let R be non degenerated Ring;
let a be Element of R;
cluster X-a -> linear monic;
coherence
proof
deg(X-a) = 1 by HURWITZ:27;
hence X-a is linear by FIELD_5:def 1;
thus thesis;
end;
cluster X+a -> linear monic;
coherence
proof
deg(X+a) = 1 by HURWITZ:27;
hence X+a is linear by FIELD_5:def 1;
thus thesis;
end;
end;
begin :: Quadratic Polynomials
definition
let R be Ring;
let p be Polynomial of R;
attr p is quadratic means :defquadr:
deg p = 2;
end;
registration
let R be non degenerated Ring;
cluster monic quadratic for Polynomial of R;
existence
proof
take rpoly(2,0.R);
thus thesis by HURWITZ:27;
end;
cluster monic quadratic for Element of the carrier of Polynom-Ring R;
existence
proof
reconsider p = rpoly(2,0.R) as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
take p;
thus thesis by HURWITZ:27;
end;
end;
registration
let R be non degenerated Ring;
cluster -> non constant for quadratic Polynomial of R;
coherence
proof
let p be quadratic Polynomial of R;
deg p = 2 by defquadr;
hence thesis by RATFUNC1:def 2;
end;
cluster -> non constant for quadratic Element of the carrier of Polynom-Ring R;
coherence
proof
let p be quadratic Element of the carrier of Polynom-Ring R;
deg p = 2 by defquadr;
hence thesis by RING_4:def 4;
end;
end;
definition
let L be non empty ZeroStr;
let a,b,c be Element of L;
func <%c,b,a%> -> sequence of L equals
0_.(L)+*(0,c)+*(1,b)+*(2,a);
correctness;
end;
qua1:
for L being non empty ZeroStr
for a,b,c being Element of L
holds <%c,b,a%>.0 = c & <%c,b,a%>.1 = b & <%c,b,a%>.2 = a &
for n being Nat st n >= 3 holds <%c,b,a%>.n = 0.L
proof
let L be non empty ZeroStr; let a,b,c be Element of L;
A1: 0 in dom 0_.(L);
thus <%c,b,a%>.0 = (0_.(L)+*(0,c)+*(1,b)).0 by FUNCT_7:32
.= (0_.(L)+*(0,c)).0 by FUNCT_7:32
.= c by A1,FUNCT_7:31;
1 in NAT;
then H: 1 in dom (0_.(L)+*(0,c)) by FUNCT_2:def 1;
thus <%c,b,a%>.1 = (0_.(L)+*(0,c)+*(1,b)).1 by FUNCT_7:32
.= b by H,FUNCT_7:31;
A2: 2 in NAT;
2 in dom (0_.(L)+*(0,c)+*(1,b)) by A2,FUNCT_2:def 1;
hence <%c,b,a%>.2 = a by FUNCT_7:31;
let n be Nat;
assume
A3: n >= 3;
then n >= 1+1+1;
then H1: n > 0+1+1 by NAT_1:13;
then H2: n > 0 + 1 by NAT_1:13;
thus <%c,b,a%>.n = (0_.(L)+*(0,c)+*(1,b)).n by H1,FUNCT_7:32
.= (0_.(L)+*(0,c)).n by H2,FUNCT_7:32
.= (0_.(L)).n by A3,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
registration
let L be non empty ZeroStr;
let a,b,c be Element of L;
cluster <%c,b,a%> -> finite-Support;
coherence
proof
take 3;
let n be Nat;
thus thesis by qua1;
end;
end;
theorem
for L being non empty ZeroStr
for a,b,c being Element of L
holds <%c,b,a%>.0 = c & <%c,b,a%>.1 = b & <%c,b,a%>.2 = a &
for n being Nat st n >= 3 holds <%c,b,a%>.n = 0.L by qua1;
qua2:
for L be non empty ZeroStr for a,b,c be Element of L holds len <%c,b,a%> <= 3
proof
let L be non empty ZeroStr; let a,b,c be Element of L;
3 is_at_least_length_of <%c,b,a%> by qua1;
hence thesis by ALGSEQ_1:def 3;
end;
theorem
for L being non empty ZeroStr
for a,b,c being Element of L holds deg <%c,b,a%> <= 2
proof
let L be non empty ZeroStr; let a,b,c be Element of L;
len <%c,b,a%> - 1 <= 3 - 1 by qua2,XREAL_1:9;
hence thesis by HURWITZ:def 2;
end;
qua3:
for L be non empty ZeroStr for a,b,c be Element of L st a <> 0.L
holds len <%c,b,a%> = 3
proof
let L be non empty ZeroStr; let a,b,c be Element of L;
assume a <> 0.L;
then <%c,b,a%>.2 <> 0.L by qua1; then
A1: for n be Nat st n is_at_least_length_of <%c,b,a%> holds 2+1 <= n
by NAT_1:13;
3 is_at_least_length_of <%c,b,a%> by qua1;
hence thesis by A1,ALGSEQ_1:def 3;
end;
theorem qua4:
for L being non empty ZeroStr
for a,b,c being Element of L holds deg <%c,b,a%> = 2 iff a <> 0.L
proof
let L be non empty ZeroStr; let a,b,c be Element of L;
H: deg <%c,b,a%> = len <%c,b,a%> - 1 by HURWITZ:def 2;
A: now assume a <> 0.L;
then len <%c,b,a%> = 3 by qua3;
hence deg <%c,b,a%> = 2 by H;
end;
now assume deg <%c,b,a%> = 2;
then len <%c,b,a%> = 2 + 1 by H;
then <%c,b,a%>.2 <> 0.L by ALGSEQ_1:10;
hence a <> 0.L by qua1;
end;
hence thesis by A;
end;
registration
let R be non degenerated Ring;
let a be non zero Element of R, b,c be Element of R;
cluster <%c,b,a%> -> quadratic;
coherence by qua4;
end;
registration
let R be non degenerated Ring;
let b,c be Element of R;
cluster <%c,b,1.R%> -> quadratic monic;
coherence
proof
A: 3-'1 = 3-1 by XREAL_0:def 2;
len <%c,b,1.R%> = 3 by qua3;
then <%c,b,1.R%>.(len <%c,b,1.R%>-'1) = 1.R by A,qua1;
then LC <%c,b,1.R%> = 1.R by RATFUNC1:def 6;
hence thesis by RATFUNC1:def 7;
end;
end;
registration
let R be domRing;
let a,x be non zero Element of R, b,c be Element of R;
cluster x * <%c,b,a%> -> quadratic;
coherence
proof
deg(x * <%c,b,a%>) = deg <%c,b,a%> by RING_5:4 .= 2 by qua4;
hence thesis;
end;
end;
theorem qua6:
for R being Ring
for a,b,c,x being Element of R holds x * <%c,b,a%> = <%x*c,x*b,x*a%>
proof
let R be Ring; let a,b,c,x be Element of R;
set p = <%x*c,x*b,x*a%>;
H: len <%c,b,a%> <= 3 & len p <= 3 by qua2;
now let i be Element of NAT;
i <= 2 implies i = 0 or ... or i = 2; then
per cases;
suppose B: i = 0;
then <%c,b,a%>.i = c by qua1;
hence (x*<%c,b,a%>).i = x * c by POLYNOM5:def 4 .= p.i by B,qua1;
end;
suppose B: i = 1;
then <%c,b,a%>.i = b by qua1;
hence (x*<%c,b,a%>).i = x * b by POLYNOM5:def 4 .= p.i by B,qua1;
end;
suppose B: i = 2;
then <%c,b,a%>.i = a by qua1;
hence (x*<%c,b,a%>).i = x * a by POLYNOM5:def 4 .= p.i by B,qua1;
end;
suppose i > 2;
then i + 1 > 2 + 1 by XREAL_1:6;
then C: i >= 3 by NAT_1:13;
then <%c,b,a%>.i = 0.R by H,XXREAL_0:2,ALGSEQ_1:8;
hence (x*<%c,b,a%>).i = x * 0.R by POLYNOM5:def 4
.= p.i by C,H,XXREAL_0:2,ALGSEQ_1:8;
end;
end;
hence thesis;
end;
theorem evalq:
for R being Ring
for a,b,c,x being Element of R holds eval(<%c,b,a%>,x) = c + b * x + a * x^2
proof
let R be Ring; let a,b,c,x be Element of R;
consider F be FinSequence of the carrier of R such that
A1: eval(<%c,b,a%>,x) = Sum F and
A2: len F = len <%c,b,a%> and
A3: for n be Element of NAT st n in dom F
holds F.n = <%c,b,a%>.(n-'1) * (power R).(x,n-'1) by POLYNOM4:def 2;
len F = 0 or ... or len F = 3 by A2,qua2;
then per cases;
suppose
len F = 0; then
A4: <%c,b,a%> = 0_.(R) by A2,POLYNOM4:5;
hence eval(<%c,b,a%>,x)
= (0_.(R)).0 by POLYNOM4:17
.= c + (0_.(R)).1 * x by A4,qua1
.= c + b * x + (0_.(R)).2 * x^2 by A4,qua1
.= c + b * x + a * x^2 by A4,qua1;
end;
suppose
A5: len F = 1;
then 0+1 in Seg len F by FINSEQ_1:4;
then 1 in dom F by FINSEQ_1:def 3;
then F.1 = <%c,b,a%>.(1-'1) * (power R).(x,1-'1) by A3
.= <%c,b,a%>.0 * (power R).(x,1-'1) by XREAL_1:232
.= <%c,b,a%>.0 * (power R).(x,0) by XREAL_1:232
.= c * (power R).(x,0) by qua1
.= c * 1_R by GROUP_1:def 7
.= c;
then F = <*c*> by A5,FINSEQ_1:40;
hence eval(<%c,b,a%>,x)
= c + 0.R * x by A1,RLVECT_1:44
.= c + <%c,b,a%>.1 * x by A2,A5,ALGSEQ_1:8
.= c + b * x + 0.R * x^2 by qua1
.= c + b * x + <%c,b,a%>.2 * x^2 by A2,A5,ALGSEQ_1:8
.= c + b * x + a * x^2 by qua1;
end;
suppose
A6: len F = 2; then
A7: F.1 = <%c,b,a%>.(1-'1) * (power R).(x,1-'1) by A3,FINSEQ_3:25
.= <%c,b,a%>.0 * (power R).(x,1-'1) by XREAL_1:232
.= <%c,b,a%>.0 * (power R).(x,0) by XREAL_1:232
.= c * (power R).(x,0) by qua1
.= c * 1_R by GROUP_1:def 7
.= c;
A8: 2-'1 = 2-1 by XREAL_0:def 2;
F.2 = <%c,b,a%>.(2-'1) * (power R).(x,2-'1) by A3,A6,FINSEQ_3:25
.= b * (power R).(x,1) by A8,qua1
.= b * x by GROUP_1:50;
then F = <*c,b*x*> by A6,A7,FINSEQ_1:44;
hence eval(<%c,b,a%>,x)
= c + b * x + 0.R * x^2 by A1,RLVECT_1:45
.= c + b * x + <%c,b,a%>.2 * x^2 by A2,A6,ALGSEQ_1:8
.= c + b * x + a * x^2 by qua1;
end;
suppose
A9: len F = 3; then
A10: F.1 = <%c,b,a%>.(1-'1) * (power R).(x,1-'1) by A3,FINSEQ_3:25
.= <%c,b,a%>.0 * (power R).(x,1-'1) by XREAL_1:232
.= <%c,b,a%>.0 * (power R).(x,0) by XREAL_1:232
.= c * (power R).(x,0) by qua1
.= c * 1_R by GROUP_1:def 7
.= c;
A11: 2-'1 = 2-1 by XREAL_0:def 2;
A12: F.2 = <%c,b,a%>.(2-'1) * (power R).(x,2-'1) by A3,A9,FINSEQ_3:25
.= b * (power R).(x,1) by A11,qua1
.= b * x by GROUP_1:50;
A13: 3-'1 = 3-1 by XREAL_0:def 2;
F.3 = <%c,b,a%>.(3-'1) * (power R).(x,3-'1) by A3,A9,FINSEQ_3:25
.= a * (power R).(x,2) by A13,qua1
.= a * (x * x) by GROUP_1:51
.= a * x^2 by O_RING_1:def 1;
then F = <*c,b*x,a*x^2*> by A9,A10,A12,FINSEQ_1:45;
hence thesis by A1,RLVECT_1:46;
end;
end;
theorem qua5:
for R being non degenerated Ring,
p being Polynomial of R holds
p is quadratic iff
ex a being non zero Element of R, b,c being Element of R st p = <%c,b,a%>
proof
let R be non degenerated Ring, p be Polynomial of R;
now assume A: p is quadratic;
B: deg p = len p - 1 by HURWITZ:def 2;
reconsider a = p.2, b = p.1, c = p.0 as Element of R;
now let i be Element of NAT;
i <= 2 implies i = 0 or ... or i = 2; then
per cases;
suppose i = 0;
hence p.i = <%c,b,a%>.i by qua1;
end;
suppose i = 1;
hence p.i = <%c,b,a%>.i by qua1;
end;
suppose i = 2;
hence p.i = <%c,b,a%>.i by qua1;
end;
suppose i > 2;
then i + 1 > 2 + 1 by XREAL_1:6;
then C: i >= 3 by NAT_1:13;
hence <%c,b,a%>.i = 0.R by qua1 .= p.i by A,B,C,ALGSEQ_1:8;
end;
end; then
D: p = <%c,b,a%>;
len p = 2 + 1 by B,A;
then a is non zero by ALGSEQ_1:10;
hence ex a being non zero Element of R,
b,c being Element of R st p = <%c,b,a%> by D;
end;
hence thesis;
end;
theorem qua5a:
for R being non degenerated Ring,
p being monic Polynomial of R holds
p is quadratic iff ex b,c being Element of R st p = <%c,b,1.R%>
proof
let R be non degenerated Ring, p be monic Polynomial of R;
now assume p is quadratic; then
consider a being non zero Element of R, b,c being Element of R such that
A: p = <%c,b,a%> by qua5;
H: 3-'1 = 3-1 & a <> 0.R by XREAL_0:def 2;
1.R = LC p by RATFUNC1:def 7
.= p.(len p-'1) by RATFUNC1:def 6
.= p.2 by H,A,qua3
.= a by A,qua1;
hence ex b,c being Element of R st p = <%c,b,1.R%> by A;
end;
hence thesis;
end;
theorem eval2:
for R being non degenerated Ring,
S being RingExtension of R
for a1,b1,c1 being Element of R,
a2,b2,c2 being Element of S st a1 = a2 & b1 = b2 & c1 = c2
holds <%c2,b2,a2%> = <%c1,b1,a1%>
proof
let R be non degenerated Ring, S be RingExtension of R;
let a1,b1,c1 be Element of R, a2,b2,c2 be Element of S;
assume A: a1 = a2 & b1 = b2 & c1 = c2;
set p = <%c2,b2,a2%>, q = <%c1,b1,a1%>;
H: R is Subring of S by FIELD_4:def 1;
B: len p <= 3 & len q <= 3 by qua2;
now let i be Element of NAT;
i <= 2 implies i = 0 or ... or i = 2; then
per cases;
suppose C: i = 0;
hence p.i = c1 by A,qua1 .= q.i by C,qua1;
end;
suppose C: i = 1;
hence p.i = b1 by A,qua1 .= q.i by C,qua1;
end;
suppose C: i = 2;
hence p.i = a1 by A,qua1 .= q.i by C,qua1;
end;
suppose i > 2;
then i + 1 > 2 + 1 by XREAL_1:6;
then C: i >= 3 by NAT_1:13;
hence p.i = 0.S by B,XXREAL_0:2,ALGSEQ_1:8
.= 0.R by H,C0SP1:def 3
.= q.i by C,B,XXREAL_0:2,ALGSEQ_1:8;
end;
end;
hence thesis;
end;
definition
let R be non degenerated Ring;
let p be Polynomial of R;
attr p is purely_quadratic means :defpur:
ex a being non zero Element of R, c being Element of R st p = <%c,0.R,a%>;
end;
registration
let R be non degenerated Ring;
let a be non zero Element of R, c be Element of R;
cluster <%c,0.R,a%> -> purely_quadratic;
coherence;
end;
registration
let R be non degenerated Ring;
cluster monic purely_quadratic for Polynomial of R;
existence
proof
take p = <%0.R,0.R,1.R%>;
thus thesis;
end;
end;
registration
let R be non degenerated Ring;
cluster purely_quadratic -> quadratic for Polynomial of R;
coherence;
end;
definition
let R be Ring;
let a be Element of R;
func X^2-a -> Element of the carrier of Polynom-Ring R equals
<%-a,0.R,1.R%>;
coherence by POLYNOM3:def 10;
func X^2+a -> Element of the carrier of Polynom-Ring R equals
<%a,0.R,1.R%>;
coherence by POLYNOM3:def 10;
end;
registration
let R be non degenerated Ring;
cluster linear -> non quadratic for Polynomial of R;
coherence by FIELD_5:def 1;
cluster quadratic -> non linear for Polynomial of R;
coherence;
end;
registration
let R be non degenerated Ring;
let a be Element of R;
cluster X^2-a -> purely_quadratic monic non constant;
coherence;
cluster X^2+a -> purely_quadratic monic non constant;
coherence;
end;
theorem lemred1:
for F being Field
for b1,c1,b2,c2 being Element of F
holds <%c1,b1%> *' <%c2,b2%> = <%c1*c2,b1*c2+b2*c1,b1*b2%>
proof
let F be Field; let b1,c1,b2,c2 be Element of F;
set p1 = <%c1,b1%>, p2 = <%c2,b2%>, q = <%c1*c2,b1*c2+b2*c1,b1*b2%>;
J: 4 -' 1 = 4 - 1 by XREAL_0:def 2; then
K: 2 -' 1 = 2 - 1 & 3 -' 1 = 3 - 1 & 3 -' 2 = 3 - 2 & 4 -' 1 = 3
by XREAL_0:def 2;
A: dom(p1*'p2) = NAT by FUNCT_2:def 1 .= dom q by FUNCT_2:def 1;
now let o be object;
assume o in dom q;
then reconsider i = o as Element of NAT;
consider r being FinSequence of the carrier of F such that
B1: len r = i+1 & (p1*'p2).i = Sum r &
for k being Element of NAT st k in dom r
holds r.k = p1.(k-'1) * p2.(i+1-'k) by POLYNOM3:def 9;
i <= 2 implies i = 0 or ... or i = 2; then
per cases;
suppose C: i = 0;
then B2: r = <*r.1*> by B1,FINSEQ_1:40;
then dom r = {1} by FINSEQ_1:2,FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then r.1 = p1.(1-'1) * p2.(0+1-'1) by C,B1
.= p1.(1-'1) * p2.0 by NAT_2:8
.= p1.0 * p2.0 by NAT_2:8
.= c1 * p2.0 by POLYNOM5:38
.= c1 * c2 by POLYNOM5:38;
then Sum r = c1*c2 by B2,RLVECT_1:44;
hence (p1*'p2).o = q.o by B1,C,qua1;
end;
suppose C: i = 1;
then B3: r = <*r.1,r.2*> by B1,FINSEQ_1:44;
B4: dom r = {1,2} by B1,C,FINSEQ_1:def 3,FINSEQ_1:2;
then 1 in dom r by TARSKI:def 2;
then B5: r.1 = p1.(1-'1) * p2.(1+1-'1) by C,B1
.= p1.0 * p2.1 by K,NAT_2:8
.= c1 * p2.1 by POLYNOM5:38
.= c1 * b2 by POLYNOM5:38;
2 in dom r by B4,TARSKI:def 2;
then r.2 = p1.(2-'1) * p2.(1+1-'2) by C,B1
.= p1.1 * p2.0 by K,NAT_2:8
.= b1 * p2.0 by POLYNOM5:38
.= b1 * c2 by POLYNOM5:38;
then Sum r = c1 * b2 + b1 * c2 by B3,B5,RLVECT_1:45
.= b1 * c2 + b2 * c1 by GROUP_1:def 12;
hence (p1*'p2).o = q.o by B1,C,qua1;
end;
suppose C: i = 2;
then B3: r = <*r.1,r.2,r.3*> by B1,FINSEQ_1:45;
B4: dom r = Seg 3 by B1,C,FINSEQ_1:def 3
.= Seg 2 \/ {2+1} by FINSEQ_1:9
.= {1,2,3} by FINSEQ_1:2,ENUMSET1:3;
then 1 in dom r by ENUMSET1:def 1;
then B5: r.1 = p1.(1-'1) * p2.(2+1-'1) by C,B1
.= p1.0 * p2.2 by K,NAT_2:8
.= p1.0 * 0.F by POLYNOM5:38;
2 in dom r by B4,ENUMSET1:def 1;
then B6: r.2 = p1.1 * p2.1 by K,C,B1
.= b1 * p2.1 by POLYNOM5:38
.= b1 * b2 by POLYNOM5:38;
3 in dom r by B4,ENUMSET1:def 1;
then r.3 = p1.2 * p2.(2+1-'3) by K,C,B1
.= 0.F * p2.(2+1-'3) by POLYNOM5:38;
then Sum r = 0.F + b1 * b2 + 0.F by B3,B5,B6,RLVECT_1:46;
hence (p1*'p2).o = q.o by B1,C,qua1;
end;
suppose C: i > 2;
D: len q <= 3 by qua2;
C1: i >= 2 + 1 by C,NAT_1:13;
then E: q.i = 0.F by D,XXREAL_0:2,ALGSEQ_1:8;
len p1 <= 2 & len p2 <= 2 by POLYNOM5:39;
then len p1 + len p2 <= 2 + 2 by XREAL_1:7;
then F: len p1 + len p2 -' 1 <= 2 + 2 -' 1 by lemmonus;
len(p1*'p2) <= len p1 + len p2 -' 1 by leng;
then len(p1*'p2) <= 2 + 2 -' 1 by F,XXREAL_0:2;
hence (p1*'p2).o = q.o by J,C1,XXREAL_0:2,E,ALGSEQ_1:8;
end;
end;
hence thesis by A;
end;
lemred3:
for F being Field
for c1,c2 being Element of F
holds <%-c1,1.F%> *' <%-c2,1.F%> = <%c1*c2,-(c1+c2),1.F%>
proof
let F be Field; let c1,c2 be Element of F;
thus <%-c1,1.F%> *' <%-c2,1.F%>
= <%(-c1)*(-c2),(1.F)*(-c2)+(1.F)*(-c1),(1.F)*(1.F)%> by lemred1
.= <%c1*c2,(-c2)+(-c1),1.F%> by VECTSP_1:10
.= <%c1*c2,-(c1+c2),1.F%> by RLVECT_1:31;
end;
lemred3z:
for F being Field
for c1,c2 being Element of F
holds rpoly(1,c1) *' rpoly(1,c2) = <%c1*c2,-(c1+c2),1.F%>
proof
let F be Field; let c1,c2 be Element of F;
thus rpoly(1,c1) *' rpoly(1,c2)
= <%-c1,1.F%> *' rpoly(1,c2) by RING_5:10
.= <%-c1,1.F%> *' <%-c2,1.F%> by RING_5:10
.= <%c1*c2,-(c1+c2),1.F%> by lemred3;
end;
theorem lemeval:
for F being non 2-characteristic Field
for a being non zero Element of F, b,c being Element of F
for w being Element of F st w^2 = b^2 - 4 '*' a * c
holds eval(<%c,b,a%>,(-b + w) * (2 '*' a)") = 0.F &
eval(<%c,b,a%>,(-b - w) * (2 '*' a)") = 0.F
proof
let F be non 2-characteristic Field;
let a be non zero Element of F, b,c be Element of F;
let w be Element of F;
set r1 = (-b + w) * (2 '*' a)";
assume AS: w^2 = b^2 - 4 '*' a * c;
Char F <> 2 by RING_3:def 6; then
I: 2 '*' 1.F <> 0.F by REALALG2:24;
H: now assume 4 '*' a = 0.F;
then 0.F = (2 * 2) '*' a
.= 2 '*' (2 '*' (1.F * a)) by RING_3:65
.= 2 '*' ((2 '*' 1.F) * a) by REALALG2:5
.= 2 '*' (a * (2 '*' 1.F)) by GROUP_1:def 12
.= (2 '*' a) * (2 '*' 1.F) by REALALG2:5;
then 2 '*' a = 0.F by I,VECTSP_2:def 1;
hence contradiction by ch2;
end; then
L: 2 '*' a <> 0.F & 4 '*' a <> 0.F by ch2;
(2 '*' a) * r1 = (2 '*' a) * ((2 '*' a)" * (-b + w)) by GROUP_1:def 12
.= ((2 '*' a) * (2 '*' a)") * (-b + w) by GROUP_1:def 3
.= ((2 '*' a)" * (2 '*' a)) * (-b + w) by GROUP_1:def 12
.= 1.F * (-b + w) by L,VECTSP_1:def 10; then
b + 2 '*' a * r1 = (b + -b) + w by RLVECT_1:def 3
.= 0.F + w by RLVECT_1:5; then
b^2 - 4 '*' a * c
= (2'*'a*r1)^2 + 2'*'(2'*'a*r1)*b + b^2 by AS,REALALG2:7
.= (2'*'a*r1)^2 + (2'*'(2'*'(a*r1)))*b + b^2 by REALALG2:5
.= (2'*'a*r1)^2 + ((2*2)'*'(a*r1))*b + b^2 by RING_3:65
.= (2'*'a*r1)^2 + 4'*'a*r1*b + b^2 by REALALG2:5; then
(b^2 + -4 '*' a * c) - b^2
= (2'*'a*r1)^2 + 4'*'a*r1*b + (b^2 - b^2) by RLVECT_1:def 3
.= (2'*'a*r1)^2 + 4'*'a*r1*b + 0.F by RLVECT_1:15; then
(2'*'a*r1)^2 + 4'*'a*r1*b
= -4 '*' a * c + (b^2 + -b^2) by RLVECT_1:def 3
.= - 4 '*' a * c + 0.F by RLVECT_1:5; then
0.F = (2'*'a*r1)^2 + 4'*'a*r1*b + 4'*'a*c by RLVECT_1:5
.= (2'*'a)^2 * r1^2 + 4'*'a*r1*b + 4'*'a*c by ch0
.= ((2^2) '*' a^2) * r1^2 + 4'*'a*r1*b + 4'*'a*c by ch1
.= ((2*2) '*' a^2) * r1^2 + 4'*'a*r1*b + 4'*'a*c by SQUARE_1:def 1
.= (4 '*' (a * a)) * r1^2 + 4'*'a*r1*b + 4'*'a*c by O_RING_1:def 1
.= ((4 '*' a) * a) * r1^2 + 4'*'a*r1*b + 4'*'a*c by REALALG2:5
.= (4 '*' a) * (a * r1^2) + (4'*'a)*r1*b + (4'*'a)*c by GROUP_1:def 3
.= ((4 '*' a) * (a * r1^2) + (4'*'a)*(r1*b)) + (4'*'a)*c by GROUP_1:def 3
.= (4 '*' a) * (a * r1^2 + r1*b) + (4'*'a)*c by VECTSP_1:def 2
.= (4 '*' a) * ((a * r1^2 + r1*b) + c) by VECTSP_1:def 2; then
E: 0.F = ((a * r1^2) + r1*b) + c by H,VECTSP_2:def 1
.= a * r1^2 + b * r1 + c by GROUP_1:def 12;
thus eval(<%c,b,a%>,r1)
= c + b * r1 + a * r1^2 by evalq
.= 0.F by E,RLVECT_1:def 3;
set r1 = (-b - w) * (2 '*' a)";
J: (-w)^2 = (-w) * (-w) by O_RING_1:def 1
.= w * w by VECTSP_1:10
.= w^2 by O_RING_1:def 1;
(2 '*' a) * r1 = (2 '*' a) * ((2 '*' a)" * (-b - w)) by GROUP_1:def 12
.= ((2 '*' a) * (2 '*' a)") * (-b - w) by GROUP_1:def 3
.= ((2 '*' a)" * (2 '*' a)) * (-b - w) by GROUP_1:def 12
.= 1.F * (-b - w) by L,VECTSP_1:def 10; then
b + 2 '*' a * r1 = (b + -b) - w by RLVECT_1:def 3
.= 0.F - w by RLVECT_1:5; then
b^2 - 4 '*' a * c
= (2'*'a*r1)^2 + 2'*'(2'*'a*r1)*b + b^2 by J,AS,REALALG2:7
.= (2'*'a*r1)^2 + (2'*'(2'*'(a*r1)))*b + b^2 by REALALG2:5
.= (2'*'a*r1)^2 + ((2*2)'*'(a*r1))*b + b^2 by RING_3:65
.= (2'*'a*r1)^2 + 4'*'a*r1*b + b^2 by REALALG2:5; then
(b^2 + -4 '*' a * c) - b^2
= (2'*'a*r1)^2 + 4'*'a*r1*b + (b^2 - b^2) by RLVECT_1:def 3
.= (2'*'a*r1)^2 + 4'*'a*r1*b + 0.F by RLVECT_1:15; then
(2'*'a*r1)^2 + 4'*'a*r1*b
= -4 '*' a * c + (b^2 + -b^2) by RLVECT_1:def 3
.= - 4 '*' a * c + 0.F by RLVECT_1:5; then
0.F = (2'*'a*r1)^2 + 4'*'a*r1*b + 4'*'a*c by RLVECT_1:5
.= (2'*'a)^2 * r1^2 + 4'*'a*r1*b + 4'*'a*c by ch0
.= ((2^2) '*' a^2) * r1^2 + 4'*'a*r1*b + 4'*'a*c by ch1
.= ((2*2) '*' a^2) * r1^2 + 4'*'a*r1*b + 4'*'a*c by SQUARE_1:def 1
.= (4 '*' (a * a)) * r1^2 + 4'*'a*r1*b + 4'*'a*c by O_RING_1:def 1
.= ((4 '*' a) * a) * r1^2 + 4'*'a*r1*b + 4'*'a*c by REALALG2:5
.= (4 '*' a) * (a * r1^2) + (4'*'a)*r1*b + (4'*'a)*c by GROUP_1:def 3
.= ((4 '*' a) * (a * r1^2) + (4'*'a)*(r1*b)) + (4'*'a)*c by GROUP_1:def 3
.= (4 '*' a) * (a * r1^2 + r1*b) + (4'*'a)*c by VECTSP_1:def 2
.= (4 '*' a) * ((a * r1^2 + r1*b) + c) by VECTSP_1:def 2; then
E: 0.F = ((a * r1^2) + r1*b) + c by H,VECTSP_2:def 1
.= a * r1^2 + b * r1 + c by GROUP_1:def 12;
thus eval(<%c,b,a%>,r1)
= c + b * r1 + a * r1^2 by evalq
.= 0.F by E,RLVECT_1:def 3;
end;
theorem lemeval2:
for F being Field
for a being non zero Element of F, b,c being Element of F
st Roots <%c,b,a%> <> {} holds b^2 - 4 '*' a * c is square
proof
let F be Field;
let a be non zero Element of F, b,c be Element of F;
set p = <%c,b,a%>, r = the Element of Roots <%c,b,a%>;
assume AS: Roots <%c,b,a%> <> {}; then
r in Roots p; then
reconsider r as Element of F;
r is_a_root_of p by AS,POLYNOM5:def 10; then
0.F = c + b * r + a * r^2 by evalq
.= a * r^2 + b * r + c by RLVECT_1:def 3
.= a * r^2 + r * b + c by GROUP_1:def 12; then
0.F = (4 '*' a) * (a * r^2 + r*b + c)
.= (4 '*' a) * (a * r^2 + r*b) + (4'*'a)*c by VECTSP_1:def 2
.= ((4 '*' a) * (a * r^2) + (4'*'a)*(r*b)) + (4'*'a)*c by VECTSP_1:def 2
.= (4 '*' a) * (a * r^2) + (4'*'a)*r*b + (4'*'a)*c by GROUP_1:def 3
.= ((4 '*' a) * a) * r^2 + 4'*'a*r*b + 4'*'a*c by GROUP_1:def 3
.= (4 '*' (a * a)) * r^2 + 4'*'a*r*b + 4'*'a*c by REALALG2:5
.= ((2*2) '*' a^2) * r^2 + 4'*'a*r*b + 4'*'a*c by O_RING_1:def 1
.= ((2^2) '*' a^2) * r^2 + 4'*'a*r*b + 4'*'a*c by SQUARE_1:def 1
.= (2'*'a)^2 * r^2 + 4'*'a*r*b + 4'*'a*c by ch1
.= (2'*'a*r)^2 + 4'*'a*r*b + 4'*'a*c by ch0; then
- 4'*'a*c = (2'*'a*r)^2 + 4'*'a*r*b + 4'*'a*c - 4'*'a*c
.= (2'*'a*r)^2 + 4'*'a*r*b + (4'*'a*c - 4'*'a*c) by RLVECT_1:def 3
.= (2'*'a*r)^2 + 4'*'a*r*b + 0.F by RLVECT_1:15; then
b^2 + -4'*'a*c = (2'*'a*r)^2 + ((2*2)'*'(a*r))*b + b^2 by REALALG2:5
.= (2'*'a*r)^2 + (2'*'(2'*'(a*r)))*b + b^2 by RING_3:65
.= (2'*'a*r)^2 + (2'*'(2'*'a*r))*b + b^2 by REALALG2:5
.= (2'*'a*r + b)^2 by REALALG2:7;
hence thesis;
end;
theorem TC0:
for F being non 2-characteristic Field
for a being non zero Element of F,
b,c being Element of F
for w being Element of F st w^2 = b^2 - 4 '*' a * c
holds Roots <%c,b,a%> = { (-b + w) * (2 '*' a)", (-b - w) * (2 '*' a)" }
proof
let F be non 2-characteristic Field; let a be non zero Element of F;
let b,c be Element of F; let w be Element of F;
reconsider p = <%c,b,a%> as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
set r1 = (-b + w) * (2 '*' a)", r2 = (-b - w) * (2 '*' a)";
assume AS: w^2 = b^2 - 4 '*' a * c;
L: 2 '*' a <> 0.F by ch2;
C: now let o be object;
assume C1: o in Roots p; then
reconsider r = o as Element of F;
r is_a_root_of p by C1,POLYNOM5:def 10; then
0.F = c + b * r + a * r^2 by evalq
.= a * r^2 + b * r + c by RLVECT_1:def 3
.= a * r^2 + r * b + c by GROUP_1:def 12; then
0.F = (4 '*' a) * (a * r^2 + r*b + c)
.= (4 '*' a) * (a * r^2 + r*b) + (4'*'a)*c by VECTSP_1:def 2
.= ((4 '*' a) * (a * r^2) + (4'*'a)*(r*b)) + (4'*'a)*c by VECTSP_1:def 2
.= (4 '*' a) * (a * r^2) + (4'*'a)*r*b + (4'*'a)*c by GROUP_1:def 3
.= ((4 '*' a) * a) * r^2 + 4'*'a*r*b + 4'*'a*c by GROUP_1:def 3
.= (4 '*' (a * a)) * r^2 + 4'*'a*r*b + 4'*'a*c by REALALG2:5
.= ((2*2) '*' a^2) * r^2 + 4'*'a*r*b + 4'*'a*c by O_RING_1:def 1
.= ((2^2) '*' a^2) * r^2 + 4'*'a*r*b + 4'*'a*c by SQUARE_1:def 1
.= (2'*'a)^2 * r^2 + 4'*'a*r*b + 4'*'a*c by ch1
.= (2'*'a*r)^2 + 4'*'a*r*b + 4'*'a*c by ch0; then
- 4'*'a*c = (2'*'a*r)^2 + 4'*'a*r*b + 4'*'a*c - 4'*'a*c
.= (2'*'a*r)^2 + 4'*'a*r*b + (4'*'a*c - 4'*'a*c) by RLVECT_1:def 3
.= (2'*'a*r)^2 + 4'*'a*r*b + 0.F by RLVECT_1:15; then
b^2 + -4'*'a*c = (2'*'a*r)^2 + ((2*2)'*'(a*r))*b + b^2 by REALALG2:5
.= (2'*'a*r)^2 + (2'*'(2'*'(a*r)))*b + b^2 by RING_3:65
.= (2'*'a*r)^2 + (2'*'(2'*'a*r))*b + b^2 by REALALG2:5
.= (2'*'a*r + b)^2 by REALALG2:7;
then per cases by AS,REALALG2:10;
suppose w = 2'*'a*r + b; then
-b + w = 2'*'a*r + (b + -b) by RLVECT_1:def 3
.= 2'*'a*r + 0.F by RLVECT_1:5
.= (2'*'a)*r; then
(2'*'a)" * (-b + w) = ((2'*'a)" * (2'*'a)) * r by GROUP_1:def 3
.= 1.F * r by L,VECTSP_1:def 10; then
r = (-b + w) * (2 '*' a)" by GROUP_1:def 12;
hence o in { r1, r2 } by TARSKI:def 2;
end;
suppose w = -(2'*'a*r + b); then
-b + -w = 2'*'a*r + (b + -b) by RLVECT_1:def 3
.= 2'*'a*r + 0.F by RLVECT_1:5
.= (2'*'a)*r;then
(2'*'a)" * (-b + -w) = ((2'*'a)" * (2'*'a)) * r by GROUP_1:def 3
.= 1.F * r by L,VECTSP_1:def 10; then
r = (-b - w) * (2 '*' a)" by GROUP_1:def 12;
hence o in { r1, r2 } by TARSKI:def 2;
end;
end;
now let o be object;
assume o in { r1, r2 }; then
per cases by TARSKI:def 2;
suppose D: o = r1;
r1 is_a_root_of p by AS,lemeval;
hence o in Roots p by D,POLYNOM5:def 10;
end;
suppose D: o = r2;
r2 is_a_root_of p by AS,lemeval;
hence o in Roots p by D,POLYNOM5:def 10;
end;
end;
hence thesis by C,TARSKI:2;
end;
theorem lemred:
for F being non 2-characteristic Field
for a being non zero Element of F,
b,c being Element of F
for w being Element of F st w^2 = b^2 - 4 '*' a * c
for r1,r2 being Element of F
st r1 = (-b + w) * (2 '*' a)" & r2 = (-b - w) * (2 '*' a)"
holds <%c,b,a%> = a * (X-r1) *' (X-r2)
proof
let F be non 2-characteristic Field;
let a be non zero Element of F, b,c being Element of F;
let w be Element of F;
assume AS1: w^2 = b^2 - 4 '*' a * c;
let r1,r2 be Element of F;
assume AS2: r1 = (-b+w) * (2'*'a)" & r2 = (-b-w) * (2'*'a)";
rpoly(1,r1) *' rpoly(1,r2) = <%r1*r2,-(r1+r2),1.F%> by lemred3z; then
A: <%a*(r1*r2),a*(-(r1+r2)),a*1.F%> = a * rpoly(1,r1)*'rpoly(1,r2) by qua6;
Char F <> 2 by RING_3:def 6; then
I: 2 '*' 1.F <> 0.F by REALALG2:24;
L: now assume 4 '*' a = 0.F;
then 0.F = (2 * 2) '*' a
.= 2 '*' (2 '*' (1.F * a)) by RING_3:65
.= 2 '*' ((2 '*' 1.F) * a) by REALALG2:5
.= 2 '*' (a * (2 '*' 1.F)) by GROUP_1:def 12
.= (2 '*' a) * (2 '*' 1.F) by REALALG2:5;
then 2 '*' a = 0.F by I,VECTSP_2:def 1;
hence contradiction by ch2;
end; then
M: 2 '*' a <> 0.F & 4 '*' a <> 0.F & a <> 0.F by ch2;
B: a*(r1*r2) = c
proof
((-b+w) * (2'*'a)") * ((-b-w) * (2'*'a)")
= ((2'*'a)" * (-b+w)) * ((-b-w) * (2'*'a)") by GROUP_1:def 12
.= (2'*'a)" * ((-b+w) * ((-b-w) * (2'*'a)")) by GROUP_1:def 3
.= (2'*'a)" * (((-b+w) * (-b-w)) * (2'*'a)") by GROUP_1:def 3
.= (2'*'a)" * ((2'*'a)" * ((-b+w) * (-b-w))) by GROUP_1:def 12
.= ((2'*'a)" * (2'*'a)") * ((-b+w) * (-b-w)) by GROUP_1:def 3
.= ((2'*'a) * (2'*'a))" * ((-b+w) * (-b-w)) by M,VECTSP_2:11
.= (2'*'(a * (2'*'a)))" * ((-b+w) * (-b-w)) by REALALG2:5
.= (2'*'((2'*'a)*a))" * ((-b+w) * (-b-w)) by GROUP_1:def 12
.= (2'*'(2 '*' (a*a)))" * ((-b+w) * (-b-w)) by REALALG2:5
.= ((2*2) '*' (a*a))" * ((-b+w) * (-b-w)) by RING_3:65
.= (4 '*' (a*a))" * ((-b)^2 - (b^2 - 4 '*' a * c)) by AS1,REALALG2:9
.= (4 '*' (a*a))" * ((-b)*(-b) - (b^2 - 4 '*' a * c)) by O_RING_1:def 1
.= (4 '*' (a*a))" * (b*b - (b^2 - 4 '*' a * c)) by VECTSP_1:10
.= (4 '*' (a*a))" * (b^2 - (b^2 - 4 '*' a * c)) by O_RING_1:def 1
.= (4 '*' (a*a))" * ((b^2 - b^2) + 4 '*' a * c) by RLVECT_1:29
.= (4 '*' (a*a))" * (0.F + 4 '*' a * c) by RLVECT_1:15
.= ((4 '*' a)*a)" * (4 '*' a * c) by REALALG2:5
.= (a" * (4 '*' a)") * ((4 '*' a) * c) by L,VECTSP_2:11
.= a" * ((4 '*' a)" * ((4 '*' a) * c)) by GROUP_1:def 3
.= a" * (((4 '*' a)" * (4 '*' a)) * c) by GROUP_1:def 3
.= a" * (1.F * c) by L,VECTSP_1:def 10;
hence a*(r1*r2) = (a * a") * c by AS2,GROUP_1:def 3
.= (a" * a) * c by GROUP_1:def 12
.= 1.F * c by I,VECTSP_1:def 10
.= c;
end;
a*(-(r1+r2)) = b
proof
per cases;
suppose C0: b = 0.F;
((-b+w) * (2'*'a)") + ((-b-w) * (2'*'a)")
= (w + -w) * (2'*'a)" by C0,VECTSP_1:def 3
.= 0.F * ((2'*'a)") by RLVECT_1:5;
hence thesis by C0,AS2;
end;
suppose C1: b <> 0.F;
0.F = - 0.F; then
-b <> 0.F by C1; then
C: 2 '*' (-b) <> 0.F by ch2;
((-b+w) * (2'*'a)") + ((-b-w) * (2'*'a)")
= ((-b+w) + (-b-w)) * ((2'*'a)") by VECTSP_1:def 3
.= (-b + (w + (-b + -w))) * ((2'*'a)") by RLVECT_1:def 3
.= (-b + ((w + -w) + -b)) * ((2'*'a)") by RLVECT_1:def 3
.= (-b + (0.F + -b)) * ((2'*'a)") by RLVECT_1:5
.= (2 '*' (-b)) * ((2'*'a)") by RING_5:2
.= (-b) * a" by M,C,ch0a;
then -(r1+r2) = (--b) * a" by AS2,VECTSP_1:9;
hence a*(-(r1+r2)) = a * (a" * b) by GROUP_1:def 12
.= (a * a") * b by GROUP_1:def 3
.= (a" * a) * b by GROUP_1:def 12
.= 1.F * b by I,VECTSP_1:def 10
.= b;
end;
end;
hence thesis by A,B;
end;
definition
let R be non degenerated Ring;
let p be quadratic Polynomial of R;
func Discriminant p -> Element of R means :defDC:
ex a being non zero Element of R, b,c being Element of R
st p = <%c,b,a%> & it = b^2 - 4 '*' a * c;
existence
proof
consider a being non zero Element of R, b,c being Element of R
such that H: p = <%c,b,a%> by qua5;
b^2 - 4 '*' a * c is Element of R;
hence thesis by H;
end;
uniqueness
proof
let x,y be Element of R;
assume that
A1: ex a1 being non zero Element of R, b1,c1 being Element of R
st p = <%c1,b1,a1%> & x = b1^2 - 4 '*' a1 * c1 and
A2: ex a2 being non zero Element of R, b2,c2 being Element of R
st p = <%c2,b2,a2%> & y = b2^2 - 4 '*' a2 * c2;
consider a1 being non zero Element of R, b1,c1 being Element of R
such that A3: p = <%c1,b1,a1%> & x = b1^2 - 4 '*' a1 * c1 by A1;
consider a2 being non zero Element of R, b2,c2 being Element of R
such that A4: p = <%c2,b2,a2%> & y = b2^2 - 4 '*' a2 * c2 by A2;
A5: a1 = <%c2,b2,a2%>.2 by A3,A4,qua1 .= a2 by qua1;
A6: b1 = <%c2,b2,a2%>.1 by A3,A4,qua1 .= b2 by qua1;
c1 = <%c2,b2,a2%>.0 by A3,A4,qua1 .= c2 by qua1;
hence thesis by A5,A6,A3,A4;
end;
end;
notation
let R be non degenerated Ring;
let p be quadratic Polynomial of R;
synonym DC p for Discriminant p;
end;
definition
let R be non degenerated Ring;
let p be monic quadratic Polynomial of R;
redefine func Discriminant p means :defDCm: :: redefines Discriminant (FIELD_9, definition)
ex b,c being Element of R st p = <%c,b,1.R%> & it = b^2 - 4 '*' c;
compatibility
proof
Y: now let x be Element of R;
assume x = DC p; then
consider a being non zero Element of R, b,c being Element of R such that
A: p = <%c,b,a%> & x = b^2 - 4 '*' a * c by defDC;
H: len p = 3 by A,qua3;
3 -' 1 = 3 - 1 by XREAL_0:def 2; then
a = p.(len p -' 1) by H,A,qua1 .= LC p by RATFUNC1:def 6; then
B: a = 1.R by RATFUNC1:def 7; then
b^2 - 4 '*' a * c = b^2 - 4 '*' (1.R * c) by REALALG2:5;
hence ex b,c being Element of R
st p = <%c,b,1.R%> & x = b^2 - 4 '*' c by A,B;
end;
now let x be Element of R;
assume ex b,c being Element of R
st p = <%c,b,1.R%> & x = b^2 - 4 '*' c; then
consider b,c being Element of R such that
C: p = <%c,b,1.R%> & x = b^2 - 4 '*' c;
4 '*' 1.R * c = 4 '*' (1.R * c) by REALALG2:5;
hence x = DC p by C,defDC;
end;
hence thesis by Y;
end;
end;
definition
let R be non degenerated Ring;
let p be monic purely_quadratic Polynomial of R;
redefine func Discriminant p means :defDCpq: :: redefines Discriminant (FIELD_9, redefinition) → Discriminant (FIELD_9, definition)
ex c being Element of R st p = <%c,0.R,1.R%> & it = - 4 '*' c;
compatibility
proof
consider a1 being non zero Element of R,
c1 being Element of R such that H: p = <%c1,0.R,a1%> by defpur;
Y: now let x be Element of R;
assume x = DC p; then
consider b,c being Element of R such that
A: p = <%c,b,1.R%> & x = b^2 - 4 '*' c by defDCm;
B: b = <%c1,0.R,a1%>.1 by A,H,qua1 .= 0.R by qua1;
thus ex c being Element of R
st p = <%c,0.R,1.R%> & x = - 4 '*' c by A,B;
end;
now let x be Element of R;
assume ex c being Element of R
st p = <%c,0.R,1.R%> & x = - 4 '*' c; then
consider c being Element of R such that
C: p = <%c,0.R,1.R%> & x = - 4 '*' c;
- 4 '*' c = (0.R)^2 - 4 '*' (1.R * c);
hence x = DC p by C,defDCm;
end;
hence thesis by Y;
end;
end;
theorem TC1:
for F being non 2-characteristic Field,
p being quadratic Polynomial of F holds Roots p <> {} iff DC p is square
proof
let F be non 2-characteristic Field, p be quadratic Polynomial of F;
consider a being non zero Element of F, b,c being Element of F such that
A: p = <%c,b,a%> by qua5;
B: now assume DC p is square; then
b^2 - 4 '*' a * c is being_a_square by A,defDC; then
consider w being Element of F such that
B1: b^2 - 4 '*' a * c = w^2 by O_RING_1:def 2;
(-b + w) * (2 '*' a)" is_a_root_of p by A,B1,lemeval;
hence Roots p <> {} by POLYNOM5:def 10;
end;
now assume Roots p <> {};
then b^2 - 4 '*' a * c is square by A,lemeval2;
hence DC p is square by A,defDC;
end;
hence thesis by B;
end;
theorem
for F being non 2-characteristic Field,
p being quadratic Polynomial of F holds card(Roots p) = 1 iff DC p = 0.F
proof
let F be non 2-characteristic Field, p be quadratic Polynomial of F;
consider a being non zero Element of F, b,c being Element of F such that
A: p = <%c,b,a%> by qua5;
set r = the Element of Roots p;
B: now assume DC p = 0.F; then
B0: b^2 - 4 '*' a * c = 0.F by A,defDC; then
consider w being Element of F such that
B1: b^2 - 4 '*' a * c = w^2 by O_RING_1:def 2;
B2: Roots p = { (-b + w) * (2 '*' a)", (-b - w) * (2 '*' a)" } by B1,A,TC0;
0.F = w * w by B0,B1,O_RING_1:def 1; then
w = 0.F by VECTSP_2:def 1; then
Roots p = { (-b + w) * (2 '*' a)" } by B2,ENUMSET1:29;
hence card(Roots p) = 1 by CARD_1:30;
end;
L: 2 '*' a <> 0.F by ch2;
now assume B0: card(Roots p) = 1;
then Roots p <> {};
then DC p is square by TC1;
then b^2 - 4 '*' a * c is square by A,defDC; then
consider w being Element of F such that
B1: b^2 - 4 '*' a * c = w^2 by O_RING_1:def 2;
B2: Roots p = { (-b + w) * (2 '*' a)", (-b - w) * (2 '*' a)" } by B1,A,TC0;
(-b + w) * (2 '*' a)" = (-b - w) * (2 '*' a)" by B0,B2,CARD_2:57;
then ((-b + w) * (2 '*' a)") * (2 '*' a)
= (-b - w) * ((2 '*' a)" * (2 '*' a)) by GROUP_1:def 3
.= (-b - w) * 1.F by L,VECTSP_1:def 10;
then - b - w = (-b + w) * ((2 '*' a)" * (2 '*' a) ) by GROUP_1:def 3
.= (-b + w) * 1.F by L,VECTSP_1:def 10;
then b + ((-b) - w) = (b + (-b)) + w by RLVECT_1:def 3
.= 0.F + w by RLVECT_1:5;
then w = (b + (-b)) + -w by RLVECT_1:def 3 .= 0.F + -w by RLVECT_1:5;
then w + w = 0.F by RLVECT_1:5;
then 2 '*' w = 0.F by RING_5:2;
then w = 0.F by ch2;
hence DC p = 0.F by B1,A,defDC;
end;
hence thesis by B;
end;
theorem
for F being non 2-characteristic Field,
p being quadratic Polynomial of F
holds card(Roots p) = 2 iff DC p is non zero square
proof
let F be non 2-characteristic Field, p be quadratic Polynomial of F;
consider a being non zero Element of F, b,c being Element of F such that
A: p = <%c,b,a%> by qua5;
L: 2 '*' a <> 0.F by ch2;
B: now assume B0: card(Roots p) = 2;
then Roots p <> {};
then DC p is square by TC1;
then b^2 - 4 '*' a * c is square by A,defDC; then
consider w being Element of F such that
B1: b^2 - 4 '*' a * c = w^2 by O_RING_1:def 2;
B2: Roots p = { (-b + w) * (2 '*' a)", (-b - w) * (2 '*' a)" } by B1,A,TC0;
B3: now assume (-b + w) * (2'*'a)" = (-b - w) * (2'*'a)";
then Roots p = { (-b + w) * (2 '*' a)" } by B2,ENUMSET1:29;
hence contradiction by B0,CARD_2:42;
end;
now assume b^2 - 4 '*' a * c = 0.F;
then w * w = 0.F by B1,O_RING_1:def 1;
then w = 0.F by VECTSP_2:def 1;
hence contradiction by B3;
end;
hence DC p is non zero square by A,defDC,B1;
end;
now assume C0: DC p is non zero square;
then b^2 - 4 '*' a * c is square by A,defDC;
then consider w being Element of F such that
C1: w^2 = b^2 - 4 '*' a * c by O_RING_1:def 2;
C2: Roots <%c,b,a%> = {(-b + w) * (2'*'a)",(-b - w) * (2'*'a)"} by C1,TC0;
now assume (-b + w) * (2'*'a)" = (-b - w) * (2'*'a)";
then ((-b + w) * (2 '*' a)") * (2 '*' a)
= (-b - w) * ((2 '*' a)" * (2 '*' a)) by GROUP_1:def 3
.= (-b - w) * 1.F by L,VECTSP_1:def 10;
then - b - w = (-b + w) * ((2 '*' a)" * (2 '*' a) ) by GROUP_1:def 3
.= (-b + w) * 1.F by L,VECTSP_1:def 10;
then b + ((-b) - w) = (b + (-b)) + w by RLVECT_1:def 3
.= 0.F + w by RLVECT_1:5;
then w = (b + (-b)) + -w by RLVECT_1:def 3 .= 0.F + -w by RLVECT_1:5;
then w + w = 0.F by RLVECT_1:5;
then 2 '*' w = 0.F by RING_5:2;
then w = 0.F by ch2;
hence contradiction by C0,C1,A,defDC;
end;
hence card(Roots p) = 2 by A,C2,CARD_2:57;
end;
hence thesis by B;
end;
theorem naH:
for F being non 2-characteristic Field
for p being quadratic Element of the carrier of Polynom-Ring F
holds p is reducible iff DC p is square
proof
let F be non 2-characteristic Field;
let p be quadratic Element of the carrier of Polynom-Ring F;
consider a being non zero Element of F, b,c being Element of F such that
H0: p = <%c,b,a%> by qua5;
Z:now assume DC p is square;
then consider w being Element of F such that
A: w^2 = DC p by O_RING_1:def 2;
A1: DC p = b^2 - 4 '*' a * c by H0,defDC;
set r1 = (-b + w) * (2 '*' a)", r2 = (-b - w) * (2 '*' a)";
set q1 = X-r1, q2 = X-r2;
reconsider qq1 = q1, qq2 = a * q2, p1 = p as Element of Polynom-Ring F
by POLYNOM3:def 10;
p = a * (q1 *' q2) by H0,A,A1,lemred
.= q1 *' (a * q2) by RING_4:10
.= qq1 * qq2 by POLYNOM3:def 10; then
B: qq1 divides p1 by GCD_1:def 1;
C: deg q1 = 1 by HURWITZ:27;
deg p = 2 by defquadr;
hence p is reducible by C,B,RING_4:40,RING_4:def 3;
end;
now assume Y: p is reducible;
p <> 0_.(F) & p is non unital; then
consider q being Element of the carrier of Polynom-Ring F such that
A: q divides p & 1 <= deg q & deg q < deg p by Y,RING_4:41;
reconsider pp = p, qq = q as Polynomial of F;
consider rr being Polynomial of F such that
B: pp = qq *' rr by A,RING_4:1;
reconsider degq = deg q as Element of NAT by A,INT_1:3;
E: deg p = 2 by defquadr;
degq < 1 + 1 by A,defquadr; then
E0: degq >= 1 & degq <= 1 by A,NAT_1:13; then
E0a: degq = 1 by XXREAL_0:1;
consider x1,c1 being Element of F such that
E1: x1 <> 0.F & q = x1 * rpoly(1,c1) by E0,XXREAL_0:1,HURWITZ:28;
E2: qq <> 0_.(F) by A,HURWITZ:20;
rr <> 0_.(F) by B; then
deg qq + deg rr = 2 by B,E,E2,HURWITZ:23; then
consider x2,c2 being Element of F such that
E3: x2 <> 0.F & rr = x2 * rpoly(1,c2) by E0a,HURWITZ:28;
reconsider x = x1 * x2 as non zero Element of F
by E3,E1,VECTSP_2:def 1,STRUCT_0:def 12;
qq *' rr
= x2 * (rpoly(1,c2) *' (x1 * rpoly(1,c1))) by E1,E3,RATFUNC1:6
.= x2 * (x1 * (rpoly(1,c2) *' rpoly(1,c1))) by RATFUNC1:6
.= (x2 * x1) * (rpoly(1,c2) *' rpoly(1,c1)) by RING_4:11
.= x * (rpoly(1,c2) *' rpoly(1,c1)) by GROUP_1:def 12
.= x * <%c1*c2,-(c1+c2),1.F%> by lemred3z
.= <%x*(c1*c2),x*(-(c1+c2)),x*1.F%> by qua6;
then DC p
= (x*(-(c1+c2)))^2 - 4 '*' x * (x*(c1*c2)) by B,defDC
.= (x*(-c1+-c2))^2 - 4 '*' x * (x*(c1*c2)) by RLVECT_1:31
.= (x*(-c1)+x*(-c2))^2 - 4 '*' x * (x*(c1*c2)) by VECTSP_1:def 2
.= ((x*(-c1))^2 + 2 '*' (x*(-c1)) * (x*(-c2)) + (x*(-c2))^2)
- 4 '*' x * (x*(c1*c2)) by REALALG2:7
.= ((x*(-c1))^2 + 2 '*' ((x*(-c1)) * (x*(-c2))) + (x*(-c2))^2)
- 4 '*' x * (x*(c1*c2)) by REALALG2:5
.= ((x*(-c1))^2 + 2 '*' (x*((-c1) * (x*(-c2)))) + (x*(-c2))^2)
- 4 '*' x * (x*(c1*c2)) by GROUP_1:def 3
.= ((x*(-c1))^2 + 2 '*' (x*((x*(-c2)) * (-c1))) + (x*(-c2))^2)
- 4 '*' x * (x*(c1*c2)) by GROUP_1:def 12
.= ((x*(-c1))^2 + 2 '*' (x*(x*((-c2) * (-c1)))) + (x*(-c2))^2)
- 4 '*' x * (x*(c1*c2)) by GROUP_1:def 3
.= ((x*(-c1))^2 + 2 '*' (x*(x*(c2 * c1))) + (x*(-c2))^2)
- 4 '*' x * (x*(c1*c2)) by VECTSP_1:10
.= ((x*(-c1))^2 + 2 '*' (x*(x*(c1 * c2))) + (x*(-c2))^2)
- 4 '*' x * (x*(c1*c2)) by GROUP_1:def 12
.= (((x*(-c1))^2 + 2 '*' (x*(x*(c1 * c2)))) +
-(4 '*' x * (x*(c1*c2)))) + (x*(-c2))^2 by RLVECT_1:def 3
.= ((x*(-c1))^2 + (2 '*' (x*(x*(c1 * c2))) +
-(4 '*' x * (x*(c1*c2))))) + (x*(-c2))^2 by RLVECT_1:def 3
.= ((x*(-c1))^2 + (2 '*' (x*(x*(c1 * c2))) +
-(4 '*' (x * (x*(c1*c2)))))) + (x*(-c2))^2 by REALALG2:5
.= ((x*(-c1))^2 + (2 '*' (x*(x*(c1 * c2))) +
((-4) '*' (x * (x*(c1*c2))))) + (x*(-c2))^2) by RING_3:63
.= ((x*(-c1))^2 + (2 + -4) '*' (x*(x*(c1 * c2)))) +
(x*(-c2))^2 by RING_3:62
.= ((x*(-c1))^2 + (-2) '*' (x*(x*(c1 * c2)))) + (x*(-c2))^2
.= ((x*(-c1))^2 + -(2 '*' (x*(x*(c1 * c2))))) + (x*(-c2))^2
by RING_3:63
.= ((x*(-c1))^2 + -(2 '*' (x*(x*((-c1) * (-c2)))))) + (x*(-c2))^2
by VECTSP_1:10
.= ((x*(-c1))^2 + -(2 '*' (x*(x*((-c2) * (-c1)))))) + (x*(-c2))^2
by GROUP_1:def 12
.= ((x*(-c1))^2 - 2 '*' (x*((x*(-c2)) * (-c1))) + (x*(-c2))^2)
by GROUP_1:def 3
.= ((x*(-c1))^2 - 2 '*' (x*((-c1) * (x*(-c2)))) + (x*(-c2))^2)
by GROUP_1:def 12
.= ((x*(-c1))^2 - 2 '*' ((x*(-c1)) * (x*(-c2))) + (x*(-c2))^2)
by GROUP_1:def 3
.= (x*(-c1))^2 - 2 '*' (x*(-c1)) * (x*(-c2)) + (x*(-c2))^2
by REALALG2:5
.= (x*(-c1) - x*(-c2))^2 by REALALG2:8;
hence DC p is square;
end;
hence thesis by Z;
end;
theorem naH2:
for F being non 2-characteristic Field
for a being Element of F holds X^2-a is reducible iff a is square
proof
let F be non 2-characteristic Field; let a be Element of F;
H: 2 '*' 1.F <> 0.F & 4 '*' 1.F <> 0.F by ch2,ch4;
B: now assume X^2-a is reducible;
then DC <%-a,0.F,1.F%> is square by naH;
then - 4 '*' (-a) is square by defDCpq;
then 4 '*' (--a) is square by REALALG2:6; then
consider w being Element of F such that
C: w^2 = 4 '*' a by O_RING_1:def 2;
w * w = 4 '*' (1.F * a) by C,O_RING_1:def 1
.= (4 '*' 1.F) * a by REALALG2:5
.= a * (4 '*' 1.F) by GROUP_1:def 12; then
(w * w) * (4 '*' 1.F)"
= a * ((4 '*' 1.F) * (4 '*' 1.F)") by GROUP_1:def 3
.= a * ((4 '*' 1.F)" * (4 '*' 1.F)) by GROUP_1:def 12
.= a * 1.F by H,VECTSP_1:def 10; then
a = (w * w) * ((2*2) '*' 1.F)"
.= (w * w) * ((2 '*' 1.F) * (2 '*' 1.F))" by RING_3:67
.= (w * w) * ((2 '*' 1.F)" * (2 '*' 1.F)") by H,VECTSP_2:11
.= w * (w * ((2 '*' 1.F)" * (2 '*' 1.F)")) by GROUP_1:def 3
.= w * ((w * (2 '*' 1.F)") * (2 '*' 1.F)") by GROUP_1:def 3
.= w * ((2 '*' 1.F)" * (w * (2 '*' 1.F)")) by GROUP_1:def 12
.= (w * (2 '*' 1.F)") * (w * (2 '*' 1.F)") by GROUP_1:def 3
.= (w * (2 '*' 1.F)")^2 by O_RING_1:def 1;
hence a is square;
end;
now assume a is square; then
consider w being Element of F such that
C: w^2 = a by O_RING_1:def 2;
(2 '*' w)^2 = (2 '*' w) * (2 '*' w) by O_RING_1:def 1
.= 2 '*' (w * (2 '*' w)) by REALALG2:5
.= 2 '*' ((2 '*' w) * w) by GROUP_1:def 12
.= 2 '*' (2 '*' (w * w)) by REALALG2:5
.= (2*2) '*' (w * w) by RING_3:65
.= 4 '*' a by C,O_RING_1:def 1;
then 4 '*' (--a) is square;
then - 4 '*' (-a) is square by REALALG2:6;
then DC <%-a,0.F,1.F%> is square by defDCpq;
hence X^2-a is reducible by naH;
end;
hence thesis by B;
end;
begin :: Quadratic Polynomials over Z/2
theorem cz2:
the carrier of Z/2 = { 0.(Z/2), 1.(Z/2) }
proof
H: INT.Ring(2) =
doubleLoopStr(#Segm(2),addint(2),multint(2),In(1,Segm(2)),In(0,Segm(2))#)
by INT_3:def 12;
I: In(1,Segm(2)) = 1 & In(0,Segm(2)) = 0 by NAT_1:44,SUBSET_1:def 8;
A: now let o be object;
assume A1: o in the carrier of Z/2;
then reconsider k = o as Nat by H;
per cases by H,A1,NAT_1:44,NAT_1:23;
suppose k = 0;
hence o in { 0.(Z/2), 1.(Z/2) } by I,H,TARSKI:def 2;
end;
suppose k = 1;
hence o in { 0.(Z/2), 1.(Z/2) } by I,H,TARSKI:def 2;
end;
end;
for o being object holds o in { 0.(Z/2), 1.(Z/2) }
implies o in the carrier of Z/2;
hence thesis by A,TARSKI:2;
end;
theorem cz2a:
- 1.(Z/2) = 1.(Z/2) by FIELD_3:4,RLVECT_1:def 10;
registration
cluster Z/2 -> polynomial_disjoint;
coherence
proof
2 is non trivial by NAT_2:def 1;
hence thesis;
end;
end;
registration
cluster -> square for Element of Z/2;
coherence
proof
let a be Element of Z/2;
per cases by cz2,TARSKI:def 2;
suppose a = 0.(Z/2);
hence a is square;
end;
suppose a = 1.(Z/2);
hence a is square;
end;
end;
end;
registration
cluster -> monic for non zero Polynomial of Z/2;
coherence
proof
let p be non zero Polynomial of Z/2;
LC p = 1.(Z/2) by cz2,TARSKI:def 2;
hence thesis by RATFUNC1:def 7;
end;
cluster -> monic for non zero Element of the carrier of Polynom-Ring Z/2;
coherence;
end;
definition
func X^2 -> quadratic Element of the carrier of Polynom-Ring Z/2 equals
<%0.(Z/2),0.(Z/2),1.(Z/2)%>;
coherence by POLYNOM3:def 10;
func X^2+1 -> quadratic Element of the carrier of Polynom-Ring Z/2 equals
<%1.(Z/2),0.(Z/2),1.(Z/2)%>;
coherence by POLYNOM3:def 10;
func X^2+X -> quadratic Element of the carrier of Polynom-Ring Z/2 equals
<%0.(Z/2),1.(Z/2),1.(Z/2)%>;
coherence by POLYNOM3:def 10;
func X^2+X+1 -> quadratic Element of the carrier of Polynom-Ring Z/2 equals
<%1.(Z/2),1.(Z/2),1.(Z/2)%>;
coherence by POLYNOM3:def 10;
func X_ -> linear Element of the carrier of Polynom-Ring Z/2 equals
<%0.(Z/2),1.(Z/2)%>;
coherence by POLYNOM3:def 10;
func X-1 -> linear Element of the carrier of Polynom-Ring Z/2 equals
<%1.(Z/2),1.(Z/2)%>;
coherence by POLYNOM3:def 10;
end;
theorem pz2:
the set of all p where p is quadratic Polynomial of Z/2
= { X^2, X^2+1, X^2+X, X^2+X+1 }
proof
set M = { <%0.(Z/2), 0.(Z/2), 1.(Z/2)%>, <%1.(Z/2), 0.(Z/2), 1.(Z/2)%>,
<%0.(Z/2), 1.(Z/2), 1.(Z/2)%>, <%1.(Z/2), 1.(Z/2), 1.(Z/2)%> };
A: now let o be object;
assume o in M;
then o is quadratic Polynomial of Z/2 by ENUMSET1:def 2;
hence o in the set of all p where p is quadratic Polynomial of Z/2;
end;
now let o be object;
assume o in the set of all q where q is quadratic Polynomial of Z/2;
then consider p being quadratic Polynomial of Z/2 such that A1: o = p;
consider b,c being Element of Z/2 such that
A2: p = <%c,b,1.(Z/2)%> by qua5a;
per cases by cz2,TARSKI:def 2;
suppose A3: b = 1.(Z/2);
per cases by cz2,TARSKI:def 2;
suppose c = 1.(Z/2);
hence o in M by A3,A2,A1,ENUMSET1:def 2;
end;
suppose c = 0.(Z/2);
hence o in M by A3,A2,A1,ENUMSET1:def 2;
end;
end;
suppose A3: b = 0.(Z/2);
per cases by cz2,TARSKI:def 2;
suppose c = 1.(Z/2);
hence o in M by A3,A2,A1,ENUMSET1:def 2;
end;
suppose c = 0.(Z/2);
hence o in M by A3,A2,A1,ENUMSET1:def 2;
end;
end;
end;
hence thesis by A,TARSKI:2;
end;
theorem
card(the set of all p where p is quadratic Polynomial of Z/2) = 4
proof
H1: X^2.0 = 0.(Z/2) & X^2.1 = 0.(Z/2)by qua1;
H2: X^2+1.0 = 1.(Z/2) & X^2+1.1 = 0.(Z/2) by qua1;
H3: X^2+X.0 = 0.(Z/2) & X^2+X.1 = 1.(Z/2) by qua1;
A1: X^2 <> X^2+1 by H1,qua1;
A2: X^2 <> X^2+X by H1,qua1;
A3: X^2 <> X^2+X+1 by H1,qua1;
A4: X^2+1 <> X^2+X by H2,qua1;
A5: X^2+1 <> X^2+X+1 by H2,qua1;
X^2+X <> X^2+X+1 by H3,qua1;
hence thesis by pz2,A1,A2,A3,A4,A5,CARD_2:59;
end;
theorem
for p being quadratic Polynomial of Z/2 holds DC p is square;
theorem z21:
X^2 = X_ *' X_ & Roots X^2 = { 0.(Z/2) }
proof
A: X_ *' X_ = rpoly(1,-0.(Z/2)) *' <%0.(Z/2),1.(Z/2)%> by RING_5:10
.= rpoly(1,0.(Z/2)) *' rpoly(1,-0.(Z/2)) by RING_5:10;
thus B: X_ *' X_ = <%0.(Z/2)*0.(Z/2),-(0.(Z/2)+0.(Z/2)),1.(Z/2)%> by lemred3
.= X^2;
Roots rpoly(1,0.(Z/2)) = { 0.(Z/2) } by RING_5:18;
then Roots(rpoly(1,0.(Z/2)) *' rpoly(1,0.(Z/2)))
= { 0.(Z/2) } \/ { 0.(Z/2) } by UPROOTS:23
.= { 0.(Z/2) };
hence thesis by A,B;
end;
theorem z22:
X^2+1 = (X-1) *' (X-1) & Roots X^2+1 = { 1.(Z/2) }
proof
A: X-1 *' X-1 = rpoly(1,-1.(Z/2)) *' <%1.(Z/2),--1.(Z/2)%> by RING_5:10
.= rpoly(1,1.(Z/2)) *' rpoly(1,1.(Z/2)) by cz2a,RING_5:10;
hence B: X-1 *' X-1
= <%1.(Z/2)*1.(Z/2),-(1.(Z/2)+1.(Z/2)),1.(Z/2)%> by lemred3z
.= X^2+1 by FIELD_3:4;
Roots rpoly(1,1.(Z/2)) = { 1.(Z/2) } by RING_5:18;
then Roots(rpoly(1,1.(Z/2)) *' rpoly(1,1.(Z/2)))
= { 1.(Z/2) } \/ { 1.(Z/2) } by UPROOTS:23
.= { 1.(Z/2) };
hence thesis by A,B;
end;
theorem z23:
X^2+X = X_ *' (X-1) & Roots X^2+X = { 0.(Z/2), 1.(Z/2) }
proof
A: X_ *' X-1 = rpoly(1,-0.(Z/2)) *' <%1.(Z/2),--1.(Z/2)%> by RING_5:10
.= rpoly(1,0.(Z/2)) *' rpoly(1,1.(Z/2)) by cz2a,RING_5:10;
hence B: X_ *' X-1
= <%0.(Z/2)*1.(Z/2),-(0.(Z/2)+1.(Z/2)),1.(Z/2)%> by lemred3z
.= X^2+X by FIELD_3:4,RLVECT_1:def 10;
Roots rpoly(1,1.(Z/2)) = { 1.(Z/2) } &
Roots rpoly(1,0.(Z/2)) = { 0.(Z/2) } by RING_5:18;
then Roots(rpoly(1,0.(Z/2)) *' rpoly(1,1.(Z/2)))
= { 0.(Z/2) } \/ { 1.(Z/2) } by UPROOTS:23
.= { 0.(Z/2), 1.(Z/2) } by ENUMSET1:1;
hence thesis by A,B;
end;
theorem z24:
Roots X^2+X+1 = {}
proof
set p = <%1.(Z/2), 1.(Z/2), 1.(Z/2)%>;
set a = the Element of Roots p;
now assume A: Roots p <> {};
then a in Roots p;
then reconsider a as Element of Z/2;
B: a is_a_root_of p by A,POLYNOM5:def 10;
per cases by cz2,TARSKI:def 2;
suppose a = 0.(Z/2); then
eval(p,a) = 1.(Z/2) + 1.(Z/2) * 0.(Z/2) + 1.(Z/2) * (0.(Z/2))^2
by evalq
.= 1.(Z/2);
hence contradiction by B;
end;
suppose a = 1.(Z/2);then
eval(p,a) = 1.(Z/2) + 1.(Z/2) * 1.(Z/2) + 1.(Z/2) * (1.(Z/2))^2
by evalq
.= 1.(Z/2) + 0.(Z/2) by FIELD_3:4;
hence contradiction by B;
end;
end;
hence thesis;
end;
registration
cluster X^2 -> reducible;
coherence by z21;
cluster X^2+1 -> reducible;
coherence by z22;
cluster X^2+X -> reducible;
coherence by z23;
cluster X^2+X+1 -> irreducible;
coherence
proof
now assume X^2+X+1 is reducible; then
consider q being Element of the carrier of Polynom-Ring Z/2 such that
C2: q divides X^2+X+1 & 1 <= deg q & deg q < deg X^2+X+1 by RING_4:41;
deg X^2+X+1 = 2 by qua4; then
deg q + 1 <= 2 by C2,INT_1:7; then
(deg q + 1) - 1 <= 2 - 1 by XREAL_1:9; then
consider x,a being Element of Z/2 such that
C3: x <> 0.(Z/2) & q = x * rpoly(1,a) by C2,XXREAL_0:1,HURWITZ:28;
consider p being Polynomial of Z/2 such that
C4: X^2+X+1 = q *' p by C2,RING_4:1;
thus contradiction by C3,C4,z24;
end;
hence thesis;
end;
end;
z25:
for p being quadratic Polynomial of Z/2 holds
p splits_in Z/2 iff p <> <%1.(Z/2), 1.(Z/2), 1.(Z/2)%>
proof
let p be quadratic Polynomial of Z/2;
H: p in { <%0.(Z/2), 0.(Z/2), 1.(Z/2)%>, <%1.(Z/2), 0.(Z/2), 1.(Z/2)%>,
<%0.(Z/2), 1.(Z/2), 1.(Z/2)%>, <%1.(Z/2), 1.(Z/2), 1.(Z/2)%> }
by pz2;
A: now assume p splits_in Z/2; then
consider a being non zero Element of Z/2, q being Ppoly of Z/2 such that
A1: p = a * q by FIELD_4:def 5;
thus p <> <%1.(Z/2), 1.(Z/2), 1.(Z/2)%> by A1,z24;
end;
now assume p <> <%1.(Z/2), 1.(Z/2), 1.(Z/2)%>;
then per cases by H,ENUMSET1:def 2;
suppose p = <%0.(Z/2), 0.(Z/2), 1.(Z/2)%>;
then B: p = rpoly(1,-0.(Z/2)) *' <%0.(Z/2),1.(Z/2)%> by z21,RING_5:10
.= 1.(Z/2) * (rpoly(1,0.(Z/2))*'rpoly(1,0.(Z/2))) by RING_5:10;
rpoly(1,0.(Z/2)) is Ppoly of Z/2 by RING_5:51; then
rpoly(1,0.(Z/2)) *' rpoly(1,0.(Z/2)) is Ppoly of Z/2 by RING_5:52;
hence p splits_in Z/2 by B,FIELD_4:def 5;
end;
suppose p = <%1.(Z/2), 0.(Z/2), 1.(Z/2)%>; then
B: p = rpoly(1,-1.(Z/2)) *' <%1.(Z/2),--1.(Z/2)%> by z22,RING_5:10
.= 1.(Z/2) * (rpoly(1,1.(Z/2)) *' rpoly(1,1.(Z/2))) by RING_5:10,cz2a;
rpoly(1,1.(Z/2)) is Ppoly of Z/2 by RING_5:51; then
rpoly(1,1.(Z/2)) *' rpoly(1,1.(Z/2)) is Ppoly of Z/2 by RING_5:52;
hence p splits_in Z/2 by B,FIELD_4:def 5;
end;
suppose p = <%0.(Z/2), 1.(Z/2), 1.(Z/2)%>; then
B: p = rpoly(1,-0.(Z/2)) *' <%1.(Z/2),--1.(Z/2)%> by z23,RING_5:10
.= 1.(Z/2) * (rpoly(1,0.(Z/2)) *' rpoly(1,1.(Z/2))) by RING_5:10,cz2a;
rpoly(1,1.(Z/2)) is Ppoly of Z/2 &
rpoly(1,0.(Z/2)) is Ppoly of Z/2 by RING_5:51; then
rpoly(1,1.(Z/2)) *' rpoly(1,0.(Z/2)) is Ppoly of Z/2 by RING_5:52;
hence p splits_in Z/2 by B,FIELD_4:def 5;
end;
end;
hence thesis by A;
end;
z26:
for p being quadratic Element of the carrier of Polynom-Ring Z/2
st p <> <%1.(Z/2), 1.(Z/2), 1.(Z/2)%> holds Z/2 is SplittingField of p
proof
let p be quadratic Element of the carrier of Polynom-Ring Z/2;
assume A: p <> <%1.(Z/2), 1.(Z/2), 1.(Z/2)%>;
B: Z/2 is FieldExtension of Z/2 by FIELD_4:6;
now let E be FieldExtension of Z/2;
assume C: p splits_in E & E is Subfield of Z/2; then
D: the carrier of E c= the carrier of Z/2 &
the addF of E = (the addF of Z/2) || the carrier of E &
the multF of E = (the multF of Z/2) || the carrier of E &
1.E = 1.Z/2 & 0.E = 0.Z/2 by EC_PF_1:def 1;
now let o be object;
assume o in the carrier of Z/2; then
per cases by cz2,TARSKI:def 2;
suppose o = 0.Z/2;
hence o in the carrier of E by D;
end;
suppose o = 1.Z/2;
hence o in the carrier of E by D;
end;
end;
then the carrier of E = the carrier of Z/2 by D,TARSKI:2;
then Z/2 is Subfield of E by D,EC_PF_1:def 1;
hence E == Z/2 by C,FIELD_7:def 2;
end;
hence thesis by A,z25,B,FIELD_8:def 1;
end;
theorem
Z/2 is SplittingField of X^2
proof
A: X^2.0 = 0.(Z/2) by qua1;
<%1.(Z/2), 1.(Z/2), 1.(Z/2)%>.0 = 1.(Z/2) by qua1;
hence thesis by A,z26;
end;
theorem
Z/2 is SplittingField of X^2+1
proof
A: X^2+1.1 = 0.(Z/2) by qua1;
<%1.(Z/2), 1.(Z/2), 1.(Z/2)%>.1 = 1.(Z/2) by qua1;
hence thesis by A,z26;
end;
theorem
Z/2 is SplittingField of X^2+X
proof
A: X^2+X.0 = 0.(Z/2) by qua1;
<%1.(Z/2), 1.(Z/2), 1.(Z/2)%>.0 = 1.(Z/2) by qua1;
hence thesis by A,z26;
end;
definition
func alpha -> Element of embField(canHomP X^2+X+1) equals
KrRootP X^2+X+1;
coherence;
end;
definition
func alpha-1 -> Element of embField(canHomP X^2+X+1) equals
alpha - 1.embField(canHomP X^2+X+1);
coherence;
end;
registration
cluster alpha -> non zero (Z/2)-algebraic;
coherence;
end;
lemZ2:
X^2+X+1 = (X-alpha) *' (X-alpha") &
alpha" = -(alpha + 1.embField(canHomP X^2+X+1)) &
-alpha = alpha" + 1.embField(canHomP X^2+X+1)
proof
set F = embField(canHomP X^2+X+1);
A0: Z/2 is Subring of F by FIELD_4:def 1;
the carrier of Polynom-Ring Z/2 c= the carrier of Polynom-Ring F by FIELD_4:10;
then reconsider p = X^2+X+1 as Element of the carrier of Polynom-Ring F;
eval(p,alpha) = Ext_eval(X^2+X+1,alpha) by FIELD_4:26
.= 0.(Z/2) by FIELD_5:17
.= 0.F by A0,C0SP1:def 3;
then alpha is_a_root_of p;
then consider q being Polynomial of F such that
A1: p = rpoly(1,alpha) *' q by HURWITZ:33;
H0: now assume H1: q = 0_.(F);
deg p = deg X^2+X+1 by FIELD_4:20;
hence contradiction by H1,A1,HURWITZ:20;
end;
H1: alpha <> 0.F;
2 = deg X^2+X+1 by qua4
.= deg p by FIELD_4:20
.= deg rpoly(1,alpha) + deg q by A1,H0,HURWITZ:23
.= 1 + deg q by HURWITZ:27; then
consider x,b being Element of F such that
A2: x <> 0.F & q = x * rpoly(1,b) by HURWITZ:28;
A3: rpoly(1,b) = <%-b,1.F%> & rpoly(1,alpha) = <%-alpha,1.F%> by RING_5:10;
then q = <%x*(-b),x*1.F%> by A2,qua20; then
A4: p = <%(-alpha)*(x*(-b)),(1.F)*(x*(-b))+(x*1.F)*(-alpha),(1.F)*(x*1.F)%>
by A1,A3,lemred1
.= <%(-alpha)*(x*(-b)),x*(-b)+x*(-alpha),x%>; then
A5: x = X^2+X+1.2 by qua1 .= 1.(Z/2) by qua1
.= 1.F by A0,C0SP1:def 3; then
p = <%alpha*b,(-b)+(-alpha),1.F%> by A4,VECTSP_1:10; then
alpha*b = X^2+X+1.0 by qua1 .= 1.(Z/2) by qua1 .= 1.F by A0,C0SP1:def 3; then
A7: b * alpha = 1.F by GROUP_1:def 12; then
A6: b = alpha" by H1,VECTSP_1:def 10;
thus X^2+X+1 = (X-alpha) *' (X-alpha") by A1,A5,A7,A2,VECTSP_1:def 10;
-(b+alpha) = (-b)+(-alpha) by RLVECT_1:31
.= p.1 by A4,A5,qua1 .= 1.(Z/2) by qua1
.= 1.F by A0,C0SP1:def 3; then
b + (alpha + -alpha) = (-alpha) - 1.F by RLVECT_1:def 3; then
A8: alpha" + 0.F = (-alpha) + -1.F by A6,RLVECT_1:5;
hence alpha" = (-alpha) - 1.F .= -(alpha + 1.F) by RLVECT_1:30;
alpha" + 1.F = -alpha + (-1.F + 1.F) by A8,RLVECT_1:def 3
.= (-alpha) + 0.F by RLVECT_1:5;
hence -alpha = alpha" + 1.embField(canHomP X^2+X+1);
end;
theorem lemalph:
-alpha = alpha & alpha" = alpha-1 & alpha" <> alpha
proof
J: Char(Z/2) = 2 by RING_3:def 6;
Z/2 is Subring of embField(canHomP X^2+X+1) by FIELD_4:def 1; then
I: Char embField(canHomP X^2+X+1) = 2 by J,RING_3:89;
H: 2 '*' alpha = 2 '*' (1.embField(canHomP X^2+X+1) * alpha)
.= (2 '*' 1.embField(canHomP X^2+X+1)) * alpha by REALALG2:5
.= 0.embField(canHomP X^2+X+1) * alpha by I,REALALG2:24; then
alpha + alpha = 0.embField(canHomP X^2+X+1) by RING_5:2; then
0.embField(canHomP X^2+X+1) - alpha
= alpha + (alpha - alpha) by RLVECT_1:def 3
.= alpha + 0.embField(canHomP X^2+X+1) by RLVECT_1:15;
hence H3: -alpha = alpha;
thus alpha" = alpha-1 by lemZ2,H3,RLVECT_1:31;
now assume alpha" = alpha; then
alpha = -alpha + -1.embField(canHomP X^2+X+1) by RLVECT_1:31,lemZ2; then
alpha + alpha
= (alpha + -alpha) + -1.embField(canHomP X^2+X+1) by RLVECT_1:def 3
.= 0.embField(canHomP X^2+X+1) + -1.embField(canHomP X^2+X+1)
by RLVECT_1:5; then
-0.embField(canHomP X^2+X+1) = --1.embField(canHomP X^2+X+1) by H,RING_5:2;
hence contradiction;
end;
hence thesis;
end;
theorem
X^2+X+1 = (X-alpha) *' (X-alpha") = (X-alpha) *' (X-(alpha-1))
by lemZ2,lemalph;
theorem lemZ2roots:
Roots(FAdj(Z/2,{alpha}),X^2+X+1) = { alpha, alpha-1 }
proof
set F = FAdj(Z/2,{alpha});
H: embField(canHomP X^2+X+1) is FieldExtension of F by FIELD_4:7;
alpha in {alpha} & {alpha} is Subset of F by TARSKI:def 1,FIELD_6:35; then
reconsider a = alpha as Element of F;
alpha" = a" by FIELD_6:18; then
reconsider ai = alpha" as Element of F;
C: rpoly(1,alpha) = rpoly(1,a) & rpoly(1,alpha") = rpoly(1,ai) by H,FIELD_4:21;
reconsider q = rpoly(1,a) *' rpoly(1,ai)
as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
A: X^2+X+1 = rpoly(1,a) *' rpoly(1,ai) by H,C,lemZ2,FIELD_4:17;
Roots rpoly(1,a) = {a} & Roots rpoly(1,ai) = {ai} by RING_5:18; then
Roots(rpoly(1,a) *' rpoly(1,ai))
= {a} \/ {ai} by UPROOTS:23
.= {a,ai} by ENUMSET1:1; then
{a,ai} = Roots q .= Roots(F,X^2+X+1) by A,FIELD_7:13;
hence thesis by lemalph;
end;
theorem
card Roots(FAdj(Z/2,{alpha}),X^2+X+1) = 2 by lemZ2roots,lemalph,CARD_2:57;
theorem lemZ2min:
MinPoly(alpha,Z/2) = X^2+X+1
proof
H: Z/2 is Subring of embField(canHomP X^2+X+1) by FIELD_4:def 1;
Ext_eval(X^2+X+1,alpha) = 0.(Z/2) by FIELD_5:17
.= 0.embField(canHomP X^2+X+1) by H,C0SP1:def 3;
hence thesis by FIELD_6:52;
end;
theorem
deg(FAdj(Z/2,{alpha}),Z/2) = 2
proof
thus deg(FAdj(Z/2,{alpha}),Z/2)
= deg MinPoly(alpha,Z/2) by FIELD_6:67
.= 2 by lemZ2min,qua4;
end;
theorem
FAdj(Z/2,{alpha}) is SplittingField of X^2+X+1
proof
set p = X^2+X+1, F = FAdj(Z/2,{alpha});
H: embField(canHomP X^2+X+1) is FieldExtension of F by FIELD_4:7;
alpha in {alpha} & {alpha} is Subset of F by TARSKI:def 1,FIELD_6:35; then
reconsider a = alpha as Element of F;
alpha" = a" by FIELD_6:18; then
reconsider ai = alpha" as Element of F;
C: rpoly(1,alpha) = rpoly(1,a) & rpoly(1,alpha") = rpoly(1,ai) by H,FIELD_4:21;
reconsider q = rpoly(1,a) *' rpoly(1,ai)
as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
B: X^2+X+1 = 1.F * (rpoly(1,a) *' rpoly(1,ai)) by lemZ2,H,C,FIELD_4:17;
rpoly(1,a) is Ppoly of F & rpoly(1,ai) is Ppoly of F by RING_5:51; then
rpoly(1,a) *' rpoly(1,ai) is Ppoly of F by RING_5:52; then
A: p splits_in F by B,FIELD_4:def 5;
now let E be FieldExtension of Z/2;
assume D0: p splits_in E & E is Subfield of F; then
D3: F is E-extending by FIELD_4:7;
D4: Roots(F,p) c= the carrier of E by D3,D0,A,FIELD_8:27;
alpha in Roots(F,p) by lemZ2roots,TARSKI:def 2; then
alpha in the carrier of E by D4; then
D1: {alpha} c= the carrier of E by TARSKI:def 1;
D2: E is Subfield of embField(canHomP X^2+X+1) by D0,EC_PF_1:5;
Z/2 is Subfield of E by FIELD_4:7;
then F is Subfield of E by D1,D2,FIELD_6:37;
hence E == F by D0,FIELD_7:def 2;
end;
hence thesis by A,FIELD_8:def 1;
end;
begin :: Fields with non-squares
definition
let R be Ring;
attr R is quadratic_complete means :defqc:
the carrier of R c= SQ R;
end;
registration
cluster -1.F_Real -> non square;
coherence
proof
set R = F_Real; set P = the Ordering of R;
A: -1.R in -P by REALALG1:14,REALALG1:25;
not -1.R in {0.R};
then -1.R in -P \ {0.R} by A,XBOOLE_0:def 5;
hence thesis by REALALG2:83;
end;
cluster -1.F_Rat -> non square;
coherence
proof
set R = F_Rat; set P = the Ordering of R;
A: -1.R in -P by REALALG1:14,REALALG1:25;
-1.R <> -0.R;
then not -1.R in {0.R} by TARSKI:def 1;
then -1.R in -P \ {0.R} by A,XBOOLE_0:def 5;
hence thesis by REALALG2:83;
end;
end;
registration
cluster algebraic-closed -> quadratic_complete for non degenerated Ring;
coherence
proof
let R be non degenerated Ring;
assume AS: R is algebraic-closed;
now let o be object;
assume o in the carrier of R;
then reconsider a = o as Element of R;
set p = X^2-a;
2 = deg p by qua4 .= len p - 1 by HURWITZ:def 2; then
len p = 3; then
consider b being Element of R such that
A: b is_a_root_of p by AS,POLYNOM5:def 8;
0.R = (-a) + 0.R * b + 1.R * b^2 by A,evalq .= b^2 - a;
then b^2 = --a by RLVECT_1:6;
then a in {x where x is Element of R : x is square };
hence o in SQ R by REALALG1:def 10;
end;
hence thesis by TARSKI:def 3;
end;
cluster preordered -> non quadratic_complete for non degenerated Ring;
coherence
proof
let R be non degenerated Ring;
assume R is preordered; then
A: not -1.R in QS R by REALALG2:def 3;
now assume R is quadratic_complete;
then B: the carrier of R c= SQ R;
SQ R c= QS R by REALALG1:18;
hence contradiction by A,B;
end;
hence thesis;
end;
end;
registration
cluster F_Rat -> non quadratic_complete;
coherence;
cluster F_Real -> non quadratic_complete;
coherence;
cluster F_Complex -> quadratic_complete;
coherence;
end;
registration
cluster non quadratic_complete polynomial_disjoint strict for Field;
existence
proof
take F_Real;
thus thesis;
end;
cluster quadratic_complete strict for Field;
existence
proof
take F_Complex;
thus thesis;
end;
end;
registration
cluster non quadratic_complete -> non degenerated for Ring;
coherence
proof
let R be Ring;
assume A: R is non quadratic_complete;
now assume B: R is degenerated;
now let o be object;
assume o in the carrier of R;
then reconsider a = o as Element of R;
a = a * 1.R .= 0.R by B;
then a in {x where x is Element of R : x is square};
hence o in SQ R by REALALG1:def 10;
end;
then the carrier of R c= SQ R;
hence contradiction by A;
end;
hence thesis;
end;
end;
registration
let R be non quadratic_complete Ring;
cluster non square for Element of R;
existence
proof
not the carrier of R c= SQ R by defqc; then
consider a being Element of R such that A: not a in SQ R;
SQ R = {x where x is Element of R : x is square} by REALALG1:def 10;
then not(a is square) by A;
hence thesis;
end;
end;
registration
cluster strict polynomial_disjoint
non quadratic_complete non 2-characteristic for Field;
existence
proof
take F_Rat;
Char F_Rat <> 2 by RING_3:def 6;
hence thesis by RING_3:def 6;
end;
end;
registration
let F be non quadratic_complete non 2-characteristic Field;
cluster monic quadratic irreducible
for Element of the carrier of Polynom-Ring F;
existence
proof
set a = the non square Element of F;
reconsider p = X^2-a as quadratic Element of the carrier of Polynom-Ring F;
take p;
A: DC p = - 4 '*' (-a) by defDCpq .= --(4 '*' a) by REALALG2:6;
H: 2 '*' 1.F <> 0.F & 4 '*' 1.F <> 0.F by ch2,ch4;
now assume DC p is square; then
consider w being Element of F such that
C: w^2 = 4 '*' a by A,O_RING_1:def 2;
w * w = 4 '*' (1.F * a) by C,O_RING_1:def 1
.= (4 '*' 1.F) * a by REALALG2:5
.= a * (4 '*' 1.F) by GROUP_1:def 12; then
(w * w) * (4 '*' 1.F)"
= a * ((4 '*' 1.F) * (4 '*' 1.F)") by GROUP_1:def 3
.= a * ((4 '*' 1.F)" * (4 '*' 1.F)) by GROUP_1:def 12
.= a * 1.F by H,VECTSP_1:def 10; then
a = (w * w) * ((2*2) '*' 1.F)"
.= (w * w) * ((2 '*' 1.F) * (2 '*' 1.F))" by RING_3:67
.= (w * w) * ((2 '*' 1.F)" * (2 '*' 1.F)") by H,VECTSP_2:11
.= w * (w * ((2 '*' 1.F)" * (2 '*' 1.F)")) by GROUP_1:def 3
.= w * ((w * (2 '*' 1.F)") * (2 '*' 1.F)") by GROUP_1:def 3
.= w * ((2 '*' 1.F)" * (w * (2 '*' 1.F)")) by GROUP_1:def 12
.= (w * (2 '*' 1.F)") * (w * (2 '*' 1.F)") by GROUP_1:def 3
.= (w * (2 '*' 1.F)")^2 by O_RING_1:def 1;
hence contradiction;
end;
hence thesis by naH;
end;
end;
registration
let F be non 2-characteristic Field;
let a be square Element of F;
cluster X^2-a -> reducible;
coherence by naH2;
end;
registration
let F be non quadratic_complete non 2-characteristic Field;
let a be non square Element of F;
cluster X^2-a -> irreducible;
coherence by naH2;
end;
definition
let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field;
let a be non square Element of F;
func sqrt a -> Element of embField(canHomP X^2-a) equals
KrRootP(X^2-a);
coherence;
end;
registration
let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field;
let a be non square Element of F;
cluster sqrt a -> non zero F-algebraic;
coherence
proof
set E = embField(canHomP X^2-a);
A0: F is Subring of E by FIELD_4:def 1;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E by FIELD_4:10;
then reconsider q = X^2-a as Element of the carrier of Polynom-Ring E;
A1: eval(q,KrRootP(X^2-a)) = Ext_eval(X^2-a,sqrt a) by FIELD_4:26
.= 0.F by FIELD_5:17;
now assume sqrt a = 0.E; then
reconsider o = sqrt a as Element of F by A0,C0SP1:def 3;
o is_a_root_of X^2-a by A1,FIELD_4:27; then
X^2-a is with_roots;
hence contradiction;
end;
hence thesis;
end;
end;
registration
let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field;
let a be non square Element of F;
cluster embField(canHomP X^2-a) -> (FAdj(F,{sqrt a}))-extending;
coherence by FIELD_4:7;
end;
m30:
for F being non 2-characteristic
non quadratic_complete polynomial_disjoint Field
for a being non square Element of F holds MinPoly(sqrt a,F) = X^2-a
proof
let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field;
let a be non square Element of F;
Ext_eval(X^2-a,sqrt a) = 0.F by FIELD_5:17
.= 0.embField(canHomP X^2-a) by FIELD_2:def 7;
hence thesis by FIELD_6:52;
end;
dega:
for F being non 2-characteristic
non quadratic_complete polynomial_disjoint Field
for a being non square Element of F holds deg(FAdj(F,{sqrt a}),F) = 2
proof
let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field;
let a be non square Element of F;
thus deg(FAdj(F,{sqrt a}),F)
= deg MinPoly(sqrt a,F) by FIELD_6:67
.= deg X^2-a by m30
.= 2 by qua4;
end;
registration
let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field;
let a be non square Element of F;
cluster sqrt a -> (FAdj(F,{sqrt a}))-membered non F-membered;
coherence
proof
A: {sqrt a} is Subset of FAdj(F,{sqrt a}) by FIELD_6:35;
sqrt a in {sqrt a} by TARSKI:def 1;
hence (sqrt a) is (FAdj(F,{sqrt a}))-membered by A,FIELD_7:def 5;
now assume B: sqrt a is F-membered;
then reconsider sqrta = sqrt a as Element of F by FIELD_7:def 5;
C: deg rpoly(1,sqrta) = 1 by HURWITZ:27;
D: rpoly(1,sqrta) = rpoly(1,sqrt a) by FIELD_4:21;
MinPoly(sqrt a,F) = rpoly(1,sqrt a) by B,FIELD_7:def 5,FIELD_6:54;
then deg(FAdj(F,{sqrt a}),F) = deg rpoly(1,sqrta) by D,FIELD_6:67;
hence contradiction by C,dega;
end;
hence (sqrt a) is non F-membered;
end;
end;
reserve
F for non 2-characteristic non quadratic_complete polynomial_disjoint Field;
theorem m1:
for a being non square Element of F holds (sqrt a) * (sqrt a) = a
proof
let a be non square Element of F;
B: F is Subring of embField(canHomP X^2-a) by FIELD_4:def 1; then
the carrier of F c= the carrier of embField(canHomP X^2-a) by C0SP1:def 3; then
reconsider b = a as Element of embField(canHomP X^2-a);
H: -a = -b &
0.F = 0.embField(canHomP X^2-a) &
1.F = 1.embField(canHomP X^2-a) by FIELD_6:17,B,C0SP1:def 3;
0.embField(canHomP X^2-a) = 0.F by B,C0SP1:def 3
.= Ext_eval(X^2-a,sqrt a) by FIELD_5:17
.= eval(X^2-b,sqrt a) by H,FIELD_4:26
.= (-b) + (0.embField(canHomP X^2-a)) * (sqrt a)
+ (1.embField(canHomP X^2-a)) * (sqrt a)^2 by evalq
.= (sqrt a) * (sqrt a) - b by O_RING_1:def 1;
hence thesis by RLVECT_1:21;
end;
theorem
for a being non square Element of F holds MinPoly(sqrt a,F) = X^2-a by m30;
theorem
for a being non square Element of F holds deg(FAdj(F,{sqrt a}),F) = 2 by dega;
theorem Fi1a:
for a being non square Element of F holds (X-(sqrt a)) *' (X+(sqrt a)) = X^2-a
proof
let a be non square Element of F;
set E = embField(canHomP X^2-a);
H: F is Subring of E by FIELD_4:def 1; then
the carrier of F c= the carrier of E by C0SP1:def 3; then
reconsider b = a as Element of E;
A: (sqrt a) * (-(sqrt a)) = -((sqrt a) * (sqrt a)) by VECTSP_1:8 .= -b by m1;
-((sqrt a) + -(sqrt a)) = -0.E by RLVECT_1: 5 .= 0.E; then
B: (X-(sqrt a)) *' (X--(sqrt a)) = <%-b,0.E,1.E%> by A,lemred3z;
0.E = 0.F & 1.E = 1.F by H,C0SP1:def 3;
hence thesis by B,H,FIELD_6:17;
end;
theorem Fi2a:
for a being non square Element of F
holds Roots(FAdj(F,{sqrt a}),X^2-a) = { sqrt a, -(sqrt a) }
proof
let a be non square Element of F;
set E = FAdj(F,{sqrt a});
reconsider p = X^2-a as Element of the carrier of Polynom-Ring F;
reconsider b = sqrt a as Element of E by FIELD_7:def 5;
reconsider q = rpoly(1,b) *' rpoly(1,-b) as
Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
H: E is Subring of embField(canHomP X^2-a) by FIELD_4:def 1; then
H1: -b = -(sqrt a) by FIELD_6:17;
Roots rpoly(1,b) = {b} & Roots rpoly(1,-b) = {-b} by RING_5:18; then
A: Roots(rpoly(1,b) *' rpoly(1,-b))
= {b} \/ {-b} by UPROOTS:23
.= {b,-b} by ENUMSET1:1;
I: X-b = X-(sqrt a) by FIELD_4:21;
K: X+b = X+(sqrt a) by H1,FIELD_4:21;
rpoly(1,b) *' rpoly(1,-b)
= (X-(sqrt a)) *' (X+(sqrt a)) by I,K,FIELD_4:17
.= X^2-a by Fi1a;
then Roots(E,p) = Roots(q) by FIELD_7:13;
hence thesis by A,H,FIELD_6:17;
end;
theorem Fi3a:
for a being non square Element of F
holds FAdj(F,{sqrt a}) is SplittingField of X^2-a
proof
let a be non square Element of F;
set E = FAdj(F,{sqrt a});
reconsider p = X^2-a as Element of the carrier of Polynom-Ring F;
reconsider b = sqrt a as Element of E by FIELD_7:def 5;
reconsider q = rpoly(1,b) *' rpoly(1,-b) as
Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
E is Subring of embField(canHomP X^2-a) by FIELD_4:def 1; then
H: -b = -(sqrt a) by FIELD_6:17;
I: X-b = X-(sqrt a) by FIELD_4:21;
K: X+b = X+(sqrt a) by H,FIELD_4:21;
rpoly(1,b) *' rpoly(1,-b)
= (X-(sqrt a)) *' (X+(sqrt a)) by I,K,FIELD_4:17
.= X^2-a by Fi1a; then
D: X^2-a = 1.E * q;
rpoly(1,b) is Ppoly of E & rpoly(1,-b) is Ppoly of E by RING_5:51;
then q is Ppoly of E by RING_5:52; then
A: X^2-a splits_in E by D,FIELD_4:def 5;
now let U be FieldExtension of F;
assume D0: X^2-a splits_in U & U is Subfield of E; then
D3: E is U-extending by FIELD_4:7;
D4: Roots(E,X^2-a) c= the carrier of U by D3,D0,A,FIELD_8:27;
Roots(E,p) = { sqrt a, -(sqrt a) } by Fi2a; then
sqrt a in Roots(E,p) by TARSKI:def 2; then
sqrt a in the carrier of U by D4; then
D1: {sqrt a} c= the carrier of U by TARSKI:def 1;
D2: U is Subfield of embField(canHomP X^2-a) by D0,EC_PF_1:5;
F is Subfield of U by FIELD_4:7;
then E is Subfield of U by D1,D2,FIELD_6:37;
hence E == U by D0,FIELD_7:def 2;
end;
hence thesis by A,FIELD_8:def 1;
end;
qbase1:
for a being non square Element of F holds Base(sqrt a) = {1.F, sqrt a}
proof
let a be non square Element of F;
MinPoly(sqrt a,F) = X^2-a by m30; then
A: deg MinPoly(sqrt a,F) = 2 by qua4;
H: F is Subfield of embField(canHomP X^2-a) by FIELD_4:7;
B: now let x be object;
assume x in {1.F, sqrt a}; then
per cases by TARSKI:def 2;
suppose x = 1.F;
then x = 1_embField(canHomP X^2-a) by H,EC_PF_1:def 1
.= (sqrt a)|^0 by BINOM:8;
hence x in Base(sqrt a) by A;
end;
suppose x = sqrt a;
then x = (sqrt a)|^1 by BINOM:8;
hence x in Base(sqrt a) by A;
end;
end;
now let o be object;
assume o in Base(sqrt a); then
consider n being Element of NAT such that
C1: o = (sqrt a)|^n & n < 2 by A;
n is trivial by C1,NAT_2:29; then
per cases by NAT_2:def 1;
suppose n = 0;
then o = 1_embField(canHomP X^2-a) by C1,BINOM:8
.= 1.F by H,EC_PF_1:def 1;
hence o in {1.F, sqrt a} by TARSKI:def 2;
end;
suppose n = 1;
then o = sqrt a by C1,BINOM:8;
hence o in {1.F, sqrt a} by TARSKI:def 2;
end;
end;
hence Base(sqrt a) = {1.F, sqrt a} by B,TARSKI:2;
end;
theorem qbase4:
for a being non square Element of F
holds {1.F, sqrt a} is Basis of VecSp(FAdj(F,{sqrt a}),F)
proof
let a be non square Element of F;
Base(sqrt a) = {1.F, sqrt a} by qbase1;
hence thesis by FIELD_6:65;
end;
qbase2:
for a being non square Element of F
for x being object holds
x in the carrier of FAdj(F,{sqrt a}) iff
ex y,z being F-membered Element of FAdj(F,{sqrt a})
st x = y + @(sqrt a) * z
proof
let a be non square Element of F; let x be object;
H: the carrier of RAdj(F,{sqrt a})
= the set of all Ext_eval(p,sqrt a) where p is Polynomial of F by FIELD_6:45;
now assume x in FAdj(F,{sqrt a}); then
x in the set of all Ext_eval(p,sqrt a) where p is Polynomial of F
by H,FIELD_6:56;
then consider p1 being Polynomial of F such that
A: x = Ext_eval(p1,sqrt a);
set ma = MinPoly(sqrt a,F), p = p1 mod ma;
B: F is Subring of embField(canHomP X^2-a) by FIELD_4:def 1;
C: p1 = (p1 div ma) *' ma + p by RING_4:4;
D: Ext_eval(p1,sqrt a)
= Ext_eval((p1 div ma) *' ma,sqrt a) + Ext_eval(p,sqrt a)
by C,B,ALGNUM_1:15
.= (Ext_eval(p1 div ma,sqrt a) * Ext_eval(ma,sqrt a)) + Ext_eval(p,sqrt a)
by B,ALGNUM_1:20
.= (Ext_eval(p1 div ma,sqrt a) * 0.embField(canHomP X^2-a))
+ Ext_eval(p,sqrt a) by FIELD_6:52
.= Ext_eval(p,sqrt a);
deg p < deg ma by FIELD_5:16; then
deg p < deg X^2-a by m30; then
deg p < 2 by qua4; then
consider y,z being F-membered Element of FAdj(F,{sqrt a}) such that
E: Ext_eval(p,@(sqrt a)) = y + @(sqrt a) * z by deg2evale;
p is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
then Ext_eval(p,@(sqrt a)) = x by A,D,FIELD_7:14;
hence ex y,z being F-membered Element of FAdj(F,{sqrt a})
st x = y + @(sqrt a) * z by E;
end;
hence thesis;
end;
theorem
for a being non square Element of F
holds the carrier of FAdj(F,{sqrt a}) =
the set of all y + @(sqrt a) * z
where y,z is F-membered Element of FAdj(F,{sqrt a})
proof
let a be non square Element of F;
A: now let o be object;
assume o in the carrier of FAdj(F,{sqrt a});
then ex y,z being F-membered Element of FAdj(F,{sqrt a})
st o = y + @(sqrt a) * z by qbase2;
hence o in the set of all y + @(sqrt a) * z
where y,z is F-membered Element of FAdj(F,{sqrt a});
end;
now let o be object;
assume o in the set of all y + @(sqrt a) * z
where y,z is F-membered Element of FAdj(F,{sqrt a});
then ex y,z being F-membered Element of FAdj(F,{sqrt a})
st o = y + @(sqrt a) * z;
hence o in the carrier of FAdj(F,{sqrt a});
end;
hence thesis by A,TARSKI:2;
end;
theorem
for a being non square Element of F
for a1,a2,b1,b2 being F-membered Element of FAdj(F,{sqrt a})
st a1 + @(sqrt a) * b1 = a2 + @(sqrt a) * b2 holds a1 = a2 & b1 = b2
proof
let a be non square Element of F;
let a1,a2,b1,b2 be F-membered Element of FAdj(F,{sqrt a});
set E = FAdj(F,{sqrt a}), j = @(sqrt a);
set V = VecSp(E,F);
assume a1 + @(sqrt a) * b1 = a2 + @(sqrt a) * b2; then
AS: 0.E = (a1 + j * b1) - (a2 + j * b2) by RLVECT_1:15
.= (a1 + j * b1) + (-a2 + -(j * b2)) by RLVECT_1:31
.= (a1 + j * b1) + (-a2 + (j * (-b2))) by VECTSP_1:8
.= j * b1 + (a1 + (-a2 + (j * (-b2)))) by RLVECT_1:def 3
.= j * b1 + ((a1 + -a2) + (j * (-b2))) by RLVECT_1:def 3
.= (j * b1 + (j * (-b2))) + (a1 + -a2) by RLVECT_1:def 3
.= (a1 - a2) + j * (b1 - b2) by VECTSP_1:def 2;
reconsider 1V = 1.E, jV = j as Element of V by FIELD_4:def 6;
reconsider a1R = a1, a2R = a2, b1R = b1, b2R = b2 as Element of F
by FIELD_7:def 5;
I0: F is Subring of E by FIELD_4:def 1; then
-a2 = -a2R & -b2 = -b2R by FIELD_6:17; then
I1: a1 - a2 = a1R - a2R & b1 - b2 = b1R - b2R by I0,FIELD_6:15;
defpred P[object,object] means
($1 = 1.E & $2 = a1 - a2) or ($1 = j & $2 = b1 - b2) or
($1 <> 1.E & $1 <> j & $2 = 0.F);
A: for x being object st x in the carrier of V
ex y being object st y in the carrier of F & P[x,y]
proof
let x be object;
assume x in the carrier of V;
per cases;
suppose x = 1.E;
hence ex y being object st y in the carrier of F & P[x,y] by I1;
end;
suppose x = j;
hence ex y being object st y in the carrier of F & P[x,y] by I1;
end;
suppose x <> 1.E & x <> j;
hence ex y being object st y in the carrier of F & P[x,y];
end;
end;
consider l being Function of the carrier of V,the carrier of F such that
L: for x being object st x in the carrier of V holds P[x,l.x]
from FUNCT_2:sch 1(A);
reconsider l as Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:8;
for v being Element of V st not v in {1V,jV} holds l.v = 0.F
proof
let v being Element of V;
assume not v in {1V,jV};
then v <> 1.E & v <> j by TARSKI:def 2;
hence l.v = 0.F by L;
end;
then reconsider l as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume o in Carrier l;
then consider v being Element of V such that
A1: o = v & l.v <> 0.F by VECTSP_6:1;
(v = 1.E & l.v = a1 - a2) or (v = j & l.v = b1 - b2) by L,A1;
hence o in {1V,jV} by A1,TARSKI:def 2;
end;
then Carrier(l) c= {1V,jV};
then reconsider l as Linear_Combination of {1V,jV} by VECTSP_6:def 4;
1.E = 1.F by I0,C0SP1:def 3; then
I3: 1V <> jV by FIELD_7:def 5;
{1.F, sqrt a} = {1V,jV} by I0,C0SP1:def 3; then
I2: {1V,jV} is linearly-independent by qbase4;
I8: [a1-a2,1.E] in [:the carrier of F,the carrier of E:]
by I1,ZFMISC_1:def 2;
I6: l.1V * 1V
= ((the multF of E)|[:the carrier of F,the carrier of E:]).(l.1V,1.E)
by FIELD_4:def 6
.= ((the multF of E)|[:the carrier of F,the carrier of E:]).(a1-a2,1.E)
by I3,L
.= (a1 - a2) * 1.E by I8,FUNCT_1:49;
I8: [b1-b2,j] in [:the carrier of F,the carrier of E:]
by I1,ZFMISC_1:def 2;
I7: l.jV * jV
= ((the multF of E)|[:the carrier of F,the carrier of E:]).(l.jV,j)
by FIELD_4:def 6
.= ((the multF of E)|[:the carrier of F,the carrier of E:]).(b1-b2,j)
by I3,L
.= (b1 - b2) * j by I8,FUNCT_1:49
.= j * (b1 - b2) by GROUP_1:def 12;
l.1V * 1V + l.jV * jV
= (the addF of E).(a1-a2,j*(b1-b2)) by I6,I7,FIELD_4:def 6
.= 0.V by AS,FIELD_4:def 6; then
I5: l.1V = 0.F & l.jV = 0.F by I2,I3,VECTSP_7:6;
l.1V = a1 - a2 by I3,L; then
a1 - a2 = 0.E by I5,I0,C0SP1:def 3;
hence a1 = a2 by RLVECT_1:21;
l.jV = b1 - b2 by I3,L; then
b1 - b2 = 0.E by I5,I0,C0SP1:def 3;
hence b1 = b2 by RLVECT_1:21;
end;
begin :: Splittingfields for quadratic Polynomials
definition
let F be non 2-characteristic Field;
let p be quadratic Element of the carrier of Polynom-Ring F;
attr p is DC-square means :defDCps:
DC p is square;
end;
registration
let F be non 2-characteristic Field;
cluster monic DC-square for
quadratic Element of the carrier of Polynom-Ring F;
existence
proof
reconsider p = <%0.F,0.F,1.F%> as
quadratic Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
DC p = - 4 '*' 0.F by defDCpq
.= (-4) '*' (1.F * 0.F) by RING_3:63
.= ((-4) '*' 1.F) * 0.F by REALALG2:5;
then p is DC-square;
hence thesis;
end;
end;
registration
let F be non quadratic_complete non 2-characteristic Field;
cluster monic non DC-square for
quadratic Element of the carrier of Polynom-Ring F;
existence
proof
set a = the non square Element of F;
reconsider p = <%-a,0.F,1.F%> as
quadratic Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
take p;
A: DC p = - 4 '*' (-a) by defDCpq.= --(4 '*' a) by REALALG2:6;
H: 2 '*' 1.F <> 0.F & 4 '*' 1.F <> 0.F by ch2,ch4;
now assume p is DC-square; then
consider w being Element of F such that
C: w^2 = 4 '*' a by A,O_RING_1:def 2;
w * w = 4 '*' (1.F * a) by C,O_RING_1:def 1
.= (4 '*' 1.F) * a by REALALG2:5
.= a * (4 '*' 1.F) by GROUP_1:def 12; then
(w * w) * (4 '*' 1.F)"
= a * ((4 '*' 1.F) * (4 '*' 1.F)") by GROUP_1:def 3
.= a * ((4 '*' 1.F)" * (4 '*' 1.F)) by GROUP_1:def 12
.= a * 1.F by H,VECTSP_1:def 10; then
a = (w * w) * ((2*2) '*' 1.F)"
.= (w * w) * ((2 '*' 1.F) * (2 '*' 1.F))" by RING_3:67
.= (w * w) * ((2 '*' 1.F)" * (2 '*' 1.F)") by H,VECTSP_2:11
.= w * (w * ((2 '*' 1.F)" * (2 '*' 1.F)")) by GROUP_1:def 3
.= w * ((w * (2 '*' 1.F)") * (2 '*' 1.F)") by GROUP_1:def 3
.= w * ((2 '*' 1.F)" * (w * (2 '*' 1.F)")) by GROUP_1:def 12
.= (w * (2 '*' 1.F)") * (w * (2 '*' 1.F)") by GROUP_1:def 3
.= (w * (2 '*' 1.F)")^2 by O_RING_1:def 1;
hence contradiction;
end;
hence thesis;
end;
end;
registration
let F be non quadratic_complete non 2-characteristic Field;
let p be non DC-square quadratic Element of the carrier of Polynom-Ring F;
cluster DC p -> non square;
coherence by defDCps;
end;
registration
let F be non quadratic_complete non 2-characteristic Field;
let p be non DC-square quadratic Element of the carrier of Polynom-Ring F;
cluster X^2-(DC p) -> irreducible;
coherence;
end;
registration
let F be non 2-characteristic Field;
let p be DC-square quadratic Element of the carrier of Polynom-Ring F;
cluster X^2-(DC p) -> reducible;
coherence
proof
DC p is square by defDCps; hence thesis;
end;
end;
theorem
for F being non 2-characteristic Field,
p being quadratic Element of the carrier of Polynom-Ring F
holds F is SplittingField of p iff DC p is square
proof
let F be non 2-characteristic Field;
let p be quadratic Element of the carrier of Polynom-Ring F;
consider a being non zero Element of F, b,c being Element of F such that
A: p = <%c,b,a%> by qua5;
B: now assume DC p is square; then
b^2 - 4 '*' a * c is square by A,defDC; then
consider w being Element of F such that
C: w^2 = b^2 - 4 '*' a * c by O_RING_1:def 2;
set r1 = (-b + w) * (2 '*' a)", r2 = (-b - w) * (2 '*' a)";
D: <%c,b,a%> = a * (X-r1) *' (X-r2) by C,lemred;
rpoly(1,r1) is Ppoly of F & rpoly(1,r2) is Ppoly of F by RING_5:51; then
E: rpoly(1,r1) *' rpoly(1,r2) is Ppoly of F by RING_5:52;
F: F is FieldExtension of F by FIELD_4:6;
now let E be FieldExtension of F;
assume F1: p splits_in E & E is Subfield of F;
F is Subfield of E by FIELD_4:7;
hence E == F by F1,FIELD_7:def 2;
end;
hence F is SplittingField of p by E,F,A,D,FIELD_4:def 5,FIELD_8:def 1;
end;
now assume F is SplittingField of p; then
p splits_in F by FIELD_8:def 1; then
consider x being non zero Element of F, q being Ppoly of F such that
G: p = x * q by FIELD_4:def 5;
Roots p <> {} by G; then
b^2 - 4 '*' a * c is square by A,lemeval2;
hence DC p is square by A,defDC;
end;
hence thesis by B;
end;
registration
let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field,
p be non DC-square quadratic Element of the carrier of Polynom-Ring F;
cluster sqrt(DC p) -> non zero F-algebraic;
coherence;
end;
definition
let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field,
p be non DC-square quadratic Element of the carrier of Polynom-Ring F;
func RootDC p -> Element of FAdj(F,{sqrt(DC p)}) equals
sqrt(DC p);
coherence
proof
sqrt(DC p) in {sqrt(DC p)} &
{sqrt(DC p)} is Subset of FAdj(F,{sqrt(DC p)}) by TARSKI:def 1,FIELD_6:35;
hence thesis;
end;
end;
definition
let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field,
p be non DC-square quadratic Element of the carrier of Polynom-Ring F;
func Root1 p -> Element of FAdj(F,{sqrt(DC p)}) equals
(-@(p.1,FAdj(F,{sqrt(DC p)})) + (RootDC p))
* (2 '*' @(p.2,FAdj(F,{sqrt(DC p)})))";
coherence;
func Root2 p -> Element of FAdj(F,{sqrt(DC p)}) equals
(-@(p.1,FAdj(F,{sqrt(DC p)})) - (RootDC p))
* (2 '*' @(p.2,FAdj(F,{sqrt(DC p)})))";
coherence;
end;
reserve
p for non DC-square quadratic Element of the carrier of Polynom-Ring F;
theorem Z1:
(RootDC p) * (RootDC p) = DC p
proof
A: FAdj(F,{sqrt(DC p)}) is Subring of embField(canHomP X^2-(DC p))
by FIELD_4:def 1;
thus (RootDC p) * (RootDC p)
= sqrt(DC p) * sqrt(DC p) by A,FIELD_6:16 .= DC p by m1;
end;
theorem Z2:
for a being non zero Element of FAdj(F,{sqrt(DC p)}),
b,c being Element of FAdj(F,{sqrt(DC p)})
st p = <%c,b,a%>
holds Root1 p = (-b + (RootDC p)) * (2 '*' a)" &
Root2 p = (-b - (RootDC p)) * (2 '*' a)"
proof
let a be non zero Element of FAdj(F,{sqrt(DC p)}),
b,c be Element of FAdj(F,{sqrt(DC p)});
reconsider E = FAdj(F,{sqrt(DC p)}) as
F-extending FieldExtension of FAdj(F,{sqrt(DC p)}) by FIELD_4:6;
assume p = <%c,b,a%>; then
H: p.1 = b & p.2 = a by qua1;
A: @(b,E) = b & @(a,E) = a by FIELD_7:def 4; then
@(b,E) = @(p.1,E) by H,FIELD_7:def 4;
hence thesis by A,H,FIELD_7:def 4;
end;
theorem Z5:
p = @(LC p,FAdj(F,{sqrt(DC p)})) * (X-(Root1 p)) *' (X-(Root2 p))
proof
set E = FAdj(F,{sqrt(DC p)});
K: F is Subring of E by FIELD_4:def 1; then
H: E is non 2-characteristic;
consider a being non zero Element of F, b,c being Element of F such that
A: p = <%c,b,a%> by qua5;
I: @(c,E) = c & @(b,E) = b & @(a,E) = a by FIELD_7:def 4; then
B: p = <%@(c,E),@(b,E),@(a,E)%> by A,eval2;
E: now assume E1: @(a,E) is zero;
a = @(a,E) by FIELD_7:def 4 .= 0.F by E1,K,C0SP1:def 3;
hence contradiction;
end;
C: Root1 p = (-@(b,E) + (RootDC p)) * (2 '*' @(a,E))" by E,B,Z2;
D: Root2 p = (-@(b,E) - (RootDC p)) * (2 '*' @(a,E))" by E,B,Z2;
J: (RootDC p)^2 = (RootDC p) * (RootDC p) by O_RING_1:def 1
.= DC p by Z1
.= b^2 - 4 '*' a * c by A,defDC;
J1: b^2 = b * b by O_RING_1:def 1
.= @(b,E) * @(b,E) by I,K,FIELD_6:16
.= @(b,E)^2 by O_RING_1:def 1;
4 '*' a * c = 4 '*' (a * c) by REALALG2:5
.= 4 '*' (@(a,E) * @(c,E)) by Z3,I,K,FIELD_6:16
.= 4 '*' @(a,E) * @(c,E) by REALALG2:5; then
- (4 '*' a * c) = - (4 '*' @(a,E) * @(c,E)) by K,FIELD_6:17;
then
F: b^2 - 4 '*' a * c = @(b,E)^2 - 4 '*' @(a,E) * @(c,E) by K,J1,FIELD_6:15;
len p = 3 by A,qua3; then
G: len p -' 1 = 3 - 1 by XREAL_0:def 2;
@(a,E) = a by FIELD_7:def 4
.= p.2 by A,qua1
.= LC p by G,RATFUNC1:def 6
.= @(LC p,E) by FIELD_7:def 4;
hence thesis by F,J,H,E,D,C,B,lemred;
end;
theorem Z4:
Roots(FAdj(F,{sqrt(DC p)}),p) = { Root1 p, Root2 p }
proof
set E = FAdj(F,{sqrt(DC p)}), r1 = Root1 p, r2 = Root2 p;
reconsider q = @(LC p,E) * (X-r1) *' (X-r2) as
Element of the carrier of Polynom-Ring E by POLYNOM3:def 10;
K: F is Subring of E by FIELD_4:def 1;
Y: Roots(E,p) = Roots(q) by Z5,FIELD_7:13;
Z: now assume Y1: @(LC p,E) is zero;
LC p = @(LC p,E) by FIELD_7:def 4 .= 0.F by Y1,K,C0SP1:def 3;
hence contradiction;
end;
Roots rpoly(1,r1) = {r1} & Roots rpoly(1,r2) = {r2} by RING_5:18; then
Roots(rpoly(1,r1) *' rpoly(1,r2))
= {r1} \/ {r2} by UPROOTS:23 .= {r1,r2} by ENUMSET1:1;
hence thesis by Y,Z,RING_5:19;
end;
theorem
Root1 p <> Root2 p
proof
set E = FAdj(F,{sqrt(DC p)}), w = RootDC p;
consider a1 being non zero Element of F,
b1,c1 being Element of F such that
A: p = <%c1,b1,a1%> by qua5;
set a = @(a1,E), b = @(b1,E), c = @(c1,E);
I: a = a1 & b = b1 & c = c1 by FIELD_7:def 4; then
B: p = <%c,b,a%> by A,eval2;
J: E is Subring of embField(canHomP X^2-(DC p)) by FIELD_4:def 1;
K: F is Subring of E by FIELD_4:def 1;
E: a is non zero by I,K,C0SP1:def 3;
M: E is non 2-characteristic by K; then
L: 2 '*' a <> 0.E by E,ch2;
now assume Root1 p = Root2 p; then
(-b + w)*(2'*'a)" = Root2 p by E,B,Z2 .= (-b - w)*(2'*'a)" by E,B,Z2;
then ((-b + w) * (2 '*' a)") * (2 '*' a)
= (-b - w) * ((2 '*' a)" * (2 '*' a)) by GROUP_1:def 3
.= (-b - w) * 1.E by L,VECTSP_1:def 10;
then - b - w = (-b + w) * ((2 '*' a)" * (2 '*' a) ) by GROUP_1:def 3
.= (-b + w) * 1.E by L,VECTSP_1:def 10;
then b + ((-b) - w) = (b + (-b)) + w by RLVECT_1:def 3
.= 0.E + w by RLVECT_1:5;
then w = (b + (-b)) + -w by RLVECT_1:def 3 .= 0.E + -w by RLVECT_1:5;
then w + w = 0.E by RLVECT_1:5;
then 2 '*' w = 0.E by RING_5:2;
then w = 0.E by M,ch2
.= 0.embField(canHomP X^2-(DC p)) by J,C0SP1:def 3;
hence contradiction;
end;
hence thesis;
end;
theorem
deg(FAdj(F,{sqrt(DC p)}),F) = 2 by dega;
theorem
FAdj(F,{sqrt(DC p)}) is SplittingField of p
proof
set E = FAdj(F,{sqrt(DC p)}), r1 = Root1 p, r2 = Root2 p;
reconsider q = rpoly(1,r1) *' rpoly(1,r2) as
Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
K: F is Subring of E by FIELD_4:def 1;
Y: now assume Y1: @(LC p,E) is zero;
LC p = @(LC p,E) by FIELD_7:def 4 .= 0.F by Y1,K,C0SP1:def 3;
hence contradiction;
end;
rpoly(1,r1) *' rpoly(1,r2) = (X-r1) *' (X-r2); then
D: p = @(LC p,FAdj(F,{sqrt(DC p)})) * (rpoly(1,r1) *' rpoly(1,r2)) by Z5;
rpoly(1,r1) is Ppoly of E & rpoly(1,r2) is Ppoly of E by RING_5:51;
then rpoly(1,r1) *' rpoly(1,r2) is Ppoly of E by RING_5:52; then
A: p splits_in E by Y,D,FIELD_4:def 5;
now let U be FieldExtension of F;
assume D0: p splits_in U & U is Subfield of E; then
D3: E is U-extending & U is Subring of E by FIELD_5:12,FIELD_4:7;
D4: Roots(E,p) c= the carrier of U by D3,D0,A,FIELD_8:27;
Roots(E,p) = { Root1 p, Root2 p } by Z4; then
Root1 p in Roots(E,p) by TARSKI:def 2; then
reconsider w = Root1 p as Element of U by D4;
sqrt(DC p) in the carrier of U
proof
consider aF being non zero Element of F,
bF,cF being Element of F such that
A1: p = <%cF,bF,aF%> by qua5;
set aE = @(aF,E), bE = @(bF,E), cE = @(cF,E);
C1: now assume C2: aE is zero;
aF = 0.E by C2,FIELD_7:def 4 .= 0.F by K,C0SP1:def 3;
hence contradiction;
end;
E is non 2-characteristic by K; then
C3: 2 '*' aE <> 0.E by C1,ch2;
I1: aE = aF & bE = bF & cE = cF by FIELD_7:def 4; then
p = <%cE,bE,aE%> by A1,eval2; then
Root1 p = (-bE + (RootDC p)) * (2 '*' aE)" by C1,Z2; then
(Root1 p) * (2 '*' aE)
= (-bE + (RootDC p)) * ((2 '*' aE)" * (2 '*' aE)) by GROUP_1:def 3
.= (-bE + (RootDC p)) * 1.E by C3,VECTSP_1:def 10; then
B: bE + (Root1 p) * (2 '*' aE)
= (bE + -bE) + (RootDC p) by RLVECT_1:def 3
.= 0.E + RootDC p by RLVECT_1:5;
set aU = @(aF,U), bU = @(bF,U), cU = @(cF,U);
I2: aU = aF & bU = bF & cU = cF by FIELD_7:def 4;
2 '*' aU = 2 '*' aE by D3,I2,Z3,FIELD_7:def 4; then
w * (2 '*' aU) = (Root1 p) * (2 '*' aE) by D3,FIELD_6:16; then
bU + w * (2 '*' aU) = bE + (Root1 p) * (2 '*' aE) by D3,I1,I2,FIELD_6:15;
hence thesis by B;
end; then
D1: {sqrt(DC p)} c= the carrier of U by TARSKI:def 1;
D2: U is Subfield of embField(canHomP X^2-(DC p)) by D0,EC_PF_1:5;
F is Subfield of U by FIELD_4:7;
then E is Subfield of U by D1,D2,FIELD_6:37;
hence U == E by D0,FIELD_7:def 2;
end;
hence thesis by A,FIELD_8:def 1;
end;
begin :: Quadratic Extensions
definition
let F be Field,
E be FieldExtension of F;
attr E is F-quadratic means
deg(E,F) = 2;
end;
registration
let F be non quadratic_complete polynomial_disjoint non 2-characteristic Field;
cluster F-quadratic for FieldExtension of F;
existence
proof
set a = the non square Element of F;
take FAdj(F,{sqrt a});
thus thesis by dega;
end;
end;
registration
let F be Field;
cluster F-quadratic -> F-finite for FieldExtension of F;
coherence
proof
let E be FieldExtension of F;
assume E is F-quadratic;
then VecSp(E,F) is finite-dimensional by FIELD_4:def 7;
hence E is F-finite by FIELD_4:def 8;
end;
end;
registration
let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field;
let a be non square Element of F;
cluster FAdj(F,{sqrt a}) -> F-quadratic;
coherence by dega;
end;
theorem m105:
for F being Field
for a,b being Element of F st b^2 = a holds eval(X^2-a,b) = 0.F
proof
let F be Field; let a,b be Element of F;
assume b^2 = a; then
A: - a = -(b * b) by O_RING_1:def 1 .= b * (-b) by VECTSP_1:8;
thus eval(X^2-a,b)
= eval(<%-a,-0.F,1.F%>,b)
.= eval(<%b*(-b),-(b+-b),1.F%>,b) by A,RLVECT_1:5
.= eval(rpoly(1,b) *' rpoly(1,-b),b) by lemred3z
.= eval(rpoly(1,b),b) * eval(rpoly(1,-b),b) by POLYNOM4:24
.= (b - b) * eval(X--b,b) by HURWITZ:29
.= 0.F * eval(X--b,b) by RLVECT_1:15
.= 0.F;
end;
theorem m102:
for F being non 2-characteristic Field,
E being FieldExtension of F
for a being Element of F st not(ex b being Element of F st a = b^2)
for b being Element of E st b^2 = a
holds FAdj(F,{b}) is SplittingField of X^2-a & deg(FAdj(F,{b}),F) = 2
proof
let F be non 2-characteristic Field, E be FieldExtension of F;
let a be Element of F;
assume AS1: not(ex b being Element of F st a = b^2);
let b be Element of E;
assume AS2: b^2 = a;
reconsider a1 = a as square Element of E by AS2;
F is Subring of E by FIELD_4:def 1; then
H1: 0.E = 0.F & 1.E = 1.F & -a1 = -a by FIELD_6:17,C0SP1:def 3;
H0: b*(-b) = -(b*b) by VECTSP_1:8 .= -a1 by AS2,O_RING_1:def 1;
H2: X^2-a = <%-a1,-0.E,1.E%> by H1
.= <%b*(-b),-(b+(-b)),1.E%> by H0,RLVECT_1:5
.= rpoly(1,b) *' rpoly(1,-b) by lemred3z;
rpoly(1,b) is Ppoly of E & rpoly(1,-b) is Ppoly of E by RING_5:51;
then reconsider p = X^2-a as Ppoly of E by H2,RING_5:52;
H3: 1.E * p = X^2-a; then
H11: X^2-a splits_in E by FIELD_4:def 5;
H5: Roots rpoly(1,b) = {b} & Roots rpoly(1,-b) = {-b} by RING_5:18;
H9: Roots(E,X^2-a) = Roots X^2-a1 by H1,FIELD_7:13
.= {b} \/ {-b} by H2,H1,H5,UPROOTS:23
.= {b,-b} by ENUMSET1:1; then
X^2-a splits_in FAdj(F,{b,-b}) by H3,FIELD_8:30,FIELD_4:def 5; then
H: X^2-a splits_in FAdj(F,{b}) by ext1;
now let U be FieldExtension of F;
assume AS: X^2-a splits_in U & U is Subfield of FAdj(F,{b}); then
H8: FAdj(F,{b}) is FieldExtension of U &
E is FieldExtension of FAdj(F,{b}) by FIELD_4:7; then
H6: U is Subfield of E by FIELD_4:7;
H7: F is Subfield of U by FIELD_4:7;
Roots(E,X^2-a) = Roots(U,X^2-a) by H11,AS,H8,FIELD_8:29; then
H10: b in Roots(U,X^2-a) by H9,TARSKI:def 2;
now let o be object;
assume o in {b};
then o = b by TARSKI:def 1;
hence o in the carrier of U by H10;
end;
then {b} c= the carrier of U;
then FAdj(F,{b}) is Subfield of U by H6,H7,FIELD_6:37;
hence U == FAdj(F,{b}) by AS,FIELD_7:def 2;
end;
hence FAdj(F,{b}) is SplittingField of X^2-a by H,FIELD_8:def 1;
eval(X^2-a1,b) = 0.E by AS2,m105; then
H12: Ext_eval(X^2-a,b) = 0.E by H1,FIELD_4:26; then
reconsider b1 = b as F-algebraic Element of E by FIELD_6:43;
X^2-a is irreducible by naH2,AS1,O_RING_1:def 2; then
H11: MinPoly(b1,F) = NormPolynomial X^2-a by H12,FIELD_8:15
.= X^2-a by RING_4:24;
deg X^2-a = 2 by defquadr;
hence thesis by H11,FIELD_6:67;
end;
unique20:
for F1,F2 being Field
st F1 is Subfield of F2 & F2 is Subfield of F1
for f being Function of F1,F2 st f = id F1 holds f is isomorphism
proof
let F1,F2 be Field;
assume AS1: F1 is Subfield of F2 & F2 is Subfield of F1;
let f be Function of F1,F2;
assume AS2: f = id F1;
the carrier of F1 c= the carrier of F2 &
the carrier of F2 c= the carrier of F1 by AS1,EC_PF_1:def 1; then
A: the carrier of F2 = the carrier of F1 by TARSKI:2;
C: the addF of F1
= (the addF of F2) || the carrier of F1 by AS1,EC_PF_1:def 1
.= the addF of F2 by A;
D: the multF of F1
= (the multF of F2) || the carrier of F1 by AS1,EC_PF_1:def 1
.= the multF of F2 by A;
f is additive multiplicative unity-preserving by C,D,AS2,AS1,EC_PF_1:def 1;
hence thesis by A,AS2;
end;
theorem
for F being non 2-characteristic Field
for E being FieldExtension of F
holds deg(E,F) = 2 iff
(ex a being Element of F
st not(ex b being Element of F st a = b^2) &
ex b being Element of E st a = b^2 & E == FAdj(F,{b}))
proof
let F be non 2-characteristic Field;
let E be FieldExtension of F;
H1: F is Subring of E & F is Subfield of E by FIELD_4:def 1,FIELD_4:7; then
H2: the carrier of F c= the carrier of E by C0SP1:def 3;
A:now assume AS: E is F-quadratic; then
reconsider K = E as F-finite FieldExtension of F;
now assume not ex a being Element of K st not a in the carrier of F;
then the carrier of K c= the carrier of F;
hence contradiction by H2,TARSKI:2,AS,FIELD_7:7;
end; then
consider a being Element of K such that A: not a in the carrier of F;
B: deg(FAdj(F,{a}),F) = 2
proof
K is FAdj(F,{a})-extending by FIELD_4:7; then
C1: deg(FAdj(F,{a}),F) <= 2 by AS,FIELD_5:15;
now assume deg(FAdj(F,{a}),F) < 1 + 1; then
C2: deg(FAdj(F,{a}),F) <= 1 by NAT_1:13;
deg(FAdj(F,{a}),F) + 1 > 0 + 1 by XREAL_1:6; then
deg(FAdj(F,{a}),F) >= 1 by NAT_1:13; then
C3: the carrier of FAdj(F,{a}) = the carrier of F
by C2,XXREAL_0:1,FIELD_7:7;
C4: {a} is Subset of FAdj(F,{a}) by FIELD_6:35;
a in {a} by TARSKI:def 1;
hence contradiction by A,C3,C4;
end;
hence thesis by C1,XXREAL_0:1;
end; then
deg MinPoly(a,F) = 2 by FIELD_6:67; then
reconsider p = MinPoly(a,F) as
quadratic Element of the carrier of Polynom-Ring F by defquadr;
D: K == FAdj(F,{a})
proof
D1: VecSp(K,F) is finite-dimensional by FIELD_4:def 8;
D2: dim VecSp(K,F) = 2 by AS,FIELD_4:def 7
.= dim VecSp(FAdj(F,{a}),F) by B,FIELD_4:def 7;
K is FAdj(F,{a})-extending by FIELD_4:7; then
VecSp(FAdj(F,{a}),F) is Subspace of VecSp(K,F) by FIELD_5:14; then
(Omega).VecSp(K,F) = (Omega).VecSp(FAdj(F,{a}),F) by D1,D2,VECTSP_9:28;
then the carrier of VecSp(K,F)
= the carrier of (Omega).VecSp(FAdj(F,{a}),F) by VECTSP_4:def 4
.= the carrier of VecSp(FAdj(F,{a}),F) by VECTSP_4:def 4
.= the carrier of FAdj(F,{a}) by FIELD_4:def 6; then
D3: the carrier of K = the carrier of FAdj(F,{a}) by FIELD_4:def 6;
K is Subfield of FAdj(F,{a})
proof
the addF of FAdj(F,{a}) = (the addF of K)||the carrier of FAdj(F,{a}) &
the multF of FAdj(F,{a}) = (the multF of K)||the carrier of FAdj(F,{a})
& 1.FAdj(F,{a}) = 1.K & 0.FAdj(F,{a}) = 0.K by EC_PF_1:def 1;
hence thesis by D3,EC_PF_1:def 1;
end;
hence thesis by FIELD_7:def 2;
end;
consider b,c being Element of F such that E: p = <%c,b,1.F%> by qua5a;
reconsider b1 = b, c1 = c as Element of K by H2;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring K by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring K;
1.F = 1.K by H1,C0SP1:def 3; then
F: p = <%c1,b1,1.K%> by E,eval2;
0.K = Ext_eval(p,a) by FIELD_6:51 .= eval(p1,a) by FIELD_4:26; then
a is_a_root_of p1; then
G: a in Roots p1 by POLYNOM5:def 10;
G1: b1^2 = b1 * b1 by O_RING_1:def 1
.= b * b by H1,FIELD_6:16 .= b^2 by O_RING_1:def 1;
4 '*' c1 = 4 '*' c by Z3; then
- (4 '*' c1) = - (4 '*' c) by H1,FIELD_6:17; then
U2: b1^2 - 4 '*' c1 = b^2 - 4 '*' c by G1,H1,FIELD_6:15;
I: b1^2 - 4 '*' 1.K * c1
= b1^2 - 4 '*' (1.K * c1) by REALALG2:5
.= b1^2 - 4 '*' c1; then
consider u being Element of K such that
U1: u^2 = b1^2 - 4 '*' c1 by G,F,lemeval2,O_RING_1:def 2;
reconsider u1 = u as Element of E;
L0: K is non 2-characteristic by H1; then
L1: Roots <%c1,b1,1.K%> = {(-b1+u) * (2'*'1.K)", (-b1-u) * (2'*'1.K)" }
by I,U1,TC0;
G5: 2 '*' 1.K is non zero by L0,ch2;
0.K = Ext_eval(p,a) by FIELD_6:51 .= eval(p1,a) by FIELD_4:26; then
a is_a_root_of p1; then
L2: a in Roots p1 by POLYNOM5:def 10;
L3: u = b1 + a * (2 '*' 1.K) or u = -(b1 + a * (2 '*' 1.K))
proof
per cases by L2,F,L1,TARSKI:def 2;
suppose a = (-b1 + u) * (2 '*' 1.K)";
then a * (2 '*' 1.K)
= (-b1 + u) * ((2 '*' 1.K)" * (2 '*' 1.K)) by GROUP_1:def 3
.= (-b1 + u) * 1.K by G5,VECTSP_1:def 10;
then b1 + a * (2 '*' 1.K)
= (b1 + -b1) + u by RLVECT_1:def 3
.= 0.K + u by RLVECT_1:5;
hence thesis;
end;
suppose a = (-b1 - u) * (2 '*' 1.K)";
then a * (2 '*' 1.K)
= (-b1 - u) * ((2 '*' 1.K)" * (2 '*' 1.K)) by GROUP_1:def 3
.= (-b1 - u) * 1.K by G5,VECTSP_1:def 10;
then b1 + a * (2 '*' 1.K)
= (b1 + -b1) - u by RLVECT_1:def 3
.= 0.K - u by RLVECT_1:5;
hence thesis;
end;
end;
U3: FAdj(F,{a}) = FAdj(F,{u})
proof
G2: K is FAdj(F,{a})-extending &
K is FAdj(F,{u})-extending by FIELD_4:7; then
G3: F is Subfield of FAdj(F,{u}) & F is Subfield of FAdj(F,{a}) &
FAdj(F,{u}) is Subring of K & FAdj(F,{a}) is Subring of K
by FIELD_6:36,FIELD_4:def 1; then
I1: the carrier of F c= the carrier of FAdj(F,{u}) &
the carrier of F c= the carrier of FAdj(F,{a}) by EC_PF_1:def 1;
I2: {u} is Subset of FAdj(F,{u}) & {a} is Subset of FAdj(F,{a})
by FIELD_6:35;
u in {u} by TARSKI:def 1; then
reconsider b2 = b, c2 = c, u2 = u as Element of FAdj(F,{u}) by I1,I2;
a = (-b2 + u2) * (2 '*' 1.FAdj(F,{u}))" or
a = (-b2 - u2) * (2 '*' 1.FAdj(F,{u}))"
proof
1.K = 1.FAdj(F,{u}) by G3,C0SP1:def 3; then
2 '*' 1.K = 2 '*' 1.FAdj(F,{u}) by G2,Z3; then
G4: (2 '*' 1.K)" = (2 '*' 1.FAdj(F,{u}))" by G5,FIELD_6:18;
G6: -b1 = -b2 & -u = -u2 by G3,FIELD_6:17;
per cases by L2,F,L1,TARSKI:def 2;
suppose K: a = (-b1 + u) * (2 '*' 1.K)";
(-b1 + u) = (-b2 + u2) by G6,G3,FIELD_6:15;
hence thesis by K,G3,G4,FIELD_6:16;
end;
suppose K: a = (-b1 - u) * (2 '*' 1.K)";
(-b1 - u) = (-b2 - u2) by G6,G3,FIELD_6:15;
hence thesis by K,G3,G4,FIELD_6:16;
end;
end; then
a in the carrier of FAdj(F,{u}); then
{a} c= the carrier of FAdj(F,{u}) by TARSKI:def 1; then
G4: FAdj(F,{a}) is Subfield of FAdj(F,{u}) by G3,FIELD_6:37;
a in {a} by TARSKI:def 1; then
reconsider b2 = b, c2 = c, a2 = a as Element of FAdj(F,{a}) by I1,I2;
u = b2 + a2 * (2 '*' 1.FAdj(F,{a})) or
u = -(b2 + a2 * (2 '*' 1.FAdj(F,{a})))
proof
1.K = 1.FAdj(F,{a}) by G3,C0SP1:def 3; then
2 '*' 1.K = 2 '*' 1.FAdj(F,{a}) by G2,Z3; then
G6: a * (2 '*' 1.K) = a2 * (2 '*' 1.FAdj(F,{a})) by G3,FIELD_6:16; then
G5: b1 + a * (2 '*' 1.K) = b2 + a2 * (2 '*' 1.FAdj(F,{a}))
by G3,FIELD_6:15;
per cases by L3;
suppose u = b1 + a * (2 '*' 1.K);
hence thesis by G6,G3,FIELD_6:15;
end;
suppose u = -(b1 + a * (2 '*' 1.K));
hence thesis by G3,G5,FIELD_6:17;
end;
end; then
u in the carrier of FAdj(F,{a}); then
{u} c= the carrier of FAdj(F,{a}) by TARSKI:def 1; then
FAdj(F,{u}) is Subfield of FAdj(F,{a}) by G3,FIELD_6:37;
hence FAdj(F,{a}) = FAdj(F,{u}) by G4,EC_PF_1:4;
end;
U4: now assume ex w being Element of F st b^2 - 4 '*' c = w^2; then
consider w being Element of F such that G7: b^2 - 4 '*' c = w^2;
1.F = 1.K by H1,C0SP1:def 3; then
F2: 2 '*' 1.F = 2 '*' 1.K by Z3;
2 '*' 1.K is non zero by L0,ch2; then
F3: (2 '*' 1.F)" = (2 '*' 1.K)" by H1,F2,FIELD_6:18;
F4: -b1 = -b by H1,FIELD_6:17;
per cases by G7,U1,U2,lemquadr;
suppose S: u = w; then
-b1 + u = -b + w by H1,F4,FIELD_6:15; then
F5: (-b1 + u) * (2 '*' 1.K)" = (-b + w) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
-u = -w by H1,S,FIELD_6:17; then
(-b1 - u) = (-b - w) by H1,F4,FIELD_6:15; then
F6: (-b1 - u) * (2 '*' 1.K)" = (-b - w) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
per cases by L2,F,L1,TARSKI:def 2;
suppose a = (-b1 + u) * (2 '*' 1.K)";
hence contradiction by F5,A;
end;
suppose a = (-b1 - u) * (2 '*' 1.K)";
hence contradiction by F6,A;
end;
end;
suppose S: u = -w;then
-b1 + u = -b + (-w) by H1,F4,FIELD_6:15; then
F5: (-b1 + u) * (2 '*' 1.K)" = (-b + (-w)) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
-u = --w by H1,S,FIELD_6:17; then
(-b1 - u) = (-b + w) by H1,F4,FIELD_6:15; then
F6: (-b1 - u) * (2 '*' 1.K)" = (-b + w) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
per cases by L2,F,L1,TARSKI:def 2;
suppose a = (-b1 + u) * (2 '*' 1.K)";
hence contradiction by F5,A;
end;
suppose a = (-b1 - u) * (2 '*' 1.K)";
hence contradiction by F6,A;
end;
end;
end;
thus ex a being Element of F
st not(ex b being Element of F st a = b^2) &
ex b being Element of E
st a = b^2 & E == FAdj(F,{b}) by U1,U2,U3,U4,D;
end;
now assume ex a being Element of F
st not(ex b being Element of F st a = b^2) &
ex b being Element of E st a = b^2 & E == FAdj(F,{b}); then
consider a being Element of F such that
B: not(ex b being Element of F st a = b^2) &
ex b being Element of E
st a = b^2 & E == FAdj(F,{b});
consider b being Element of E such that
C: a = b^2 & E == FAdj(F,{b}) by B;
deg(FAdj(F,{b}),F) = 2 by B,C,m102;
hence deg(E,F) = 2 by C,FIELD_7:5;
end;
hence thesis by A;
end;
theorem
for E being FieldExtension of F holds
E is F-quadratic iff
ex a being non square Element of F st E,FAdj(F,{sqrt a}) are_isomorphic_over F
proof
let E be FieldExtension of F;
H1: F is Subring of E & F is Subfield of E by FIELD_4:def 1,FIELD_4:7; then
H2: the carrier of F c= the carrier of E by C0SP1:def 3;
A:now assume AS: E is F-quadratic; then
reconsider K = E as F-finite FieldExtension of F;
now assume not ex a being Element of K st not a in the carrier of F;
then the carrier of K c= the carrier of F;
hence contradiction by AS,H2,TARSKI:2,FIELD_7:7;
end; then
consider a being Element of K such that A: not a in the carrier of F;
B: deg(FAdj(F,{a}),F) = 2
proof
K is FAdj(F,{a})-extending by FIELD_4:7; then
C1: deg(FAdj(F,{a}),F) <= 2 by AS,FIELD_5:15;
now assume deg(FAdj(F,{a}),F) < 1 + 1; then
C2: deg(FAdj(F,{a}),F) <= 1 by NAT_1:13;
deg(FAdj(F,{a}),F) + 1 > 0 + 1 by XREAL_1:6; then
deg(FAdj(F,{a}),F) >= 1 by NAT_1:13; then
C3: the carrier of FAdj(F,{a}) = the carrier of F
by C2,XXREAL_0:1,FIELD_7:7;
C4: {a} is Subset of FAdj(F,{a}) by FIELD_6:35;
a in {a} by TARSKI:def 1;
hence contradiction by A,C3,C4;
end;
hence thesis by C1,XXREAL_0:1;
end; then
deg MinPoly(a,F) = 2 by FIELD_6:67; then
reconsider p = MinPoly(a,F) as
quadratic Element of the carrier of Polynom-Ring F by defquadr;
D: K, FAdj(F,{a}) are_isomorphic_over F
proof
D1: VecSp(K,F) is finite-dimensional by FIELD_4:def 8;
D2: dim VecSp(K,F) = 2 by AS,FIELD_4:def 7
.= dim VecSp(FAdj(F,{a}),F) by B,FIELD_4:def 7;
D3: K is FAdj(F,{a})-extending by FIELD_4:7;
VecSp(FAdj(F,{a}),F) is Subspace of VecSp(K,F) by D3,FIELD_5:14; then
(Omega).VecSp(K,F) = (Omega).VecSp(FAdj(F,{a}),F) by D1,D2,VECTSP_9:28;
then
D4: the carrier of VecSp(K,F)
= the carrier of (Omega).VecSp(FAdj(F,{a}),F) by VECTSP_4:def 4
.= the carrier of VecSp(FAdj(F,{a}),F) by VECTSP_4:def 4
.= the carrier of FAdj(F,{a}) by FIELD_4:def 6; then
D8: the carrier of K = the carrier of FAdj(F,{a}) by FIELD_4:def 6;
D6: K is Subfield of FAdj(F,{a})
proof
the addF of FAdj(F,{a}) = (the addF of K)||the carrier of FAdj(F,{a}) &
the multF of FAdj(F,{a}) = (the multF of K)||the carrier of FAdj(F,{a})
& 1.FAdj(F,{a}) = 1.K & 0.FAdj(F,{a}) = 0.K by EC_PF_1:def 1;
hence thesis by D8,EC_PF_1:def 1;
end;
reconsider f = id K as Function of K,FAdj(F,{a}) by D4,FIELD_4:def 6;
D7: f is isomorphism by D6,unique20;
now let a be Element of F;
reconsider a1 = a as Element of E by H2;
f.a1 = a1;
hence f.a = a;
end;
then f is F-fixing;
hence thesis by D7,FIELD_8:def 5;
end;
consider b,c being Element of F such that E: p = <%c,b,1.F%> by qua5a;
reconsider b1 = b, c1 = c as Element of K by H2;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring K by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring K;
1.F = 1.K by H1,C0SP1:def 3; then
F: p = <%c1,b1,1.K%> by E,eval2;
0.K = Ext_eval(p,a) by FIELD_6:51 .= eval(p1,a) by FIELD_4:26; then
a is_a_root_of p1; then
G: a in Roots p1 by POLYNOM5:def 10;
G1: b1^2 = b1 * b1 by O_RING_1:def 1
.= b * b by H1,FIELD_6:16 .= b^2 by O_RING_1:def 1;
4 '*' c1 = 4 '*' c by Z3; then
- (4 '*' c1) = - (4 '*' c) by H1,FIELD_6:17; then
U2: b1^2 - 4 '*' c1 = b^2 - 4 '*' c by G1,H1,FIELD_6:15;
I: b1^2 - 4 '*' 1.K * c1
= b1^2 - 4 '*' (1.K * c1) by REALALG2:5
.= b1^2 - 4 '*' c1; then
consider u being Element of K such that
U1: u^2 = b1^2 - 4 '*' c1 by G,F,lemeval2,O_RING_1:def 2;
L0: K is non 2-characteristic by H1; then
L1: Roots <%c1,b1,1.K%> = {(-b1+u) * (2'*'1.K)", (-b1-u) * (2'*'1.K)" }
by I,U1,TC0;
G5: 2 '*' 1.K is non zero by L0,ch2;
0.K = Ext_eval(p,a) by FIELD_6:51 .= eval(p1,a) by FIELD_4:26; then
a is_a_root_of p1; then
L2: a in Roots p1 by POLYNOM5:def 10;
L3: u = b1 + a * (2 '*' 1.K) or u = -(b1 + a * (2 '*' 1.K))
proof
per cases by L2,F,L1,TARSKI:def 2;
suppose a = (-b1 + u) * (2 '*' 1.K)";
then a * (2 '*' 1.K)
= (-b1 + u) * ((2 '*' 1.K)" * (2 '*' 1.K)) by GROUP_1:def 3
.= (-b1 + u) * 1.K by G5,VECTSP_1:def 10;
then b1 + a * (2 '*' 1.K)
= (b1 + -b1) + u by RLVECT_1:def 3
.= 0.K + u by RLVECT_1:5;
hence thesis;
end;
suppose a = (-b1 - u) * (2 '*' 1.K)";
then a * (2 '*' 1.K)
= (-b1 - u) * ((2 '*' 1.K)" * (2 '*' 1.K)) by GROUP_1:def 3
.= (-b1 - u) * 1.K by G5,VECTSP_1:def 10;
then b1 + a * (2 '*' 1.K)
= (b1 + -b1) - u by RLVECT_1:def 3
.= 0.K - u by RLVECT_1:5;
hence thesis;
end;
end;
U3: FAdj(F,{a}) = FAdj(F,{u})
proof
G2: K is FAdj(F,{a})-extending &
K is FAdj(F,{u})-extending by FIELD_4:7; then
G3: F is Subfield of FAdj(F,{u}) & F is Subfield of FAdj(F,{a}) &
FAdj(F,{u}) is Subring of K & FAdj(F,{a}) is Subring of K
by FIELD_6:36,FIELD_4:def 1; then
I1: the carrier of F c= the carrier of FAdj(F,{u}) &
the carrier of F c= the carrier of FAdj(F,{a}) by EC_PF_1:def 1;
I2: {u} is Subset of FAdj(F,{u}) & {a} is Subset of FAdj(F,{a})
by FIELD_6:35;
u in {u} by TARSKI:def 1; then
reconsider b2 = b, c2 = c, u2 = u as Element of FAdj(F,{u}) by I1,I2;
a = (-b2 + u2) * (2 '*' 1.FAdj(F,{u}))" or
a = (-b2 - u2) * (2 '*' 1.FAdj(F,{u}))"
proof
1.K = 1.FAdj(F,{u}) by G3,C0SP1:def 3; then
2 '*' 1.K = 2 '*' 1.FAdj(F,{u}) by G2,Z3; then
G4: (2 '*' 1.K)" = (2 '*' 1.FAdj(F,{u}))" by G5,FIELD_6:18;
G6: -b1 = -b2 & -u = -u2 by G3,FIELD_6:17;
per cases by L2,F,L1,TARSKI:def 2;
suppose K: a = (-b1 + u) * (2 '*' 1.K)";
(-b1 + u) = (-b2 + u2) by G6,G3,FIELD_6:15;
hence thesis by K,G3,G4,FIELD_6:16;
end;
suppose K: a = (-b1 - u) * (2 '*' 1.K)";
(-b1 - u) = (-b2 - u2) by G6,G3,FIELD_6:15;
hence thesis by K,G3,G4,FIELD_6:16;
end;
end; then
a in the carrier of FAdj(F,{u}); then
{a} c= the carrier of FAdj(F,{u}) by TARSKI:def 1; then
G4: FAdj(F,{a}) is Subfield of FAdj(F,{u}) by G3,FIELD_6:37;
a in {a} by TARSKI:def 1; then
reconsider b2 = b, c2 = c, a2 = a as Element of FAdj(F,{a}) by I1,I2;
u = b2 + a2 * (2 '*' 1.FAdj(F,{a})) or
u = -(b2 + a2 * (2 '*' 1.FAdj(F,{a})))
proof
1.K = 1.FAdj(F,{a}) by G3,C0SP1:def 3; then
2 '*' 1.K = 2 '*' 1.FAdj(F,{a}) by G2,Z3; then
G6: a * (2 '*' 1.K) = a2 * (2 '*' 1.FAdj(F,{a})) by G3,FIELD_6:16; then
G5: b1 + a * (2 '*' 1.K) = b2 + a2 * (2 '*' 1.FAdj(F,{a}))
by G3,FIELD_6:15;
per cases by L3;
suppose u = b1 + a * (2 '*' 1.K);
hence thesis by G6,G3,FIELD_6:15;
end;
suppose u = -(b1 + a * (2 '*' 1.K));
hence thesis by G3,G5,FIELD_6:17;
end;
end; then
u in the carrier of FAdj(F,{a}); then
{u} c= the carrier of FAdj(F,{a}) by TARSKI:def 1; then
FAdj(F,{u}) is Subfield of FAdj(F,{a}) by G3,FIELD_6:37;
hence FAdj(F,{a}) = FAdj(F,{u}) by G4,EC_PF_1:4;
end;
U4: now assume ex w being Element of F st b^2 - 4 '*' c = w^2; then
consider w being Element of F such that G7: b^2 - 4 '*' c = w^2;
1.F = 1.K by H1,C0SP1:def 3; then
F2: 2 '*' 1.F = 2 '*' 1.K by Z3;
2 '*' 1.K is non zero by L0,ch2; then
F3: (2 '*' 1.F)" = (2 '*' 1.K)" by H1,F2,FIELD_6:18;
F4: -b1 = -b by H1,FIELD_6:17;
per cases by G7,U1,U2,lemquadr;
suppose S: u = w; then
-b1 + u = -b + w by H1,F4,FIELD_6:15; then
F5: (-b1 + u) * (2 '*' 1.K)" = (-b + w) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
-u = -w by H1,S,FIELD_6:17; then
(-b1 - u) = (-b - w) by H1,F4,FIELD_6:15; then
F6: (-b1 - u) * (2 '*' 1.K)" = (-b - w) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
per cases by L2,F,L1,TARSKI:def 2;
suppose a = (-b1 + u) * (2 '*' 1.K)";
hence contradiction by F5,A;
end;
suppose a = (-b1 - u) * (2 '*' 1.K)";
hence contradiction by F6,A;
end;
end;
suppose S: u = -w;then
-b1 + u = -b + (-w) by H1,F4,FIELD_6:15; then
F5: (-b1 + u) * (2 '*' 1.K)" = (-b + (-w)) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
-u = --w by H1,S,FIELD_6:17; then
(-b1 - u) = (-b + w) by H1,F4,FIELD_6:15; then
F6: (-b1 - u) * (2 '*' 1.K)" = (-b + w) * (2 '*' 1.F)"
by H1,F3,FIELD_6:16;
per cases by L2,F,L1,TARSKI:def 2;
suppose a = (-b1 + u) * (2 '*' 1.K)";
hence contradiction by F5,A;
end;
suppose a = (-b1 - u) * (2 '*' 1.K)";
hence contradiction by F6,A;
end;
end;
end; then
reconsider v = b^2 - 4'*'c as non square Element of F by O_RING_1:def 2;
F5: FAdj(F,{sqrt v}) is SplittingField of (X^2-v) by Fi3a;
F6: FAdj(F,{a}) is SplittingField of (X^2-v) by U1,U2,U3,U4,m102;
FAdj(F,{a}),FAdj(F,{sqrt v}) are_isomorphic_over F by F5,F6,FIELD_8:58;
hence ex a being non square Element of F
st E,FAdj(F,{sqrt a}) are_isomorphic_over F by D,FIELD_8:44;
end;
now given a being non square Element of F such that
A: E,FAdj(F,{sqrt a}) are_isomorphic_over F;
FAdj(F,{sqrt a}),E are_isomorphic_over F by A,FIELD_8:43;
hence deg(E,F) = deg(FAdj(F,{sqrt a}),F) by FIELD_8:45 .= 2 by dega;
end;
hence thesis by A;
end;