English
There is a canonical morphism from P.obj(op X) to the multiequalizer of the index given by S, under HasMultiequalizer (S.index P). This is used to express the sheaf condition via multiequalizers.
Русский
Существет каноническое отображение из P.obj(op X) к мультиэквилизу, соответствующему индексу S, при условии HasMultiequalizer (S.index P). Это для выражения условияSheaf через мультиэквалайзеры.
LaTeX
$$$P.obj(\mathrm{Opposite.op}\,X) \to \mathrm{multiequalizer}(S.index\,P)$$$
Lean4
/-- The canonical map from `P.obj (op X)` to the multiequalizer associated to a covering sieve,
assuming such a multiequalizer exists. This will be used in `Sheaf.lean` to provide an equivalent
sheaf condition in terms of multiequalizers. -/
noncomputable abbrev toMultiequalizer {D : Type u₁} [Category.{v₁} D] (S : J.Cover X) (P : Cᵒᵖ ⥤ D)
[Limits.HasMultiequalizer (S.index P)] : P.obj (Opposite.op X) ⟶ Limits.multiequalizer (S.index P) :=
Limits.Multiequalizer.lift _ _ (fun I => P.map I.f.op)
(by
intro I
dsimp only [shape, index, Relation.fst, Relation.snd]
simp only [← P.map_comp, ← op_comp, I.r.w])
