diagonalObjPullbackFstIso_inv_snd_snd

English

A specialized IsPullback statement for a diagonal-lifted diagram asserts a universal property for the diagonal map in the presence of a diagonal map and a mapped diagonal.

Русский

Утверждается универсальное свойство диагонали в присутствии диагонального отображения и отображения диагонали.

LaTeX

$$$$ IsPullback (pullback.fst f g) (pullback.map (g ≫ f) f f f g (id_X) (id_S) (by simp) (by simp)) (diagonal f) (pullback.map (g ≫ f) (id_X ≫ f) f f g (id_X) (id_S) (by simp) (by simp)) $$$$

Lean4

@[reassoc (attr := simp)]
theorem diagonalObjPullbackFstIso_inv_snd_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (diagonalObjPullbackFstIso f g).inv ≫ pullback.snd _ _ ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.snd _ _ :=
  by
  delta diagonalObjPullbackFstIso
  simp

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