pullbacks_le

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.pullbacks_le

English

Assuming base-change stability, pullbacks form a substructure: P.pullbacks ≤ P.

Русский

При условии устойчивости к изменению основания пуллбэки формируют подструктуру: P.pullbacks ≤ P.

LaTeX

$$P.pullbacks ≤ P$$

Lean4

theorem pullbacks_le [P.IsStableUnderBaseChange] : P.pullbacks ≤ P := by
  rwa [← isStableUnderBaseChange_iff_pullbacks_le]

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

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

Разделы

Аффилиация

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