id_lift_eqToHom_domain

Mathlib.CategoryTheory.FiberedCategory.HomLift

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

← MathLib Explorer

English

If R = S and p.obj a = R, then p.IsHomLift (eqToHom hRS) (𝟙 a) for hRS: R = S.

Русский

Если R = S и p.obj a = R, то p.IsHomLift (eqToHom hRS) (𝟙 a) для hRS: R = S.

LaTeX

$$$$ p.IsHomLift (eqToHom hRS) (\mathbf{1}_a) $$$$

Lean4

theorem id_lift_eqToHom_domain {p : 𝒳 ⥤ 𝒮} {R S : 𝒮} (hRS : R = S) {a : 𝒳} (ha : p.obj a = R) :
    p.IsHomLift (eqToHom hRS) (𝟙 a) := by subst hRS ha; simp

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

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

Разделы

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

Аффилиация

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