lift_comp_id

Mathlib.CategoryTheory.FiberedCategory.HomLift

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

English

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

Русский

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

LaTeX

$$$$ p.IsHomLift (eqToHom hRS) (\mathrm{Id}_b) $$$$

Lean4

instance lift_comp_id : p.IsHomLift (f ≫ 𝟙 S) φ := by simp_all

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

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

Разделы

Аффилиация

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