pullbackMap

Mathlib.CategoryTheory.FiberedCategory.HasFibers

URI: https://scilib.ai/kg/mathlib#HasFibers.pullbackMap

Lean4

/-- A Cartesian morphism lifting `f : R ⟶ S` with domain in the image of `Fib p R` -/
noncomputable def pullbackMap : (ι R).obj (mkPullback f ha) ⟶ a :=
  (Fib.mkIsoSelf (domain_eq p f (IsPreFibered.pullbackMap ha f))).hom ≫ (IsPreFibered.pullbackMap ha f)

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

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

Разделы

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

Аффилиация

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