Lean4
/-- Taking skyscraper presheaf at a point is functorial: `c ↦ skyscraper p₀ c` defines a functor by
sending every `f : a ⟶ b` to the natural transformation `α` defined as: `α(U) = f : a ⟶ b` if
`p₀ ∈ U` and the unique morphism to a terminal object in `C` if `p₀ ∉ U`.
-/
@[simps]
def map' {a b : C} (f : a ⟶ b) : skyscraperPresheaf p₀ a ⟶ skyscraperPresheaf p₀ b
where
app
U :=
if h : p₀ ∈ U.unop then eqToHom (if_pos h) ≫ f ≫ eqToHom (if_pos h).symm
else ((if_neg h).symm.ndrec terminalIsTerminal).from _
naturality U V
i := by
simp only [skyscraperPresheaf_map]
by_cases hV : p₀ ∈ V.unop
· have hU : p₀ ∈ U.unop := leOfHom i.unop hV
simp only [skyscraperPresheaf_obj, hU, hV, ↓reduceDIte, eqToHom_trans_assoc, Category.assoc, eqToHom_trans]
· apply ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext
