English
The plusFunctor sends a presheaf P to the presheaf J.plusObj P, forming a functor on the opposite category.
Русский
Plus-функтор отправляет предобращение P в предобращение J.plusObj P, образуя функтор в противоположной категории.
LaTeX
$$$\\mathrm{plusFunctor}\\;J : (C^{op} \\to D) \\to (C^{op} \\to D)$$$
Lean4
/-- The canonical map from `P` to `J.plusObj P`.
See `toPlusNatTrans` for a functorial version. -/
def toPlus : P ⟶ J.plusObj P
where
app X := Cover.toMultiequalizer (⊤ : J.Cover X.unop) P ≫ colimit.ι (J.diagram P X.unop) (op ⊤)
naturality := by
intro X Y f
dsimp [plusObj]
delta Cover.toMultiequalizer
simp only [diagramPullback_app, colimit.ι_pre, ι_colimMap_assoc, Category.assoc]
dsimp only [Functor.op, unop_op]
let e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE (OrderTop.le_top _)
rw [← colimit.w _ e.op, ← Category.assoc, ← Category.assoc, ← Category.assoc]
congr 1
refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)
simp only [Category.assoc]
dsimp [Cover.Arrow.base]
simp
