C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
⊢ stalkSpecializes F h ≫ (stalkFunctor C x).map f = (stalkFunctor C y).map f ≫ stalkSpecializes G h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
⊢ stalkSpecializes F h ≫ (stalkFunctor C x).map f = (stalkFunctor C y).map f ≫ stalkSpecializes G h
change (_ : colimit _ ⟶  _) = (_ : colimit _ ⟶  _)
case w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds y)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      stalkSpecializes F h ≫ (stalkFunctor C x).map f =
    colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      (stalkFunctor C y).map f ≫ stalkSpecializes G h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
⊢ stalkSpecializes F h ≫ (stalkFunctor C x).map f = (stalkFunctor C y).map f ≫ stalkSpecializes G h
ext
case w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds y)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      stalkSpecializes F h ≫
        ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x)) ⋙ colim).map f =
    colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      ((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y)) ⋙ colim).map f ≫
        stalkSpecializes G h
case w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds y)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      stalkSpecializes F h ≫ (stalkFunctor C x).map f =
    colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      (stalkFunctor C y).map f ≫ stalkSpecializes G h
delta stalkFunctor
no goals
case w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds y)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      stalkSpecializes F h ≫
        ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x)) ⋙ colim).map f =
    colimit.ι (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y))).obj F) j✝ ≫
      ((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion y)) ⋙ colim).map f ≫
        stalkSpecializes G h
simpa [stalkSpecializes] using by rfl
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds y)ᵒᵖ
⊢ f.app j✝.unop.obj.op ≫
      colimit.ι (Functor.op (OpenNhds.inclusion x) ⋙ G)
        { obj := j✝.unop.obj, property := (_ : x ∈ j✝.unop.obj.carrier) }.op =
    f.app ((OpenNhds.inclusion y).obj j✝.unop).op ≫
      colimit.ι (Functor.op (OpenNhds.inclusion x) ⋙ G)
        { obj := j✝.unop.obj, property := (_ : x ∈ j✝.unop.obj.carrier) }.op
rfl