homIso_natural — Mathlib

English

The bijection homIso for Cofork.IsLimit is natural in Z, i.e., for any q: Z' → Z and k: Z → t.pt, the isomorphism respects composition with q.

Русский

Единица биекции homIso для Cofork.IsLimit естественна по Z, то есть для любого q: Z' → Z и k: Z → t.pt изоморфизм сохраняет композицию с q.

LaTeX

$$$(\mathrm{Cofork.IsLimit.homIso}\ ht\ _ (q \circ k)) = q \circ (\mathrm{Cofork.IsLimit.homIso}\ ht\ _ k).$$$

Lean4

/-- The bijection of `Fork.IsLimit.homIso` is natural in `Z`. -/
theorem homIso_natural {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt) :
    (Fork.IsLimit.homIso ht _ (q ≫ k) : Z' ⟶ X) = q ≫ (Fork.IsLimit.homIso ht _ k : Z ⟶ X) :=
  Category.assoc _ _ _

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