eqToHom_domain_lift_id

Mathlib.CategoryTheory.FiberedCategory.HomLift

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

← MathLib Explorer

English

If a = b and p.obj b = S, then p.IsHomLift (𝟙 S) (eqToHom hab).

Русский

Если a = b и p.obj b = S, тогда p.IsHomLift (𝟙 S) (eqToHom hab).

LaTeX

$$$$ p.IsHomLift (\mathrm{eqToHom}(hab)) $$$$

Lean4

theorem eqToHom_domain_lift_id {p : 𝒳 ⥤ 𝒮} {a b : 𝒳} (hab : a = b) {R : 𝒮} (hR : p.obj a = R) :
    p.IsHomLift (𝟙 R) (eqToHom hab) := by subst hR hab; simp

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

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

Разделы

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

Аффилиация

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