attachCellsιFunctorObjOfSmall

Mathlib.CategoryTheory.SmallObject.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.attachCellsιFunctorObjOfSmall

Lean4

/-- The morphism `ιFunctorObj f πX : X ⟶ functorObj f πX` is obtained by
attaching `f`-cells, and the index type can be chosen to be in `Type t`
if the category is `t`-locally small and the index type for `f`
is `t`-small. -/
noncomputable def attachCellsιFunctorObjOfSmall : AttachCells.{t} f (ιFunctorObj f πX) :=
  (attachCellsιFunctorObj f πX).reindex (equivShrink.{t} _).symm

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

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

Разделы

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

Аффилиация

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