diagonalObjPullbackFstIso_inv_snd_fst

English

The inverse diagonal interaction with snd and fst yields a canonical relation connecting the pullback projections.

Русский

Взаимодействие обратной диагонали с snd и fst даёт каноническое соотношение между проекциями предела.

LaTeX

$$$$ (diagonalObjPullbackFstIso\ f g).inv \circ snd \circ fst = fst \circ fst $$$$

Lean4

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

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