coconeOfHom_fac — Mathlib

English

If F.cocones is corepresented by X, the cocone corresponding to f : X ⟶ Y is the colimit cocone extended by f; i.e. coconeOfHom h f = (colimitCocone h).extend f.

Русский

Если коконы F корпредставлены X, кокон, соответствующий f : X ⟶ Y, равен колимитному кокону, расширенному по f; то есть coconeOfHom h f = (colimitCocone h).extend f.

LaTeX

$$$\mathrm{coconeOfHom}\ h\; f = (\mathrm{colimitCocone}\ h).\mathrm{extend} f$$$

Lean4

/-- If `F.cocones` is corepresented by `X`, the cocone corresponding to a morphism `f : Y ⟶ X` is
the colimit cocone extended by `f`. -/
theorem coconeOfHom_fac {Y : C} (f : X ⟶ Y) : coconeOfHom h f = (colimitCocone h).extend f :=
  by
  dsimp [coconeOfHom, colimitCocone, Cocone.extend]
  congr
  conv_lhs => rw [← Category.id_comp f]
  exact h.homEquiv_comp f (𝟙 X)

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