Theorems · Definition · algebraic geometry

AlgebraicGeometry.sigmaSpec

{ι : Type u} →
  (R : ι → CommRingCat) →
    (∐ fun i => AlgebraicGeometry.Spec (R i)) ⟶ AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i)))

The canonical map ∐ Spec Rᵢ ⟶ Spec (Π Rᵢ). This is an isomorphism when the product is finite.

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

7 results in Mathlib

Foundations

Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound