mkConeMorphism

Mathlib.CategoryTheory.Limits.IsLimit

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsLimit.mkConeMorphism

Lean4

/-- Alternative constructor for `isLimit`,
providing a morphism of cones rather than a morphism between the cone points
and separately the factorisation condition.
-/
@[simps]
def mkConeMorphism {t : Cone F} (lift : ∀ s : Cone F, s ⟶ t) (uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s) : IsLimit t
    where
  lift s := (lift s).hom
  uniq s m
    w :=
    have : ConeMorphism.mk m w = lift s := by apply uniq
    congrArg ConeMorphism.hom this

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

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

Разделы

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

Аффилиация

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