pullbackDiagonalMapIdIso_inv_snd_snd

English

There is an IsPullback structure for the pullback along the diagonal, relative to the diagonal map and a map between two pullbacks, expressing a robust universal property of the diagonal with respect to pullbacks.

Русский

Существует структура IsPullback для диагонального предела по диагонали вместе с отображением между двумя предельными объектами, выражающая универсальное свойство диагонали относительно пределов.

LaTeX

$$$$ IsPullback (fst\ f g) (map f g (f i) (g i) ...) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g ...) $$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackDiagonalMapIdIso_inv_snd_snd :
    (pullbackDiagonalMapIdIso f g i).inv ≫ pullback.snd _ _ ≫ pullback.snd _ _ = pullback.snd _ _ :=
  by
  rw [Iso.inv_comp_eq]
  simp

Похожие утверждения