English
Let C be a category with pullbacks, and F, G, H be functors D ⥤ C. For any arrows f: F ⟶ H and g: G ⟶ H and any object d ∈ D, the canonical isomorphism between the pullback of f and g at d and the pullback in C at the components f.app d and g.app d satisfies the relation that its hom component composed with the second projection equals the second projection of the pullback in C at d.
Русский
Пусть C — категория с вытянутыми диаграммами, и F, G, H — функторы D ⥤ C. Для любых стрелок f: F ⟶ H и g: G ⟶ H и для любого объекта d ∈ D, канонический изоморфизм между pullback-объектом f и g в d и pullback в C на компонентах f.app d и g.app d удовлетворяет соотношению, что его компонента hom, композиция с вторым проецированием, равна второму проецированию pullback в C на d.
LaTeX
$$$ (pullbackObjIso\, f\, g\, d).hom \\;\\circ\\; pullback.snd\\left( f.{\\rm app}\\, d\\right)\\left( g.{\\rm app}\\, d\\right) = (pullback.snd\\, f\\, g).app\\, d $$$
Lean4
@[reassoc (attr := simp)]
theorem pullbackObjIso_hom_comp_snd (f : F ⟶ H) (g : G ⟶ H) (d : D) :
(pullbackObjIso f g d).hom ≫ pullback.snd (f.app d) (g.app d) = (pullback.snd f g).app d := by simp [pullbackObjIso]
