Metamath Proof Explorer

Theorem rhmpreimacn

Description: The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of EGA, p. 83. Notice that the direction of the continuous map G is reverse: the original ring homomorphism F goes from R to S , but the continuous map G goes from B to A . This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024)

Ref Expression
Hypotheses rhmpreimacn.t 
|- T = ( Spec ` R )
rhmpreimacn.u 
|- U = ( Spec ` S )
rhmpreimacn.a 
|- A = ( PrmIdeal ` R )
rhmpreimacn.b 
|- B = ( PrmIdeal ` S )
rhmpreimacn.j 
|- J = ( TopOpen ` T )
rhmpreimacn.k 
|- K = ( TopOpen ` U )
rhmpreimacn.g 
|- G = ( i e. B |-> ( `' F " i ) )
rhmpreimacn.r 
|- ( ph -> R e. CRing )
rhmpreimacn.s 
|- ( ph -> S e. CRing )
rhmpreimacn.f 
|- ( ph -> F e. ( R RingHom S ) )
rhmpreimacn.1 
|- ( ph -> ran F = ( Base ` S ) )
Assertion rhmpreimacn 
|- ( ph -> G e. ( K Cn J ) )

Proof

Step Hyp Ref Expression
1 rhmpreimacn.t 
 |-  T = ( Spec ` R )
2 rhmpreimacn.u 
 |-  U = ( Spec ` S )
3 rhmpreimacn.a 
 |-  A = ( PrmIdeal ` R )
4 rhmpreimacn.b 
 |-  B = ( PrmIdeal ` S )
5 rhmpreimacn.j 
 |-  J = ( TopOpen ` T )
6 rhmpreimacn.k 
 |-  K = ( TopOpen ` U )
7 rhmpreimacn.g 
 |-  G = ( i e. B |-> ( `' F " i ) )
8 rhmpreimacn.r 
 |-  ( ph -> R e. CRing )
9 rhmpreimacn.s 
 |-  ( ph -> S e. CRing )
10 rhmpreimacn.f 
 |-  ( ph -> F e. ( R RingHom S ) )
11 rhmpreimacn.1 
 |-  ( ph -> ran F = ( Base ` S ) )
12 2 6 4 zartopon 
 |-  ( S e. CRing -> K e. ( TopOn ` B ) )
13 9 12 syl 
 |-  ( ph -> K e. ( TopOn ` B ) )
14 1 5 3 zartopon 
 |-  ( R e. CRing -> J e. ( TopOn ` A ) )
15 8 14 syl 
 |-  ( ph -> J e. ( TopOn ` A ) )
16 9 adantr 
 |-  ( ( ph /\ i e. B ) -> S e. CRing )
17 10 adantr 
 |-  ( ( ph /\ i e. B ) -> F e. ( R RingHom S ) )
18 simpr 
 |-  ( ( ph /\ i e. B ) -> i e. B )
19 18 4 eleqtrdi 
 |-  ( ( ph /\ i e. B ) -> i e. ( PrmIdeal ` S ) )
20 3 rhmpreimaprmidl 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ i e. ( PrmIdeal ` S ) ) -> ( `' F " i ) e. A )
21 16 17 19 20 syl21anc 
 |-  ( ( ph /\ i e. B ) -> ( `' F " i ) e. A )
22 21 7 fmptd 
 |-  ( ph -> G : B --> A )
23 4 fvexi 
 |-  B e. _V
24 23 rabex 
 |-  { k e. B | j C_ k } e. _V
25 sseq1 
 |-  ( l = j -> ( l C_ k <-> j C_ k ) )
26 25 rabbidv 
 |-  ( l = j -> { k e. B | l C_ k } = { k e. B | j C_ k } )
27 26 cbvmptv 
 |-  ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) = ( j e. ( LIdeal ` S ) |-> { k e. B | j C_ k } )
28 24 27 fnmpti 
 |-  ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) Fn ( LIdeal ` S )
29 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> F e. ( R RingHom S ) )
30 11 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> ran F = ( Base ` S ) )
31 simplr 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> a e. ( LIdeal ` R ) )
32 eqid 
 |-  ( Base ` S ) = ( Base ` S )
33 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
34 eqid 
 |-  ( LIdeal ` S ) = ( LIdeal ` S )
35 32 33 34 rhmimaidl 
 |-  ( ( F e. ( R RingHom S ) /\ ran F = ( Base ` S ) /\ a e. ( LIdeal ` R ) ) -> ( F " a ) e. ( LIdeal ` S ) )
36 29 30 31 35 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> ( F " a ) e. ( LIdeal ` S ) )
37 fveqeq2 
 |-  ( b = ( F " a ) -> ( ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` b ) = ( `' G " x ) <-> ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` ( F " a ) ) = ( `' G " x ) ) )
38 37 adantl 
 |-  ( ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) /\ b = ( F " a ) ) -> ( ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` b ) = ( `' G " x ) <-> ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` ( F " a ) ) = ( `' G " x ) ) )
39 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> R e. CRing )
40 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> S e. CRing )
41 25 rabbidv 
 |-  ( l = j -> { k e. A | l C_ k } = { k e. A | j C_ k } )
42 41 cbvmptv 
 |-  ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) = ( j e. ( LIdeal ` R ) |-> { k e. A | j C_ k } )
43 1 2 3 4 5 6 7 39 40 29 30 31 42 27 rhmpreimacnlem 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` ( F " a ) ) = ( `' G " ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) ) )
44 simpr 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x )
45 44 imaeq2d 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> ( `' G " ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) ) = ( `' G " x ) )
46 43 45 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` ( F " a ) ) = ( `' G " x ) )
47 36 38 46 rspcedvd 
 |-  ( ( ( ( ph /\ x e. ( Clsd ` J ) ) /\ a e. ( LIdeal ` R ) ) /\ ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) -> E. b e. ( LIdeal ` S ) ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` b ) = ( `' G " x ) )
48 3 fvexi 
 |-  A e. _V
49 48 rabex 
 |-  { k e. A | j C_ k } e. _V
50 49 42 fnmpti 
 |-  ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) Fn ( LIdeal ` R )
51 simpr 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> x e. ( Clsd ` J ) )
52 8 adantr 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> R e. CRing )
53 1 5 3 42 zartopn 
 |-  ( R e. CRing -> ( J e. ( TopOn ` A ) /\ ran ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) = ( Clsd ` J ) ) )
54 53 simprd 
 |-  ( R e. CRing -> ran ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) = ( Clsd ` J ) )
55 52 54 syl 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> ran ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) = ( Clsd ` J ) )
56 51 55 eleqtrrd 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> x e. ran ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) )
57 fvelrnb 
 |-  ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) Fn ( LIdeal ` R ) -> ( x e. ran ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) <-> E. a e. ( LIdeal ` R ) ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x ) )
58 57 biimpa 
 |-  ( ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) Fn ( LIdeal ` R ) /\ x e. ran ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ) -> E. a e. ( LIdeal ` R ) ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x )
59 50 56 58 sylancr 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> E. a e. ( LIdeal ` R ) ( ( l e. ( LIdeal ` R ) |-> { k e. A | l C_ k } ) ` a ) = x )
60 47 59 r19.29a 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> E. b e. ( LIdeal ` S ) ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` b ) = ( `' G " x ) )
61 fvelrnb 
 |-  ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) Fn ( LIdeal ` S ) -> ( ( `' G " x ) e. ran ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) <-> E. b e. ( LIdeal ` S ) ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` b ) = ( `' G " x ) ) )
62 61 biimpar 
 |-  ( ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) Fn ( LIdeal ` S ) /\ E. b e. ( LIdeal ` S ) ( ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) ` b ) = ( `' G " x ) ) -> ( `' G " x ) e. ran ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) )
63 28 60 62 sylancr 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> ( `' G " x ) e. ran ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) )
64 2 6 4 27 zartopn 
 |-  ( S e. CRing -> ( K e. ( TopOn ` B ) /\ ran ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) = ( Clsd ` K ) ) )
65 64 simprd 
 |-  ( S e. CRing -> ran ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) = ( Clsd ` K ) )
66 9 65 syl 
 |-  ( ph -> ran ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) = ( Clsd ` K ) )
67 66 adantr 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> ran ( l e. ( LIdeal ` S ) |-> { k e. B | l C_ k } ) = ( Clsd ` K ) )
68 63 67 eleqtrd 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> ( `' G " x ) e. ( Clsd ` K ) )
69 68 ralrimiva 
 |-  ( ph -> A. x e. ( Clsd ` J ) ( `' G " x ) e. ( Clsd ` K ) )
70 iscncl 
 |-  ( ( K e. ( TopOn ` B ) /\ J e. ( TopOn ` A ) ) -> ( G e. ( K Cn J ) <-> ( G : B --> A /\ A. x e. ( Clsd ` J ) ( `' G " x ) e. ( Clsd ` K ) ) ) )
71 70 biimpar 
 |-  ( ( ( K e. ( TopOn ` B ) /\ J e. ( TopOn ` A ) ) /\ ( G : B --> A /\ A. x e. ( Clsd ` J ) ( `' G " x ) e. ( Clsd ` K ) ) ) -> G e. ( K Cn J ) )
72 13 15 22 69 71 syl22anc 
 |-  ( ph -> G e. ( K Cn J ) )