let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; 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 )
let E be FieldExtension of F; ( E is F -quadratic iff ex a being non square Element of F st E, FAdj (F,{(sqrt a)}) are_isomorphic_over 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 ( E is F -quadratic implies ex a being non square Element of F st E, FAdj (F,{(sqrt a)}) are_isomorphic_over F )assume AS:
E is
F -quadratic
;
ex a being non square Element of F st E, FAdj (F,{(sqrt a)}) are_isomorphic_over Fthen reconsider K =
E as
F -finite FieldExtension of
F ;
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 not deg ((FAdj (F,{a})),F) < 1 + 1assume
deg (
(FAdj (F,{a})),
F)
< 1
+ 1
;
contradictionthen 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;
verum end;
hence
deg (
(FAdj (F,{a})),
F)
= 2
by C1, XXREAL_0:1;
verum
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})
reconsider f =
id K as
Function of
K,
(FAdj (F,{a})) by D4, FIELD_4:def 6;
D7:
f is
isomorphism
by D6, unique20;
then
f is
F -fixing
;
hence
K,
FAdj (
F,
{a})
are_isomorphic_over F
by D7, FIELD_8:def 5;
verum
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:
not
K is 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:
not 2
'*' (1. K) is
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)))) )
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})))) ") )
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})))))) )
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;
verum
end; U4:
now for w being Element of F holds not (b ^2) - (4 '*' c) = w ^2 assume
ex
w being
Element of
F st
(b ^2) - (4 '*' c) = w ^2
;
contradictionthen 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;
not 2
'*' (1. K) is
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
( u = w or u = - w )
by G7, U1, U2, lemquadr;
suppose S:
u = w
;
contradictionthen
(- 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;
end; suppose S:
u = - w
;
contradictionthen
(- 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;
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;
verum end;
hence
( E is F -quadratic iff ex a being non square Element of F st E, FAdj (F,{(sqrt a)}) are_isomorphic_over F )
by A; verum