of_id_fst

Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsPullback.of_id_fst

English

A square with identity on the left edge is a pullback when the obvious right-hand leg is pulled back to itself.

Русский

Квадрат со связкой identity слева является пуллбаком, когда правая часть соответствует самопроводнику.

LaTeX

$$$ IsPullback( id_X, f, f, id_Z ) $$$

Lean4

theorem of_id_fst : IsPullback (𝟙 _) f f (𝟙 _) :=
  IsPullback.of_horiz_isIso ⟨by simp⟩

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

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

Разделы

Аффилиация

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