map_homMk

Mathlib.CategoryTheory.FiberedCategory.HasFibers

URI: https://scilib.ai/kg/mathlib#HasFibers.Fib.map_homMk

← MathLib Explorer

English

The map of morphisms under ι S commutes with homMk: (ι S).map (homMk φ) = φ.

Русский

Отображение морфизмов через ι_S коммутации с homMk: (ι_S).map (homMk φ) = φ.

LaTeX

$$$ (ι S).map (homMk φ) = φ $$$

Lean4

@[simp]
theorem map_homMk {S : 𝒮} {a b : Fib p S} (φ : (ι S).obj a ⟶ (ι S).obj b) [IsHomLift p (𝟙 S) φ] :
    (ι S).map (homMk φ) = φ := by simp [Fib.homMk, congr_hom (inducedFunctor_comp p S)]

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

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

Разделы

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

Аффилиация

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