sigmaToPi_bijective — Mathlib

English

If ι is finite and each R_i is a commutative ring, then sigmaToPi R is a bijection on prime spectra; it is injective and surjective.

Русский

Если ι конечен и каждый R_i — коммутативное кольцо, то sigmaToPi R образует биекцию спектров; она инъективна и сюръективна.

LaTeX

$$$\\text{sigmaToPi } R \\text{ is bijective}$$$

Lean4

theorem sigmaToPi_bijective {ι : Type*} (R : ι → Type*) [∀ i, CommRing (R i)] [Finite ι] :
    Function.Bijective (sigmaToPi R) := by
  refine ⟨sigmaToPi_injective R, ?_⟩
  intro q
  obtain ⟨i, q, rfl⟩ := exists_comap_evalRingHom_eq q
  exact ⟨⟨i, q⟩, rfl⟩

Похожие утверждения