hasPullback_of_right_factors_mono

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

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

English

Let f: X → Z and i: Z → W with Mono i. Then HasPullback i (f ≫ i).

Русский

Пусть f: X → Z и i: Z → W имеют моно i. Тогда HasPullback i (f ≫ i).

LaTeX

$$$HasPullback\ i\ (f \circ i).$$$

Lean4

instance hasPullback_of_right_factors_mono : HasPullback i (f ≫ i) := by
  simpa only [Category.id_comp] using hasPullback_of_comp_mono (𝟙 Z) f i

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

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

Разделы

Аффилиация

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