English
Given a chain of pullbacks, the composed pullback maps equal the pullback map built from the composed legs; i.e., pullback.map is functorial in each leg.
Русский
Для последовательности пулбэпов диаграммы отображения сохраняются; отображение pullback работает по составу стрелок в каждом перемещаемом аргументе.
LaTeX
$$$\text{pullback.map } f g f' g' i_1 i_2 i_3 e_1 e_2 \,;\, \text{pullback.map } f' g' f'' g'' j_1 j_2 j_3 e_3 e_4 =
\text{pullback.map } f g f'' g'' (i_1 \;\;≫\;\; j_1) (i_2 \;\;≫\;\; j_2) (i_3 \;\;≫\;\; j_3) (by rw [reassoc_of% e_1, e_3, Category.assoc]) (by rw [reassoc_of% e_2, e_4, Category.assoc]).$$$
Lean4
@[reassoc]
theorem map_comp {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
{f'' : X'' ⟶ Z''} {g'' : Y'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y') (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z')
(j₃ : Z' ⟶ Z'') [HasPullback f g] [HasPullback f' g'] [HasPullback f'' g''] (e₁ e₂ e₃ e₄) :
pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄ =
pullback.map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) (by rw [reassoc_of% e₁, e₃, Category.assoc])
(by rw [reassoc_of% e₂, e₄, Category.assoc]) :=
by ext <;> simp
