Lean4
/-- Taking stalks of a sheaf is the left adjoint functor to `skyscraperSheafFunctor`
-/
def stalkSkyscraperSheafAdjunction [HasColimits C] :
Sheaf.forget C X ⋙ Presheaf.stalkFunctor _ p₀ ⊣ skyscraperSheafFunctor p₀ where
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext1` is changed to `Sheaf.Hom.ext`,
unit :=
{ app := fun 𝓕 => ⟨(StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app 𝓕.1⟩
naturality := fun 𝓐 𝓑 f => Sheaf.Hom.ext <| by apply (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).naturality }
counit := StalkSkyscraperPresheafAdjunctionAuxs.counit p₀
left_triangle_components X := ((skyscraperPresheafStalkAdjunction p₀).left_triangle_components X.val)
right_triangle_components _ := Sheaf.Hom.ext ((skyscraperPresheafStalkAdjunction p₀).right_triangle_components _)
