let F be non 2 -characteristic Field; for E being FieldExtension of F holds
( deg (E,F) = 2 iff ex a being Element of F st
( ( for b being Element of F holds not a = b ^2 ) & ex b being Element of E st
( a = b ^2 & E == FAdj (F,{b}) ) ) )
let E be FieldExtension of F; ( deg (E,F) = 2 iff ex a being Element of F st
( ( for b being Element of F holds not a = b ^2 ) & ex b being Element of E st
( a = b ^2 & E == FAdj (F,{b}) ) ) )
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 Element of F st
( ( for b being Element of F holds not a = b ^2 ) & ex b being Element of E st
( a = b ^2 & E == FAdj (F,{b}) ) ) )assume AS:
E is
F -quadratic
;
ex a being Element of F st
( ( for b being Element of F holds not a = b ^2 ) & ex b being Element of E st
( a = b ^2 & E == FAdj (F,{b}) ) )then 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})
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})
hence
K == FAdj (
F,
{a})
by FIELD_7:def 2;
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;
reconsider u1 =
u as
Element of
E ;
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; thus
ex
a being
Element of
F st
( ( for
b being
Element of
F holds not
a = b ^2 ) & ex
b being
Element of
E st
(
a = b ^2 &
E == FAdj (
F,
{b}) ) )
by U1, U2, U3, U4, D;
verum end;
now ( ex a being Element of F st
( ( for b being Element of F holds not a = b ^2 ) & ex b being Element of E st
( a = b ^2 & E == FAdj (F,{b}) ) ) implies deg (E,F) = 2 )assume
ex
a being
Element of
F st
( ( for
b being
Element of
F holds not
a = b ^2 ) & ex
b being
Element of
E st
(
a = b ^2 &
E == FAdj (
F,
{b}) ) )
;
deg (E,F) = 2then consider a being
Element of
F such that B:
( ( for
b being
Element of
F holds not
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;
verum end;
hence
( deg (E,F) = 2 iff ex a being Element of F st
( ( for b being Element of F holds not a = b ^2 ) & ex b being Element of E st
( a = b ^2 & E == FAdj (F,{b}) ) ) )
by A; verum