English
In the left-hand and right-hand forks, the induced maps agree after projection onto the pullback, giving equality of two composed maps.
Русский
В левом и правом форках получаем согласование отображений после проекции на выемку, что даёт равенство композиции.
LaTeX
$$$forkMap R P \\; ;\\; firstMap R P = forkMap R P \\; ;\\; secondMap R P$$$
Lean4
theorem isSheaf_iff_multiequalizer [∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)] :
IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P) :=
by
rw [isSheaf_iff_multifork]
refine forall₂_congr fun X S => ⟨?_, ?_⟩
· rintro ⟨h⟩
let e : P.obj (op X) ≅ multiequalizer (S.index P) := h.conePointUniqueUpToIso (limit.isLimit _)
exact (inferInstance : IsIso e.hom)
· intro h
refine ⟨IsLimit.ofIsoLimit (limit.isLimit _) (Cones.ext ?_ ?_)⟩
· apply (@asIso _ _ _ _ _ h).symm
· intro a
symm
simp
