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	No typesetting found for \|- T = ( Spec ` R ) with typecode \|-
	rhmpreimacn.u	No typesetting found for \|- U = ( Spec ` S ) with typecode \|-
	rhmpreimacn.a	No typesetting found for \|- A = ( PrmIdeal ` R ) with typecode \|-
	rhmpreimacn.b	No typesetting found for \|- B = ( PrmIdeal ` S ) with typecode \|-
	rhmpreimacn.j	$⊢ J = TopOpen (T)$
	rhmpreimacn.k	$⊢ K = TopOpen (U)$
	rhmpreimacn.g	$⊢ G = (i \in B ⟼ F^{-1} [i])$
	rhmpreimacn.r	$⊢ φ \to R \in CRing$
	rhmpreimacn.s	$⊢ φ \to S \in CRing$
	rhmpreimacn.f	$⊢ φ \to F \in (R RingHom S)$
	rhmpreimacn.1	$⊢ φ \to ran F = {Base}_{S}$
Assertion	rhmpreimacn	$⊢ φ \to G \in (K Cn J)$

Proof

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

Metamath Proof Explorer

Theorem rhmpreimacn

Proof