HasPullbacks

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreZeroHypercover.HasPullbacks

Lean4

/-- The assumption that the pullback of `X i₁` and `X i₂` over `S` exists
for any `i₁` and `i₂`. -/
abbrev HasPullbacks :=
  ∀ (i₁ i₂ : E.I₀), HasPullback (E.f i₁) (E.f i₂)

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

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

Разделы

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

Аффилиация

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