English
There is an IsPullback for the square formed by the pushforward along map and diagonal i, relative to pullback diagonals and maps, expressing universal property of the diagonal with these maps.
Русский
Существует IsPullback для квадрата, образованного отображением map и диагональю i, относительно диагоналей и отображений предела, выражающий универсальное свойство диагонали.
LaTeX
$$$$ IsPullback (fst f g) (map f g (f i) (g i) ...) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g ...) $$$$
Lean4
theorem pullback_map_diagonal_isPullback :
IsPullback (pullback.fst _ _ ≫ f)
(pullback.map f g (f ≫ i) (g ≫ i) _ _ i (Category.id_comp _).symm (Category.id_comp _).symm) (diagonal i)
(pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 _) (Category.comp_id _) (Category.comp_id _)) :=
by
apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm
· simp
· ext <;> simp
· constructor
ext <;> simp [condition]
