lift

Mathlib.CategoryTheory.Limits.Shapes.KernelPair

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsKernelPair.lift

Lean4

/-- Given a pair of morphisms `p`, `q` to `X` which factor through `f`, they factor through any kernel
pair of `f`.
-/
noncomputable def lift {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : p ≫ f = q ≫ f) : S ⟶ R :=
  PullbackCone.IsLimit.lift k.isLimit _ _ w

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

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

Разделы

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

Аффилиация

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