down

Mathlib.CategoryTheory.Limits.Types.ColimitType

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.CoconeTypes.IsColimitCore.down

Lean4

/-- Any structure `IsColimitCore.{max w₂ w₃} c` can be
lowered to `IsColimitCore.{w₂} c` -/
def down (hc : IsColimitCore.{max w₂ w₃} c) : IsColimitCore.{w₂} c
    where
  desc c' := Equiv.ulift.toFun.comp (hc.desc (c'.postcomp Equiv.ulift.{w₃}.symm))
  fac c'
    j := by
    rw [Function.comp_assoc, hc.fac]
    rfl
  funext {T f g}
    h :=
    by
    suffices Equiv.ulift.{w₃}.invFun.comp f = Equiv.ulift.invFun.comp g
      by
      ext x
      simpa using congr_fun this x
    exact hc.funext (fun j ↦ by simp [Function.comp_assoc, h])

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

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

Разделы

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

Аффилиация

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