English
A compatibility condition for a fork diagram holds: the composition through forkMap with firstMap equals the composition through forkMap with secondMap for presheaves over a presieve.
Русский
Согласование диаграммы-ветви: композиция через forkMap затем через firstMap равна композиции через forkMap затем через secondMap.
LaTeX
$$$forkMap\,R\,P \circ firstMap\,R\,P = forkMap\,R\,P \circ secondMap\,R\,P$$$
Lean4
theorem w : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P :=
by
apply limit.hom_ext
rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩
simp only [firstMap, secondMap, forkMap, limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app, Subtype.coe_mk]
rw [← P.map_comp, ← op_comp, pullback.condition]
simp
