cocone_fac — Mathlib

English

If F.cocones is corepresented by X, any cocone s for F is obtained by extending the colimit cocone by the canonical morphism homOfCocone h s.

Русский

Если коконы F корпредставлены X, любой кокон s для F получается расширением колимитного кокона по каноническому морфизму homOfCocone h s.

LaTeX

$$$(\text{colimitCocone } h).\mathrm{extend}(\mathrm{homOfCocone}\ h\; s) = s$$$

Lean4

/-- If `F.cocones` is corepresented by `X`, any cocone is the extension of the colimit cocone by the
corresponding morphism. -/
theorem cocone_fac (s : Cocone F) : (colimitCocone h).extend (homOfCocone h s) = s :=
  by
  rw [← coconeOfHom_homOfCocone h s]
  conv_lhs => simp only [homOfCocone_coconeOfHom]
  apply (coconeOfHom_fac _ _).symm

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