homIso_natural — Mathlib

English

The isomorphism homIso for a Cotrident IsColimit is natural in the target Z; i.e., changing the codomain via a map q yields a commutative relation with respect to composition with the cotrident isomorphisms.

Русский

Изоморфизм homIso для Cotrident IsColimit естественным образом зависим от модуля целевого объекта Z: переход по каналу q образует коммутативность при композициях с изоморфизмами котридента.

LaTeX

$$$(Cotrident.IsColimit.homIso ht _ (k ≫ q) : Y ⟶ Z') = (Cotrident.IsColimit.homIso ht _ k : Y ⟶ Z) ≫ q$$$

Lean4

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

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