Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y)
      (X.presheaf.stalkSpecializes h)

Defined in

Mathlib.Geometry.RingedSpace.Stalks

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimits