id_lift_eqToHom_codomain

Mathlib.CategoryTheory.FiberedCategory.HomLift

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem id_lift_eqToHom_codomain {p : 𝒳 ⥤ 𝒮} {R S : 𝒮} (hRS : R = S) {b : 𝒳} (hb : p.obj b = S) :
    p.IsHomLift (eqToHom hRS) (𝟙 b) := by subst hRS hb; simp

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

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

Разделы

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

Аффилиация

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