homIso_hom — Mathlib

English

The homomorphism part of the colimit homIso matches the cocone map via the constant functor.

Русский

Часть гомоморфизма из colimit.homIso совпадает с отображением кокона через константный функтор.

LaTeX

$$$\\bigl(\\text{colimit.homIso } F W\\bigr) \\;\\mathrm{hom} \; f = (\\text{colimit.cocone } F) .\\iota \\; (\\text{const } J).map f$$$

Lean4

@[simp]
theorem homIso_hom (F : J ⥤ C) [HasColimit F] {W : C} (f : ULift (colimit F ⟶ W)) :
    (colimit.homIso F W).hom f = (colimit.cocone F).ι ≫ (const J).map f.down :=
  (colimit.isColimit F).homIso_hom f

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