homIso_natural — Mathlib

English

The bijection given by Trident.IsLimit.homIso is natural in the ambient object Z; precomposing its input with a morphism q is compatible with postcomposing the output by q.

Русский

Биекция, задаваемая Trident.IsLimit.homIso, естественна по отношению к объекту Z; предкомпозиция входа q согласуется с посткомпозицией выхода q.

LaTeX

$$$(Trident.IsLimit.homIso ht _ (q \gg k)) = q \gg (Trident.IsLimit.homIso ht _ k)$$$

Lean4

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

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