pullback_obj_mk — Mathlib

English

If a certain square is a pullback, then pulling back along f sends mk i to mk j.

Русский

Если квадрат является вытягиванием, то вытягивание вдоль f отправляет mk i в mk j.

LaTeX

$$$\text{IsPullback}(f', j, i, f) \Rightarrow (pullback f).obj(\mathrm{mk}(i)) = \mathrm{mk}(j)$$$

Lean4

theorem pullback_obj_mk {A B X Y : C} {f : Y ⟶ X} {i : A ⟶ X} [Mono i] {j : B ⟶ Y} [Mono j] {f' : B ⟶ A}
    (h : IsPullback f' j i f) : (pullback f).obj (mk i) = mk j :=
  ((equivMonoOver Y).inverse.mapIso (MonoOver.pullbackObjIsoOfIsPullback _ _ _ _ h)).to_eq

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