skyscraperPresheafCoconeIsColimitOfSpecializes

Lean4

/-- The cocone at `A` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∈ closure {p₀}` is a
colimit
-/
noncomputable def skyscraperPresheafCoconeIsColimitOfSpecializes {y : X} (h : p₀ ⤳ y) :
    IsColimit (skyscraperPresheafCoconeOfSpecializes p₀ A h)
    where
  desc c := eqToHom (if_pos trivial).symm ≫ c.ι.app (op ⊤)
  fac c
    U := by
    dsimp
    rw [← c.w (homOfLE <| (le_top : unop U ≤ _)).op]
    change _ ≫ _ ≫ dite _ _ _ ≫ _ = _
    rw [dif_pos]
    · simp only [eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, op_unop]
    · exact h.mem_open U.unop.1.2 U.unop.2
  uniq c f
    h := by
    dsimp
    rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]

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