lift_base

Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.WidePullback.lift_base

← MathLib Explorer

English

The lift map composed with the base map equals the original map f: lift f fs w ≫ base arrows = f.

Русский

lift f fs w сопоставляет базу так, что lift f fs w ≫ base arrows = f.

LaTeX

$$$\\mathrm{lift}(f,fs,w) \\;\\circ\\; \\text{base arrows} = f$.$$

Lean4

@[reassoc]
theorem lift_base : lift f fs w ≫ base arrows = f := by
  simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

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

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

Разделы

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

Аффилиация

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