instIsLeftAdjointPresheafStalkFunctor

English

There is a classical instance showing that Presheaf.stalkFunctor C p0 is a left adjoint to the skyscraperPresheafFunctor.

Русский

Существует классический инстанс, что Presheaf.stalkFunctor p0 является левым адъюнктом к skyscraperPresheafFunctor.

LaTeX

$$$(Presheaf.stalkFunctor\, C\, p_0).IsLeftAdjoint$$$

Lean4

instance [HasColimits C] : (Presheaf.stalkFunctor C p₀).IsLeftAdjoint :=
  -- Use a classical instance instead of the one from `variable`s

  have : ∀ U : Opens X, Decidable (p₀ ∈ U) := fun _ ↦ Classical.dec _
  (skyscraperPresheafStalkAdjunction _).isLeftAdjoint

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