zero

Mathlib.CategoryTheory.Shift.Induced

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

Lean4

/-- The `zero` field of the `ShiftMkCore` structure for the induced shift. -/
noncomputable def zero : s 0 ≅ 𝟭 D :=
  ((whiskeringLeft C D D).obj F).preimageIso
    ((i 0) ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm)

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

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

Разделы

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

Аффилиация

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