let A be non degenerated commutative Ring; for q being proper Ideal of A holds (canHom q) .: (sqrt q) = nilrad (A / q)
let q be proper Ideal of A; (canHom q) .: (sqrt q) = nilrad (A / q)
A1:
for x being object st x in nilrad (A / q) holds
x in (canHom q) .: (sqrt q)
proof
let x be
object ;
( x in nilrad (A / q) implies x in (canHom q) .: (sqrt q) )
assume
x in nilrad (A / q)
;
x in (canHom q) .: (sqrt q)
then
x in sqrt {(0. (A / q))}
by TOPZARI1:17;
then
x in { a where a is Element of (A / q) : ex n being Element of NAT st a |^ n in {(0. (A / q))} }
by IDEAL_1:def 24;
then consider x1 being
Element of
(A / q) such that A3:
x1 = x
and A4:
ex
n being
Element of
NAT st
x1 |^ n in {(0. (A / q))}
;
consider n1 being
Element of
NAT such that A5:
x1 |^ n1 in {(0. (A / q))}
by A4;
consider y1 being
Element of
A such that A6:
x1 = Class (
(EqRel (A,q)),
y1)
by RING_1:11;
A7:
x1 = (canHom q) . y1
by A6, RING_2:def 5;
Class (
(EqRel (A,q)),
(0. A)) =
0. (A / q)
by RING_1:def 6
.=
x1 |^ n1
by A5, TARSKI:def 1
.=
Class (
(EqRel (A,q)),
(y1 |^ n1))
by A6, FIELD_1:2
;
then
(y1 |^ n1) - (0. A) in q
by RING_1:6;
then
y1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in q }
;
then A8:
y1 in sqrt q
by IDEAL_1:def 24;
dom (canHom q) = [#] A
by FUNCT_2:def 1;
hence
x in (canHom q) .: (sqrt q)
by A3, FUNCT_1:def 6, A7, A8;
verum
end;
(canHom q) .: (sqrt q) c= nilrad (A / q)
proof
let x be
object ;
TARSKI:def 3 ( not x in (canHom q) .: (sqrt q) or x in nilrad (A / q) )
assume
x in (canHom q) .: (sqrt q)
;
x in nilrad (A / q)
then consider x1 being
object such that A11:
x1 in dom (canHom q)
and A12:
x1 in sqrt q
and A13:
x = (canHom q) . x1
by FUNCT_1:def 6;
reconsider x1 =
x1 as
Element of
A by A11;
A14:
x1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in q }
by A12, IDEAL_1:def 24;
consider x0 being
Element of
A such that A15:
x0 = x1
and A16:
ex
n being
Element of
NAT st
x0 |^ n in q
by A14;
consider n1 being
Element of
NAT such that A17:
x0 |^ n1 in q
by A16;
A18:
(x0 |^ n1) - (0. A) in q
by A17;
A19:
x = Class (
(EqRel (A,q)),
x0)
by A13, A15, RING_2:def 5;
x in rng (canHom q)
by A11, A13, FUNCT_1:def 3;
then reconsider y =
x as
Element of
(A / q) ;
y |^ n1 =
Class (
(EqRel (A,q)),
(x0 |^ n1))
by A19, FIELD_1:2
.=
Class (
(EqRel (A,q)),
(0. A))
by A18, RING_1:6
.=
0. (A / q)
by RING_1:def 6
;
then
y |^ n1 in {(0. (A / q))}
by TARSKI:def 1;
then
y in { a where a is Element of (A / q) : ex n being Element of NAT st a |^ n in {(0. (A / q))} }
;
then
y in sqrt {(0. (A / q))}
by IDEAL_1:def 24;
hence
x in nilrad (A / q)
by TOPZARI1:17;
verum
end;
hence
(canHom q) .: (sqrt q) = nilrad (A / q)
by A1, TARSKI:2; verum