English
For any presheaf P and any sheaf Q, the interaction between plus-map and the toPlus map is compatible: applying plus to the map P ⟶ Q and then lifting along Q is the same as lifting η∘γ with γ being the map Q ⟶ R, provided R is a sheaf. Concretely, J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P).
Русский
Для любого пресшефа P и для любого шейфа Q совместимость между плюс-отображением и отображением toPlus: (P ⟶ Q) затем преобразование через плюс эквивалентно преобразованию через плюс применённому к P. Конкретно: J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P).
LaTeX
$$$ J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P) $$$
Lean4
/-- `(P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺` -/
@[simp]
theorem plusMap_toPlus : J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P) :=
by
ext X : 2
refine colimit.hom_ext (fun S => ?_)
dsimp only [plusMap, toPlus]
let e : S.unop ⟶ ⊤ := homOfLE (OrderTop.le_top _)
rw [ι_colimMap, ← colimit.w _ e.op, ← Category.assoc, ← Category.assoc]
congr 1
refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)
erw [Multiequalizer.lift_ι]
simp only [unop_op, op_unop, diagram_map, Category.assoc, limit.lift_π, Multifork.ofι_π_app]
let ee : (J.pullback (I.map e).f).obj S.unop ⟶ ⊤ := homOfLE (OrderTop.le_top _)
erw [← colimit.w _ ee.op, ι_colimMap_assoc, colimit.ι_pre, diagramPullback_app, ← Category.assoc, ← Category.assoc]
congr 1
refine Multiequalizer.hom_ext _ _ _ (fun II => ?_)
convert
Multiequalizer.condition (S.unop.index P)
{ fst := I, snd := II.base, r.Z := II.Y, r.g₁ := II.f, r.g₂ := 𝟙 II.Y } using
1
all_goals simp
