diagonalObjPullbackFstIso_hom_fst_fst

English

There is an IsPullback for the square consisting of pullback.fst composed with f and the pullback map against diagonal, establishing compatibility of diagonal with pullback constructions.

Русский

Существует IsPullback для квадрата, состоящего из pullback.fst скомпонованного с f и отображения map против диагонали; устанавливает совместимость диагонали с конструкциями предела.

LaTeX

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

Lean4

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

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