feat(RingTheory): PrimeSpectrum.sigmaToPi is an open embedding

Mathlib/RingTheory/Spectrum/Prime/RingHom.lean

@@ -117,13 +117,20 @@ section Pi
 
 variable {ι} (R : ι → Type*) [∀ i, CommSemiring (R i)]
 
-/-- The canonical map from a disjoint union of prime spectra of commutative semirings to
-the prime spectrum of the product semiring. -/
-/- TODO: show this is always a topological embedding (even when ι is infinite)
-and is a homeomorphism when ι is finite. -/
-@[simps! asIdeal] def sigmaToPi : (Σ i, PrimeSpectrum (R i)) → PrimeSpectrum (Π i, R i)
+/--
+The canonical map from a disjoint union of prime spectra of commutative semirings to
+the prime spectrum of the product semiring.
+This is always an open embedding, see `PrimeSpectrum.isOpenEmbedding_sigmaToPi` and
+a homeomorphism if `ι` is finite, see `PrimeSpectrum.sigmaHomeoPi`.
+-/
+def sigmaToPi : (Σ i, PrimeSpectrum (R i)) → PrimeSpectrum (Π i, R i)
   | ⟨i, p⟩ => comap (Pi.evalRingHom R i) p
 
+@[simp]
+lemma sigmaToPi_apply (i : ι) (p : PrimeSpectrum (R i)) :
+    sigmaToPi R ⟨i, p⟩ = comap (Pi.evalRingHom R i) p :=
+  rfl
+
 theorem sigmaToPi_injective : (sigmaToPi R).Injective := fun ⟨i, p⟩ ⟨j, q⟩ eq ↦ by
   classical
   obtain rfl | ne := eq_or_ne i j

Mathlib/RingTheory/Spectrum/Prime/Topology.lean

@@ -675,6 +675,64 @@ instance : QuasiSeparatedSpace (PrimeSpectrum R) :=
 
 end BasicOpen
 
+section Pi
+
+variable {ι : Type*} {R : ι → Type*} [∀ i, CommRing (R i)]
+
+lemma comap_evalRingHom_basicOpen [DecidableEq ι] (i : ι) (f : R i) :
+    comap (Pi.evalRingHom R i) '' basicOpen f = basicOpen (Pi.single i f) := by
+  ext p
+  refine ⟨?_, ?_⟩
+  · rintro ⟨p, hp, rfl⟩
+    simpa
+  · intro hp
+    have : p ∈ Set.range (PrimeSpectrum.comap (Pi.evalRingHom R i)) := by
+      rw [range_comap_of_surjective _ _ (RingHom.surjective _), mem_zeroLocus,
+        SetLike.coe_subset_coe]
+      intro x hx
+      rw [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
+      have : Pi.single i f * x = 0 := by
+        ext j
+        by_cases h : i = j
+        · subst h
+          simp [hx]
+        · simp [h]
+      obtain (h | h) := Ideal.IsPrime.mem_or_mem_of_mul_eq_zero p.isPrime this <;> tauto
+    obtain ⟨q, rfl⟩ := this
+    exact ⟨q, by simpa using hp, by ext; simp⟩
+
+lemma sigmaToPi_mk_basicOpen [DecidableEq ι] (i : ι) (f : R i) :
+    sigmaToPi R '' (Sigma.mk i '' basicOpen f) = basicOpen (Pi.single i f) := by
+  simp only [Set.image_image, sigmaToPi_apply]
+  exact PrimeSpectrum.comap_evalRingHom_basicOpen _ _
+
+variable (R) in
+lemma isOpenEmbedding_sigmaToPi : Topology.IsOpenEmbedding (sigmaToPi R) := by
+  classical
+  refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
+  · rw [continuous_sigma_iff]
+    intro i
+    exact continuous_comap (Pi.evalRingHom R i)
+  · exact sigmaToPi_injective R
+  · rw [isOpenMap_sigma]
+    intro i
+    simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]
+    rintro - ⟨f, rfl⟩
+    rw [PrimeSpectrum.comap_evalRingHom_basicOpen]
+    exact isOpen_basicOpen
+
+/-- If `ι` is finite, the disjoint union of the prime spectra of the `R i` is homeomorphic
+to the prime spectrum of the product. -/
+noncomputable def sigmaHomeoPi {ι : Type*} (R : ι → Type*) [∀ i, CommRing (R i)] [Finite ι] :
+    (Σ i, PrimeSpectrum (R i)) ≃ₜ PrimeSpectrum (Π i, R i) :=
+  (isOpenEmbedding_sigmaToPi R).toHomeomorphOfSurjective (sigmaToPi_bijective R).surjective
+
+lemma sigmaHomeoPi_apply [Finite ι] (p : Σ i, PrimeSpectrum (R i)) :
+    sigmaHomeoPi R p = sigmaToPi R p :=
+  rfl
+
+end Pi
+
 section DiscreteTopology
 
 variable (R) [DiscreteTopology (PrimeSpectrum R)]