quotient

Mathlib.CategoryTheory.Shift.Quotient

URI: https://scilib.ai/kg/mathlib#CategoryTheory.HasShift.quotient

Lean4

/-- The shift by a monoid `A` induced on a quotient category `Quotient r` when the
relation `r` is compatible with the shift. -/
noncomputable instance quotient [r.IsCompatibleWithShift A] : HasShift (Quotient r) A :=
  HasShift.induced (Quotient.functor r) A
    (fun a =>
      Quotient.lift r (shiftFunctor C a ⋙ Quotient.functor r)
        (fun _ _ _ _ hfg => Quotient.sound r (HomRel.IsCompatibleWithShift.condition _ _ _ hfg)))
    (fun _ => Quotient.lift.isLift _ _ _)

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

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

Разделы

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

Аффилиация

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