Lean4
/-- A skyscraper presheaf is a presheaf supported at a single point: if `p₀ ∈ X` is a specified
point, then the skyscraper presheaf `𝓕` with value `A` is defined by `U ↦ A` if `p₀ ∈ U` and
`U ↦ *` if `p₀ ∉ A` where `*` is some terminal object.
-/
@[simps]
def skyscraperPresheaf : Presheaf C X
where
obj U := if p₀ ∈ unop U then A else terminal C
map {U V}
i :=
if h : p₀ ∈ unop V then eqToHom <| by rw [if_pos h, if_pos (by simpa using i.unop.le h)]
else ((if_neg h).symm.ndrec terminalIsTerminal).from _
map_id
U := (em (p₀ ∈ U.unop)).elim (fun h => dif_pos h) fun h => ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext _ _
map_comp {U V W} iVU
iWV := by
by_cases hW : p₀ ∈ unop W
· have hV : p₀ ∈ unop V := leOfHom iWV.unop hW
simp only [dif_pos hW, dif_pos hV, eqToHom_trans]
· dsimp; rw [dif_neg hW]; apply ((if_neg hW).symm.ndrec terminalIsTerminal).hom_ext
