right_ore_of_pullbacks

Mathlib.CategoryTheory.Sites.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.right_ore_of_pullbacks

English

If pullbacks exist, then the category satisfies the right Ore condition.

Русский

Если существуют квадратные тени (pullbacks), то категория удовлетворяет правой условию Ора.

LaTeX

$$$\mathrm{HasPullbacks}(C) \Rightarrow \mathrm{RightOreCondition}(C)$$$

Lean4

theorem right_ore_of_pullbacks [Limits.HasPullbacks C] : RightOreCondition C := fun _ _ =>
  ⟨_, _, _, Limits.pullback.condition⟩

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

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

Разделы

Аффилиация

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