inducedFunctor

Mathlib.CategoryTheory.FiberedCategory.Fiber

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Fiber.inducedFunctor

Lean4

/-- Given a functor `F : C ⥤ 𝒳` such that `F ⋙ p` is constant at some `S : 𝒮`, then
we get an induced functor `C ⥤ Fiber p S` that `F` factors through. -/
def inducedFunctor : C ⥤ Fiber p S
    where
  obj x := ⟨F.obj x, by simp only [← comp_obj, hF, const_obj_obj]⟩
  map φ := ⟨F.map φ, of_commsq _ _ _ (congr_obj hF _) (congr_obj hF _) <| by simpa using (eqToIso hF).hom.naturality φ⟩

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

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

Разделы

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

Аффилиация

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