let F be Field; for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being FieldExtension of F st p splits_in E holds
p is_square-free_over E )
let p be non constant Element of the carrier of (Polynom-Ring F); ( p is separable iff for E being FieldExtension of F st p splits_in E holds
p is_square-free_over E )
A:
now ( p is separable implies for E being FieldExtension of F st p splits_in E holds
p is_square-free_over E )assume AS:
p is
separable
;
for E being FieldExtension of F st p splits_in E holds
p is_square-free_over Enow ( ex E being FieldExtension of F st
( p splits_in E & not p is_square-free_over E ) implies p is inseparable )assume
ex
E being
FieldExtension of
F st
(
p splits_in E & not
p is_square-free_over E )
;
p is inseparable then consider E being
FieldExtension of
F such that A:
(
p splits_in E & not
p is_square-free_over E )
;
consider q1 being non
constant Polynomial of
E,
q2 being
Polynomial of
E such that B:
(
q2 = p &
q1 `^ 2
divides q2 )
by A, FIELD_14:def 2;
H2:
q2 is
Element of the
carrier of
(Polynom-Ring E)
by POLYNOM3:def 10;
then
(
deg p > 0 &
deg p = deg q2 )
by B, FIELD_4:20, RING_4:def 4;
then reconsider q2 =
q2 as non
constant Polynomial of
E by RATFUNC1:def 2;
H3:
q1 `^ 2
= q1 *' q1
by POLYNOM5:17;
then consider r being
Polynomial of
E such that H0:
(q1 *' q1) *' r = q2
by B, RING_4:1;
reconsider r =
r as non
zero Polynomial of
E by H0;
H5:
q2 = q1 *' (q1 *' r)
by H0, POLYNOM3:33;
q1 is
with_roots
proof
q1 <> 0_. E
;
then C0:
len q1 <> 0
by POLYNOM4:5;
q1 is
Element of the
carrier of
(Polynom-Ring E)
by POLYNOM3:def 10;
then
(
deg (NormPolynomial q1) = deg q1 &
deg q1 > 0 )
by REALALG3:11, RATFUNC1:def 2;
then C4:
not
NormPolynomial q1 is
constant
by RATFUNC1:def 2;
consider x being non
zero Element of
E,
v being
Ppoly of
E such that C1:
p = x * v
by A, FIELD_4:def 5;
C5:
(
v is
Element of the
carrier of
(Polynom-Ring E) &
x * v is
Element of the
carrier of
(Polynom-Ring E) &
q1 is
Element of the
carrier of
(Polynom-Ring E) &
p is
Element of the
carrier of
(Polynom-Ring E) )
by C1, POLYNOM3:def 10;
now for a being Element of E st a is_a_root_of v holds
multiplicity (v,a) = 1let a be
Element of
E;
( a is_a_root_of v implies multiplicity (v,a) = 1 )assume
a is_a_root_of v
;
multiplicity (v,a) = 1then D:
0. E =
x * (eval (v,a))
.=
eval (
(x * v),
a)
by POLYNOM5:30
.=
Ext_eval (
p,
a)
by C1, C5, FIELD_4:26
;
multiplicity (
v,
a) =
multiplicity (
(x * v),
a)
by lems
.=
multiplicity (
p,
a)
by C1, FIELD_14:def 6
;
hence
multiplicity (
v,
a)
= 1
by D, AS, A, ThSep0, FIELD_4:def 2;
verum end;
then C2:
v is
Ppoly of
E,
(Roots v)
by FIELD_14:30;
consider u being
Polynomial of
E such that C7:
x * v = q1 *' u
by C1, B, H5;
C8:
x <> 0. E
;
q1 *' ((x ") * u) =
(x ") * (x * v)
by C7, RING_4:10
.=
((x ") * x) * v
by RING_4:11
.=
(1. E) * v
by C8, VECTSP_1:def 10
.=
v
;
then
NormPolynomial q1 divides v
by C5, RING_4:25, RING_4:1;
then consider S being non
empty finite Subset of
E such that C3:
(
NormPolynomial q1 is
Ppoly of
E,
S &
S c= Roots v )
by C4, C2, FIELD_14:50;
thus
q1 is
with_roots
by C3, C0, POLYNOM5:60;
verum
end; then consider a being
Element of
E such that C:
a is_a_root_of q1
;
H1:
multiplicity (
q1,
a)
>= 1
by C, UPROOTS:52;
q1 `^ 2
= q1 *' q1
by POLYNOM5:17;
then
multiplicity (
(q1 `^ 2),
a)
= (multiplicity (q1,a)) + (multiplicity (q1,a))
by UPROOTS:55;
then H5:
multiplicity (
(q1 `^ 2),
a)
>= 1
+ 1
by H1, XREAL_1:7;
(multiplicity ((q1 `^ 2),a)) + (multiplicity (r,a)) >= multiplicity (
(q1 `^ 2),
a)
by NAT_1:11;
then
(multiplicity ((q1 `^ 2),a)) + (multiplicity (r,a)) >= 2
by H5, XXREAL_0:2;
then
multiplicity (
q2,
a)
>= 1
+ 1
by H3, H0, UPROOTS:55;
then D:
multiplicity (
q2,
a)
> 1
by NAT_1:13;
E:
multiplicity (
q2,
a)
= multiplicity (
p,
a)
by B, FIELD_14:def 6;
eval (
q2,
a) =
(eval ((q1 *' q1),a)) * (eval (r,a))
by H0, POLYNOM4:24
.=
((0. E) * (eval (q1,a))) * (eval (r,a))
by C, POLYNOM4:24
;
then
Ext_eval (
p,
a)
= 0. E
by H2, B, FIELD_4:26;
hence
p is
inseparable
by D, E, A, ThSep0, FIELD_4:def 2;
verum end; hence
for
E being
FieldExtension of
F st
p splits_in E holds
p is_square-free_over E
by AS;
verum end;
now ( p is inseparable implies ex E being FieldExtension of F st
( p splits_in E & not p is_square-free_over E ) )assume
p is
inseparable
;
ex E being FieldExtension of F st
( p splits_in E & not p is_square-free_over E )then consider E being
FieldExtension of
F such that A:
(
p splits_in E & ex
a being
Element of
E st
(
a is_a_root_of p,
E & not
multiplicity (
p,
a)
= 1 ) )
by ThSep0;
consider a being
Element of
E such that B:
(
a is_a_root_of p,
E & not
multiplicity (
p,
a)
= 1 )
by A;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider q =
p as
Element of the
carrier of
(Polynom-Ring E) ;
reconsider q =
q as
Polynomial of
E ;
(
deg p > 0 &
deg p = deg q )
by FIELD_4:20, RING_4:def 4;
then reconsider q =
q as non
constant Polynomial of
E by RATFUNC1:def 2;
eval (
q,
a) =
Ext_eval (
p,
a)
by FIELD_4:26
.=
0. E
by B, FIELD_4:def 2
;
then
a is_a_root_of q
;
then
multiplicity (
q,
a)
>= 1
by UPROOTS:52;
then
multiplicity (
q,
a)
> 1
by B, FIELD_14:def 6, XXREAL_0:1;
then
multiplicity (
q,
a)
>= 1
+ 1
by INT_1:7;
then
(X- a) `^ 2
divides q
by mulzero1;
hence
ex
E being
FieldExtension of
F st
(
p splits_in E & not
p is_square-free_over E )
by A, FIELD_14:def 2;
verum end;
hence
( p is separable iff for E being FieldExtension of F st p splits_in E holds
p is_square-free_over E )
by A; verum