Theorems · Theorem · algebraic geometry

AlgebraicGeometry.stalkMap_toStalk_apply

∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : ↑R),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom p))
      ((CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.StructureSheaf.toStalk (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)))
        x) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toStalk (↑S) p)))
      x

Defined in

Mathlib.AlgebraicGeometry.Spec

Cited by

1 results in Mathlib

Foundations

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