homIso_natural — Mathlib

English

The naturality of the homIso bijection for Cofork.IsColimit with respect to changes in Z holds; i.e., precomposition with q preserves the bijection structure.

Русский

Естественность биекции homIso для Cofork.IsColimit по отношению к изменениям Z сохраняется; то есть предварительная композиция с q сохраняет структуру биекции.

LaTeX

$$$\mathrm{homIso}_{Z'}(k \circ q) = k \circ \mathrm{homIso}_Z(q).$$$

Lean4

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

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