colimitIsColimit

Mathlib.Algebra.Category.MonCat.Colimits

URI: https://scilib.ai/kg/mathlib#MonCat.Colimits.colimitIsColimit

Lean4

/-- Evidence that the proposed colimit is the colimit. -/
def colimitIsColimit : IsColimit (colimitCocone F)
    where
  desc s := descMorphism F s
  uniq s m
    w := by
    ext x
    induction x using Quot.inductionOn with
    | h x => ?_
    induction x with
    | of j =>
      change _ = s.ι.app j _
      rw [← w j]
      rfl
    | one =>
      rw [quot_one, map_one]
      rfl
    | mul x y hx hy =>
      rw [quot_mul, map_mul, hx, hy]
      solve_by_elim

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

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

Разделы

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

Аффилиация

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