let A, B be non degenerated commutative Ring; for h being Function of A,B
for E being Subset of A st h is RingHomomorphism holds
(Spec h) " (PrimeIdeals (A,E)) = PrimeIdeals (B,(h .: E))
let h be Function of A,B; for E being Subset of A st h is RingHomomorphism holds
(Spec h) " (PrimeIdeals (A,E)) = PrimeIdeals (B,(h .: E))
let E be Subset of A; ( h is RingHomomorphism implies (Spec h) " (PrimeIdeals (A,E)) = PrimeIdeals (B,(h .: E)) )
assume A1:
h is RingHomomorphism
; (Spec h) " (PrimeIdeals (A,E)) = PrimeIdeals (B,(h .: E))
thus
(Spec h) " (PrimeIdeals (A,E)) c= PrimeIdeals (B,(h .: E))
XBOOLE_0:def 10 PrimeIdeals (B,(h .: E)) c= (Spec h) " (PrimeIdeals (A,E))proof
let x be
object ;
TARSKI:def 3 ( not x in (Spec h) " (PrimeIdeals (A,E)) or x in PrimeIdeals (B,(h .: E)) )
assume A3:
x in (Spec h) " (PrimeIdeals (A,E))
;
x in PrimeIdeals (B,(h .: E))
then A4:
(
x in dom (Spec h) &
(Spec h) . x in PrimeIdeals (
A,
E) )
by FUNCT_1:def 7;
reconsider x1 =
x as
Point of
(ZariskiTS B) by A3;
h " x1 in { p where p is prime Ideal of A : E c= p }
by A1, Def9, A4;
then consider q being
prime Ideal of
A such that A6:
q = h " x1
and A7:
E c= q
;
A8:
h .: E c= h .: (h " x1)
by A6, A7, RELAT_1:123;
h .: (h " x1) c= x1
by FUNCT_1:75;
then A9:
h .: E c= x1
by A8;
x1 in the
carrier of
(ZariskiTS B)
;
then
x1 in Spectrum B
by Def7;
then
x1 is
prime Ideal of
B
by Th22;
hence
x in PrimeIdeals (
B,
(h .: E))
by A9;
verum
end;
let x be object ; TARSKI:def 3 ( not x in PrimeIdeals (B,(h .: E)) or x in (Spec h) " (PrimeIdeals (A,E)) )
assume
x in PrimeIdeals (B,(h .: E))
; x in (Spec h) " (PrimeIdeals (A,E))
then consider q being prime Ideal of B such that
A12:
x = q
and
A13:
h .: E c= q
;
A14:
h " (h .: E) c= h " q
by A13, RELAT_1:143;
E c= h " (h .: E)
by FUNCT_2:42;
then A15:
E c= h " q
by A14;
h " q is prime Ideal of A
by A1, Th51;
then A17:
h " q in PrimeIdeals (A,E)
by A15;
A18:
dom (Spec h) = the carrier of (ZariskiTS B)
by FUNCT_2:def 1;
q in Spectrum B
;
then reconsider q1 = q as Point of (ZariskiTS B) by Def7;
(Spec h) . q1 in PrimeIdeals (A,E)
by A17, A1, Def9;
hence
x in (Spec h) " (PrimeIdeals (A,E))
by A12, A18, FUNCT_1:def 7; verum