Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc

∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) {Z : CommRingCat}
  (h :
    ((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj
            (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
        p ⟶
      Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p)
      (CategoryTheory.CategoryStruct.comp
        ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.c) h)

Defined in

Mathlib.AlgebraicGeometry.Spec

Cited by

0 results in Mathlib

Foundations

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