mkCoconeMorphism

Mathlib.CategoryTheory.Limits.IsLimit

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsColimit.mkCoconeMorphism

Lean4

/-- Alternative constructor for `IsColimit`,
providing a morphism of cocones rather than a morphism between the cocone points
and separately the factorisation condition.
-/
@[simps]
def mkCoconeMorphism {t : Cocone F} (desc : ∀ s : Cocone F, t ⟶ s) (uniq' : ∀ (s : Cocone F) (m : t ⟶ s), m = desc s) :
    IsColimit t where
  desc s := (desc s).hom
  uniq s m
    w :=
    have : CoconeMorphism.mk m w = desc s := by apply uniq'
    congrArg CoconeMorphism.hom this

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru