inducedMap

Mathlib.CategoryTheory.FiberedCategory.HasFibers

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

Lean4

/-- Given a fibered category p, b' b in Fib R, and a pullback ψ : b ⟶ a in 𝒳, i.e.
```
b'       b --ψ--> a
|        |        |
v        v        v
R ====== R --f--> S
```
Then the induced map τ : b' ⟶ b can be lifted to the fiber over R -/
noncomputable def inducedMap : b ⟶ b' :=
  Fib.homMk (IsCartesian.map p f ψ φ)

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

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

Разделы

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

Аффилиация

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