fiberInclusion_homMk

Mathlib.CategoryTheory.FiberedCategory.Fiber

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

Lean4

@[simp]
theorem fiberInclusion_homMk (p : 𝒳 ⥤ 𝒮) (S : 𝒮) {a b : 𝒳} (φ : a ⟶ b) [IsHomLift p (𝟙 S) φ] :
    fiberInclusion.map (homMk p S φ) = φ :=
  rfl

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

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

Разделы

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

Аффилиация

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