English
Let P be a presheaf on a category C and S a presieve on an object X. Then the two natural maps obtained from the fork via firstMap and secondMap become equal after applying forkMap; i.e., the fork commutes: forkMap P S ≫ firstMap P S = forkMap P S ≫ secondMap P S.
Русский
Пусть P — расслоенная по категории C предрасслоение, и S — предрассление на объекте X. Тогда два канонических отображения, полученные через firstMap и secondMap и затем применённые к forkMap, совпадают: forkMap P S ≫ firstMap P S = forkMap P S ≫ secondMap P S.
LaTeX
$$$\\operatorname{forkMap}(P,S) \\circ \\operatorname{firstMap}(P,S) = \\operatorname{forkMap}(P,S) \\circ \\operatorname{secondMap}(P,S)$$$
Lean4
theorem w : forkMap P (S : Presieve X) ≫ firstMap P S = forkMap P S ≫ secondMap P S :=
by
ext
simp [firstMap, secondMap, forkMap]
