transport

Mathlib.CategoryTheory.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Grothendieck.transport

Lean4

/-- If `F : C ⥤ Cat` is a functor and `t : c ⟶ d` is a morphism in `C`, then `transport` maps each
`c`-based element of `Grothendieck F` to a `d`-based element.
-/
@[simps]
def transport (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : Grothendieck F :=
  ⟨c, (F.map t).obj x.fiber⟩

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

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

Разделы

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

Аффилиация

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