instIsHomLiftIdObj

Mathlib.CategoryTheory.FiberedCategory.HomLift

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsHomLift.instIsHomLiftIdObj

English

Identity morphisms lift via IsHomLift when p.obj a equals a base object.

Русский

Идентичности поднимаются через IsHomLift, когда p.obj a равен базовому объекту.

LaTeX

$$$\\text{IsHomLift}(p)(\\mathrm{id}_{p(a)}, \\mathrm{id}_a)$$$

Lean4

@[simp]
instance (a : 𝒳) : p.IsHomLift (𝟙 (p.obj a)) (𝟙 a) := by rw [← p.map_id]; infer_instance

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

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

Разделы

Аффилиация

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