Theorems · Theorem · algebraic geometry

AlgebraicGeometry.coprodSpec_inr_assoc

∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (R × S)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coprodSpec R S) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S))) h

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRing