mk

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

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

Lean4

/-- This is a slightly more convenient method to verify that a cofork is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content -/
def mk (t : Cofork f g) (desc : ∀ s : Cofork f g, t.pt ⟶ s.pt)
    (fac : ∀ s : Cofork f g, Cofork.π t ≫ desc s = Cofork.π s)
    (uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt) (_ : t.π ≫ m = s.π), m = desc s) : IsColimit t :=
  { desc
    fac := fun s j => WalkingParallelPair.casesOn j (by simp_all) (fac s)
    uniq := by aesop }

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

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

Разделы

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

Аффилиация

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