English
There is an instance that pullback.map f1 f2 g1 g2 i1 i2 i3 is an isomorphism whenever i1,i2,i3 are isomorphisms and the pullback squares commute.
Русский
Существует экземпляр, что отображение pullback.map является изоморфизмом при условии, что i1,i2,i3 — изоморфизмы, и квадраты пулабэка коммутируют.
LaTeX
$$$\mathrm{IsIso}\big(\mathrm{pullback.map} f_1 f_2 g_1 g_2 i_1 i_2 i_3 eq_1 eq_2\big)$$$
Lean4
@[reassoc]
theorem map_comp {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
{f'' : X'' ⟶ Y''} {g'' : X'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y') (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z')
(j₃ : Z' ⟶ Z'') [HasPushout f g] [HasPushout f' g'] [HasPushout f'' g''] (e₁ e₂ e₃ e₄) :
pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
pushout.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
