English
There exists a canonical morphism from the apex of a multifork to the value of the sheaf at S, and this morphism satisfies compatibility with every leg of the multifork: for each i0, composing with F.map (E.f i0)^{op} recovers the i0-th leg.
Русский
Существует каноническое отображение от вершины мультифорка к значению линейного шарфа в S, и оно совместимо с каждым основанием мультифорка: для каждого i0 композиция с F.map (E.f i0)^{op} возвращает i0-ю ножку.
LaTeX
$$$\mathrm{multiforkLift} : c.pt \to F.\mathrm{val}.obj(\mathrm{Opposite.op}\, S) \\ \forall i_0,\; \mathrm{multiforkLift}(c) \gg F.\mathrm{val}.map (E.f i_0).op = c.ι i_0$$$
Lean4
/-- Auxiliary definition of `isLimitMultifork`. -/
noncomputable def multiforkLift : c.pt ⟶ F.val.obj (Opposite.op S) :=
F.cond.amalgamateOfArrows _ E.mem₀ c.ι
(fun W i₁ i₂ p₁ p₂ w => by
apply F.cond.hom_ext ⟨_, E.mem₁ _ _ _ _ w⟩
rintro ⟨T, g, j, h, fac₁, fac₂⟩
dsimp
simp only [assoc, ← Functor.map_comp, ← op_comp, fac₁, fac₂]
simp only [op_comp, Functor.map_comp]
simpa using c.condition ⟨⟨i₁, i₂⟩, j⟩ =≫ F.val.map h.op)
