skyscraperPresheafCoconeOfSpecializes

Lean4

/-- The cocone at `A` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∈ closure {p₀}`
-/
@[simps]
def skyscraperPresheafCoconeOfSpecializes {y : X} (h : p₀ ⤳ y) :
    Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
    where
  pt := A
  ι :=
    { app := fun U => eqToHom <| if_pos <| h.mem_open U.unop.1.2 U.unop.2
      naturality := fun U V inc => by
        change dite _ _ _ ≫ _ = _; rw [dif_pos]
        swap
        · exact h.mem_open V.unop.1.2 V.unop.2
        ·
          simp only [Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, unop_op, Functor.const_obj_obj,
            eqToHom_trans, Functor.const_obj_map, Category.comp_id] }

Похожие утверждения