homEquiv_apply — Mathlib

English

For a colimit t of F, and any morphism f : t.pt → W, the image under the bijection h.homEquiv equals the ι-component of the extended cocone: h.homEquiv f = (t.extend f).ι.

Русский

Для колимитного кокона t функторa F и произвольного отображения f: t.pt → W образ через биекцию h.homEquiv равен ι-компоненте расширенного кокона: h.homEquiv f = (t.extend f).ι.

LaTeX

$$$h.homEquiv\,f = (t.\mathrm{extend} f).\mathrm{ι}$$$

Lean4

@[simp]
theorem homEquiv_apply (h : IsColimit t) {W : C} (f : t.pt ⟶ W) : h.homEquiv f = (t.extend f).ι :=
  rfl

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