Theorems · Definition · algebraic geometry

AlgebraicGeometry.coprodSpec

(R S : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      AlgebraicGeometry.Spec (CommRingCat.of R) ⨿ AlgebraicGeometry.Spec (CommRingCat.of S) ⟶
        AlgebraicGeometry.Spec (CommRingCat.of (R × S))

The map Spec R ⨿ Spec S ⟶ Spec (R × S). This is an isomorphism as witnessed by an IsIso instance provided below.

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingCommRing